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 ( ( Ex z,G = (Ex z,H) / x,y implies All z,('not' G) = (All z,('not' H)) / x,y ) & ( All z,('not' G) = (All z,('not' H)) / x,y implies Ex z,G = (Ex z,H) / x,y ) & ( 'not' G = ('not' H) / x,y implies All z,('not' G) = (All z,('not' H)) / x,y ) & ( All z,('not' G) = (All z,('not' H)) / x,y implies 'not' G = ('not' H) / x,y ) & ( 'not' G = ('not' H) / x,y implies G = H / x,y ) & ( G = H / x,y implies 'not' G = ('not' H) / x,y ) ) by Th170, Th173;
hence ( Ex z,G = (Ex z,H) / x,y iff G = H / x,y ) ; :: thesis: verum