let H be ZF-formula; for x, y being Variable st H is biconditional holds
H / (x,y) is biconditional
let x, y be Variable; ( H is biconditional implies H / (x,y) is biconditional )
given H1, H2 being ZF-formula such that A1:
H = H1 <=> H2
; ZF_LANG:def 22 H / (x,y) is biconditional
H / (x,y) = (H1 / (x,y)) <=> (H2 / (x,y))
by A1, Th163;
hence
H / (x,y) is biconditional
; verum