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_2:3, ORDINAL1:22;
hence (def_func' H,f) .: u in W by CLASSES1:2; :: 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:19; :: thesis: verum