Chapter 11: Axioms and Theorems Chapter 11: Axioms and Theorems

(11.3) Axiom, Set membership:  If  x  dnof in   P ,  then
                                         |-      P {x | R: E}         ($| R: P = E) .

(11.4) Axiom, Extensionality:  If  x  dnof in  S,T ,  then
                                         |-    S = T         ("|: x S      x T) .

(11.5)  Theorem:  If  x  dnof in  S ,  then  |-      S   =   {x | x S} .

(11.6)  Theorem:  If  y  dnof in  R,E ,  then
                                        

|-    {x | R: E}   =   {y | ($| R: y = E)} .

(11.7)  Theorem:   x {x | R}      R
(11.9)  Theorem:   {x | Q}  =  {x | R}         ("|: Q R)
(11.10) Metatheorem:   |-    {x | Q}  =  {x | R}   if and only if    |-    Q R .

(11.12) Axiom, Size:  If  x  dnof in  S , then   |-     #S   =   (| x S: 1).

(11.13) Axiom, Subset: If  x  dnof in  S,T , then
                                         |-     S T     ("| x S: x T).

(11.14) Axiom, Proper subset:   S T             S  S T
(11.15) Axiom, Superset:   T S     S T
(11.16) Axiom, Proper superset:   T S         S T

(11.17) Axiom, Complement:   x    ~ S         x S

(11.19) Theorem:   ~ ~ S   =   S

(11.20) Axiom, Union:   x S T          x S      x T

(11.21) Axiom, Intersection:   x S T          x S      x T

(11.22) Axiom, Difference:   x S-T         x S      x T

(11.23) Axiom, Power set:   y PS        y S


You may also use the following facts without giving references for them:
(1) |-  x      false ,   and   |-  x U      true .
(2) {E1, , En}  means  {x|  (x = E1)        (x = En)} , if  x  dnof in  E1,,En .
(3) {x| R}  is an abbreviation for  {x| R: x} .   You may also use Dummy Renaming for set comprehensions from class. Always mention ``dnof'' restrictions and take steps to satisfy them as necessary.


File translated from TEX by TTH, version 2.60.
On 15 Mar 2001, 19:27.