Theorem eleqtri 2860

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145

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-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837

This theorem is used by:  eleqtrri  2861  3eltr3i  2874  prid2  4727  indf  12251  2eluzge0  12933  faclbnd4lem1  14359  cats1fv  14932  bpoly2  16147  bpoly3  16148  bpoly4  16149  ef0lem  16168  phi1  16868  gsumws1  18948  lt6abl  20023  uvcvvcl  22001  mhpvarcl  22377  smadiadetlem4  22892  indiscld  23317  cnrehmeo  25182  ovolicc1  25745  dvcjbr  26178  vieta1lem2  26542  dvloglem  26883  logdmopn  26884  efopnlem2  26892  cxpcn  26980  loglesqrt  26996  log2ublem2  27182  efrlim  27204  precsexlem11  28480  tgcgr4  28871  axlowdimlem16  29400  axlowdimlem17  29401  nlelchi  32528  hmopidmchi  32618  evl1deg2  33974  evl1deg3  33975  esplyfvaln  34071  raddcn  34426  xrge0tmd  34442  ballotlem1ri  35033  chtvalz  35124  circlemethhgt  35138  dvtanlem  38405  ftc1cnnc  38428  dvasin  38440  dvacos  38441  dvreasin  38442  dvreacos  38443  areacirclem2  38445  areacirclem4  38447  cncfres  38502  resuppsinopn  43225  jm2.23  43824  0finon  44275  1finon  44276  2finon  44277  3finon  44278  4finon  44279  fvnonrel  44424  frege54cor1c  44742  fourierdlem28  46950  fourierdlem57  46978  fourierdlem59  46980  fourierdlem62  46983  fourierdlem68  46989  fouriersw  47046  etransclem23  47072  etransclem35  47084  etransclem38  47087  etransclem39  47088  etransclem44  47093  etransclem45  47094  etransclem47  47096  rrxtopn0  47108  hoidmvlelem2  47411  vonicclem2  47499  fmtno4prmfac  48462  gpg5grlim  48996  gpg5grlic  48997  dvsec  50676  dvcsc  50677  dvcot  50678  veroquadgsumlem  50803