UnionAxiomObject Show Code edit
thm (UnionAxiomObject ((A y z w)) () (∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w A))))))
x A w MembershipBuilderLL
(→ (= x A) (↔ (∈ w x) (∈ w A)))
(∈ z w) buildConjunctionLLInConsequent
(→ (= x A) (↔ (∧ (∈ z w) (∈ w x)) (∧ (∈ z w) (∈ w A))))
w buildThereExistsInConsequent
(→ (= x A) (↔ (∃ w (∧ (∈ z w) (∈ w x))) (∃ w (∧ (∈ z w) (∈ w A)))))
(∈ z y) buildBiconditionalLLInConsequent
(→ (= x A) (↔ (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w x)))) (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w A))))))
z buildForAllInConsequent
(→ (= x A) (↔ (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w x))))) (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w A)))))))
y buildThereExistsInConsequent
(→ (= x A) (↔ (∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w x)))))) (∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w A))))))))
y z w x UnionAxiom
(∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w x))))))
VariableToObject
(∃ y (∀ z (↔ (∈ z y) (∃ w (∧ (∈ z w) (∈ w A))))))
)
edit