let W be Universe; for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
for H being ZF-formula
for f being Function of VAR,W st {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of W holds (def_func' (H,f)) .: u in W
proof
let H be
ZF-formula;
for f being Function of VAR,W st {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of W holds (def_func' (H,f)) .: u in Wlet f be
Function of
VAR,
W;
( {(x. 0),(x. 1),(x. 2)} misses Free H & W,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of W holds (def_func' (H,f)) .: u in W )
assume that
{(x. 0),(x. 1),(x. 2)} misses Free H
and
W,
f |= All (
(x. 3),
(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
;
for u being Element of W holds (def_func' (H,f)) .: u in W
let u be
Element of
W;
(def_func' (H,f)) .: u in W
card u in card W
by CLASSES2:1;
then
card ((def_func' (H,f)) .: u) in card W
by CARD_1:67, ORDINAL1:12;
hence
(def_func' (H,f)) .: u in W
by CLASSES1:1;
verum
end;
hence
for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
W |= the_axiom_of_substitution_for H
by ZFMODEL1:15; verum