theorem
for
E being non
empty set st
E is
being_a_model_of_ZF holds
(
E is
epsilon-transitive & ( for
u,
v being
Element of
E st ( for
w being
Element of
E holds
(
w in u iff
w in v ) ) holds
u = v ) & ( for
u,
v being
Element of
E holds
{u,v} in E ) & ( for
u being
Element of
E holds
union u in E ) & ex
u being
Element of
E st
(
u <> {} & ( for
v being
Element of
E st
v in u holds
ex
w being
Element of
E st
(
v c< w &
w in u ) ) ) & ( for
u being
Element of
E holds
E /\ (bool u) in E ) & ( for
H being
ZF-formula for
f being
Function of
VAR,
E st
{(x. 0),(x. 1),(x. 2)} misses Free H &
E,
f |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for
u being
Element of
E holds
(def_func' (H,f)) .: u in E ) )
by Lm3, Th2, Th4, Th6, Th8, Th15;