Theorem sseqtri 4007

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

Syntax hints:   = wceq 1540   ⊆ wss 3926

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  sseqtrri  4008  3sstr3i  4009  eqimssi  4019  abssi  4045  ssun2  4154  unixpss  5789  0ima  6065  fvssunirnOLD  6909  mptexgf  7213  difex2  7752  oelim2  8605  omopthlem2  8670  sbthlem7  9101  unifpw  9365  fiuni  9438  dmttrcl  9733  rnttrcl  9734  ttrclexg  9735  rankuni  9875  rankc2  9883  rankxpu  9888  rankmapu  9890  rankxplim  9891  infxpenlem  10025  cf0  10263  fin23lem17  10350  fin23lem31  10355  smobeth  10598  nqerf  10942  dmrecnq  10980  ackbijnn  15842  divalglem2  16412  divalglem5  16414  bitsfzolem  16451  0bits  16456  bezoutlem2  16557  bezoutlem3  16558  lcmcllem  16613  lcmledvds  16616  lcmfval  16638  lcmfcllem  16642  lcmfledvds  16649  odzcllem  16810  odzdvds  16813  unbenlem  16926  4sqlem13  16975  4sqlem14  16976  4sqlem17  16979  4sqlem18  16980  vdwlem8  17006  vdwnnlem3  17015  ramcl2lem  17027  ramtcl  17028  ramtub  17030  strle1  17175  prdsvallem  17466  wunfunc  17912  wunnat  17970  psssdm2  18589  tsrss  18597  gicer  19258  symgsssg  19446  symgfisg  19447  odfval  19511  odlem2  19518  gexlem2  19561  torsubg  19833  dprd2da  20023  zringlpirlem2  21422  zringlpirlem3  21423  fermltlchr  21488  pjfval  21664  pjpm  21666  toponsspwpw  22858  eltg4i  22896  ntrss2  22993  isopn3  23002  mretopd  23028  leordtval2  23148  ptbasfi  23517  hmphtop  23714  hmpher  23720  restutop  24174  ucnprima  24218  tngtopn  24587  tgioo  24733  xrtgioo  24744  ovolicc2lem4  25471  nulmbl2  25487  iundisj  25499  dyadmax  25549  i1f1  25641  dvfval  25848  dvcnp2  25871  dvcnp2OLD  25872  lhop1lem  25968  lhop2  25970  elqaalem1  26277  elqaalem3  26279  taylthlem2  26332  taylthlem2OLD  26333  pserulm  26381  psercn2  26382  psercn2OLD  26383  psercnlem2  26384  psercnlem1  26385  psercn  26386  pserdvlem1  26387  pserdvlem2  26388  pserdv  26389  pserdv2  26390  abelth  26401  dvlog  26610  efopnlem2  26616  logtayl  26619  cxpcn3lem  26707  cxpcn3  26708  resqrtcn  26709  dvatan  26895  atancn  26896  rlimcnp  26925  rlimcnp2  26926  wilthlem3  27030  ftalem4  27036  ftalem5  27037  dchrisum0lem2a  27478  bdayimaon  27655  noetasuplem4  27698  noetainflem4  27702  nocvxminlem  27739  nocvxmin  27740  noeta2  27746  etasslt2  27776  scutbdaybnd2lim  27779  bday1s  27793  lrrecfr  27893  addsbdaylem  27966  negsunif  28004  zs12bday  28341  cchhllem  28812  axlowdimlem6  28872  hhssabloilem  31188  choc1  31254  chub2i  31397  span0  31469  spanuni  31471  sshhococi  31473  chsup0  31475  spansnpji  31505  mayetes3i  31656  nlelshi  31987  pjimai  32103  pj3i  32135  shatomistici  32288  hatomistici  32289  atcvat4i  32324  iundisjf  32516  rinvf1o  32554  mptctf  32641  iundisjfi  32719  xrge0mulgnn0  32956  gsumpart  32997  znfermltl  33327  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ccfldsrarelvec  33658  ccfldextdgrr  33659  2sqr3minply  33760  xrge0iifcnv  33910  xrge0iifiso  33912  xrge0iifhom  33914  esumcvgsum  34065  coinfliprv  34461  signsply0  34529  signstcl  34543  signstf  34544  kur14lem6  35179  mthmsta  35546  filnetlem3  36344  filnetlem4  36345  onint1  36413  oninhaus  36414  bj-nuliotaALT  37022  imadifss  37565  poimirlem3  37593  poimirlem32  37622  dvtan  37640  itg2addnclem2  37642  ftc1anclem6  37668  heiborlem3  37783  isdrngo2  37928  elrfi  42664  mapfzcons1  42687  eldioph4b  42781  dnnumch3lem  43017  dnnumch3  43018  dgraalem  43116  dgraaub  43119  resnonrel  43563  cotrcltrcl  43696  cotrclrcl  43713  frege131d  43735  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  relopabVD  44873  rabexgf  44996  fzssnn0  45293  iuneqfzuzlem  45309  allbutfiinf  45395  uzublem  45405  sumnnodd  45607  lptioo2cn  45622  lptioo1cn  45623  fourierdlem31  46115  fourierdlem102  46185  fourierdlem114  46197  fouriercn  46209  elaa2lem  46210  etransclem48  46259  salexct  46311  salgencntex  46320  sge0resplit  46383  meaiuninclem  46457  caratheodorylem1  46503  hoicvr  46525  hoicvrrex  46533  hoidmvlelem3  46574  hoidmvlelem4  46575  gricrel  47880  grlicrel  47959