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:
Proof not loaded.