Primitive. The name wsbc is a term of type ((set → prop) → ((set → prop) → prop)).
In Proofgold the corresponding term root is dfea97... and object id is a0cd6a...
Primitive. The name wceq is a term of type ((set → prop) → ((set → prop) → prop)).
In Proofgold the corresponding term root is eab77d... and object id is e1f96c...
Axiom. (ax_mp) We take the following as an axiom:
(∀ph : prop, (∀ps : prop, ph → (wi ph ps) → ps))
In Proofgold the corresponding term root is 261f32... and proposition id is c627de...
Axiom. (ax_frege52c) We take the following as an axiom:
(∀ph : (set → prop), (∀A2 : (set → (set → prop)), (∀B2 : (set → (set → prop)), (∀x3 : set, (wi (wceq (A2 x3) (B2 x3)) (wi (wsbc (λx3 : set ⇒ (ph x3)) (A2 x3)) (wsbc (λx3 : set ⇒ (ph x3)) (B2 x3))))))))
In Proofgold the corresponding term root is 247a9e... and proposition id is f4ba48...
Axiom. (ax_frege8) We take the following as an axiom:
(∀ph : prop, (∀ps : prop, (∀ch : prop, (wi (wi ph (wi ps ch)) (wi ps (wi ph ch))))))
In Proofgold the corresponding term root is a5ffbb... and proposition id is 545653...
Theorem. (frege53c)
(∀ph : (set → prop), (∀A2 : (set → (set → prop)), (∀B2 : (set → (set → prop)), (∀x3 : set, (wi (wsbc (λx3 : set ⇒ (ph x3)) (A2 x3)) (wi (wceq (A2 x3) (B2 x3)) (wsbc (λx3 : set ⇒ (ph x3)) (B2 x3))))))))
In Proofgold the corresponding term root is 89e42f... and proposition id is 24ac9f...
Proof:
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)))).
∎