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 232	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  sseqtrri  3985  3sstr3i  3986  eqimssi  3996  abssi  4021  ssun2  4131  unixpss  5781  0ima  6064  mptexgf  7202  difex2  7739  oelim2  8560  omopthlem2  8625  sbthlem7  9061  unifpw  9295  fiuni  9371  dmttrcl  9673  rnttrcl  9674  ttrclexg  9675  rankuni  9818  rankc2  9826  rankxpu  9831  rankmapu  9833  rankxplim  9834  infxpenlem  9966  cf0  10204  fin23lem17  10292  fin23lem31  10297  smobeth  10541  nqerf  10885  dmrecnq  10923  ackbijnn  15841  divalglem2  16412  divalglem5  16414  bitsfzolem  16451  0bits  16456  bezoutlem2  16557  bezoutlem3  16558  lcmcllem  16613  lcmledvds  16616  lcmfval  16638  lcmfcllem  16642  lcmfledvds  16649  odzcllem  16811  odzdvds  16814  unbenlem  16927  4sqlem13  16976  4sqlem14  16977  4sqlem17  16980  4sqlem18  16981  vdwlem8  17007  vdwnnlem3  17016  ramcl2lem  17028  ramtcl  17029  ramtub  17031  strle1  17177  prdsvallem  17466  wunfunc  17917  wunnat  17975  psssdm2  18596  tsrss  18604  gicer  19300  symgsssg  19490  symgfisg  19491  odfval  19555  odlem2  19562  gexlem2  19605  torsubg  19877  dprd2da  20067  zringlpirlem2  21495  zringlpirlem3  21496  fermltlchr  21561  pjfval  21738  pjpm  21740  toponsspwpw  22962  eltg4i  23000  ntrss2  23097  isopn3  23106  mretopd  23132  leordtval2  23252  ptbasfi  23621  hmphtop  23818  hmpher  23824  restutop  24277  ucnprima  24321  tngtopn  24690  tgioo  24836  xrtgioo  24847  ovolicc2lem4  25562  nulmbl2  25578  iundisj  25590  dyadmax  25640  i1f1  25732  dvfval  25939  dvcnp2  25962  lhop1lem  26055  lhop2  26057  elqaalem1  26360  elqaalem3  26362  taylthlem2  26414  pserulm  26462  psercn2  26463  psercnlem2  26464  psercnlem1  26465  psercn  26466  pserdvlem1  26467  pserdvlem2  26468  pserdv  26469  pserdv2  26470  abelth  26481  dvlog  26693  efopnlem2  26699  logtayl  26702  cxpcn3lem  26789  cxpcn3  26790  resqrtcn  26791  dvatan  26977  atancn  26978  rlimcnp  27007  rlimcnp2  27008  wilthlem3  27111  ftalem4  27117  ftalem5  27118  dchrisum0lem2a  27558  bdayimaon  27734  noetasuplem4  27777  noetainflem4  27781  nobdaymin  27823  nocvxminlem  27824  noeta2  27831  etaslts2  27864  cutbdaybnd2lim  27867  bday1  27884  lrrecfr  28013  addbdaylem  28087  negsunif  28125  oniso  28341  bdayons  28346  cchhllem  29033  axlowdimlem6  29094  hhssabloilem  31410  choc1  31476  chub2i  31619  span0  31691  spanuni  31693  sshhococi  31695  chsup0  31697  spansnpji  31727  mayetes3i  31878  nlelshi  32209  pjimai  32325  pj3i  32357  shatomistici  32510  hatomistici  32511  atcvat4i  32546  iundisjf  32738  rinvf1o  32782  mptctf  32868  iundisjfi  32948  xrge0mulgnn0  33154  gsumpart  33204  znfermltl  33513  ply1degltel  33751  ply1degleel  33752  ply1degltlss  33753  0mplrim  33772  ccfldsrarelvec  33929  ccfldextdgrr  33930  2sqr3minply  34038  xrge0iifcnv  34191  xrge0iifiso  34193  xrge0iifhom  34195  esumcvgsum  34346  coinfliprv  34741  signsply0  34809  signstcl  34823  signstf  34824  kur14lem6  35525  mthmsta  35892  filnetlem3  36704  filnetlem4  36705  onint1  36773  oninhaus  36774  bj-nuliotaALT  37507  imadifss  38058  poimirlem3  38086  poimirlem32  38115  dvtan  38133  itg2addnclem2  38135  ftc1anclem6  38161  heiborlem3  38276  isdrngo2  38421  elrfi  43239  mapfzcons1  43262  eldioph4b  43352  dnnumch3lem  43587  dnnumch3  43588  dgraalem  43686  dgraaub  43689  resnonrel  44132  cotrcltrcl  44265  cotrclrcl  44282  frege131d  44304  binomcxplemdvbinom  44893  binomcxplemdvsum  44895  binomcxplemnotnn0  44896  relopabVD  45440  rabexgf  45568  fzssnn0  45859  iuneqfzuzlem  45874  allbutfiinf  45958  uzublem  45968  sumnnodd  46170  lptioo2cn  46183  lptioo1cn  46184  fourierdlem31  46676  fourierdlem102  46746  fourierdlem114  46758  fouriercn  46770  elaa2lem  46771  etransclem48  46820  salexct  46872  salgencntex  46881  sge0resplit  46944  meaiuninclem  47018  caratheodorylem1  47064  hoicvr  47086  hoicvrrex  47094  hoidmvlelem3  47135  hoidmvlelem4  47136  gricrel  48505  grlicrel  48592