Theorem sseqtri 3956

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  sseqtrri  3957  3sstr3i  3958  eqimssi  3968  abssi  3993  ssun2  4177  unixpss  5787  0ima  6200  imadifssranOLD  6202  mptexgf  7228  difex2  7774  oelim2  8607  omopthlem2  8672  sbthlem7  9115  unifpw  9347  fiuni  9423  dmttrcl  9725  rnttrcl  9726  ttrclexg  9727  rankuni  9882  rankc2  9891  rankxpu  9896  rankmapu  9898  rankxplim  9899  infxpenlem  10095  cf0  10331  fin23lem17  10419  fin23lem31  10424  smobeth  10674  nqerf  11018  dmrecnq  11056  ackbijnn  16002  divalglem2  16570  divalglem5  16572  bitsfzolem  16609  0bits  16614  bezoutlem2  16718  bezoutlem3  16719  lcmcllem  16776  lcmledvds  16779  lcmfval  16801  lcmfcllem  16805  lcmfledvds  16812  odzcllem  16975  odzdvds  16978  unbenlem  17091  4sqlem13  17140  4sqlem14  17141  4sqlem17  17144  4sqlem18  17145  vdwlem8  17171  vdwnnlem3  17180  ramcl2lem  17192  ramtcl  17193  ramtub  17195  strle1  17341  prdsvallem  17630  wunfunc  18081  wunnat  18139  psssdm2  18760  tsrss  18768  gicer  19496  symgsssg  19686  symgfisg  19687  odfval  19751  odlem2  19758  gexlem2  19801  torsubg  20073  dprd2da  20263  ricrel  20749  zringlpirlem2  21774  zringlpirlem3  21775  fermltlchr  21840  pjfval  22017  pjpm  22019  toponsspwpw  23245  eltg4i  23283  ntrss2  23380  isopn3  23389  mretopd  23415  leordtval2  23535  ptbasfi  23905  hmphtop  24102  hmpher  24108  restutop  24561  ucnprima  24605  tngtopn  24974  tgioo  25120  xrtgioo  25131  ovolicc2lem4  25846  nulmbl2  25862  iundisj  25874  dyadmax  25924  i1f1  26016  dvfval  26222  dvcnp2  26245  lhop1lem  26338  lhop2  26340  elqaalem1  26647  elqaalem3  26649  taylthlem2  26706  pserulm  26754  psercn2  26755  psercnlem2  26756  psercnlem1  26757  psercn  26758  pserdvlem1  26759  pserdvlem2  26760  pserdv  26761  pserdv2  26762  abelth  26773  dvlog  26984  efopnlem2  26990  logtayl  26993  cxpcn3lem  27080  cxpcn3  27081  resqrtcn  27082  dvatan  27268  atancn  27269  rlimcnp  27298  rlimcnp2  27299  wilthlem3  27402  ftalem4  27408  ftalem5  27409  dchrisum0lem2a  27849  bdayimaon  28055  noetasuplem4  28098  noetainflem4  28102  nobdaymin  28144  nocvxminlem  28145  noeta2  28152  etaslts2  28185  cutbdaybnd2lim  28188  bday1  28205  lrrecfr  28334  addbdaylem  28408  negsunif  28446  oniso  28662  bdayons  28667  cchhllem  29469  axlowdimlem6  29530  hhssabloilem  31868  choc1  31934  chub2i  32077  span0  32149  spanuni  32151  sshhococi  32153  chsup0  32155  spansnpji  32185  mayetes3i  32336  nlelshi  32667  pjimai  32783  pj3i  32815  shatomistici  32968  hatomistici  32969  atcvat4i  33004  iundisjf  33230  rinvf1o  33271  mptctf  33355  iundisjfi  33434  xrge0mulgnn0  33622  gsumpart  33670  znfermltl  33968  ply1degltel  34172  ply1degleel  34173  ply1degltlss  34174  0mplrim  34192  ccfldsrarelvec  34349  ccfldextdgrr  34350  2sqr3minply  34458  xrge0iifcnv  34611  xrge0iifiso  34613  xrge0iifhom  34615  esumcvgsum  34766  coinfliprv  35161  signsply0  35226  signstcl  35240  signstf  35241  kur14lem6  36062  mthmsta  36429  filnetlem3  37260  filnetlem4  37261  onint1  37329  oninhaus  37330  bj-nuliotaALT  38065  imadifss  38616  poimirlem3  38634  poimirlem32  38663  dvtan  38681  itg2addnclem2  38683  ftc1anclem6  38709  heiborlem3  38840  isdrngo2  38985  elrfi  43798  mapfzcons1  43821  eldioph4b  43911  dnnumch3lem  44146  dnnumch3  44147  dgraalem  44240  dgraaub  44243  resnonrel  44685  cotrcltrcl  44818  cotrclrcl  44835  frege131d  44857  binomcxplemdvbinom  45430  binomcxplemdvsum  45432  binomcxplemnotnn0  45433  relopabVD  45976  hfstructhf  46123  rabexgf  46134  fzssnn0  46424  iuneqfzuzlem  46439  allbutfiinf  46523  uzublem  46533  sumnnodd  46735  lptioo2cn  46748  lptioo1cn  46749  fourierdlem31  47241  fourierdlem102  47311  fourierdlem114  47323  fouriercn  47335  elaa2lem  47336  etransclem48  47385  salexct  47437  salgencntex  47446  sge0resplit  47509  meaiuninclem  47583  caratheodorylem1  47629  hoicvr  47651  hoicvrrex  47659  hoidmvlelem3  47700  hoidmvlelem4  47701  gricrel  49110  grlicrel  49197