Theorem sseqtri 3983

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

Syntax hints:   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  sseqtrri  3984  3sstr3i  3985  eqimssi  3995  abssi  4020  ssun2  4129  unixpss  5750  0ima  6027  mptexgf  7156  difex2  7693  oelim2  8510  omopthlem2  8575  sbthlem7  9006  unifpw  9239  fiuni  9312  dmttrcl  9611  rnttrcl  9612  ttrclexg  9613  rankuni  9753  rankc2  9761  rankxpu  9766  rankmapu  9768  rankxplim  9769  infxpenlem  9901  cf0  10139  fin23lem17  10226  fin23lem31  10231  smobeth  10474  nqerf  10818  dmrecnq  10856  ackbijnn  15732  divalglem2  16303  divalglem5  16305  bitsfzolem  16342  0bits  16347  bezoutlem2  16448  bezoutlem3  16449  lcmcllem  16504  lcmledvds  16507  lcmfval  16529  lcmfcllem  16533  lcmfledvds  16540  odzcllem  16701  odzdvds  16704  unbenlem  16817  4sqlem13  16866  4sqlem14  16867  4sqlem17  16870  4sqlem18  16871  vdwlem8  16897  vdwnnlem3  16906  ramcl2lem  16918  ramtcl  16919  ramtub  16921  strle1  17066  prdsvallem  17355  wunfunc  17805  wunnat  17863  psssdm2  18484  tsrss  18492  gicer  19187  symgsssg  19377  symgfisg  19378  odfval  19442  odlem2  19449  gexlem2  19492  torsubg  19764  dprd2da  19954  zringlpirlem2  21398  zringlpirlem3  21399  fermltlchr  21464  pjfval  21641  pjpm  21643  toponsspwpw  22835  eltg4i  22873  ntrss2  22970  isopn3  22979  mretopd  23005  leordtval2  23125  ptbasfi  23494  hmphtop  23691  hmpher  23697  restutop  24150  ucnprima  24194  tngtopn  24563  tgioo  24709  xrtgioo  24720  ovolicc2lem4  25446  nulmbl2  25462  iundisj  25474  dyadmax  25524  i1f1  25616  dvfval  25823  dvcnp2  25846  dvcnp2OLD  25847  lhop1lem  25943  lhop2  25945  elqaalem1  26252  elqaalem3  26254  taylthlem2  26307  taylthlem2OLD  26308  pserulm  26356  psercn2  26357  psercn2OLD  26358  psercnlem2  26359  psercnlem1  26360  psercn  26361  pserdvlem1  26362  pserdvlem2  26363  pserdv  26364  pserdv2  26365  abelth  26376  dvlog  26585  efopnlem2  26591  logtayl  26594  cxpcn3lem  26682  cxpcn3  26683  resqrtcn  26684  dvatan  26870  atancn  26871  rlimcnp  26900  rlimcnp2  26901  wilthlem3  27005  ftalem4  27011  ftalem5  27012  dchrisum0lem2a  27453  bdayimaon  27630  noetasuplem4  27673  noetainflem4  27677  nobdaymin  27714  nocvxminlem  27715  noeta2  27722  etasslt2  27753  scutbdaybnd2lim  27756  bday1s  27773  lrrecfr  27884  addsbdaylem  27957  negsunif  27995  onsiso  28203  bdayon  28207  zs12bday  28392  cchhllem  28863  axlowdimlem6  28923  hhssabloilem  31236  choc1  31302  chub2i  31445  span0  31517  spanuni  31519  sshhococi  31521  chsup0  31523  spansnpji  31553  mayetes3i  31704  nlelshi  32035  pjimai  32151  pj3i  32183  shatomistici  32336  hatomistici  32337  atcvat4i  32372  iundisjf  32564  rinvf1o  32607  mptctf  32694  iundisjfi  32773  xrge0mulgnn0  32991  gsumpart  33032  znfermltl  33326  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ccfldsrarelvec  33679  ccfldextdgrr  33680  2sqr3minply  33788  xrge0iifcnv  33941  xrge0iifiso  33943  xrge0iifhom  33945  esumcvgsum  34096  coinfliprv  34491  signsply0  34559  signstcl  34573  signstf  34574  kur14lem6  35243  mthmsta  35610  filnetlem3  36413  filnetlem4  36414  onint1  36482  oninhaus  36483  bj-nuliotaALT  37091  imadifss  37634  poimirlem3  37662  poimirlem32  37691  dvtan  37709  itg2addnclem2  37711  ftc1anclem6  37737  heiborlem3  37852  isdrngo2  37997  elrfi  42726  mapfzcons1  42749  eldioph4b  42843  dnnumch3lem  43078  dnnumch3  43079  dgraalem  43177  dgraaub  43180  resnonrel  43624  cotrcltrcl  43757  cotrclrcl  43774  frege131d  43796  binomcxplemdvbinom  44385  binomcxplemdvsum  44387  binomcxplemnotnn0  44388  relopabVD  44932  rabexgf  45060  fzssnn0  45356  iuneqfzuzlem  45372  allbutfiinf  45457  uzublem  45467  sumnnodd  45669  lptioo2cn  45682  lptioo1cn  45683  fourierdlem31  46175  fourierdlem102  46245  fourierdlem114  46257  fouriercn  46269  elaa2lem  46270  etransclem48  46319  salexct  46371  salgencntex  46380  sge0resplit  46443  meaiuninclem  46517  caratheodorylem1  46563  hoicvr  46585  hoicvrrex  46593  hoidmvlelem3  46634  hoidmvlelem4  46635  gricrel  47949  grlicrel  48036