Theorem sseqtri 3984

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

Syntax hints:   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  sseqtrri  3985  3sstr3i  3986  eqimssi  3996  abssi  4022  ssun2  4133  unixpss  5767  0ima  6045  mptexgf  7178  difex2  7715  oelim2  8533  omopthlem2  8598  sbthlem7  9033  unifpw  9267  fiuni  9343  dmttrcl  9642  rnttrcl  9643  ttrclexg  9644  rankuni  9787  rankc2  9795  rankxpu  9800  rankmapu  9802  rankxplim  9803  infxpenlem  9935  cf0  10173  fin23lem17  10260  fin23lem31  10265  smobeth  10509  nqerf  10853  dmrecnq  10891  ackbijnn  15763  divalglem2  16334  divalglem5  16336  bitsfzolem  16373  0bits  16378  bezoutlem2  16479  bezoutlem3  16480  lcmcllem  16535  lcmledvds  16538  lcmfval  16560  lcmfcllem  16564  lcmfledvds  16571  odzcllem  16732  odzdvds  16735  unbenlem  16848  4sqlem13  16897  4sqlem14  16898  4sqlem17  16901  4sqlem18  16902  vdwlem8  16928  vdwnnlem3  16937  ramcl2lem  16949  ramtcl  16950  ramtub  16952  strle1  17097  prdsvallem  17386  wunfunc  17837  wunnat  17895  psssdm2  18516  tsrss  18524  gicer  19218  symgsssg  19408  symgfisg  19409  odfval  19473  odlem2  19480  gexlem2  19523  torsubg  19795  dprd2da  19985  zringlpirlem2  21430  zringlpirlem3  21431  fermltlchr  21496  pjfval  21673  pjpm  21675  toponsspwpw  22878  eltg4i  22916  ntrss2  23013  isopn3  23022  mretopd  23048  leordtval2  23168  ptbasfi  23537  hmphtop  23734  hmpher  23740  restutop  24193  ucnprima  24237  tngtopn  24606  tgioo  24752  xrtgioo  24763  ovolicc2lem4  25489  nulmbl2  25505  iundisj  25517  dyadmax  25567  i1f1  25659  dvfval  25866  dvcnp2  25889  dvcnp2OLD  25890  lhop1lem  25986  lhop2  25988  elqaalem1  26295  elqaalem3  26297  taylthlem2  26350  taylthlem2OLD  26351  pserulm  26399  psercn2  26400  psercn2OLD  26401  psercnlem2  26402  psercnlem1  26403  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  pserdv2  26408  abelth  26419  dvlog  26628  efopnlem2  26634  logtayl  26637  cxpcn3lem  26725  cxpcn3  26726  resqrtcn  26727  dvatan  26913  atancn  26914  rlimcnp  26943  rlimcnp2  26944  wilthlem3  27048  ftalem4  27054  ftalem5  27055  dchrisum0lem2a  27496  bdayimaon  27673  noetasuplem4  27716  noetainflem4  27720  nobdaymin  27761  nocvxminlem  27762  noeta2  27769  etaslts2  27802  cutbdaybnd2lim  27805  bday1  27822  lrrecfr  27951  addbdaylem  28025  negsunif  28063  oniso  28279  bdayons  28284  cchhllem  28971  axlowdimlem6  29032  hhssabloilem  31348  choc1  31414  chub2i  31557  span0  31629  spanuni  31631  sshhococi  31633  chsup0  31635  spansnpji  31665  mayetes3i  31816  nlelshi  32147  pjimai  32263  pj3i  32295  shatomistici  32448  hatomistici  32449  atcvat4i  32484  iundisjf  32675  rinvf1o  32719  mptctf  32805  iundisjfi  32886  xrge0mulgnn0  33107  gsumpart  33156  znfermltl  33458  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  ccfldsrarelvec  33848  ccfldextdgrr  33849  2sqr3minply  33957  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  esumcvgsum  34265  coinfliprv  34660  signsply0  34728  signstcl  34742  signstf  34743  kur14lem6  35424  mthmsta  35791  filnetlem3  36593  filnetlem4  36594  onint1  36662  oninhaus  36663  bj-nuliotaALT  37300  imadifss  37840  poimirlem3  37868  poimirlem32  37897  dvtan  37915  itg2addnclem2  37917  ftc1anclem6  37943  heiborlem3  38058  isdrngo2  38203  elrfi  43045  mapfzcons1  43068  eldioph4b  43162  dnnumch3lem  43397  dnnumch3  43398  dgraalem  43496  dgraaub  43499  resnonrel  43942  cotrcltrcl  44075  cotrclrcl  44092  frege131d  44114  binomcxplemdvbinom  44703  binomcxplemdvsum  44705  binomcxplemnotnn0  44706  relopabVD  45250  rabexgf  45378  fzssnn0  45672  iuneqfzuzlem  45687  allbutfiinf  45772  uzublem  45782  sumnnodd  45984  lptioo2cn  45997  lptioo1cn  45998  fourierdlem31  46490  fourierdlem102  46560  fourierdlem114  46572  fouriercn  46584  elaa2lem  46585  etransclem48  46634  salexct  46686  salgencntex  46695  sge0resplit  46758  meaiuninclem  46832  caratheodorylem1  46878  hoicvr  46900  hoicvrrex  46908  hoidmvlelem3  46949  hoidmvlelem4  46950  gricrel  48273  grlicrel  48360