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