consider F, G being ZF-formula such that
A2: H = F => G by A1, Def21;
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