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  4727  2eluzge0  12840  faclbnd4lem1  14258  cats1fv  14825  bpoly2  16023  bpoly3  16024  bpoly4  16025  ef0lem  16044  phi1  16743  gsumws1  18765  lt6abl  19825  uvcvvcl  21696  mhpvarcl  22035  smadiadetlem4  22556  indiscld  22978  cnrehmeo  24851  cnrehmeoOLD  24852  ovolicc1  25417  dvcjbr  25853  vieta1lem2  26219  dvloglem  26557  logdmopn  26558  efopnlem2  26566  cxpcn  26654  cxpcnOLD  26655  loglesqrt  26671  log2ublem2  26857  efrlim  26879  efrlimOLD  26880  precsexlem11  28119  tgcgr4  28458  axlowdimlem16  28884  axlowdimlem17  28885  nlelchi  31990  hmopidmchi  32080  indf  32778  evl1deg2  33546  evl1deg3  33547  raddcn  33919  xrge0tmd  33935  ballotlem1ri  34526  chtvalz  34620  circlemethhgt  34634  dvtanlem  37663  ftc1cnnc  37686  dvasin  37698  dvacos  37699  dvreasin  37700  dvreacos  37701  areacirclem2  37703  areacirclem4  37705  cncfres  37759  resuppsinopn  42351  jm2.23  42985  0finon  43437  1finon  43438  2finon  43439  3finon  43440  4finon  43441  fvnonrel  43586  frege54cor1c  43904  fourierdlem28  46133  fourierdlem57  46161  fourierdlem59  46163  fourierdlem62  46166  fourierdlem68  46172  fouriersw  46229  etransclem23  46255  etransclem35  46267  etransclem38  46270  etransclem39  46271  etransclem44  46276  etransclem45  46277  etransclem47  46279  rrxtopn0  46291  hoidmvlelem2  46594  vonicclem2  46682  fmtno4prmfac  47573  gpg5grlic  48084