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