# Metamath Proof Explorer

## Theorem sseq2

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

Ref Expression
Assertion sseq2 ${⊢}{A}={B}\to \left({C}\subseteq {A}↔{C}\subseteq {B}\right)$

### Proof

Step Hyp Ref Expression
1 sstr2 ${⊢}{C}\subseteq {A}\to \left({A}\subseteq {B}\to {C}\subseteq {B}\right)$
2 1 com12 ${⊢}{A}\subseteq {B}\to \left({C}\subseteq {A}\to {C}\subseteq {B}\right)$
3 sstr2 ${⊢}{C}\subseteq {B}\to \left({B}\subseteq {A}\to {C}\subseteq {A}\right)$
4 3 com12 ${⊢}{B}\subseteq {A}\to \left({C}\subseteq {B}\to {C}\subseteq {A}\right)$
5 2 4 anim12i ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)\to \left(\left({C}\subseteq {A}\to {C}\subseteq {B}\right)\wedge \left({C}\subseteq {B}\to {C}\subseteq {A}\right)\right)$
6 eqss ${⊢}{A}={B}↔\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$
7 dfbi2 ${⊢}\left({C}\subseteq {A}↔{C}\subseteq {B}\right)↔\left(\left({C}\subseteq {A}\to {C}\subseteq {B}\right)\wedge \left({C}\subseteq {B}\to {C}\subseteq {A}\right)\right)$
8 5 6 7 3imtr4i ${⊢}{A}={B}\to \left({C}\subseteq {A}↔{C}\subseteq {B}\right)$