Def  !x:A. P(x) == x:A. x is the x:A. P(x)

is mentioned by

Thm*  P:(ABProp). (x:A. !y:B. P(x;y))  (A ~ (y:B{x:A| P(x;y) }))	[partition_type]
Thm*  Dec(P)  (!i:2. if i=0 P else P fi)	[decidable_vs_unique_nsub2]
Def  1-1-Corr x:A,y:B. R(x;y) == (x:A. !y:B. R(x;y)) & (y:B. !x:A. R(x;y))	[is_one_one_corr_rel]

In prior sections: LogicSupplement

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