Subset Show Code edit
defthm (Subset formula (⊆ A B) ((A x) (B x)) () (↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B))))
y x A MembershipBuilderRR
(→ (= y x) (↔ (∈ y A) (∈ x A)))
y x B MembershipBuilderRR
(→ (= y x) (↔ (∈ y B) (∈ x B)))
buildImplicationInConsequent
(→ (= y x) (↔ (→ (∈ y A) (∈ y B)) (→ (∈ x A) (∈ x B))))
ChangeVariableForAll
(↔ (∀ y (→ (∈ y A) (∈ y B))) (∀ x (→ (∈ x A) (∈ x B))))
)
edit