Def  !A == {x:A| y:A. x = y }

is mentioned by

Thm*  (A ~ 1)  (!A)	[card1_iff_inhabited_uniquely]
Thm*  (A)  (!(A inj B))	[inj_from_empty_unique]

In prior sections: LogicSupplement SimpleMulFacts

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html