Theorem sseqtri 3987

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

Syntax hints:   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseqtrri  3988  3sstr3i  3989  eqimssi  3999  abssi  4024  ssun2  4134  unixpss  5788  0ima  6071  mptexgf  7210  difex2  7747  oelim2  8569  omopthlem2  8634  sbthlem7  9069  unifpw  9300  fiuni  9376  dmttrcl  9678  rnttrcl  9679  ttrclexg  9680  rankuni  9823  rankc2  9831  rankxpu  9836  rankmapu  9838  rankxplim  9839  infxpenlem  9985  cf0  10222  fin23lem17  10310  fin23lem31  10315  smobeth  10559  nqerf  10903  dmrecnq  10941  ackbijnn  15872  divalglem2  16443  divalglem5  16445  bitsfzolem  16482  0bits  16487  bezoutlem2  16588  bezoutlem3  16589  lcmcllem  16644  lcmledvds  16647  lcmfval  16669  lcmfcllem  16673  lcmfledvds  16680  odzcllem  16842  odzdvds  16845  unbenlem  16958  4sqlem13  17007  4sqlem14  17008  4sqlem17  17011  4sqlem18  17012  vdwlem8  17038  vdwnnlem3  17047  ramcl2lem  17059  ramtcl  17060  ramtub  17062  strle1  17208  prdsvallem  17497  wunfunc  17948  wunnat  18006  psssdm2  18627  tsrss  18635  gicer  19338  symgsssg  19528  symgfisg  19529  odfval  19593  odlem2  19600  gexlem2  19643  torsubg  19915  dprd2da  20105  zringlpirlem2  21573  zringlpirlem3  21574  fermltlchr  21639  pjfval  21816  pjpm  21818  toponsspwpw  23040  eltg4i  23078  ntrss2  23175  isopn3  23184  mretopd  23210  leordtval2  23330  ptbasfi  23699  hmphtop  23896  hmpher  23902  restutop  24355  ucnprima  24399  tngtopn  24768  tgioo  24914  xrtgioo  24925  ovolicc2lem4  25640  nulmbl2  25656  iundisj  25668  dyadmax  25718  i1f1  25810  dvfval  26017  dvcnp2  26040  lhop1lem  26133  lhop2  26135  elqaalem1  26441  elqaalem3  26443  taylthlem2  26495  pserulm  26543  psercn2  26544  psercnlem2  26545  psercnlem1  26546  psercn  26547  pserdvlem1  26548  pserdvlem2  26549  pserdv  26550  pserdv2  26551  abelth  26562  dvlog  26774  efopnlem2  26780  logtayl  26783  cxpcn3lem  26870  cxpcn3  26871  resqrtcn  26872  dvatan  27058  atancn  27059  rlimcnp  27088  rlimcnp2  27089  wilthlem3  27192  ftalem4  27198  ftalem5  27199  dchrisum0lem2a  27639  bdayimaon  27815  noetasuplem4  27858  noetainflem4  27862  nobdaymin  27904  nocvxminlem  27905  noeta2  27912  etaslts2  27945  cutbdaybnd2lim  27948  bday1  27965  lrrecfr  28094  addbdaylem  28168  negsunif  28206  oniso  28422  bdayons  28427  cchhllem  29145  axlowdimlem6  29206  hhssabloilem  31522  choc1  31588  chub2i  31731  span0  31803  spanuni  31805  sshhococi  31807  chsup0  31809  spansnpji  31839  mayetes3i  31990  nlelshi  32321  pjimai  32437  pj3i  32469  shatomistici  32622  hatomistici  32623  atcvat4i  32658  iundisjf  32844  rinvf1o  32887  mptctf  32973  iundisjfi  33053  xrge0mulgnn0  33248  gsumpart  33296  znfermltl  33596  ply1degltel  33801  ply1degleel  33802  ply1degltlss  33803  0mplrim  33821  ccfldsrarelvec  33978  ccfldextdgrr  33979  2sqr3minply  34087  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  esumcvgsum  34395  coinfliprv  34790  signsply0  34855  signstcl  34869  signstf  34870  kur14lem6  35574  mthmsta  35941  filnetlem3  36753  filnetlem4  36754  onint1  36822  oninhaus  36823  bj-nuliotaALT  37555  imadifss  38106  poimirlem3  38134  poimirlem32  38163  dvtan  38181  itg2addnclem2  38183  ftc1anclem6  38209  heiborlem3  38324  isdrngo2  38469  elrfi  43287  mapfzcons1  43310  eldioph4b  43400  dnnumch3lem  43635  dnnumch3  43636  dgraalem  43734  dgraaub  43737  resnonrel  44180  cotrcltrcl  44313  cotrclrcl  44330  frege131d  44352  binomcxplemdvbinom  44927  binomcxplemdvsum  44929  binomcxplemnotnn0  44930  relopabVD  45474  rabexgf  45602  fzssnn0  45893  iuneqfzuzlem  45908  allbutfiinf  45992  uzublem  46002  sumnnodd  46204  lptioo2cn  46217  lptioo1cn  46218  fourierdlem31  46710  fourierdlem102  46780  fourierdlem114  46792  fouriercn  46804  elaa2lem  46805  etransclem48  46854  salexct  46906  salgencntex  46915  sge0resplit  46978  meaiuninclem  47052  caratheodorylem1  47098  hoicvr  47120  hoicvrrex  47128  hoidmvlelem3  47169  hoidmvlelem4  47170  gricrel  48539  grlicrel  48626