Separation Show Code edit
thm (Separation () ()
(↔ (∈ C (separate x A φ)) (∧ (∈ C A) (subst C x φ)))
x A φ z SeparationAsAbstraction
(= (separate x A φ) (abstract z (∧ (∈ z A) (subst z x φ))))
C buildMembershipLL
(↔ (∈ C (separate x A φ)) (∈ C (abstract z (∧ (∈ z A) (subst z x φ)))))
C z A x φ SeparationObject
(↔ (∈ C (abstract z (∧ (∈ z A) (subst z x φ)))) (∧ (∈ C A) (subst C x φ)))
applyBiconditionalTransitivity
(↔ (∈ C (separate x A φ)) (∧ (∈ C A) (subst C x φ)))
)
edit