In what follows it is understood that lower case Greek letters represent relations, lower case Latin letters in this list are variables, upper case letters are arbitrary given expressions.

(14.2)¢, Axiom (pair equality):

|-  áA, Bñ   =   áC, Dñ      º     A = C  Ù  B = D .

(14.3)¢, Axiom (cross product): If x, y d.n.o.f. in E, S, T, then

|-  E Î S ×T      º     ($x, y  | x Î S   Ù   y Î T : E = áx,yñ)  .

(14.4)¢, Theorem (membership of an ordered pair in a cross product):

|-  áA , B ñ Î S ×T      º     A Î S   Ù  B Î T  .

(14.5)¢, Theorem:

|-  áA , B ñ Î S ×T      º     áB , A ñ Î T ×S  .

(14R), Definition (relation): Let W be a set expression. We say that W is a relation (expression) if, for some variables, x, y not occurring freely in W,

|- z Î W     Þ    ($x, y  | : z = á x,yñ) .

(14RP), Theorem (relational property): For any relation r, variables, x, y not occurring free in r, P and variable z not occurring free in r,

|- ("z | z Î r: P)     º     (" x,y | áx,yñ Î r: P[z: = áx,yñ]) .

(14RE), Theorem (relational equality): For any relations r, s, and variables x, y not occurring free in either of r, s,

|-  r = s     º     ("x,y | :áx,y ñ Î r   º   áx,y ñ Î s) .