let W be Universe; :: thesis: 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; :: thesis: 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
let f be Function of VAR,W; :: thesis: ( {(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)))))))) ; :: thesis: for u being Element of W holds (def_func' (H,f)) .: u in W
let u be Element of W; :: thesis: (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; :: thesis: 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; :: thesis: verum