Theorem eleqtri 2832

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

Syntax hints:   = wceq 1540   ∈ wcel 2108

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  eleqtrri  2833  3eltr3i  2846  prid2  4739  2eluzge0  12909  faclbnd4lem1  14311  cats1fv  14878  bpoly2  16073  bpoly3  16074  bpoly4  16075  ef0lem  16094  phi1  16792  gsumws1  18816  lt6abl  19876  uvcvvcl  21747  mhpvarcl  22086  smadiadetlem4  22607  indiscld  23029  cnrehmeo  24902  cnrehmeoOLD  24903  ovolicc1  25469  dvcjbr  25905  vieta1lem2  26271  dvloglem  26609  logdmopn  26610  efopnlem2  26618  cxpcn  26706  cxpcnOLD  26707  loglesqrt  26723  log2ublem2  26909  efrlim  26931  efrlimOLD  26932  precsexlem11  28171  tgcgr4  28510  axlowdimlem16  28936  axlowdimlem17  28937  nlelchi  32042  hmopidmchi  32132  indf  32832  evl1deg2  33590  evl1deg3  33591  raddcn  33960  xrge0tmd  33976  ballotlem1ri  34567  chtvalz  34661  circlemethhgt  34675  dvtanlem  37693  ftc1cnnc  37716  dvasin  37728  dvacos  37729  dvreasin  37730  dvreacos  37731  areacirclem2  37733  areacirclem4  37735  cncfres  37789  resuppsinopn  42406  jm2.23  43020  0finon  43472  1finon  43473  2finon  43474  3finon  43475  4finon  43476  fvnonrel  43621  frege54cor1c  43939  fourierdlem28  46164  fourierdlem57  46192  fourierdlem59  46194  fourierdlem62  46197  fourierdlem68  46203  fouriersw  46260  etransclem23  46286  etransclem35  46298  etransclem38  46301  etransclem39  46302  etransclem44  46307  etransclem45  46308  etransclem47  46310  rrxtopn0  46322  hoidmvlelem2  46625  vonicclem2  46713  fmtno4prmfac  47586  gpg5grlic  48093