SeparationWithSubst Show Code edit
thm (SeparationWithSubst ((A z result element) (φ z result)) ()
(∃ result (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ))))))
result element A x φ SeparationThereExistsSubst
(∃ result (∀ element (↔ (∈ element result) (∧ (∈ element A) (subst element x φ)))))
z element A x φ Separation-sub
(→ (= z element) (↔ (∧ (∈ z A) (subst z x φ)) (∧ (∈ element A) (subst element x φ))))
makeSubstExplicit
(↔ (subst element z (∧ (∈ z A) (subst z x φ))) (∧ (∈ element A) (subst element x φ)))
swapBiconditional
(↔ (∧ (∈ element A) (subst element x φ)) (subst element z (∧ (∈ z A) (subst z x φ))))
(∈ element result) buildBiconditionalLL
(↔ (↔ (∈ element result) (∧ (∈ element A) (subst element x φ))) (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ)))))
element buildForAll
(↔ (∀ element (↔ (∈ element result) (∧ (∈ element A) (subst element x φ)))) (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ))))))
result buildThereExists
(↔ (∃ result (∀ element (↔ (∈ element result) (∧ (∈ element A) (subst element x φ))))) (∃ result (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ)))))))
eliminateBiconditionalReverse
(→ (∃ result (∀ element (↔ (∈ element result) (∧ (∈ element A) (subst element x φ))))) (∃ result (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ)))))))
applyModusPonens
(∃ result (∀ element (↔ (∈ element result) (subst element z (∧ (∈ z A) (subst z x φ))))))
)
edit