Theorem eleqtri 2826

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  eleqtrri  2827  3eltr3i  2840  prid2  4723  2eluzge0  12816  faclbnd4lem1  14234  cats1fv  14801  bpoly2  15999  bpoly3  16000  bpoly4  16001  ef0lem  16020  phi1  16719  gsumws1  18741  lt6abl  19801  uvcvvcl  21672  mhpvarcl  22011  smadiadetlem4  22532  indiscld  22954  cnrehmeo  24827  cnrehmeoOLD  24828  ovolicc1  25393  dvcjbr  25829  vieta1lem2  26195  dvloglem  26533  logdmopn  26534  efopnlem2  26542  cxpcn  26630  cxpcnOLD  26631  loglesqrt  26647  log2ublem2  26833  efrlim  26855  efrlimOLD  26856  precsexlem11  28095  tgcgr4  28434  axlowdimlem16  28860  axlowdimlem17  28861  nlelchi  31963  hmopidmchi  32053  indf  32751  evl1deg2  33519  evl1deg3  33520  raddcn  33892  xrge0tmd  33908  ballotlem1ri  34499  chtvalz  34593  circlemethhgt  34607  dvtanlem  37636  ftc1cnnc  37659  dvasin  37671  dvacos  37672  dvreasin  37673  dvreacos  37674  areacirclem2  37676  areacirclem4  37678  cncfres  37732  resuppsinopn  42324  jm2.23  42958  0finon  43410  1finon  43411  2finon  43412  3finon  43413  4finon  43414  fvnonrel  43559  frege54cor1c  43877  fourierdlem28  46106  fourierdlem57  46134  fourierdlem59  46136  fourierdlem62  46139  fourierdlem68  46145  fouriersw  46202  etransclem23  46228  etransclem35  46240  etransclem38  46243  etransclem39  46244  etransclem44  46249  etransclem45  46250  etransclem47  46252  rrxtopn0  46264  hoidmvlelem2  46567  vonicclem2  46655  fmtno4prmfac  47546  gpg5grlic  48057