:: deftheorem defines being_a_model_of_ZF ZF_MODEL:def 12 :
for E being non empty set holds
( E is being_a_model_of_ZF iff ( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
E |= the_axiom_of_substitution_for H ) ) );