Theorem sseqtri 4013

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

Syntax hints:   = wceq 1533   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961

This theorem is referenced by:  sseqtrri  4014  eqimssi  4037  abssi  4063  ssun2  4171  unixpss  5812  0ima  6082  fvssunirnOLD  6930  mptexgf  7234  difex2  7763  oelim2  8616  omopthlem2  8681  sbthlem7  9114  unifpw  9381  fiuni  9453  dmttrcl  9746  rnttrcl  9747  ttrclexg  9748  rankuni  9888  rankc2  9896  rankxpu  9901  rankmapu  9903  rankxplim  9904  infxpenlem  10038  cf0  10276  fin23lem17  10363  fin23lem31  10368  smobeth  10611  nqerf  10955  dmrecnq  10993  ackbijnn  15810  divalglem2  16375  divalglem5  16377  bitsfzolem  16412  0bits  16417  bezoutlem2  16519  bezoutlem3  16520  lcmcllem  16570  lcmledvds  16573  lcmfval  16595  lcmfcllem  16599  lcmfledvds  16606  odzcllem  16764  odzdvds  16767  unbenlem  16880  4sqlem13  16929  4sqlem14  16930  4sqlem17  16933  4sqlem18  16934  vdwlem8  16960  vdwnnlem3  16969  ramcl2lem  16981  ramtcl  16982  ramtub  16984  strle1  17130  prdsvallem  17439  wunfunc  17890  wunfuncOLD  17891  wunnat  17949  wunnatOLD  17950  psssdm2  18576  tsrss  18584  gicer  19240  symgsssg  19434  symgfisg  19435  odfval  19499  odlem2  19506  gexlem2  19549  torsubg  19821  dprd2da  20011  zringlpirlem2  21406  zringlpirlem3  21407  fermltlchr  21476  pjfval  21657  pjpm  21659  toponsspwpw  22868  eltg4i  22907  ntrss2  23005  isopn3  23014  mretopd  23040  leordtval2  23160  ptbasfi  23529  hmphtop  23726  hmpher  23732  restutop  24186  ucnprima  24231  tngtopn  24611  tgioo  24756  xrtgioo  24766  ovolicc2lem4  25493  nulmbl2  25509  iundisj  25521  dyadmax  25571  i1f1  25663  dvfval  25870  dvcnp2  25893  dvcnp2OLD  25894  lhop1lem  25990  lhop2  25992  elqaalem1  26299  elqaalem3  26301  taylthlem2  26354  taylthlem2OLD  26355  pserulm  26403  psercn2  26404  psercn2OLD  26405  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  pserdv  26411  pserdv2  26412  abelth  26423  dvlog  26630  efopnlem2  26636  logtayl  26639  cxpcn3lem  26727  cxpcn3  26728  resqrtcn  26729  dvatan  26912  atancn  26913  rlimcnp  26942  rlimcnp2  26943  wilthlem3  27047  ftalem4  27053  ftalem5  27054  dchrisum0lem2a  27495  bdayimaon  27672  noetasuplem4  27715  noetainflem4  27719  nocvxminlem  27756  nocvxmin  27757  noeta2  27763  etasslt2  27793  scutbdaybnd2lim  27796  bday1s  27810  lrrecfr  27906  negsunif  28013  cchhllem  28769  cchhllemOLD  28770  axlowdimlem6  28830  hhssabloilem  31143  choc1  31209  chub2i  31352  span0  31424  spanuni  31426  sshhococi  31428  chsup0  31430  spansnpji  31460  mayetes3i  31611  nlelshi  31942  pjimai  32058  pj3i  32090  shatomistici  32243  hatomistici  32244  atcvat4i  32279  iundisjf  32458  rinvf1o  32496  mptctf  32581  iundisjfi  32646  xrge0mulgnn0  32834  gsumpart  32859  znfermltl  33177  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  ccfldsrarelvec  33490  ccfldextdgrr  33491  xrge0iifcnv  33665  xrge0iifiso  33667  xrge0iifhom  33669  esumcvgsum  33838  coinfliprv  34233  signsply0  34314  signstcl  34328  signstf  34329  kur14lem6  34952  mthmsta  35319  filnetlem3  35995  filnetlem4  35996  onint1  36064  oninhaus  36065  bj-nuliotaALT  36668  imadifss  37199  poimirlem3  37227  poimirlem32  37256  dvtan  37274  itg2addnclem2  37276  ftc1anclem6  37302  heiborlem3  37417  isdrngo2  37562  elrfi  42256  mapfzcons1  42279  eldioph4b  42373  dnnumch3lem  42612  dnnumch3  42613  dgraalem  42711  dgraaub  42714  resnonrel  43164  cotrcltrcl  43297  cotrclrcl  43314  frege131d  43336  binomcxplemdvbinom  43932  binomcxplemdvsum  43934  binomcxplemnotnn0  43935  relopabVD  44482  rabexgf  44528  fzssnn0  44837  iuneqfzuzlem  44854  allbutfiinf  44940  uzublem  44950  sumnnodd  45156  lptioo2cn  45171  lptioo1cn  45172  fourierdlem31  45664  fourierdlem102  45734  fourierdlem114  45746  fouriercn  45758  elaa2lem  45759  etransclem48  45808  salexct  45860  salgencntex  45869  sge0resplit  45932  meaiuninclem  46006  caratheodorylem1  46052  hoicvr  46074  hoicvrrex  46082  hoidmvlelem3  46123  hoidmvlelem4  46124  gricrel  47371