Theorem sseqtri 3979

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

Syntax hints:   = wceq 1541   ⊆ wss 3898

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 2123  ax-ext 2705

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

This theorem is referenced by:  sseqtrri  3980  3sstr3i  3981  eqimssi  3991  abssi  4017  ssun2  4128  unixpss  5754  0ima  6031  mptexgf  7162  difex2  7699  oelim2  8516  omopthlem2  8581  sbthlem7  9013  unifpw  9246  fiuni  9319  dmttrcl  9618  rnttrcl  9619  ttrclexg  9620  rankuni  9763  rankc2  9771  rankxpu  9776  rankmapu  9778  rankxplim  9779  infxpenlem  9911  cf0  10149  fin23lem17  10236  fin23lem31  10241  smobeth  10484  nqerf  10828  dmrecnq  10866  ackbijnn  15737  divalglem2  16308  divalglem5  16310  bitsfzolem  16347  0bits  16352  bezoutlem2  16453  bezoutlem3  16454  lcmcllem  16509  lcmledvds  16512  lcmfval  16534  lcmfcllem  16538  lcmfledvds  16545  odzcllem  16706  odzdvds  16709  unbenlem  16822  4sqlem13  16871  4sqlem14  16872  4sqlem17  16875  4sqlem18  16876  vdwlem8  16902  vdwnnlem3  16911  ramcl2lem  16923  ramtcl  16924  ramtub  16926  strle1  17071  prdsvallem  17360  wunfunc  17810  wunnat  17868  psssdm2  18489  tsrss  18497  gicer  19191  symgsssg  19381  symgfisg  19382  odfval  19446  odlem2  19453  gexlem2  19496  torsubg  19768  dprd2da  19958  zringlpirlem2  21402  zringlpirlem3  21403  fermltlchr  21468  pjfval  21645  pjpm  21647  toponsspwpw  22838  eltg4i  22876  ntrss2  22973  isopn3  22982  mretopd  23008  leordtval2  23128  ptbasfi  23497  hmphtop  23694  hmpher  23700  restutop  24153  ucnprima  24197  tngtopn  24566  tgioo  24712  xrtgioo  24723  ovolicc2lem4  25449  nulmbl2  25465  iundisj  25477  dyadmax  25527  i1f1  25619  dvfval  25826  dvcnp2  25849  dvcnp2OLD  25850  lhop1lem  25946  lhop2  25948  elqaalem1  26255  elqaalem3  26257  taylthlem2  26310  taylthlem2OLD  26311  pserulm  26359  psercn2  26360  psercn2OLD  26361  psercnlem2  26362  psercnlem1  26363  psercn  26364  pserdvlem1  26365  pserdvlem2  26366  pserdv  26367  pserdv2  26368  abelth  26379  dvlog  26588  efopnlem2  26594  logtayl  26597  cxpcn3lem  26685  cxpcn3  26686  resqrtcn  26687  dvatan  26873  atancn  26874  rlimcnp  26903  rlimcnp2  26904  wilthlem3  27008  ftalem4  27014  ftalem5  27015  dchrisum0lem2a  27456  bdayimaon  27633  noetasuplem4  27676  noetainflem4  27680  nobdaymin  27717  nocvxminlem  27718  noeta2  27725  etasslt2  27756  scutbdaybnd2lim  27759  bday1s  27776  lrrecfr  27887  addsbdaylem  27960  negsunif  27998  onsiso  28206  bdayon  28210  zs12bday  28395  cchhllem  28866  axlowdimlem6  28927  hhssabloilem  31243  choc1  31309  chub2i  31452  span0  31524  spanuni  31526  sshhococi  31528  chsup0  31530  spansnpji  31560  mayetes3i  31711  nlelshi  32042  pjimai  32158  pj3i  32190  shatomistici  32343  hatomistici  32344  atcvat4i  32379  iundisjf  32571  rinvf1o  32614  mptctf  32703  iundisjfi  32783  xrge0mulgnn0  33003  gsumpart  33044  znfermltl  33338  ply1degltel  33562  ply1degleel  33563  ply1degltlss  33564  ccfldsrarelvec  33705  ccfldextdgrr  33706  2sqr3minply  33814  xrge0iifcnv  33967  xrge0iifiso  33969  xrge0iifhom  33971  esumcvgsum  34122  coinfliprv  34517  signsply0  34585  signstcl  34599  signstf  34600  kur14lem6  35276  mthmsta  35643  filnetlem3  36445  filnetlem4  36446  onint1  36514  oninhaus  36515  bj-nuliotaALT  37123  imadifss  37655  poimirlem3  37683  poimirlem32  37712  dvtan  37730  itg2addnclem2  37732  ftc1anclem6  37758  heiborlem3  37873  isdrngo2  38018  elrfi  42811  mapfzcons1  42834  eldioph4b  42928  dnnumch3lem  43163  dnnumch3  43164  dgraalem  43262  dgraaub  43265  resnonrel  43709  cotrcltrcl  43842  cotrclrcl  43859  frege131d  43881  binomcxplemdvbinom  44470  binomcxplemdvsum  44472  binomcxplemnotnn0  44473  relopabVD  45017  rabexgf  45145  fzssnn0  45441  iuneqfzuzlem  45457  allbutfiinf  45542  uzublem  45552  sumnnodd  45754  lptioo2cn  45767  lptioo1cn  45768  fourierdlem31  46260  fourierdlem102  46330  fourierdlem114  46342  fouriercn  46354  elaa2lem  46355  etransclem48  46404  salexct  46456  salgencntex  46465  sge0resplit  46528  meaiuninclem  46602  caratheodorylem1  46648  hoicvr  46670  hoicvrrex  46678  hoidmvlelem3  46719  hoidmvlelem4  46720  gricrel  48043  grlicrel  48130