SeparationThereExistsObject Show Code edit
thm (SeparationThereExistsObject ((A y x) (φ y)) ()
(∃ y (∀ x (↔ (∈ x y) (∧ (∈ x A) φ))))
z A x MembershipBuilderLL
(→ (= z A) (↔ (∈ x z) (∈ x A)))
φ buildConjunctionRRInConsequent
(→ (= z A) (↔ (∧ (∈ x z) φ) (∧ (∈ x A) φ)))
(∈ x y) buildBiconditionalLLInConsequent
(→ (= z A) (↔ (↔ (∈ x y) (∧ (∈ x z) φ)) (↔ (∈ x y) (∧ (∈ x A) φ))))
x buildForAllInConsequent
(→ (= z A) (↔ (∀ x (↔ (∈ x y) (∧ (∈ x z) φ))) (∀ x (↔ (∈ x y) (∧ (∈ x A) φ)))))
y buildThereExistsInConsequent
(→ (= z A) (↔ (∃ y (∀ x (↔ (∈ x y) (∧ (∈ x z) φ)))) (∃ y (∀ x (↔ (∈ x y) (∧ (∈ x A) φ))))))
y x z φ SeparationThereExists
(∃ y (∀ x (↔ (∈ x y) (∧ (∈ x z) φ))))
VariableToObject
(∃ y (∀ x (↔ (∈ x y) (∧ (∈ x A) φ))))
)
edit