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, Th163;
hence H / (x,y) is biconditional ; :: thesis: verum