Theorem eleqtri 2904

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

Syntax hints:   = wceq 1656   ∈ wcel 2164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-cleq 2818  df-clel 2821

This theorem is referenced by:  eleqtrri  2905  3eltr3i  2918  prid2  4516  2eluzge0  12015  fz0to4untppr  12737  seqp1i  13111  faclbnd4lem1  13373  cats1fv  13980  bpoly2  15160  bpoly3  15161  bpoly4  15162  ef0lem  15181  phi1  15849  gsumws1  17729  lt6abl  18649  uvcvvcl  20493  smadiadetlem4  20844  indiscld  21266  cnrehmeo  23122  ovolicc1  23682  dvcjbr  24111  vieta1lem2  24465  dvloglem  24793  logdmopn  24794  efopnlem2  24802  cxpcn  24888  loglesqrt  24901  log2ublem2  25087  efrlim  25109  tgcgr4  25843  axlowdimlem16  26256  axlowdimlem17  26257  nlelchi  29464  hmopidmchi  29554  raddcn  30509  xrge0tmd  30526  indf  30611  ballotlem1ri  31131  chtvalz  31245  circlemethhgt  31259  dvtanlem  33995  ftc1cnnc  34020  dvasin  34032  dvacos  34033  dvreasin  34034  dvreacos  34035  areacirclem2  34037  areacirclem4  34039  cncfres  34099  jm2.23  38399  fvnonrel  38737  frege54cor1c  39042  fourierdlem28  41139  fourierdlem57  41167  fourierdlem59  41169  fourierdlem62  41172  fourierdlem68  41178  fouriersw  41235  etransclem23  41261  etransclem35  41273  etransclem38  41276  etransclem39  41277  etransclem44  41282  etransclem45  41283  etransclem47  41285  rrxtopn0  41297  hoidmvlelem2  41597  vonicclem2  41685  fmtno4prmfac  42307