Theorem sseqtri 3995

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  sseqtrri  3996  3sstr3i  3997  eqimssi  4007  abssi  4033  ssun2  4142  unixpss  5773  0ima  6049  fvssunirnOLD  6892  mptexgf  7196  difex2  7736  oelim2  8559  omopthlem2  8624  sbthlem7  9057  unifpw  9306  fiuni  9379  dmttrcl  9674  rnttrcl  9675  ttrclexg  9676  rankuni  9816  rankc2  9824  rankxpu  9829  rankmapu  9831  rankxplim  9832  infxpenlem  9966  cf0  10204  fin23lem17  10291  fin23lem31  10296  smobeth  10539  nqerf  10883  dmrecnq  10921  ackbijnn  15794  divalglem2  16365  divalglem5  16367  bitsfzolem  16404  0bits  16409  bezoutlem2  16510  bezoutlem3  16511  lcmcllem  16566  lcmledvds  16569  lcmfval  16591  lcmfcllem  16595  lcmfledvds  16602  odzcllem  16763  odzdvds  16766  unbenlem  16879  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwlem8  16959  vdwnnlem3  16968  ramcl2lem  16980  ramtcl  16981  ramtub  16983  strle1  17128  prdsvallem  17417  wunfunc  17863  wunnat  17921  psssdm2  18540  tsrss  18548  gicer  19209  symgsssg  19397  symgfisg  19398  odfval  19462  odlem2  19469  gexlem2  19512  torsubg  19784  dprd2da  19974  zringlpirlem2  21373  zringlpirlem3  21374  fermltlchr  21439  pjfval  21615  pjpm  21617  toponsspwpw  22809  eltg4i  22847  ntrss2  22944  isopn3  22953  mretopd  22979  leordtval2  23099  ptbasfi  23468  hmphtop  23665  hmpher  23671  restutop  24125  ucnprima  24169  tngtopn  24538  tgioo  24684  xrtgioo  24695  ovolicc2lem4  25421  nulmbl2  25437  iundisj  25449  dyadmax  25499  i1f1  25591  dvfval  25798  dvcnp2  25821  dvcnp2OLD  25822  lhop1lem  25918  lhop2  25920  elqaalem1  26227  elqaalem3  26229  taylthlem2  26282  taylthlem2OLD  26283  pserulm  26331  psercn2  26332  psercn2OLD  26333  psercnlem2  26334  psercnlem1  26335  psercn  26336  pserdvlem1  26337  pserdvlem2  26338  pserdv  26339  pserdv2  26340  abelth  26351  dvlog  26560  efopnlem2  26566  logtayl  26569  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  dvatan  26845  atancn  26846  rlimcnp  26875  rlimcnp2  26876  wilthlem3  26980  ftalem4  26986  ftalem5  26987  dchrisum0lem2a  27428  bdayimaon  27605  noetasuplem4  27648  noetainflem4  27652  nocvxminlem  27689  nocvxmin  27690  noeta2  27696  etasslt2  27726  scutbdaybnd2lim  27729  bday1s  27743  lrrecfr  27850  addsbdaylem  27923  negsunif  27961  onsiso  28169  bdayon  28173  zs12bday  28343  cchhllem  28814  axlowdimlem6  28874  hhssabloilem  31190  choc1  31256  chub2i  31399  span0  31471  spanuni  31473  sshhococi  31475  chsup0  31477  spansnpji  31507  mayetes3i  31658  nlelshi  31989  pjimai  32105  pj3i  32137  shatomistici  32290  hatomistici  32291  atcvat4i  32326  iundisjf  32518  rinvf1o  32554  mptctf  32641  iundisjfi  32719  xrge0mulgnn0  32956  gsumpart  32997  znfermltl  33337  ply1degltel  33560  ply1degleel  33561  ply1degltlss  33562  ccfldsrarelvec  33666  ccfldextdgrr  33667  2sqr3minply  33770  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  esumcvgsum  34078  coinfliprv  34474  signsply0  34542  signstcl  34556  signstf  34557  kur14lem6  35198  mthmsta  35565  filnetlem3  36368  filnetlem4  36369  onint1  36437  oninhaus  36438  bj-nuliotaALT  37046  imadifss  37589  poimirlem3  37617  poimirlem32  37646  dvtan  37664  itg2addnclem2  37666  ftc1anclem6  37692  heiborlem3  37807  isdrngo2  37952  elrfi  42682  mapfzcons1  42705  eldioph4b  42799  dnnumch3lem  43035  dnnumch3  43036  dgraalem  43134  dgraaub  43137  resnonrel  43581  cotrcltrcl  43714  cotrclrcl  43731  frege131d  43753  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  relopabVD  44890  rabexgf  45018  fzssnn0  45314  iuneqfzuzlem  45330  allbutfiinf  45416  uzublem  45426  sumnnodd  45628  lptioo2cn  45643  lptioo1cn  45644  fourierdlem31  46136  fourierdlem102  46206  fourierdlem114  46218  fouriercn  46230  elaa2lem  46231  etransclem48  46280  salexct  46332  salgencntex  46341  sge0resplit  46404  meaiuninclem  46478  caratheodorylem1  46524  hoicvr  46546  hoicvrrex  46554  hoidmvlelem3  46595  hoidmvlelem4  46596  gricrel  47919  grlicrel  47998