PowerSet-sub Show Code edit
thm (PowerSet-sub ((C x) (D x)) () (→ (= C D) (↔ (∀ x (→ (∈ x C) (∈ x A))) (∀ x (→ (∈ x D) (∈ x A)))))
C D x MembershipBuilderLL
(→ (= C D) (↔ (∈ x C) (∈ x D)))
(∈ x A) buildCommonConsequentInConsequent
(→ (= C D) (↔ (→ (∈ x C) (∈ x A)) (→ (∈ x D) (∈ x A))))
x buildForAllInConsequent
(→ (= C D) (↔ (∀ x (→ (∈ x C) (∈ x A))) (∀ x (→ (∈ x D) (∈ x A)))))
)
edit