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