Def  A =ext B == (x:A. x  B) & (x:B. x  A)

is mentioned by

Thm*  {x:A| if b P(x) else Q(x) fi } Thm*  =ext Thm*  if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype]
Thm*  {x:A| P(x) } =ext {x:A| P(x) }	[subset_squash_exteq]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_sq_exteq]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_exteq]
Thm*  {x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) }	[exteq_subset_vs_and]
Thm*  {a:{a:A}} =ext {a:A}	[singleton_singleton_self]
Thm*  B:(AType), P:(AProp). Thm*  (i:{i:A| P(i) }B(i)) =ext {v:(i:AB(i))| P(v/x,y. x) }	[exteq_sigma_st_dom]

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