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

proof

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

end;

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