Theorem sseqtri 4031

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

Syntax hints:   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  sseqtrri  4032  eqimssi  4055  abssi  4079  ssun2  4188  unixpss  5822  0ima  6097  fvssunirnOLD  6940  mptexgf  7241  difex2  7778  oelim2  8631  omopthlem2  8696  sbthlem7  9127  unifpw  9392  fiuni  9465  dmttrcl  9758  rnttrcl  9759  ttrclexg  9760  rankuni  9900  rankc2  9908  rankxpu  9913  rankmapu  9915  rankxplim  9916  infxpenlem  10050  cf0  10288  fin23lem17  10375  fin23lem31  10380  smobeth  10623  nqerf  10967  dmrecnq  11005  ackbijnn  15860  divalglem2  16428  divalglem5  16430  bitsfzolem  16467  0bits  16472  bezoutlem2  16573  bezoutlem3  16574  lcmcllem  16629  lcmledvds  16632  lcmfval  16654  lcmfcllem  16658  lcmfledvds  16665  odzcllem  16825  odzdvds  16828  unbenlem  16941  4sqlem13  16990  4sqlem14  16991  4sqlem17  16994  4sqlem18  16995  vdwlem8  17021  vdwnnlem3  17030  ramcl2lem  17042  ramtcl  17043  ramtub  17045  strle1  17191  prdsvallem  17500  wunfunc  17951  wunfuncOLD  17952  wunnat  18010  wunnatOLD  18011  psssdm2  18638  tsrss  18646  gicer  19307  symgsssg  19499  symgfisg  19500  odfval  19564  odlem2  19571  gexlem2  19614  torsubg  19886  dprd2da  20076  zringlpirlem2  21491  zringlpirlem3  21492  fermltlchr  21561  pjfval  21743  pjpm  21745  toponsspwpw  22943  eltg4i  22982  ntrss2  23080  isopn3  23089  mretopd  23115  leordtval2  23235  ptbasfi  23604  hmphtop  23801  hmpher  23807  restutop  24261  ucnprima  24306  tngtopn  24686  tgioo  24831  xrtgioo  24841  ovolicc2lem4  25568  nulmbl2  25584  iundisj  25596  dyadmax  25646  i1f1  25738  dvfval  25946  dvcnp2  25969  dvcnp2OLD  25970  lhop1lem  26066  lhop2  26068  elqaalem1  26375  elqaalem3  26377  taylthlem2  26430  taylthlem2OLD  26431  pserulm  26479  psercn2  26480  psercn2OLD  26481  psercnlem2  26482  psercnlem1  26483  psercn  26484  pserdvlem1  26485  pserdvlem2  26486  pserdv  26487  pserdv2  26488  abelth  26499  dvlog  26707  efopnlem2  26713  logtayl  26716  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  dvatan  26992  atancn  26993  rlimcnp  27022  rlimcnp2  27023  wilthlem3  27127  ftalem4  27133  ftalem5  27134  dchrisum0lem2a  27575  bdayimaon  27752  noetasuplem4  27795  noetainflem4  27799  nocvxminlem  27836  nocvxmin  27837  noeta2  27843  etasslt2  27873  scutbdaybnd2lim  27876  bday1s  27890  lrrecfr  27990  addsbdaylem  28063  negsunif  28101  zs12bday  28438  cchhllem  28915  cchhllemOLD  28916  axlowdimlem6  28976  hhssabloilem  31289  choc1  31355  chub2i  31498  span0  31570  spanuni  31572  sshhococi  31574  chsup0  31576  spansnpji  31606  mayetes3i  31757  nlelshi  32088  pjimai  32204  pj3i  32236  shatomistici  32389  hatomistici  32390  atcvat4i  32425  iundisjf  32608  rinvf1o  32646  mptctf  32734  iundisjfi  32803  xrge0mulgnn0  33002  gsumpart  33042  znfermltl  33373  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ccfldsrarelvec  33695  ccfldextdgrr  33696  2sqr3minply  33752  xrge0iifcnv  33893  xrge0iifiso  33895  xrge0iifhom  33897  esumcvgsum  34068  coinfliprv  34463  signsply0  34544  signstcl  34558  signstf  34559  kur14lem6  35195  mthmsta  35562  filnetlem3  36362  filnetlem4  36363  onint1  36431  oninhaus  36432  bj-nuliotaALT  37040  imadifss  37581  poimirlem3  37609  poimirlem32  37638  dvtan  37656  itg2addnclem2  37658  ftc1anclem6  37684  heiborlem3  37799  isdrngo2  37944  elrfi  42681  mapfzcons1  42704  eldioph4b  42798  dnnumch3lem  43034  dnnumch3  43035  dgraalem  43133  dgraaub  43136  resnonrel  43581  cotrcltrcl  43714  cotrclrcl  43731  frege131d  43753  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  relopabVD  44898  rabexgf  44961  fzssnn0  45267  iuneqfzuzlem  45283  allbutfiinf  45369  uzublem  45379  sumnnodd  45585  lptioo2cn  45600  lptioo1cn  45601  fourierdlem31  46093  fourierdlem102  46163  fourierdlem114  46175  fouriercn  46187  elaa2lem  46188  etransclem48  46237  salexct  46289  salgencntex  46298  sge0resplit  46361  meaiuninclem  46435  caratheodorylem1  46481  hoicvr  46503  hoicvrrex  46511  hoidmvlelem3  46552  hoidmvlelem4  46553  gricrel  47825  grlicrel  47901