:: deftheorem Def3 defines / ZF_LANG1:def 3 :
for H being ZF-formula
for x, y being Variable
for b₄ being Function holds
( b₄ = H / (x,y) iff ( dom b₄ = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies b₄ . a = y ) & ( H . a <> x implies b₄ . a = H . a ) ) ) ) );