Union-sub Show Code edit
thm (Union-sub ((C x) (D x)) () (→ (= C D) (↔ (∃ x (∧ (∈ C x) (∈ x A))) (∃ x (∧ (∈ D x) (∈ x A)))))
C D x MembershipBuilderRR
(→ (= C D) (↔ (∈ C x) (∈ D x)))
(∈ x A) buildConjunctionRRInConsequent
(→ (= C D) (↔ (∧ (∈ C x) (∈ x A)) (∧ (∈ D x) (∈ x A))))
x buildThereExistsInConsequent
(→ (= C D) (↔ (∃ x (∧ (∈ C x) (∈ x A))) (∃ x (∧ (∈ D x) (∈ x A)))))
)
edit