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

Metamath Proof Explorer

Theorem sseq2

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998)

Ref Expression
Assertion sseq2 ⊢ A = B → C ⊆ A ↔ C ⊆ B

Proof

Step Hyp Ref Expression
1 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
2 sstr2 ⊢ C ⊆ A → A ⊆ B → C ⊆ B
3 2 com12 ⊢ A ⊆ B → C ⊆ A → C ⊆ B
4 sstr2 ⊢ C ⊆ B → B ⊆ A → C ⊆ A
5 4 com12 ⊢ B ⊆ A → C ⊆ B → C ⊆ A
6 3 5 anbiim ⊢ A ⊆ B ∧ B ⊆ A → C ⊆ A ↔ C ⊆ B
7 1 6 sylbi ⊢ A = B → C ⊆ A ↔ C ⊆ B