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  4715  2eluzge0  12782  faclbnd4lem1  14200  cats1fv  14766  bpoly2  15964  bpoly3  15965  bpoly4  15966  ef0lem  15985  phi1  16684  gsumws1  18712  lt6abl  19774  uvcvvcl  21694  mhpvarcl  22033  smadiadetlem4  22554  indiscld  22976  cnrehmeo  24849  cnrehmeoOLD  24850  ovolicc1  25415  dvcjbr  25851  vieta1lem2  26217  dvloglem  26555  logdmopn  26556  efopnlem2  26564  cxpcn  26652  cxpcnOLD  26653  loglesqrt  26669  log2ublem2  26855  efrlim  26877  efrlimOLD  26878  precsexlem11  28124  tgcgr4  28476  axlowdimlem16  28902  axlowdimlem17  28903  nlelchi  32005  hmopidmchi  32095  indf  32798  evl1deg2  33512  evl1deg3  33513  raddcn  33896  xrge0tmd  33912  ballotlem1ri  34503  chtvalz  34597  circlemethhgt  34611  dvtanlem  37649  ftc1cnnc  37672  dvasin  37684  dvacos  37685  dvreasin  37686  dvreacos  37687  areacirclem2  37689  areacirclem4  37691  cncfres  37745  resuppsinopn  42336  jm2.23  42969  0finon  43421  1finon  43422  2finon  43423  3finon  43424  4finon  43425  fvnonrel  43570  frege54cor1c  43888  fourierdlem28  46116  fourierdlem57  46144  fourierdlem59  46146  fourierdlem62  46149  fourierdlem68  46155  fouriersw  46212  etransclem23  46238  etransclem35  46250  etransclem38  46253  etransclem39  46254  etransclem44  46259  etransclem45  46260  etransclem47  46262  rrxtopn0  46274  hoidmvlelem2  46577  vonicclem2  46665  fmtno4prmfac  47556  gpg5grlim  48077  gpg5grlic  48078