theorem Th10:
for
M being non
empty set for
H being
ZF-formula for
v being
Function of
VAR,
M st not
x. 0 in Free H &
M,
v |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for
m1,
m2 being
Element of
M holds
(
(def_func' (H,v)) . m1 = m2 iff
M,
(v / ((x. 3),m1)) / (
(x. 4),
m2)
|= H )