Def  R is 1-1 == x,x':A, y,y':B. R(x,y) & R(x',y')  (x = x'  y = y')

is mentioned by

Thm*  R:(ABProp). (R is 1-1) = (1-1 xA,yB. R(x;y))

[rel_1_1_eq_rel_1_1_b]

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