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 sstr2 ⊢ C ⊆ A → A ⊆ B → C ⊆ B
2 1 com12 ⊢ A ⊆ B → C ⊆ A → C ⊆ B
3 sstr2 ⊢ C ⊆ B → B ⊆ A → C ⊆ A
4 3 com12 ⊢ B ⊆ A → C ⊆ B → C ⊆ A
5 2 4 anim12i ⊢ A ⊆ B ∧ B ⊆ A → C ⊆ A → C ⊆ B ∧ C ⊆ B → C ⊆ A
6 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
7 dfbi2 ⊢ C ⊆ A ↔ C ⊆ B ↔ C ⊆ A → C ⊆ B ∧ C ⊆ B → C ⊆ A
8 5 6 7 3imtr4i ⊢ A = B → C ⊆ A ↔ C ⊆ B