Theorem sseqtri 3985

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3905

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is used by:  sseqtrri  3986  3sstr3i  3987  eqimssi  3997  abssi  4022  ssun2  4132  unixpss  5797  0ima  6080  imadifssran  6202  mptexgf  7220  difex2  7755  oelim2  8577  omopthlem2  8642  sbthlem7  9077  unifpw  9308  fiuni  9384  dmttrcl  9686  rnttrcl  9687  ttrclexg  9688  rankuni  9831  rankc2  9839  rankxpu  9844  rankmapu  9846  rankxplim  9847  infxpenlem  10002  cf0  10238  fin23lem17  10326  fin23lem31  10331  smobeth  10575  nqerf  10919  dmrecnq  10957  ackbijnn  15887  divalglem2  16457  divalglem5  16459  bitsfzolem  16496  0bits  16501  bezoutlem2  16602  bezoutlem3  16603  lcmcllem  16658  lcmledvds  16661  lcmfval  16683  lcmfcllem  16687  lcmfledvds  16694  odzcllem  16856  odzdvds  16859  unbenlem  16972  4sqlem13  17021  4sqlem14  17022  4sqlem17  17025  4sqlem18  17026  vdwlem8  17052  vdwnnlem3  17061  ramcl2lem  17073  ramtcl  17074  ramtub  17076  strle1  17222  prdsvallem  17511  wunfunc  17962  wunnat  18020  psssdm2  18641  tsrss  18649  gicer  19351  symgsssg  19541  symgfisg  19542  odfval  19606  odlem2  19613  gexlem2  19656  torsubg  19928  dprd2da  20118  ricrel  20601  zringlpirlem2  21622  zringlpirlem3  21623  fermltlchr  21688  pjfval  21865  pjpm  21867  toponsspwpw  23088  eltg4i  23126  ntrss2  23223  isopn3  23232  mretopd  23258  leordtval2  23378  ptbasfi  23747  hmphtop  23944  hmpher  23950  restutop  24403  ucnprima  24447  tngtopn  24816  tgioo  24962  xrtgioo  24973  ovolicc2lem4  25688  nulmbl2  25704  iundisj  25716  dyadmax  25766  i1f1  25858  dvfval  26065  dvcnp2  26088  lhop1lem  26181  lhop2  26183  elqaalem1  26489  elqaalem3  26491  taylthlem2  26546  pserulm  26594  psercn2  26595  psercnlem2  26596  psercnlem1  26597  psercn  26598  pserdvlem1  26599  pserdvlem2  26600  pserdv  26601  pserdv2  26602  abelth  26613  dvlog  26825  efopnlem2  26831  logtayl  26834  cxpcn3lem  26921  cxpcn3  26922  resqrtcn  26923  dvatan  27109  atancn  27110  rlimcnp  27139  rlimcnp2  27140  wilthlem3  27243  ftalem4  27249  ftalem5  27250  dchrisum0lem2a  27690  bdayimaon  27866  noetasuplem4  27909  noetainflem4  27913  nobdaymin  27955  nocvxminlem  27956  noeta2  27963  etaslts2  27996  cutbdaybnd2lim  27999  bday1  28016  lrrecfr  28145  addbdaylem  28219  negsunif  28257  oniso  28473  bdayons  28478  cchhllem  29245  axlowdimlem6  29306  hhssabloilem  31622  choc1  31688  chub2i  31831  span0  31903  spanuni  31905  sshhococi  31907  chsup0  31909  spansnpji  31939  mayetes3i  32090  nlelshi  32421  pjimai  32537  pj3i  32569  shatomistici  32722  hatomistici  32723  atcvat4i  32758  iundisjf  32943  rinvf1o  32984  mptctf  33070  iundisjfi  33150  xrge0mulgnn0  33344  gsumpart  33392  znfermltl  33690  ply1degltel  33893  ply1degleel  33894  ply1degltlss  33895  0mplrim  33913  ccfldsrarelvec  34070  ccfldextdgrr  34071  2sqr3minply  34179  xrge0iifcnv  34332  xrge0iifiso  34334  xrge0iifhom  34336  esumcvgsum  34487  coinfliprv  34882  signsply0  34947  signstcl  34961  signstf  34962  kur14lem6  35711  mthmsta  36078  filnetlem3  36919  filnetlem4  36920  onint1  36988  oninhaus  36989  bj-nuliotaALT  37722  imadifss  38274  poimirlem3  38302  poimirlem32  38331  dvtan  38349  itg2addnclem2  38351  ftc1anclem6  38377  heiborlem3  38492  isdrngo2  38637  elrfi  43453  mapfzcons1  43476  eldioph4b  43566  dnnumch3lem  43801  dnnumch3  43802  dgraalem  43900  dgraaub  43903  resnonrel  44346  cotrcltrcl  44479  cotrclrcl  44496  frege131d  44518  binomcxplemdvbinom  45091  binomcxplemdvsum  45093  binomcxplemnotnn0  45094  relopabVD  45637  rabexgf  45772  fzssnn0  46063  iuneqfzuzlem  46078  allbutfiinf  46162  uzublem  46172  sumnnodd  46374  lptioo2cn  46387  lptioo1cn  46388  fourierdlem31  46880  fourierdlem102  46950  fourierdlem114  46962  fouriercn  46974  elaa2lem  46975  etransclem48  47024  salexct  47076  salgencntex  47085  sge0resplit  47148  meaiuninclem  47222  caratheodorylem1  47268  hoicvr  47290  hoicvrrex  47298  hoidmvlelem3  47339  hoidmvlelem4  47340  gricrel  48712  grlicrel  48799