Theorem sseqtri 3970

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

Syntax hints:   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  sseqtrri  3971  3sstr3i  3972  eqimssi  3982  abssi  4006  ssun2  4115  unixpss  5760  0ima  6037  mptexgf  7173  difex2  7710  oelim2  8528  omopthlem2  8593  sbthlem7  9028  unifpw  9262  fiuni  9338  dmttrcl  9640  rnttrcl  9641  ttrclexg  9642  rankuni  9785  rankc2  9793  rankxpu  9798  rankmapu  9800  rankxplim  9801  infxpenlem  9933  cf0  10171  fin23lem17  10258  fin23lem31  10263  smobeth  10507  nqerf  10851  dmrecnq  10889  ackbijnn  15791  divalglem2  16362  divalglem5  16364  bitsfzolem  16401  0bits  16406  bezoutlem2  16507  bezoutlem3  16508  lcmcllem  16563  lcmledvds  16566  lcmfval  16588  lcmfcllem  16592  lcmfledvds  16599  odzcllem  16761  odzdvds  16764  unbenlem  16877  4sqlem13  16926  4sqlem14  16927  4sqlem17  16930  4sqlem18  16931  vdwlem8  16957  vdwnnlem3  16966  ramcl2lem  16978  ramtcl  16979  ramtub  16981  strle1  17126  prdsvallem  17415  wunfunc  17866  wunnat  17924  psssdm2  18545  tsrss  18553  gicer  19250  symgsssg  19440  symgfisg  19441  odfval  19505  odlem2  19512  gexlem2  19555  torsubg  19827  dprd2da  20017  zringlpirlem2  21445  zringlpirlem3  21446  fermltlchr  21511  pjfval  21688  pjpm  21690  toponsspwpw  22912  eltg4i  22950  ntrss2  23047  isopn3  23056  mretopd  23082  leordtval2  23202  ptbasfi  23571  hmphtop  23768  hmpher  23774  restutop  24227  ucnprima  24271  tngtopn  24640  tgioo  24786  xrtgioo  24797  ovolicc2lem4  25512  nulmbl2  25528  iundisj  25540  dyadmax  25590  i1f1  25682  dvfval  25889  dvcnp2  25912  lhop1lem  26005  lhop2  26007  elqaalem1  26310  elqaalem3  26312  taylthlem2  26364  pserulm  26412  psercn2  26413  psercnlem2  26414  psercnlem1  26415  psercn  26416  pserdvlem1  26417  pserdvlem2  26418  pserdv  26419  pserdv2  26420  abelth  26431  dvlog  26640  efopnlem2  26646  logtayl  26649  cxpcn3lem  26736  cxpcn3  26737  resqrtcn  26738  dvatan  26924  atancn  26925  rlimcnp  26954  rlimcnp2  26955  wilthlem3  27058  ftalem4  27064  ftalem5  27065  dchrisum0lem2a  27505  bdayimaon  27682  noetasuplem4  27725  noetainflem4  27729  nobdaymin  27770  nocvxminlem  27771  noeta2  27778  etaslts2  27811  cutbdaybnd2lim  27814  bday1  27831  lrrecfr  27960  addbdaylem  28034  negsunif  28072  oniso  28288  bdayons  28293  cchhllem  28980  axlowdimlem6  29041  hhssabloilem  31357  choc1  31423  chub2i  31566  span0  31638  spanuni  31640  sshhococi  31642  chsup0  31644  spansnpji  31674  mayetes3i  31825  nlelshi  32156  pjimai  32272  pj3i  32304  shatomistici  32457  hatomistici  32458  atcvat4i  32493  iundisjf  32685  rinvf1o  32729  mptctf  32815  iundisjfi  32895  xrge0mulgnn0  33101  gsumpart  33151  znfermltl  33456  ply1degltel  33684  ply1degleel  33685  ply1degltlss  33686  0mplrim  33705  ccfldsrarelvec  33862  ccfldextdgrr  33863  2sqr3minply  33971  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  esumcvgsum  34279  coinfliprv  34674  signsply0  34742  signstcl  34756  signstf  34757  kur14lem6  35446  mthmsta  35813  filnetlem3  36615  filnetlem4  36616  onint1  36684  oninhaus  36685  bj-nuliotaALT  37418  imadifss  37969  poimirlem3  37997  poimirlem32  38026  dvtan  38044  itg2addnclem2  38046  ftc1anclem6  38072  heiborlem3  38187  isdrngo2  38332  elrfi  43150  mapfzcons1  43173  eldioph4b  43263  dnnumch3lem  43498  dnnumch3  43499  dgraalem  43597  dgraaub  43600  resnonrel  44043  cotrcltrcl  44176  cotrclrcl  44193  frege131d  44215  binomcxplemdvbinom  44804  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  relopabVD  45351  rabexgf  45479  fzssnn0  45771  iuneqfzuzlem  45786  allbutfiinf  45870  uzublem  45880  sumnnodd  46082  lptioo2cn  46095  lptioo1cn  46096  fourierdlem31  46588  fourierdlem102  46658  fourierdlem114  46670  fouriercn  46682  elaa2lem  46683  etransclem48  46732  salexct  46784  salgencntex  46793  sge0resplit  46856  meaiuninclem  46930  caratheodorylem1  46976  hoicvr  46998  hoicvrrex  47006  hoidmvlelem3  47047  hoidmvlelem4  47048  gricrel  48417  grlicrel  48504