let G, H be ZF-formula; :: thesis: for y, x being Variable holds
( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) )
let y, x be Variable; :: thesis: ( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) )
( 'not' G = ('not' H) / (x,y) iff All (y,('not' G)) = (All (x,('not' H))) / (x,y) ) by Th174;
hence ( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) ) by Th170; :: thesis: verum