Theorem sseq1 3248

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

Assertion

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

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 3240	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3232	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3232	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 276	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 129	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 121	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ⊆ wss 3198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sseq12  3250  sseq1i  3251  sseq1d  3254  nssne2  3284  sbss  3600  pwjust  3651  elpw  3656  elpwg  3658  sssnr  3834  ssprr  3837  sstpr  3838  unimax  3925  trss  4194  elssabg  4236  bnd2  4261  exmidexmid  4284  exmidsssn  4290  exmidsssnc  4291  exmid1stab  4296  mss  4316  exss  4317  frforeq2  4440  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  reg2exmidlema  4630  sucprcreg  4645  ordtri2or2exmid  4667  ontri2orexmidim  4668  onintexmid  4669  tfis  4679  tfisi  4683  elomssom  4701  nnregexmid  4717  releq  4806  xpsspw  4836  iss  5057  relcnvtr  5254  iotass  5302  fununi  5395  funcnvuni  5396  funimaexglem  5410  ffoss  5612  ssimaex  5703  tfrlem1  6469  el2oss1o  6606  nnsucsssuc  6655  qsss  6758  phpm  7047  ssfiexmid  7058  ssfiexmidt  7060  findcard2d  7075  findcard2sd  7076  diffifi  7078  isinfinf  7081  fiintim  7118  fisseneq  7121  fidcenumlemrk  7147  fidcenumlemr  7148  sbthlem2  7151  isbth  7160  ctssdclemr  7305  onntri45  7452  tapeq1  7464  elinp  7687  sup3exmid  9130  zfz1isolem1  11097  zfz1iso  11098  fimaxre2  11781  sumeq1  11909  fsum2d  11989  fsumabs  12019  fsumiun  12031  prodeq1f  12106  fprod2d  12177  exmidunben  13040  ctiunct  13054  ssomct  13059  restsspw  13325  lspval  14397  uniopn  14718  fiinopn  14721  fiinbas  14766  baspartn  14767  eltg2  14770  eltg3  14774  topbas  14784  clsval  14828  neival  14860  neiint  14862  neipsm  14871  opnneissb  14872  opnssneib  14873  innei  14880  restbasg  14885  cnpdis  14959  txbas  14975  eltx  14976  neitx  14985  txlm  14996  blssexps  15146  blssex  15147  neibl  15208  metrest  15223  xmettx  15227  tgioo  15271  tgqioo  15272  limcimolemlt  15381  recnprss  15404  dvmptfsum  15442  lpvtx  15923  bj-om  16482  bj-2inf  16483  bj-nntrans  16496  bj-omtrans  16501  subctctexmid  16551  domomsubct  16552  pw1nct  16554