let H be ZF-formula; :: thesis: for x, y being Variable st H is biconditional holds
( the_left_side_of (H / x,y) = (the_left_side_of H) / x,y & the_right_side_of (H / x,y) = (the_right_side_of H) / x,y )
let x, y be Variable; :: thesis: ( H is biconditional implies ( the_left_side_of (H / x,y) = (the_left_side_of H) / x,y & the_right_side_of (H / x,y) = (the_right_side_of H) / x,y ) )
assume H is biconditional ; :: thesis: ( the_left_side_of (H / x,y) = (the_left_side_of H) / x,y & the_right_side_of (H / x,y) = (the_right_side_of H) / x,y )
then ( H = (the_left_side_of H) <=> (the_right_side_of H) & H / x,y = (the_left_side_of (H / x,y)) <=> (the_right_side_of (H / x,y)) ) by Th190, ZF_LANG:67;
hence ( the_left_side_of (H / x,y) = (the_left_side_of H) / x,y & the_right_side_of (H / x,y) = (the_right_side_of H) / x,y ) by Th177; :: thesis: verum