let G, H be ZF-formula; :: thesis: for y, x being Variable holds
( All y,G = (All x,H) / x,y iff G = H / x,y )
let y, x be Variable; :: thesis: ( All y,G = (All x,H) / x,y iff G = H / x,y )
thus ( All y,G = (All x,H) / x,y implies G = H / x,y ) :: thesis: ( G = H / x,y implies All y,G = (All x,H) / x,y )

proof

assume All y,G = (All x,H) / x,y ; :: thesis: G = H / x,y
then All y,G = All y,(H / x,y) by Lm2;
hence G = H / x,y by ZF_LANG:12; :: thesis: verum

end;

thus ( G = H / x,y implies All y,G = (All x,H) / x,y ) by Lm2; :: thesis: verum