src/ZF/ZF.thy
changeset 3906 5ae0e1324c56
parent 3840 e0baea4d485a
child 3940 1d5bee4d047f
equal deleted inserted replaced
3905:4bbfbb7a2cd3 3906:5ae0e1324c56
     5 
     5 
     6 Zermelo-Fraenkel Set Theory
     6 Zermelo-Fraenkel Set Theory
     7 *)
     7 *)
     8 
     8 
     9 ZF = FOL + Let + 
     9 ZF = FOL + Let + 
       
    10 
       
    11 global
    10 
    12 
    11 types
    13 types
    12   i
    14   i
    13 
    15 
    14 arities
    16 arities
   162   Bex_def       "Bex(A, P) == EX x. x:A & P(x)"
   164   Bex_def       "Bex(A, P) == EX x. x:A & P(x)"
   163 
   165 
   164   subset_def    "A <= B == ALL x:A. x:B"
   166   subset_def    "A <= B == ALL x:A. x:B"
   165   succ_def      "succ(i) == cons(i, i)"
   167   succ_def      "succ(i) == cons(i, i)"
   166 
   168 
       
   169 
       
   170 path ZF
       
   171 
   167 rules
   172 rules
   168 
   173 
   169   (* ZF axioms -- see Suppes p.238
   174   (* ZF axioms -- see Suppes p.238
   170      Axioms for Union, Pow and Replace state existence only,
   175      Axioms for Union, Pow and Replace state existence only,
   171      uniqueness is derivable using extensionality. *)
   176      uniqueness is derivable using extensionality. *)