Theorem sseq2 3171

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

Assertion

Ref	Expression
sseq2	⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3154	. . . 4 ⊢ (𝐶 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝐶 ⊆ 𝐵))
2	1	com12 30	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵))
3		sstr2 3154	. . . 4 ⊢ (𝐶 ⊆ 𝐵 → (𝐵 ⊆ 𝐴 → 𝐶 ⊆ 𝐴))
4	3	com12 30	. . 3 ⊢ (𝐵 ⊆ 𝐴 → (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴))
5	2, 4	anim12i 336	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
6		eqss 3162	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
7		dfbi2 386	. 2 ⊢ ((𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵) ↔ ((𝐶 ⊆ 𝐴 → 𝐶 ⊆ 𝐵) ∧ (𝐶 ⊆ 𝐵 → 𝐶 ⊆ 𝐴)))
8	5, 6, 7	3imtr4i 200	1 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1348   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sseq12  3172  sseq2i  3174  sseq2d  3177  sseqtrid  3197  nssne1  3205  sseq0  3456  un00  3461  pweq  3569  ssintab  3848  ssintub  3849  intmin  3851  treq  4093  ssexg  4128  exmidundif  4192  frforeq3  4332  frirrg  4335  iunpw  4465  ordtri2orexmid  4507  ontr2exmid  4509  onsucsssucexmid  4511  ordtri2or2exmid  4555  ontri2orexmidim  4556  fununi  5266  funcnvuni  5267  feq3  5332  ssimaexg  5558  nnawordex  6508  ereq1  6520  xpider  6584  domeng  6730  ssfiexmid  6854  fisseneq  6909  sbthlemi4  6937  sbthlemi5  6938  acfun  7184  onntri45  7218  ccfunen  7226  fprodssdc  11553  basis2  12840  eltg2  12847  clsval  12905  ntrcls0  12925  isnei  12938  neiint  12939  neipsm  12948  opnneissb  12949  opnssneib  12950  innei  12957  icnpimaex  13005  cnptoprest2  13034  neitx  13062  txcnp  13065  blssps  13221  blss  13222  metss  13288  metrest  13300  metcnp3  13305  bdssexg  13939  bj-nntrans  13986  bj-omtrans  13991