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  4708  indf  12156  2eluzge0  12822  faclbnd4lem1  14246  cats1fv  14812  bpoly2  16013  bpoly3  16014  bpoly4  16015  ef0lem  16034  phi1  16734  gsumws1  18797  lt6abl  19861  uvcvvcl  21777  mhpvarcl  22124  smadiadetlem4  22644  indiscld  23066  cnrehmeo  24930  ovolicc1  25493  dvcjbr  25926  vieta1lem2  26288  dvloglem  26625  logdmopn  26626  efopnlem2  26634  cxpcn  26722  loglesqrt  26738  log2ublem2  26924  efrlim  26946  efrlimOLD  26947  precsexlem11  28223  tgcgr4  28613  axlowdimlem16  29040  axlowdimlem17  29041  nlelchi  32147  hmopidmchi  32237  evl1deg2  33652  evl1deg3  33653  esplyfvaln  33733  raddcn  34089  xrge0tmd  34105  ballotlem1ri  34695  chtvalz  34789  circlemethhgt  34803  dvtanlem  38004  ftc1cnnc  38027  dvasin  38039  dvacos  38040  dvreasin  38041  dvreacos  38042  areacirclem2  38044  areacirclem4  38046  cncfres  38100  resuppsinopn  42809  jm2.23  43442  0finon  43893  1finon  43894  2finon  43895  3finon  43896  4finon  43897  fvnonrel  44042  frege54cor1c  44360  fourierdlem28  46581  fourierdlem57  46609  fourierdlem59  46611  fourierdlem62  46614  fourierdlem68  46620  fouriersw  46677  etransclem23  46703  etransclem35  46715  etransclem38  46718  etransclem39  46719  etransclem44  46724  etransclem45  46725  etransclem47  46727  rrxtopn0  46739  hoidmvlelem2  47042  vonicclem2  47130  fmtno4prmfac  48047  gpg5grlim  48581  gpg5grlic  48582