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 2106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816

This theorem is referenced by:  eleqtrri  2838  3eltr3i  2851  prid2  4699  2eluzge0  12633  fz0to4untppr  13359  faclbnd4lem1  14007  cats1fv  14572  bpoly2  15767  bpoly3  15768  bpoly4  15769  ef0lem  15788  phi1  16474  gsumws1  18476  lt6abl  19496  uvcvvcl  20994  mhpvarcl  21338  smadiadetlem4  21818  indiscld  22242  cnrehmeo  24116  ovolicc1  24680  dvcjbr  25113  vieta1lem2  25471  dvloglem  25803  logdmopn  25804  efopnlem2  25812  cxpcn  25898  loglesqrt  25911  log2ublem2  26097  efrlim  26119  tgcgr4  26892  axlowdimlem16  27325  axlowdimlem17  27326  nlelchi  30423  hmopidmchi  30513  raddcn  31879  xrge0tmd  31895  indf  31983  ballotlem1ri  32501  chtvalz  32609  circlemethhgt  32623  dvtanlem  35826  ftc1cnnc  35849  dvasin  35861  dvacos  35862  dvreasin  35863  dvreacos  35864  areacirclem2  35866  areacirclem4  35868  cncfres  35923  jm2.23  40818  0finon  41055  1finon  41056  2finon  41057  3finon  41058  4finon  41059  fvnonrel  41205  frege54cor1c  41523  fourierdlem28  43676  fourierdlem57  43704  fourierdlem59  43706  fourierdlem62  43709  fourierdlem68  43715  fouriersw  43772  etransclem23  43798  etransclem35  43810  etransclem38  43813  etransclem39  43814  etransclem44  43819  etransclem45  43820  etransclem47  43822  rrxtopn0  43834  hoidmvlelem2  44134  vonicclem2  44222  fmtno4prmfac  45024