Theorem eleqtri 2831

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

Syntax hints:   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808

This theorem is referenced by:  eleqtrri  2832  3eltr3i  2845  prid2  4717  2eluzge0  12785  faclbnd4lem1  14207  cats1fv  14773  bpoly2  15971  bpoly3  15972  bpoly4  15973  ef0lem  15992  phi1  16691  gsumws1  18754  lt6abl  19815  uvcvvcl  21733  mhpvarcl  22082  smadiadetlem4  22604  indiscld  23026  cnrehmeo  24898  cnrehmeoOLD  24899  ovolicc1  25464  dvcjbr  25900  vieta1lem2  26266  dvloglem  26604  logdmopn  26605  efopnlem2  26613  cxpcn  26701  cxpcnOLD  26702  loglesqrt  26718  log2ublem2  26904  efrlim  26926  efrlimOLD  26927  precsexlem11  28175  tgcgr4  28529  axlowdimlem16  28956  axlowdimlem17  28957  nlelchi  32062  hmopidmchi  32152  indf  32862  evl1deg2  33586  evl1deg3  33587  raddcn  34014  xrge0tmd  34030  ballotlem1ri  34620  chtvalz  34714  circlemethhgt  34728  dvtanlem  37782  ftc1cnnc  37805  dvasin  37817  dvacos  37818  dvreasin  37819  dvreacos  37820  areacirclem2  37822  areacirclem4  37824  cncfres  37878  resuppsinopn  42533  jm2.23  43153  0finon  43605  1finon  43606  2finon  43607  3finon  43608  4finon  43609  fvnonrel  43754  frege54cor1c  44072  fourierdlem28  46295  fourierdlem57  46323  fourierdlem59  46325  fourierdlem62  46328  fourierdlem68  46334  fouriersw  46391  etransclem23  46417  etransclem35  46429  etransclem38  46432  etransclem39  46433  etransclem44  46438  etransclem45  46439  etransclem47  46441  rrxtopn0  46453  hoidmvlelem2  46756  vonicclem2  46844  fmtno4prmfac  47734  gpg5grlim  48255  gpg5grlic  48256