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

Metamath Proof Explorer

Theorem sseq1

Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993) (Proof shortened by Andrew Salmon, 21-Jun-2011)

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

Proof

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