Theorem eleqtri 2862

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

Syntax hints:   = wceq 1562   ∈ wcel 2144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-cleq 2756  df-clel 2839

This theorem is referenced by:  eleqtrri  2863  3eltr3i  2876  prid2  4724  indf  12203  2eluzge0  12884  faclbnd4lem1  14308  cats1fv  14874  bpoly2  16089  bpoly3  16090  bpoly4  16091  ef0lem  16110  phi1  16810  gsumws1  18874  lt6abl  19937  uvcvvcl  21841  mhpvarcl  22215  smadiadetlem4  22731  indiscld  23153  cnrehmeo  25017  ovolicc1  25580  dvcjbr  26013  vieta1lem2  26377  dvloglem  26715  logdmopn  26716  efopnlem2  26724  cxpcn  26812  loglesqrt  26828  log2ublem2  27014  efrlim  27036  precsexlem11  28312  tgcgr4  28702  axlowdimlem16  29160  axlowdimlem17  29161  nlelchi  32266  hmopidmchi  32356  evl1deg2  33775  evl1deg3  33776  esplyfvaln  33873  raddcn  34228  xrge0tmd  34244  ballotlem1ri  34834  chtvalz  34925  circlemethhgt  34939  dvtanlem  38173  ftc1cnnc  38196  dvasin  38208  dvacos  38209  dvreasin  38210  dvreacos  38211  areacirclem2  38213  areacirclem4  38215  cncfres  38269  resuppsinopn  42977  jm2.23  43578  0finon  44029  1finon  44030  2finon  44031  3finon  44032  4finon  44033  fvnonrel  44178  frege54cor1c  44496  fourierdlem28  46714  fourierdlem57  46742  fourierdlem59  46744  fourierdlem62  46747  fourierdlem68  46753  fouriersw  46810  etransclem23  46836  etransclem35  46848  etransclem38  46851  etransclem39  46852  etransclem44  46857  etransclem45  46858  etransclem47  46860  rrxtopn0  46872  hoidmvlelem2  47175  vonicclem2  47263  fmtno4prmfac  48186  gpg5grlim  48720  gpg5grlic  48721