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