let G, H be ZF-formula; :: thesis: for z, x, y being Variable st z <> x holds
( Ex z,G = (Ex z,H) / x,y iff G = H / x,y )
let z, x, y be Variable; :: thesis: ( z <> x implies ( Ex z,G = (Ex z,H) / x,y iff G = H / x,y ) )
assume z <> x ; :: thesis: ( Ex z,G = (Ex z,H) / x,y iff G = H / x,y )
then ( 'not' G = ('not' H) / x,y iff All z,('not' G) = (All z,('not' H)) / x,y ) by Th173;
hence ( Ex z,G = (Ex z,H) / x,y iff G = H / x,y ) by Th170; :: thesis: verum