Theorem eleqtri 2849

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

Syntax hints:   = wceq 1539   ∈ wcel 2112

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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-clel 2831

This theorem is referenced by:  eleqtrri  2850  3eltr3i  2863  prid2  4649  2eluzge0  12318  fz0to4untppr  13044  faclbnd4lem1  13688  cats1fv  14253  bpoly2  15444  bpoly3  15445  bpoly4  15446  ef0lem  15465  phi1  16150  gsumws1  18053  lt6abl  19068  uvcvvcl  20537  mhpvarcl  20876  smadiadetlem4  21354  indiscld  21776  cnrehmeo  23639  ovolicc1  24201  dvcjbr  24633  vieta1lem2  24991  dvloglem  25323  logdmopn  25324  efopnlem2  25332  cxpcn  25418  loglesqrt  25431  log2ublem2  25617  efrlim  25639  tgcgr4  26409  axlowdimlem16  26835  axlowdimlem17  26836  nlelchi  29928  hmopidmchi  30018  raddcn  31385  xrge0tmd  31401  indf  31487  ballotlem1ri  32005  chtvalz  32113  circlemethhgt  32127  dvtanlem  35371  ftc1cnnc  35394  dvasin  35406  dvacos  35407  dvreasin  35408  dvreacos  35409  areacirclem2  35411  areacirclem4  35413  cncfres  35468  jm2.23  40295  fvnonrel  40655  frege54cor1c  40974  fourierdlem28  43128  fourierdlem57  43156  fourierdlem59  43158  fourierdlem62  43161  fourierdlem68  43167  fouriersw  43224  etransclem23  43250  etransclem35  43262  etransclem38  43265  etransclem39  43266  etransclem44  43271  etransclem45  43272  etransclem47  43274  rrxtopn0  43286  hoidmvlelem2  43586  vonicclem2  43674  fmtno4prmfac  44442