This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqss

Description: The subclass relationship is antisymmetric. Compare Theorem 4 of Suppes p. 22. (Contributed by NM, 21-May-1993)

Ref Expression
Assertion eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A

Proof

Step Hyp Ref Expression
1 albiim ⊢ ∀ x x ∈ A ↔ x ∈ B ↔ ∀ x x ∈ A → x ∈ B ∧ ∀ x x ∈ B → x ∈ A
2 dfcleq ⊢ A = B ↔ ∀ x x ∈ A ↔ x ∈ B
3 df-ss ⊢ A ⊆ B ↔ ∀ x x ∈ A → x ∈ B
4 df-ss ⊢ B ⊆ A ↔ ∀ x x ∈ B → x ∈ A
5 3 4 anbi12i ⊢ A ⊆ B ∧ B ⊆ A ↔ ∀ x x ∈ A → x ∈ B ∧ ∀ x x ∈ B → x ∈ A
6 1 2 5 3bitr4i ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A