let G1, G2, H1, H2 be ZF-formula; :: thesis: for x, y being Variable holds
( G1 <=> G2 = (H1 <=> H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) )
let x, y be Variable; :: thesis: ( G1 <=> G2 = (H1 <=> H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) )
( ( G1 <=> G2 = (H1 <=> H2) / x,y implies ( G1 => G2 = (H1 => H2) / x,y & G2 => G1 = (H2 => H1) / x,y ) ) & ( G1 => G2 = (H1 => H2) / x,y & G2 => G1 = (H2 => H1) / x,y implies G1 <=> G2 = (H1 <=> H2) / x,y ) & ( G1 => G2 = (H1 => H2) / x,y implies ( G1 = H1 / x,y & G2 = H2 / x,y ) ) & ( G1 = H1 / x,y & G2 = H2 / x,y implies G1 => G2 = (H1 => H2) / x,y ) & ( G2 => G1 = (H2 => H1) / x,y implies ( G1 = H1 / x,y & G2 = H2 / x,y ) ) & ( G1 = H1 / x,y & G2 = H2 / x,y implies G2 => G1 = (H2 => H1) / x,y ) ) by Th172, Th176;
hence ( G1 <=> G2 = (H1 <=> H2) / x,y iff ( G1 = H1 / x,y & G2 = H2 / x,y ) ) ; :: thesis: verum