:: deftheorem defines the_axiom_of_substitution_for ZF_MODEL:def 11 :
for H being ZF-formula holds the_axiom_of_substitution_for H = (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))) => (All ((x. 1),(Ex ((x. 2),(All ((x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex ((x. 3),(((x. 3) 'in' (x. 1)) '&' H))))))))));