Theorem eleqtri 2867

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

Syntax hints:   = wceq 1567   ∈ wcel 2149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844

This theorem is referenced by:  eleqtrri  2868  3eltr3i  2881  prid2  4732  indf  12224  2eluzge0  12905  faclbnd4lem1  14329  cats1fv  14896  bpoly2  16111  bpoly3  16112  bpoly4  16113  ef0lem  16132  phi1  16832  gsumws1  18897  lt6abl  19965  uvcvvcl  21906  mhpvarcl  22280  smadiadetlem4  22795  indiscld  23217  cnrehmeo  25081  ovolicc1  25644  dvcjbr  26077  vieta1lem2  26441  dvloglem  26779  logdmopn  26780  efopnlem2  26788  cxpcn  26876  loglesqrt  26892  log2ublem2  27078  efrlim  27100  precsexlem11  28376  tgcgr4  28766  axlowdimlem16  29248  axlowdimlem17  29249  nlelchi  32354  hmopidmchi  32444  evl1deg2  33812  evl1deg3  33813  esplyfvaln  33909  raddcn  34264  xrge0tmd  34280  ballotlem1ri  34870  chtvalz  34961  circlemethhgt  34975  dvtanlem  38243  ftc1cnnc  38266  dvasin  38278  dvacos  38279  dvreasin  38280  dvreacos  38281  areacirclem2  38283  areacirclem4  38285  cncfres  38339  resuppsinopn  43049  jm2.23  43650  0finon  44101  1finon  44102  2finon  44103  3finon  44104  4finon  44105  fvnonrel  44250  frege54cor1c  44568  fourierdlem28  46776  fourierdlem57  46804  fourierdlem59  46806  fourierdlem62  46809  fourierdlem68  46815  fouriersw  46872  etransclem23  46898  etransclem35  46910  etransclem38  46913  etransclem39  46914  etransclem44  46919  etransclem45  46920  etransclem47  46922  rrxtopn0  46934  hoidmvlelem2  47237  vonicclem2  47325  fmtno4prmfac  48248  gpg5grlim  48782  gpg5grlic  48783