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 230	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  sseqtrri  3983  3sstr3i  3984  eqimssi  3994  abssi  4020  ssun2  4131  unixpss  5759  0ima  6037  mptexgf  7168  difex2  7705  oelim2  8523  omopthlem2  8588  sbthlem7  9021  unifpw  9255  fiuni  9331  dmttrcl  9630  rnttrcl  9631  ttrclexg  9632  rankuni  9775  rankc2  9783  rankxpu  9788  rankmapu  9790  rankxplim  9791  infxpenlem  9923  cf0  10161  fin23lem17  10248  fin23lem31  10253  smobeth  10497  nqerf  10841  dmrecnq  10879  ackbijnn  15751  divalglem2  16322  divalglem5  16324  bitsfzolem  16361  0bits  16366  bezoutlem2  16467  bezoutlem3  16468  lcmcllem  16523  lcmledvds  16526  lcmfval  16548  lcmfcllem  16552  lcmfledvds  16559  odzcllem  16720  odzdvds  16723  unbenlem  16836  4sqlem13  16885  4sqlem14  16886  4sqlem17  16889  4sqlem18  16890  vdwlem8  16916  vdwnnlem3  16925  ramcl2lem  16937  ramtcl  16938  ramtub  16940  strle1  17085  prdsvallem  17374  wunfunc  17825  wunnat  17883  psssdm2  18504  tsrss  18512  gicer  19206  symgsssg  19396  symgfisg  19397  odfval  19461  odlem2  19468  gexlem2  19511  torsubg  19783  dprd2da  19973  zringlpirlem2  21418  zringlpirlem3  21419  fermltlchr  21484  pjfval  21661  pjpm  21663  toponsspwpw  22866  eltg4i  22904  ntrss2  23001  isopn3  23010  mretopd  23036  leordtval2  23156  ptbasfi  23525  hmphtop  23722  hmpher  23728  restutop  24181  ucnprima  24225  tngtopn  24594  tgioo  24740  xrtgioo  24751  ovolicc2lem4  25477  nulmbl2  25493  iundisj  25505  dyadmax  25555  i1f1  25647  dvfval  25854  dvcnp2  25877  dvcnp2OLD  25878  lhop1lem  25974  lhop2  25976  elqaalem1  26283  elqaalem3  26285  taylthlem2  26338  taylthlem2OLD  26339  pserulm  26387  psercn2  26388  psercn2OLD  26389  psercnlem2  26390  psercnlem1  26391  psercn  26392  pserdvlem1  26393  pserdvlem2  26394  pserdv  26395  pserdv2  26396  abelth  26407  dvlog  26616  efopnlem2  26622  logtayl  26625  cxpcn3lem  26713  cxpcn3  26714  resqrtcn  26715  dvatan  26901  atancn  26902  rlimcnp  26931  rlimcnp2  26932  wilthlem3  27036  ftalem4  27042  ftalem5  27043  dchrisum0lem2a  27484  bdayimaon  27661  noetasuplem4  27704  noetainflem4  27708  nobdaymin  27749  nocvxminlem  27750  noeta2  27757  etaslts2  27790  cutbdaybnd2lim  27793  bday1  27810  lrrecfr  27939  addbdaylem  28013  negsunif  28051  oniso  28267  bdayons  28272  cchhllem  28959  axlowdimlem6  29020  hhssabloilem  31336  choc1  31402  chub2i  31545  span0  31617  spanuni  31619  sshhococi  31621  chsup0  31623  spansnpji  31653  mayetes3i  31804  nlelshi  32135  pjimai  32251  pj3i  32283  shatomistici  32436  hatomistici  32437  atcvat4i  32472  iundisjf  32664  rinvf1o  32708  mptctf  32795  iundisjfi  32876  xrge0mulgnn0  33097  gsumpart  33146  znfermltl  33447  ply1degltel  33675  ply1degleel  33676  ply1degltlss  33677  ccfldsrarelvec  33828  ccfldextdgrr  33829  2sqr3minply  33937  xrge0iifcnv  34090  xrge0iifiso  34092  xrge0iifhom  34094  esumcvgsum  34245  coinfliprv  34640  signsply0  34708  signstcl  34722  signstf  34723  kur14lem6  35405  mthmsta  35772  filnetlem3  36574  filnetlem4  36575  onint1  36643  oninhaus  36644  bj-nuliotaALT  37259  imadifss  37792  poimirlem3  37820  poimirlem32  37849  dvtan  37867  itg2addnclem2  37869  ftc1anclem6  37895  heiborlem3  38010  isdrngo2  38155  elrfi  42932  mapfzcons1  42955  eldioph4b  43049  dnnumch3lem  43284  dnnumch3  43285  dgraalem  43383  dgraaub  43386  resnonrel  43829  cotrcltrcl  43962  cotrclrcl  43979  frege131d  44001  binomcxplemdvbinom  44590  binomcxplemdvsum  44592  binomcxplemnotnn0  44593  relopabVD  45137  rabexgf  45265  fzssnn0  45560  iuneqfzuzlem  45575  allbutfiinf  45660  uzublem  45670  sumnnodd  45872  lptioo2cn  45885  lptioo1cn  45886  fourierdlem31  46378  fourierdlem102  46448  fourierdlem114  46460  fouriercn  46472  elaa2lem  46473  etransclem48  46522  salexct  46574  salgencntex  46583  sge0resplit  46646  meaiuninclem  46720  caratheodorylem1  46766  hoicvr  46788  hoicvrrex  46796  hoidmvlelem3  46837  hoidmvlelem4  46838  gricrel  48161  grlicrel  48248