Let ph of type (set → prop) be given.
Let A2 of type (set → (set → prop)) be given.
Let B2 of type (set → (set → prop)) be given.
Let x3 of type set be given.
An
exact proof term for the current goal is
(ax_mp (wi (wceq (A2 x3) (B2 x3)) (wi (wsbc (λx3 : set ⇒ (ph x3)) (A2 x3)) (wsbc (λx3 : set ⇒ (ph x3)) (B2 x3)))) (wi (wsbc (λx3 : set ⇒ (ph x3)) (A2 x3)) (wi (wceq (A2 x3) (B2 x3)) (wsbc (λx3 : set ⇒ (ph x3)) (B2 x3)))) (ax_frege52c (λx3 : set ⇒ (ph x3)) (λx3 : set ⇒ (A2 x3)) (λx3 : set ⇒ (B2 x3)) x3) (ax_frege8 (wceq (A2 x3) (B2 x3)) (wsbc (λx3 : set ⇒ (ph x3)) (A2 x3)) (wsbc (λx3 : set ⇒ (ph x3)) (B2 x3)))).