src/ZF/ZF.thy
 changeset 3906 5ae0e1324c56 parent 3840 e0baea4d485a child 3940 1d5bee4d047f
equal 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. *)`