:: deftheorem Def2 defines def_func ZFMODEL1:def 2 :
for H being ZF-formula
for E being non empty set st Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
for b₃ being Function of E,E holds
( b₃ = def_func (H,E) iff for g being Function of VAR,E holds
( E,g |= H iff b₃ . (g . (x. 3)) = g . (x. 4) ) );