Theorem sseqtri 3986

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

Syntax hints:   = wceq 1570   ⊆ wss 3906

This theorem was proved from 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 theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseqtrri  3987  3sstr3i  3988  eqimssi  3998  abssi  4023  ssun2  4133  unixpss  5799  0ima  6082  imadifssran  6204  mptexgf  7222  difex2  7760  oelim2  8582  omopthlem2  8647  sbthlem7  9082  unifpw  9313  fiuni  9389  dmttrcl  9691  rnttrcl  9692  ttrclexg  9693  rankuni  9836  rankc2  9844  rankxpu  9849  rankmapu  9851  rankxplim  9852  infxpenlem  9998  cf0  10235  fin23lem17  10323  fin23lem31  10328  smobeth  10572  nqerf  10916  dmrecnq  10954  ackbijnn  15884  divalglem2  16454  divalglem5  16456  bitsfzolem  16493  0bits  16498  bezoutlem2  16599  bezoutlem3  16600  lcmcllem  16655  lcmledvds  16658  lcmfval  16680  lcmfcllem  16684  lcmfledvds  16691  odzcllem  16853  odzdvds  16856  unbenlem  16969  4sqlem13  17018  4sqlem14  17019  4sqlem17  17022  4sqlem18  17023  vdwlem8  17049  vdwnnlem3  17058  ramcl2lem  17070  ramtcl  17071  ramtub  17073  strle1  17219  prdsvallem  17508  wunfunc  17959  wunnat  18017  psssdm2  18638  tsrss  18646  gicer  19348  symgsssg  19538  symgfisg  19539  odfval  19603  odlem2  19610  gexlem2  19653  torsubg  19925  dprd2da  20115  zringlpirlem2  21594  zringlpirlem3  21595  fermltlchr  21660  pjfval  21837  pjpm  21839  toponsspwpw  23060  eltg4i  23098  ntrss2  23195  isopn3  23204  mretopd  23230  leordtval2  23350  ptbasfi  23719  hmphtop  23916  hmpher  23922  restutop  24375  ucnprima  24419  tngtopn  24788  tgioo  24934  xrtgioo  24945  ovolicc2lem4  25660  nulmbl2  25676  iundisj  25688  dyadmax  25738  i1f1  25830  dvfval  26037  dvcnp2  26060  lhop1lem  26153  lhop2  26155  elqaalem1  26461  elqaalem3  26463  taylthlem2  26515  pserulm  26563  psercn2  26564  psercnlem2  26565  psercnlem1  26566  psercn  26567  pserdvlem1  26568  pserdvlem2  26569  pserdv  26570  pserdv2  26571  abelth  26582  dvlog  26794  efopnlem2  26800  logtayl  26803  cxpcn3lem  26890  cxpcn3  26891  resqrtcn  26892  dvatan  27078  atancn  27079  rlimcnp  27108  rlimcnp2  27109  wilthlem3  27212  ftalem4  27218  ftalem5  27219  dchrisum0lem2a  27659  bdayimaon  27835  noetasuplem4  27878  noetainflem4  27882  nobdaymin  27924  nocvxminlem  27925  noeta2  27932  etaslts2  27965  cutbdaybnd2lim  27968  bday1  27985  lrrecfr  28114  addbdaylem  28188  negsunif  28226  oniso  28442  bdayons  28447  cchhllem  29214  axlowdimlem6  29275  hhssabloilem  31591  choc1  31657  chub2i  31800  span0  31872  spanuni  31874  sshhococi  31876  chsup0  31878  spansnpji  31908  mayetes3i  32059  nlelshi  32390  pjimai  32506  pj3i  32538  shatomistici  32691  hatomistici  32692  atcvat4i  32727  iundisjf  32912  rinvf1o  32953  mptctf  33039  iundisjfi  33119  xrge0mulgnn0  33313  gsumpart  33361  znfermltl  33659  ply1degltel  33862  ply1degleel  33863  ply1degltlss  33864  0mplrim  33882  ccfldsrarelvec  34039  ccfldextdgrr  34040  2sqr3minply  34148  xrge0iifcnv  34301  xrge0iifiso  34303  xrge0iifhom  34305  esumcvgsum  34456  coinfliprv  34851  signsply0  34916  signstcl  34930  signstf  34931  kur14lem6  35681  mthmsta  36048  filnetlem3  36869  filnetlem4  36870  onint1  36938  oninhaus  36939  bj-nuliotaALT  37672  imadifss  38224  poimirlem3  38252  poimirlem32  38281  dvtan  38299  itg2addnclem2  38301  ftc1anclem6  38327  heiborlem3  38442  isdrngo2  38587  elrfi  43405  mapfzcons1  43428  eldioph4b  43518  dnnumch3lem  43753  dnnumch3  43754  dgraalem  43852  dgraaub  43855  resnonrel  44298  cotrcltrcl  44431  cotrclrcl  44448  frege131d  44470  binomcxplemdvbinom  45043  binomcxplemdvsum  45045  binomcxplemnotnn0  45046  relopabVD  45589  rabexgf  45724  fzssnn0  46015  iuneqfzuzlem  46030  allbutfiinf  46114  uzublem  46124  sumnnodd  46326  lptioo2cn  46339  lptioo1cn  46340  fourierdlem31  46832  fourierdlem102  46902  fourierdlem114  46914  fouriercn  46926  elaa2lem  46927  etransclem48  46976  salexct  47028  salgencntex  47037  sge0resplit  47100  meaiuninclem  47174  caratheodorylem1  47220  hoicvr  47242  hoicvrrex  47250  hoidmvlelem3  47291  hoidmvlelem4  47292  gricrel  48661  grlicrel  48748