theorem :: ZFMODEL1:16

for E being non empty set st E is epsilon-transitive holds
( ( 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 )