The Theory zfc
 Parents

 hol
 Constants
 \$z SETz SETz BOOL Sepz (SETz BOOL) SETz SETz z SETz Pair SETz SETz SETz z SETz SETz \$z SETz SETz BOOL z SETz SETz RImage (SETz SETz) SETz SETz \$z SETz SETz SETz z SETz SETz \$z SETz SETz SETz \$z SETz SETz SETz relz SETz BOOL funz SETz BOOL domz SETz SETz ranz SETz SETz fieldz SETz SETz \$z SETz SETz SETz
 Types
 SETz
 Fixity

 Infix 230: z z Infix 240: z z z Infix 250: z
 Axioms
 ext_axiom s t ( u u z s u z t) s = t wf_axiom p ( s ( e e z s p e) p s) ( s p s) 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) z_axiom s u u z z s u z s replacement_axiom f s u u z RImage f s ( v v z s u = f v)
 Definitions
 z z = Sepz ( e F) ( s T) z s t s z t ( u u z s u z t) 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 = Sepz ( e e z t) 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 z f x f z x = (if y x z y z f then y x z y z f else f)
 Theorems
 z_thm s s z z set_ext_thm s t s = t ( u u z s u z t) z_ext_thm s t u u z s z t u z s u z t z_ext_thm2 t ( x x z t) ( s s z z t ( u u z t s z u)) z_ext_thm s t u u z s z t 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 relz_z_thm relz z funz_z_thm funz z domz_z_thm domz z = z ranz_z_thm ranz z = z fieldz_z_thm fieldz z = z