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