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:3; :: thesis: verum

end;

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