# The Theory zfc

 hol

 pf

## Constants

 \$z SETz SETz BOOL z SETz Sepz (SETz BOOL) SETz SETz Pair SETz SETz SETz z SETz SETz \$z SETz SETz SETz z SETz SETz \$z SETz SETz SETz relz SETz BOOL funz SETz BOOL domz SETz SETz ranz SETz SETz fieldz SETz SETz

 SETz

## Fixity

 Infix 230: z Infix 240: z z

## Axioms

 ext_axiom s t ( u u z s u z t) s = t z_axiom s s z z separation_axiom p s u u z Sepz p s u z s p u pair_axiom s t u u z Pair s t u = s u = t z_axiom s u u z z s ( v u z v v z s)

## Definitions

 z s t s z t = z (Pair s t) z s z s = Sepz ( e t t z s e z t) (z s) z s t s z t = Pair (Pair s t) (Pair s s) relz x relz x ( y y z x ( s t y = s z t)) funz x funz x relz x ( s t u s z u z x t z u z x s = t) domz x domz x = Sepz ( y z y z z z x) (z (z x)) ranz x ranz x = Sepz ( z y y z z z x) (z (z x)) fieldz x fieldz x = domz x z ranz x

## Theorems

 set_ext_thm s t s = t ( u u z s u z t) pair_eq_thm s t u v Pair s t = Pair u v s = u t = v s = v t = u z_eq_thm s t u v s z t = u z v s = u t = v