Theorem sseqtri 3982

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 3963	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	mpbi 233	1 ⊢ 𝐴 ⊆ 𝐶

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  sseqtrri  3983  3sstr3i  3984  eqimssi  3994  abssi  4019  ssun2  4128  unixpss  5795  0ima  6078  imadifssran  6201  mptexgf  7225  difex2  7763  oelim2  8587  omopthlem2  8652  sbthlem7  9095  unifpw  9326  fiuni  9402  dmttrcl  9704  rnttrcl  9705  ttrclexg  9706  rankuni  9849  rankc2  9857  rankxpu  9862  rankmapu  9864  rankxplim  9865  infxpenlem  10020  cf0  10256  fin23lem17  10344  fin23lem31  10349  smobeth  10599  nqerf  10943  dmrecnq  10981  ackbijnn  15921  divalglem2  16491  divalglem5  16493  bitsfzolem  16530  0bits  16535  bezoutlem2  16636  bezoutlem3  16637  lcmcllem  16692  lcmledvds  16695  lcmfval  16717  lcmfcllem  16721  lcmfledvds  16728  odzcllem  16890  odzdvds  16893  unbenlem  17006  4sqlem13  17055  4sqlem14  17056  4sqlem17  17059  4sqlem18  17060  vdwlem8  17086  vdwnnlem3  17095  ramcl2lem  17107  ramtcl  17108  ramtub  17110  strle1  17256  prdsvallem  17545  wunfunc  17996  wunnat  18054  psssdm2  18675  tsrss  18683  gicer  19410  symgsssg  19600  symgfisg  19601  odfval  19665  odlem2  19672  gexlem2  19715  torsubg  19987  dprd2da  20177  ricrel  20661  zringlpirlem2  21682  zringlpirlem3  21683  fermltlchr  21748  pjfval  21925  pjpm  21927  toponsspwpw  23153  eltg4i  23191  ntrss2  23288  isopn3  23297  mretopd  23323  leordtval2  23443  ptbasfi  23813  hmphtop  24010  hmpher  24016  restutop  24469  ucnprima  24513  tngtopn  24882  tgioo  25028  xrtgioo  25039  ovolicc2lem4  25754  nulmbl2  25770  iundisj  25782  dyadmax  25832  i1f1  25924  dvfval  26131  dvcnp2  26154  lhop1lem  26247  lhop2  26249  elqaalem1  26558  elqaalem3  26560  taylthlem2  26617  pserulm  26665  psercn2  26666  psercnlem2  26667  psercnlem1  26668  psercn  26669  pserdvlem1  26670  pserdvlem2  26671  pserdv  26672  pserdv2  26673  abelth  26684  dvlog  26896  efopnlem2  26902  logtayl  26905  cxpcn3lem  26992  cxpcn3  26993  resqrtcn  26994  dvatan  27180  atancn  27181  rlimcnp  27210  rlimcnp2  27211  wilthlem3  27314  ftalem4  27320  ftalem5  27321  dchrisum0lem2a  27761  bdayimaon  27937  noetasuplem4  27980  noetainflem4  27984  nobdaymin  28026  nocvxminlem  28027  noeta2  28034  etaslts2  28067  cutbdaybnd2lim  28070  bday1  28087  lrrecfr  28216  addbdaylem  28290  negsunif  28328  oniso  28544  bdayons  28549  cchhllem  29351  axlowdimlem6  29412  hhssabloilem  31750  choc1  31816  chub2i  31959  span0  32031  spanuni  32033  sshhococi  32035  chsup0  32037  spansnpji  32067  mayetes3i  32218  nlelshi  32549  pjimai  32665  pj3i  32697  shatomistici  32850  hatomistici  32851  atcvat4i  32886  iundisjf  33070  rinvf1o  33111  mptctf  33195  iundisjfi  33275  xrge0mulgnn0  33463  gsumpart  33511  znfermltl  33809  ply1degltel  34012  ply1degleel  34013  ply1degltlss  34014  0mplrim  34032  ccfldsrarelvec  34189  ccfldextdgrr  34190  2sqr3minply  34298  xrge0iifcnv  34451  xrge0iifiso  34453  xrge0iifhom  34455  esumcvgsum  34606  coinfliprv  35002  signsply0  35067  signstcl  35081  signstf  35082  kur14lem6  35798  mthmsta  36165  filnetlem3  37007  filnetlem4  37008  onint1  37076  oninhaus  37077  bj-nuliotaALT  37810  imadifss  38362  poimirlem3  38380  poimirlem32  38409  dvtan  38427  itg2addnclem2  38429  ftc1anclem6  38455  heiborlem3  38571  isdrngo2  38716  elrfi  43547  mapfzcons1  43570  eldioph4b  43660  dnnumch3lem  43895  dnnumch3  43896  dgraalem  43994  dgraaub  43997  resnonrel  44440  cotrcltrcl  44573  cotrclrcl  44590  frege131d  44612  binomcxplemdvbinom  45185  binomcxplemdvsum  45187  binomcxplemnotnn0  45188  relopabVD  45731  rabexgf  45866  fzssnn0  46157  iuneqfzuzlem  46172  allbutfiinf  46256  uzublem  46266  sumnnodd  46468  lptioo2cn  46481  lptioo1cn  46482  fourierdlem31  46974  fourierdlem102  47044  fourierdlem114  47056  fouriercn  47068  elaa2lem  47069  etransclem48  47118  salexct  47170  salgencntex  47179  sge0resplit  47242  meaiuninclem  47316  caratheodorylem1  47362  hoicvr  47384  hoicvrrex  47392  hoidmvlelem3  47433  hoidmvlelem4  47434  gricrel  48843  grlicrel  48930