let E be non empty set ; :: thesis: ( E is epsilon-transitive implies ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) )
assume A1: E is epsilon-transitive ; :: thesis: ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E )
thus ( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) implies for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) :: thesis: ( ( for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ) implies for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H )

proof

assume A2: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ; :: thesis: for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E
let F be Function; :: thesis: ( F is_parametrically_definable_in E implies for X being set st X in E holds
F .: X in E )
given H being ZF-formula, f being Function of VAR,E such that A3: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ) and
A4: F = def_func' (H,f) ; :: according to ZFMODEL1:def 4 :: thesis: for X being set st X in E holds
F .: X in E
let X be set ; :: thesis: ( X in E implies F .: X in E )
assume X in E ; :: thesis: F .: X in E
then reconsider u = X as Element of E ;
(def_func' (H,f)) .: u in E by A1, A2, A3, Th19;
hence F .: X in E by A4; :: thesis: verum

end;

assume A5: for F being Function st F is_parametrically_definable_in E holds
for X being set st X in E holds
F .: X in E ; :: thesis: for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H
for H being ZF-formula
for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E

proof

let H be ZF-formula; :: thesis: for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for u being Element of E holds (def_func' (H,f)) .: u in E
let f be Function of VAR,E; :: thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for u being Element of E holds (def_func' (H,f)) .: u in E )
assume A6: ( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ) ; :: thesis: for u being Element of E holds (def_func' (H,f)) .: u in E
let u be Element of E; :: thesis: (def_func' (H,f)) .: u in E
def_func' (H,f) is_parametrically_definable_in E by A6, Def4;
hence (def_func' (H,f)) .: u in E by A5; :: thesis: verum

end;

hence for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H by A1, Th19; :: thesis: verum