Def {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y)  y = x) }

is mentioned by

Thm* a:T, Q:(TProp). (a = !x:T. Q(x))  a  {!x:T | Q(x)}

[uni_sat_imp_in_uni_set]

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