Theorem sseqtri 3998

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)

Hypotheses

Ref	Expression
sseqtr.1	⊢ 𝐴 ⊆ 𝐵
sseqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
sseqtri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtri

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	sseq2i 3979	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	mpbi 230	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  sseqtrri  3999  3sstr3i  4000  eqimssi  4010  abssi  4036  ssun2  4145  unixpss  5776  0ima  6052  fvssunirnOLD  6895  mptexgf  7199  difex2  7739  oelim2  8562  omopthlem2  8627  sbthlem7  9063  unifpw  9313  fiuni  9386  dmttrcl  9681  rnttrcl  9682  ttrclexg  9683  rankuni  9823  rankc2  9831  rankxpu  9836  rankmapu  9838  rankxplim  9839  infxpenlem  9973  cf0  10211  fin23lem17  10298  fin23lem31  10303  smobeth  10546  nqerf  10890  dmrecnq  10928  ackbijnn  15801  divalglem2  16372  divalglem5  16374  bitsfzolem  16411  0bits  16416  bezoutlem2  16517  bezoutlem3  16518  lcmcllem  16573  lcmledvds  16576  lcmfval  16598  lcmfcllem  16602  lcmfledvds  16609  odzcllem  16770  odzdvds  16773  unbenlem  16886  4sqlem13  16935  4sqlem14  16936  4sqlem17  16939  4sqlem18  16940  vdwlem8  16966  vdwnnlem3  16975  ramcl2lem  16987  ramtcl  16988  ramtub  16990  strle1  17135  prdsvallem  17424  wunfunc  17870  wunnat  17928  psssdm2  18547  tsrss  18555  gicer  19216  symgsssg  19404  symgfisg  19405  odfval  19469  odlem2  19476  gexlem2  19519  torsubg  19791  dprd2da  19981  zringlpirlem2  21380  zringlpirlem3  21381  fermltlchr  21446  pjfval  21622  pjpm  21624  toponsspwpw  22816  eltg4i  22854  ntrss2  22951  isopn3  22960  mretopd  22986  leordtval2  23106  ptbasfi  23475  hmphtop  23672  hmpher  23678  restutop  24132  ucnprima  24176  tngtopn  24545  tgioo  24691  xrtgioo  24702  ovolicc2lem4  25428  nulmbl2  25444  iundisj  25456  dyadmax  25506  i1f1  25598  dvfval  25805  dvcnp2  25828  dvcnp2OLD  25829  lhop1lem  25925  lhop2  25927  elqaalem1  26234  elqaalem3  26236  taylthlem2  26289  taylthlem2OLD  26290  pserulm  26338  psercn2  26339  psercn2OLD  26340  psercnlem2  26341  psercnlem1  26342  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  pserdv  26346  pserdv2  26347  abelth  26358  dvlog  26567  efopnlem2  26573  logtayl  26576  cxpcn3lem  26664  cxpcn3  26665  resqrtcn  26666  dvatan  26852  atancn  26853  rlimcnp  26882  rlimcnp2  26883  wilthlem3  26987  ftalem4  26993  ftalem5  26994  dchrisum0lem2a  27435  bdayimaon  27612  noetasuplem4  27655  noetainflem4  27659  nocvxminlem  27696  nocvxmin  27697  noeta2  27703  etasslt2  27733  scutbdaybnd2lim  27736  bday1s  27750  lrrecfr  27857  addsbdaylem  27930  negsunif  27968  onsiso  28176  bdayon  28180  zs12bday  28350  cchhllem  28821  axlowdimlem6  28881  hhssabloilem  31197  choc1  31263  chub2i  31406  span0  31478  spanuni  31480  sshhococi  31482  chsup0  31484  spansnpji  31514  mayetes3i  31665  nlelshi  31996  pjimai  32112  pj3i  32144  shatomistici  32297  hatomistici  32298  atcvat4i  32333  iundisjf  32525  rinvf1o  32561  mptctf  32648  iundisjfi  32726  xrge0mulgnn0  32963  gsumpart  33004  znfermltl  33344  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  ccfldsrarelvec  33673  ccfldextdgrr  33674  2sqr3minply  33777  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  esumcvgsum  34085  coinfliprv  34481  signsply0  34549  signstcl  34563  signstf  34564  kur14lem6  35205  mthmsta  35572  filnetlem3  36375  filnetlem4  36376  onint1  36444  oninhaus  36445  bj-nuliotaALT  37053  imadifss  37596  poimirlem3  37624  poimirlem32  37653  dvtan  37671  itg2addnclem2  37673  ftc1anclem6  37699  heiborlem3  37814  isdrngo2  37959  elrfi  42689  mapfzcons1  42712  eldioph4b  42806  dnnumch3lem  43042  dnnumch3  43043  dgraalem  43141  dgraaub  43144  resnonrel  43588  cotrcltrcl  43721  cotrclrcl  43738  frege131d  43760  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  relopabVD  44897  rabexgf  45025  fzssnn0  45321  iuneqfzuzlem  45337  allbutfiinf  45423  uzublem  45433  sumnnodd  45635  lptioo2cn  45650  lptioo1cn  45651  fourierdlem31  46143  fourierdlem102  46213  fourierdlem114  46225  fouriercn  46237  elaa2lem  46238  etransclem48  46287  salexct  46339  salgencntex  46348  sge0resplit  46411  meaiuninclem  46485  caratheodorylem1  46531  hoicvr  46553  hoicvrrex  46561  hoidmvlelem3  46602  hoidmvlelem4  46603  gricrel  47923  grlicrel  48002