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

Syntax hints:   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eleqtrri  2838  3eltr3i  2851  prid2  4696  2eluzge0  12562  fz0to4untppr  13288  faclbnd4lem1  13935  cats1fv  14500  bpoly2  15695  bpoly3  15696  bpoly4  15697  ef0lem  15716  phi1  16402  gsumws1  18391  lt6abl  19411  uvcvvcl  20904  mhpvarcl  21248  smadiadetlem4  21726  indiscld  22150  cnrehmeo  24022  ovolicc1  24585  dvcjbr  25018  vieta1lem2  25376  dvloglem  25708  logdmopn  25709  efopnlem2  25717  cxpcn  25803  loglesqrt  25816  log2ublem2  26002  efrlim  26024  tgcgr4  26796  axlowdimlem16  27228  axlowdimlem17  27229  nlelchi  30324  hmopidmchi  30414  raddcn  31781  xrge0tmd  31797  indf  31883  ballotlem1ri  32401  chtvalz  32509  circlemethhgt  32523  dvtanlem  35753  ftc1cnnc  35776  dvasin  35788  dvacos  35789  dvreasin  35790  dvreacos  35791  areacirclem2  35793  areacirclem4  35795  cncfres  35850  jm2.23  40734  fvnonrel  41094  frege54cor1c  41412  fourierdlem28  43566  fourierdlem57  43594  fourierdlem59  43596  fourierdlem62  43599  fourierdlem68  43605  fouriersw  43662  etransclem23  43688  etransclem35  43700  etransclem38  43703  etransclem39  43704  etransclem44  43709  etransclem45  43710  etransclem47  43712  rrxtopn0  43724  hoidmvlelem2  44024  vonicclem2  44112  fmtno4prmfac  44912