EqualitySubset Show Code edit
thm (EqualitySubset () ()
(↔ (= A B) (∧ (⊆ A B) (⊆ B A)))
A B x ExtensionalityBiconditional
(↔ (= A B) (∀ x (↔ (∈ x A) (∈ x B))))
(∈ x A) (∈ x B) BiconditionalImplication
(↔ (↔ (∈ x A) (∈ x B)) (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x A))))
x buildForAll
(↔ (∀ x (↔ (∈ x A) (∈ x B))) (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x A)))))
applyBiconditionalTransitivity
(↔ (= A B) (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x A)))))
x
(→ (∈ x A) (∈ x B))
(→ (∈ x B) (∈ x A))
ForAllConjunction
(↔ (∀ x (∧ (→ (∈ x A) (∈ x B)) (→ (∈ x B) (∈ x A)))) (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x A)))))
applyBiconditionalTransitivity
(↔ (= A B) (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x A)))))
A B x Subset
(↔ (⊆ A B) (∀ x (→ (∈ x A) (∈ x B))))
B A x Subset
(↔ (⊆ B A) (∀ x (→ (∈ x B) (∈ x A))))
buildConjunction
(↔ (∧ (⊆ A B) (⊆ B A)) (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x A)))))
swapBiconditional
(↔ (∧ (∀ x (→ (∈ x A) (∈ x B))) (∀ x (→ (∈ x B) (∈ x A)))) (∧ (⊆ A B) (⊆ B A)))
applyBiconditionalTransitivity
(↔ (= A B) (∧ (⊆ A B) (⊆ B A)))
)
edit