Theorem sseqtri 3961

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  sseqtrri  3962  3sstr3i  3963  eqimssi  3973  abssi  3996  ssun2  4180  unixpss  5793  0ima  6213  imadifssranOLD  6215  mptexgf  7251  difex2  7798  oelim2  8632  omopthlem2  8697  sbthlem7  9140  unifpw  9372  fiuni  9447  dmttrcl  9749  rnttrcl  9750  ttrclexg  9751  rankuni  9906  rankc2  9915  rankxpu  9920  rankmapu  9922  rankxplim  9923  infxpenlem  10119  cf0  10355  fin23lem17  10443  fin23lem31  10448  smobeth  10698  nqerf  11042  dmrecnq  11080  ackbijnn  16026  divalglem2  16594  divalglem5  16596  bitsfzolem  16633  0bits  16638  bezoutlem2  16742  bezoutlem3  16743  lcmcllem  16800  lcmledvds  16803  lcmfval  16825  lcmfcllem  16829  lcmfledvds  16836  odzcllem  16999  odzdvds  17002  unbenlem  17115  4sqlem13  17164  4sqlem14  17165  4sqlem17  17168  4sqlem18  17169  vdwlem8  17195  vdwnnlem3  17204  ramcl2lem  17216  ramtcl  17217  ramtub  17219  strle1  17365  prdsvallem  17654  wunfunc  18105  wunnat  18163  psssdm2  18784  tsrss  18792  gicer  19521  symgsssg  19711  symgfisg  19712  odfval  19776  odlem2  19783  gexlem2  19826  torsubg  20098  dprd2da  20288  ricrel  20774  zringlpirlem2  21799  zringlpirlem3  21800  fermltlchr  21865  pjfval  22042  pjpm  22044  toponsspwpw  23270  eltg4i  23308  ntrss2  23405  isopn3  23414  mretopd  23440  leordtval2  23560  ptbasfi  23930  hmphtop  24127  hmpher  24133  restutop  24586  ucnprima  24630  tngtopn  24999  tgioo  25145  xrtgioo  25156  ovolicc2lem4  25871  nulmbl2  25887  iundisj  25899  dyadmax  25949  i1f1  26041  dvfval  26247  dvcnp2  26270  lhop1lem  26363  lhop2  26365  elqaalem1  26672  elqaalem3  26674  taylthlem2  26731  pserulm  26779  psercn2  26780  psercnlem2  26781  psercnlem1  26782  psercn  26783  pserdvlem1  26784  pserdvlem2  26785  pserdv  26786  pserdv2  26787  abelth  26798  dvlog  27009  efopnlem2  27015  logtayl  27018  cxpcn3lem  27105  cxpcn3  27106  resqrtcn  27107  dvatan  27293  atancn  27294  rlimcnp  27323  rlimcnp2  27324  wilthlem3  27427  ftalem4  27433  ftalem5  27434  dchrisum0lem2a  27874  bdayimaon  28080  noetasuplem4  28123  noetainflem4  28127  nobdaymin  28169  nocvxminlem  28170  noeta2  28177  etaslts2  28210  cutbdaybnd2lim  28213  bday1  28230  lrrecfr  28359  addbdaylem  28433  negsunif  28471  oniso  28687  bdayons  28692  cchhllem  29494  axlowdimlem6  29555  hhssabloilem  31893  choc1  31959  chub2i  32102  span0  32174  spanuni  32176  sshhococi  32178  chsup0  32180  spansnpji  32210  mayetes3i  32361  nlelshi  32692  pjimai  32808  pj3i  32840  shatomistici  32993  hatomistici  32994  atcvat4i  33029  iundisjf  33255  rinvf1o  33296  mptctf  33379  iundisjfi  33458  xrge0mulgnn0  33646  gsumpart  33694  znfermltl  33992  ply1degltel  34196  ply1degleel  34197  ply1degltlss  34198  0mplrim  34216  ccfldsrarelvec  34373  ccfldextdgrr  34374  2sqr3minply  34482  xrge0iifcnv  34635  xrge0iifiso  34637  xrge0iifhom  34639  esumcvgsum  34790  coinfliprv  35185  signsply0  35250  signstcl  35264  signstf  35265  kur14lem6  36143  mthmsta  36510  filnetlem3  37346  filnetlem4  37347  onint1  37415  oninhaus  37416  bj-nuliotaALT  38164  imadifss  38715  poimirlem3  38733  poimirlem32  38762  dvtan  38780  itg2addnclem2  38782  ftc1anclem6  38808  heiborlem3  38939  isdrngo2  39084  elrfi  43898  mapfzcons1  43921  eldioph4b  44011  dnnumch3lem  44246  dnnumch3  44247  dgraalem  44339  dgraaub  44342  resnonrel  44784  cotrcltrcl  44917  cotrclrcl  44934  frege131d  44956  binomcxplemdvbinom  45529  binomcxplemdvsum  45531  binomcxplemnotnn0  45532  relopabVD  46074  hfstructhf  46228  rabexgf  46246  fzssnn0  46536  iuneqfzuzlem  46551  allbutfiinf  46635  uzublem  46645  sumnnodd  46847  lptioo2cn  46860  lptioo1cn  46861  fourierdlem31  47353  fourierdlem102  47423  fourierdlem114  47435  fouriercn  47447  elaa2lem  47448  etransclem48  47497  salexct  47549  salgencntex  47558  sge0resplit  47621  meaiuninclem  47695  caratheodorylem1  47741  hoicvr  47763  hoicvrrex  47771  hoidmvlelem3  47812  hoidmvlelem4  47813  gricrel  49222  grlicrel  49309