theorem
for
M being non
empty set for
H1 being
ZF-formula for
v1 being
Function of
VAR,
M st not
x. 0 in Free H1 &
M,
v1 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) holds
ex
H2 being
ZF-formula ex
v2 being
Function of
VAR,
M st
(
(Free H1) /\ (Free H2) c= {(x. 3),(x. 4)} & not
x. 0 in Free H2 &
M,
v2 |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) &
def_func' (
H1,
v1)
= def_func' (
H2,
v2) )