let G, H be ZF-formula; :: thesis: for x, y, z being Variable st z <> x holds
( All (z,G) = (All (z,H)) / (x,y) iff G = H / (x,y) )
let x, y, z 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:3; :: thesis: verum

end;

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