consider F, G being ZF-formula such that
A2: H = F <=> G by A1, Def22;
take G ; :: thesis: ex H1 being ZF-formula st H = H1 <=> G
take F ; :: thesis: H = F <=> G
thus H = F <=> G by A2; :: thesis: verum