Theorem sseqtri 3971

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

Syntax hints:   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseqtrri  3972  3sstr3i  3973  eqimssi  3983  abssi  4009  ssun2  4120  unixpss  5759  0ima  6037  mptexgf  7170  difex2  7707  oelim2  8524  omopthlem2  8589  sbthlem7  9024  unifpw  9258  fiuni  9334  dmttrcl  9633  rnttrcl  9634  ttrclexg  9635  rankuni  9778  rankc2  9786  rankxpu  9791  rankmapu  9793  rankxplim  9794  infxpenlem  9926  cf0  10164  fin23lem17  10251  fin23lem31  10256  smobeth  10500  nqerf  10844  dmrecnq  10882  ackbijnn  15784  divalglem2  16355  divalglem5  16357  bitsfzolem  16394  0bits  16399  bezoutlem2  16500  bezoutlem3  16501  lcmcllem  16556  lcmledvds  16559  lcmfval  16581  lcmfcllem  16585  lcmfledvds  16592  odzcllem  16754  odzdvds  16757  unbenlem  16870  4sqlem13  16919  4sqlem14  16920  4sqlem17  16923  4sqlem18  16924  vdwlem8  16950  vdwnnlem3  16959  ramcl2lem  16971  ramtcl  16972  ramtub  16974  strle1  17119  prdsvallem  17408  wunfunc  17859  wunnat  17917  psssdm2  18538  tsrss  18546  gicer  19243  symgsssg  19433  symgfisg  19434  odfval  19498  odlem2  19505  gexlem2  19548  torsubg  19820  dprd2da  20010  zringlpirlem2  21453  zringlpirlem3  21454  fermltlchr  21519  pjfval  21696  pjpm  21698  toponsspwpw  22897  eltg4i  22935  ntrss2  23032  isopn3  23041  mretopd  23067  leordtval2  23187  ptbasfi  23556  hmphtop  23753  hmpher  23759  restutop  24212  ucnprima  24256  tngtopn  24625  tgioo  24771  xrtgioo  24782  ovolicc2lem4  25497  nulmbl2  25513  iundisj  25525  dyadmax  25575  i1f1  25667  dvfval  25874  dvcnp2  25897  lhop1lem  25990  lhop2  25992  elqaalem1  26296  elqaalem3  26298  taylthlem2  26351  taylthlem2OLD  26352  pserulm  26400  psercn2  26401  psercnlem2  26402  psercnlem1  26403  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  pserdv2  26408  abelth  26419  dvlog  26628  efopnlem2  26634  logtayl  26637  cxpcn3lem  26724  cxpcn3  26725  resqrtcn  26726  dvatan  26912  atancn  26913  rlimcnp  26942  rlimcnp2  26943  wilthlem3  27047  ftalem4  27053  ftalem5  27054  dchrisum0lem2a  27494  bdayimaon  27671  noetasuplem4  27714  noetainflem4  27718  nobdaymin  27759  nocvxminlem  27760  noeta2  27767  etaslts2  27800  cutbdaybnd2lim  27803  bday1  27820  lrrecfr  27949  addbdaylem  28023  negsunif  28061  oniso  28277  bdayons  28282  cchhllem  28969  axlowdimlem6  29030  hhssabloilem  31347  choc1  31413  chub2i  31556  span0  31628  spanuni  31630  sshhococi  31632  chsup0  31634  spansnpji  31664  mayetes3i  31815  nlelshi  32146  pjimai  32262  pj3i  32294  shatomistici  32447  hatomistici  32448  atcvat4i  32483  iundisjf  32674  rinvf1o  32718  mptctf  32804  iundisjfi  32884  xrge0mulgnn0  33090  gsumpart  33139  znfermltl  33441  ply1degltel  33669  ply1degleel  33670  ply1degltlss  33671  ccfldsrarelvec  33831  ccfldextdgrr  33832  2sqr3minply  33940  xrge0iifcnv  34093  xrge0iifiso  34095  xrge0iifhom  34097  esumcvgsum  34248  coinfliprv  34643  signsply0  34711  signstcl  34725  signstf  34726  kur14lem6  35409  mthmsta  35776  filnetlem3  36578  filnetlem4  36579  onint1  36647  oninhaus  36648  bj-nuliotaALT  37381  imadifss  37930  poimirlem3  37958  poimirlem32  37987  dvtan  38005  itg2addnclem2  38007  ftc1anclem6  38033  heiborlem3  38148  isdrngo2  38293  elrfi  43140  mapfzcons1  43163  eldioph4b  43257  dnnumch3lem  43492  dnnumch3  43493  dgraalem  43591  dgraaub  43594  resnonrel  44037  cotrcltrcl  44170  cotrclrcl  44187  frege131d  44209  binomcxplemdvbinom  44798  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  relopabVD  45345  rabexgf  45473  fzssnn0  45767  iuneqfzuzlem  45782  allbutfiinf  45866  uzublem  45876  sumnnodd  46078  lptioo2cn  46091  lptioo1cn  46092  fourierdlem31  46584  fourierdlem102  46654  fourierdlem114  46666  fouriercn  46678  elaa2lem  46679  etransclem48  46728  salexct  46780  salgencntex  46789  sge0resplit  46852  meaiuninclem  46926  caratheodorylem1  46972  hoicvr  46994  hoicvrrex  47002  hoidmvlelem3  47043  hoidmvlelem4  47044  gricrel  48407  grlicrel  48494