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 Th176, ZF_LANG:49;
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 Th163; :: thesis: verum