Theorem eleqtri 2860

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837

This theorem is used by:  eleqtrri  2861  3eltr3i  2874  prid2  4728  indf  12230  2eluzge0  12911  faclbnd4lem1  14336  cats1fv  14903  bpoly2  16117  bpoly3  16118  bpoly4  16119  ef0lem  16138  phi1  16838  gsumws1  18903  lt6abl  19971  uvcvvcl  21948  mhpvarcl  22322  smadiadetlem4  22837  indiscld  23259  cnrehmeo  25123  ovolicc1  25686  dvcjbr  26119  vieta1lem2  26483  dvloglem  26824  logdmopn  26825  efopnlem2  26833  cxpcn  26921  loglesqrt  26937  log2ublem2  27123  efrlim  27145  precsexlem11  28421  tgcgr4  28811  axlowdimlem16  29318  axlowdimlem17  29319  nlelchi  32424  hmopidmchi  32514  evl1deg2  33876  evl1deg3  33877  esplyfvaln  33973  raddcn  34328  xrge0tmd  34344  ballotlem1ri  34934  chtvalz  35025  circlemethhgt  35039  dvtanlem  38348  ftc1cnnc  38371  dvasin  38383  dvacos  38384  dvreasin  38385  dvreacos  38386  areacirclem2  38388  areacirclem4  38390  cncfres  38444  resuppsinopn  43152  jm2.23  43751  0finon  44202  1finon  44203  2finon  44204  3finon  44205  4finon  44206  fvnonrel  44351  frege54cor1c  44669  fourierdlem28  46877  fourierdlem57  46905  fourierdlem59  46907  fourierdlem62  46910  fourierdlem68  46916  fouriersw  46973  etransclem23  46999  etransclem35  47011  etransclem38  47014  etransclem39  47015  etransclem44  47020  etransclem45  47021  etransclem47  47023  rrxtopn0  47035  hoidmvlelem2  47338  vonicclem2  47426  fmtno4prmfac  48352  gpg5grlim  48886  gpg5grlic  48887