Theorem eleqtri 2837

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtri.1	⊢ 𝐴 ∈ 𝐵
eleqtri.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtri.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eleq2i 2831	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)
4	1, 3	mpbi 230	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1537   ∈ wcel 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-clel 2814

This theorem is referenced by:  eleqtrri  2838  3eltr3i  2851  prid2  4768  2eluzge0  12933  faclbnd4lem1  14329  cats1fv  14895  bpoly2  16090  bpoly3  16091  bpoly4  16092  ef0lem  16111  phi1  16807  gsumws1  18864  lt6abl  19928  uvcvvcl  21825  mhpvarcl  22170  smadiadetlem4  22691  indiscld  23115  cnrehmeo  24998  cnrehmeoOLD  24999  ovolicc1  25565  dvcjbr  26002  vieta1lem2  26368  dvloglem  26705  logdmopn  26706  efopnlem2  26714  cxpcn  26802  cxpcnOLD  26803  loglesqrt  26819  log2ublem2  27005  efrlim  27027  efrlimOLD  27028  precsexlem11  28256  tgcgr4  28554  axlowdimlem16  28987  axlowdimlem17  28988  nlelchi  32090  hmopidmchi  32180  evl1deg2  33582  evl1deg3  33583  raddcn  33890  xrge0tmd  33906  indf  33996  ballotlem1ri  34516  chtvalz  34623  circlemethhgt  34637  dvtanlem  37656  ftc1cnnc  37679  dvasin  37691  dvacos  37692  dvreasin  37693  dvreacos  37694  areacirclem2  37696  areacirclem4  37698  cncfres  37752  jm2.23  42985  0finon  43438  1finon  43439  2finon  43440  3finon  43441  4finon  43442  fvnonrel  43587  frege54cor1c  43905  fourierdlem28  46091  fourierdlem57  46119  fourierdlem59  46121  fourierdlem62  46124  fourierdlem68  46130  fouriersw  46187  etransclem23  46213  etransclem35  46225  etransclem38  46228  etransclem39  46229  etransclem44  46234  etransclem45  46235  etransclem47  46237  rrxtopn0  46249  hoidmvlelem2  46552  vonicclem2  46640  fmtno4prmfac  47497  gpg5grlic  47975