Theorem sseqtri 3988

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  sseqtrri  3989  3sstr3i  3990  eqimssi  4000  abssi  4025  ssun2  4135  unixpss  5802  0ima  6085  imadifssran  6207  mptexgf  7227  difex2  7768  oelim2  8590  omopthlem2  8655  sbthlem7  9091  unifpw  9322  fiuni  9398  dmttrcl  9700  rnttrcl  9701  ttrclexg  9702  rankuni  9845  rankc2  9853  rankxpu  9858  rankmapu  9860  rankxplim  9861  infxpenlem  10016  cf0  10252  fin23lem17  10340  fin23lem31  10345  smobeth  10589  nqerf  10933  dmrecnq  10971  ackbijnn  15908  divalglem2  16478  divalglem5  16480  bitsfzolem  16517  0bits  16522  bezoutlem2  16623  bezoutlem3  16624  lcmcllem  16679  lcmledvds  16682  lcmfval  16704  lcmfcllem  16708  lcmfledvds  16715  odzcllem  16877  odzdvds  16880  unbenlem  16993  4sqlem13  17042  4sqlem14  17043  4sqlem17  17046  4sqlem18  17047  vdwlem8  17073  vdwnnlem3  17082  ramcl2lem  17094  ramtcl  17095  ramtub  17097  strle1  17243  prdsvallem  17532  wunfunc  17983  wunnat  18041  psssdm2  18662  tsrss  18670  gicer  19378  symgsssg  19568  symgfisg  19569  odfval  19633  odlem2  19640  gexlem2  19683  torsubg  19955  dprd2da  20145  ricrel  20629  zringlpirlem2  21650  zringlpirlem3  21651  fermltlchr  21716  pjfval  21893  pjpm  21895  toponsspwpw  23116  eltg4i  23154  ntrss2  23251  isopn3  23260  mretopd  23286  leordtval2  23406  ptbasfi  23775  hmphtop  23972  hmpher  23978  restutop  24431  ucnprima  24475  tngtopn  24844  tgioo  24990  xrtgioo  25001  ovolicc2lem4  25716  nulmbl2  25732  iundisj  25744  dyadmax  25794  i1f1  25886  dvfval  26093  dvcnp2  26116  lhop1lem  26209  lhop2  26211  elqaalem1  26517  elqaalem3  26519  taylthlem2  26574  pserulm  26622  psercn2  26623  psercnlem2  26624  psercnlem1  26625  psercn  26626  pserdvlem1  26627  pserdvlem2  26628  pserdv  26629  pserdv2  26630  abelth  26641  dvlog  26853  efopnlem2  26859  logtayl  26862  cxpcn3lem  26949  cxpcn3  26950  resqrtcn  26951  dvatan  27137  atancn  27138  rlimcnp  27167  rlimcnp2  27168  wilthlem3  27271  ftalem4  27277  ftalem5  27278  dchrisum0lem2a  27718  bdayimaon  27894  noetasuplem4  27937  noetainflem4  27941  nobdaymin  27983  nocvxminlem  27984  noeta2  27991  etaslts2  28024  cutbdaybnd2lim  28027  bday1  28044  lrrecfr  28173  addbdaylem  28247  negsunif  28285  oniso  28501  bdayons  28506  cchhllem  29273  axlowdimlem6  29334  hhssabloilem  31650  choc1  31716  chub2i  31859  span0  31931  spanuni  31933  sshhococi  31935  chsup0  31937  spansnpji  31967  mayetes3i  32118  nlelshi  32449  pjimai  32565  pj3i  32597  shatomistici  32750  hatomistici  32751  atcvat4i  32786  iundisjf  32971  rinvf1o  33012  mptctf  33098  iundisjfi  33178  xrge0mulgnn0  33366  gsumpart  33414  znfermltl  33712  ply1degltel  33915  ply1degleel  33916  ply1degltlss  33917  0mplrim  33935  ccfldsrarelvec  34092  ccfldextdgrr  34093  2sqr3minply  34201  xrge0iifcnv  34354  xrge0iifiso  34356  xrge0iifhom  34358  esumcvgsum  34509  coinfliprv  34904  signsply0  34969  signstcl  34983  signstf  34984  kur14lem6  35723  mthmsta  36090  filnetlem3  36931  filnetlem4  36932  onint1  37000  oninhaus  37001  bj-nuliotaALT  37734  imadifss  38286  poimirlem3  38314  poimirlem32  38343  dvtan  38361  itg2addnclem2  38363  ftc1anclem6  38389  heiborlem3  38504  isdrngo2  38649  elrfi  43465  mapfzcons1  43488  eldioph4b  43578  dnnumch3lem  43813  dnnumch3  43814  dgraalem  43912  dgraaub  43915  resnonrel  44358  cotrcltrcl  44491  cotrclrcl  44508  frege131d  44530  binomcxplemdvbinom  45103  binomcxplemdvsum  45105  binomcxplemnotnn0  45106  relopabVD  45649  rabexgf  45784  fzssnn0  46075  iuneqfzuzlem  46090  allbutfiinf  46174  uzublem  46184  sumnnodd  46386  lptioo2cn  46399  lptioo1cn  46400  fourierdlem31  46892  fourierdlem102  46962  fourierdlem114  46974  fouriercn  46986  elaa2lem  46987  etransclem48  47036  salexct  47088  salgencntex  47097  sge0resplit  47160  meaiuninclem  47234  caratheodorylem1  47280  hoicvr  47302  hoicvrrex  47310  hoidmvlelem3  47351  hoidmvlelem4  47352  gricrel  48724  grlicrel  48811