Theorem eleqtri 2858

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  eleqtrri  2859  3eltr3i  2872  prid2  4724  indf  12281  2eluzge0  12963  faclbnd4lem1  14390  cats1fv  14963  bpoly2  16176  bpoly3  16177  bpoly4  16178  ef0lem  16197  phi1  16897  gsumws1  18981  lt6abl  20056  uvcvvcl  22040  mhpvarcl  22416  smadiadetlem4  22931  indiscld  23356  cnrehmeo  25221  ovolicc1  25784  dvcjbr  26216  vieta1lem2  26583  dvloglem  26925  logdmopn  26926  efopnlem2  26934  cxpcn  27022  loglesqrt  27038  log2ublem2  27224  efrlim  27246  precsexlem11  28522  tgcgr4  28913  axlowdimlem16  29454  axlowdimlem17  29455  nlelchi  32582  hmopidmchi  32672  evl1deg2  34028  evl1deg3  34029  esplyfvaln  34125  raddcn  34480  xrge0tmd  34496  ballotlem1ri  35087  chtvalz  35178  circlemethhgt  35192  dvtanlem  38501  ftc1cnnc  38524  dvasin  38536  dvacos  38537  dvreasin  38538  dvreacos  38539  areacirclem2  38541  areacirclem4  38543  cncfres  38613  resuppsinopn  43336  jm2.23  43935  0finon  44386  1finon  44387  2finon  44388  3finon  44389  4finon  44390  fvnonrel  44535  frege54cor1c  44853  fourierdlem28  47061  fourierdlem57  47089  fourierdlem59  47091  fourierdlem62  47094  fourierdlem68  47100  fouriersw  47157  etransclem23  47183  etransclem35  47195  etransclem38  47198  etransclem39  47199  etransclem44  47204  etransclem45  47205  etransclem47  47207  rrxtopn0  47219  hoidmvlelem2  47522  vonicclem2  47610  fmtno4prmfac  48573  gpg5grlim  49107  gpg5grlic  49108  dvsec  50772  dvcsc  50773  dvcot  50774  veroquadgsumlem  50899