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 ) by A1, Th15; :: 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 )

assume A2: 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 by Def4, A2;

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, Th15; :: thesis: verum

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 ) by A1, Th15; :: 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 )

assume A2: 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 by Def4, A2;

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, Th15; :: thesis: verum