SeparationObject Show Code edit
thm (SeparationObject ( (A z) (φ z)) ()
(↔ (∈ C (abstract z (∧ (∈ z A) (subst z x φ)))) (∧ (∈ C A) (subst C x φ)))
z y A x φ Separation-sub
(→ (= z y) (↔ (∧ (∈ z A) (subst z x φ)) (∧ (∈ y A) (subst y x φ))))
y C A x φ Separation-sub
(→ (= y C) (↔ (∧ (∈ y A) (subst y x φ)) (∧ (∈ C A) (subst C x φ))))
result y A x φ SeparationThereExistsSubst
(∃ result (∀ y (↔ (∈ y result) (∧ (∈ y A) (subst y x φ)))))
SetObject
(↔ (∈ C (abstract z (∧ (∈ z A) (subst z x φ)))) (∧ (∈ C A) (subst C x φ)))
)
edit