Chapter 14 Axioms and Theorems Chapter 14 Axioms and Theorems

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 r: P)         (" x,y | x,y r: P[z: = x,y]) .
(14RE), Theorem (relational equality): For any relations rs, and variables x, y not occurring free in either of rs,
|-  r = s         ("x,y | :x,y r     x,y s) .

File translated from TEX by TTH, version 2.60.
On 24 Apr 2001, 15:21.