Separation-sub Show Code edit
thm (Separation-sub () () (→ (= C D) (↔ (∧ (∈ C A) (subst C x φ)) (∧ (∈ D A) (subst D x φ))))
C D A MembershipBuilderRR
(→ (= C D) (↔ (∈ C A) (∈ D A)))
C D x φ SubstBuilderReplacement
(→ (= C D) (↔ (subst C x φ) (subst D x φ)))
buildConjunctionInConsequent
(→ (= C D) (↔ (∧ (∈ C A) (subst C x φ)) (∧ (∈ D A) (subst D x φ))))
)
edit