Theorem eleqtri 2837

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

Syntax hints:   = wceq 1547   ∈ wcel 2119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814

This theorem is referenced by:  eleqtrri  2838  3eltr3i  2851  prid2  4695  indf  12156  2eluzge0  12822  faclbnd4lem1  14246  cats1fv  14812  bpoly2  16013  bpoly3  16014  bpoly4  16015  ef0lem  16034  phi1  16734  gsumws1  18797  lt6abl  19861  uvcvvcl  21762  mhpvarcl  22136  smadiadetlem4  22652  indiscld  23074  cnrehmeo  24938  ovolicc1  25501  dvcjbr  25934  vieta1lem2  26295  dvloglem  26630  logdmopn  26631  efopnlem2  26639  cxpcn  26727  loglesqrt  26743  log2ublem2  26929  efrlim  26951  precsexlem11  28227  tgcgr4  28617  axlowdimlem16  29044  axlowdimlem17  29045  nlelchi  32150  hmopidmchi  32240  evl1deg2  33660  evl1deg3  33661  esplyfvaln  33758  raddcn  34113  xrge0tmd  34129  ballotlem1ri  34719  chtvalz  34813  circlemethhgt  34827  dvtanlem  38036  ftc1cnnc  38059  dvasin  38071  dvacos  38072  dvreasin  38073  dvreacos  38074  areacirclem2  38076  areacirclem4  38078  cncfres  38132  resuppsinopn  42840  jm2.23  43441  0finon  43892  1finon  43893  2finon  43894  3finon  43895  4finon  43896  fvnonrel  44041  frege54cor1c  44359  fourierdlem28  46578  fourierdlem57  46606  fourierdlem59  46608  fourierdlem62  46611  fourierdlem68  46617  fouriersw  46674  etransclem23  46700  etransclem35  46712  etransclem38  46715  etransclem39  46716  etransclem44  46721  etransclem45  46722  etransclem47  46724  rrxtopn0  46736  hoidmvlelem2  47039  vonicclem2  47127  fmtno4prmfac  48050  gpg5grlim  48584  gpg5grlic  48585