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