PowerSetAxiomObject Show Code edit
thm (PowerSetAxiomObject ((A y z w)) () (∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w A))))))
x A w MembershipBuilderLL
(→ (= x A) (↔ (∈ w x) (∈ w A)))
(∈ w z) buildCommonAntecedentInConsequent
(→ (= x A) (↔ (→ (∈ w z) (∈ w x)) (→ (∈ w z) (∈ w A))))
w buildForAllInConsequent
(→ (= x A) (↔ (∀ w (→ (∈ w z) (∈ w x))) (∀ w (→ (∈ w z) (∈ w A)))))
(∈ z y) buildBiconditionalLLInConsequent
(→ (= x A) (↔ (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w x)))) (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w A))))))
z buildForAllInConsequent
(→ (= x A) (↔ (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w x))))) (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w A)))))))
y buildThereExistsInConsequent
(→ (= x A) (↔ (∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w x)))))) (∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w A))))))))
y z w x PowerSetAxiom
(∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w x))))))
VariableToObject
(∃ y (∀ z (↔ (∈ z y) (∀ w (→ (∈ w z) (∈ w A))))))
)
edit