Theorem eleqtri 2835

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  eleqtrri  2836  3eltr3i  2849  prid2  4722  2eluzge0  12806  faclbnd4lem1  14228  cats1fv  14794  bpoly2  15992  bpoly3  15993  bpoly4  15994  ef0lem  16013  phi1  16712  gsumws1  18775  lt6abl  19836  uvcvvcl  21754  mhpvarcl  22103  smadiadetlem4  22625  indiscld  23047  cnrehmeo  24919  cnrehmeoOLD  24920  ovolicc1  25485  dvcjbr  25921  vieta1lem2  26287  dvloglem  26625  logdmopn  26626  efopnlem2  26634  cxpcn  26722  cxpcnOLD  26723  loglesqrt  26739  log2ublem2  26925  efrlim  26947  efrlimOLD  26948  precsexlem11  28225  tgcgr4  28615  axlowdimlem16  29042  axlowdimlem17  29043  nlelchi  32149  hmopidmchi  32239  indf  32945  evl1deg2  33670  evl1deg3  33671  esplyfvaln  33751  raddcn  34107  xrge0tmd  34123  ballotlem1ri  34713  chtvalz  34807  circlemethhgt  34821  dvtanlem  37920  ftc1cnnc  37943  dvasin  37955  dvacos  37956  dvreasin  37957  dvreacos  37958  areacirclem2  37960  areacirclem4  37962  cncfres  38016  resuppsinopn  42733  jm2.23  43353  0finon  43804  1finon  43805  2finon  43806  3finon  43807  4finon  43808  fvnonrel  43953  frege54cor1c  44271  fourierdlem28  46493  fourierdlem57  46521  fourierdlem59  46523  fourierdlem62  46526  fourierdlem68  46532  fouriersw  46589  etransclem23  46615  etransclem35  46627  etransclem38  46630  etransclem39  46631  etransclem44  46636  etransclem45  46637  etransclem47  46639  rrxtopn0  46651  hoidmvlelem2  46954  vonicclem2  47042  fmtno4prmfac  47932  gpg5grlim  48453  gpg5grlic  48454