:: deftheorem Def1 defines def_func' ZFMODEL1:def 1 :
for H being ZF-formula
for E being non empty set
for val being Function of VAR,E st not x. 0 in Free H & E,val |= 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,val) iff for g being Function of VAR,E st ( for y being Variable holds
( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds
( E,g |= H iff b₄ . (g . (x. 3)) = g . (x. 4) ) );