Theorem eleqtri 2839

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

Syntax hints:   = wceq 1548   ∈ wcel 2121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816

This theorem is referenced by:  eleqtrri  2840  3eltr3i  2853  prid2  4698  indf  12160  2eluzge0  12826  faclbnd4lem1  14250  cats1fv  14816  bpoly2  16017  bpoly3  16018  bpoly4  16019  ef0lem  16038  phi1  16738  gsumws1  18801  lt6abl  19865  uvcvvcl  21766  mhpvarcl  22140  smadiadetlem4  22656  indiscld  23078  cnrehmeo  24942  ovolicc1  25505  dvcjbr  25938  vieta1lem2  26299  dvloglem  26634  logdmopn  26635  efopnlem2  26643  cxpcn  26731  loglesqrt  26747  log2ublem2  26933  efrlim  26955  precsexlem11  28231  tgcgr4  28621  axlowdimlem16  29048  axlowdimlem17  29049  nlelchi  32154  hmopidmchi  32244  evl1deg2  33672  evl1deg3  33673  esplyfvaln  33770  raddcn  34125  xrge0tmd  34141  ballotlem1ri  34731  chtvalz  34825  circlemethhgt  34839  dvtanlem  38051  ftc1cnnc  38074  dvasin  38086  dvacos  38087  dvreasin  38088  dvreacos  38089  areacirclem2  38091  areacirclem4  38093  cncfres  38147  resuppsinopn  42855  jm2.23  43456  0finon  43907  1finon  43908  2finon  43909  3finon  43910  4finon  43911  fvnonrel  44056  frege54cor1c  44374  fourierdlem28  46592  fourierdlem57  46620  fourierdlem59  46622  fourierdlem62  46625  fourierdlem68  46631  fouriersw  46688  etransclem23  46714  etransclem35  46726  etransclem38  46729  etransclem39  46730  etransclem44  46735  etransclem45  46736  etransclem47  46738  rrxtopn0  46750  hoidmvlelem2  47053  vonicclem2  47141  fmtno4prmfac  48064  gpg5grlim  48598  gpg5grlic  48599