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 233	1 ⊢ 𝐴 ∈ 𝐶

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  eleqtrri  2863  3eltr3i  2876  prid2  4724  indf  12350  2eluzge0  13032  faclbnd4lem1  14461  cats1fv  15035  bpoly2  16249  bpoly3  16250  bpoly4  16251  ef0lem  16270  phi1  16976  gsumws1  19060  lt6abl  20136  uvcvvcl  22120  mhpvarcl  22496  smadiadetlem4  23011  indiscld  23436  cnrehmeo  25301  ovolicc1  25864  dvcjbr  26296  vieta1lem2  26661  dvloglem  27003  logdmopn  27004  efopnlem2  27012  cxpcn  27100  loglesqrt  27116  log2ublem2  27302  efrlim  27324  precsexlem11  28630  tgcgr4  29021  axlowdimlem16  29562  axlowdimlem17  29563  nlelchi  32690  hmopidmchi  32780  evl1deg2  34176  evl1deg3  34177  esplyfvaln  34273  raddcn  34628  xrge0tmd  34644  ballotlem1ri  35234  chtvalz  35325  circlemethhgt  35339  dvtanlem  38778  ftc1cnnc  38801  dvasin  38813  dvacos  38814  dvreasin  38815  dvreacos  38816  areacirclem2  38818  areacirclem4  38820  cncfres  38890  resuppsinopn  43605  jm2.23  44194  0finon  44639  1finon  44640  2finon  44641  3finon  44642  4finon  44643  fvnonrel  44787  frege54cor1c  45105  fourierdlem28  47348  fourierdlem57  47376  fourierdlem59  47378  fourierdlem62  47381  fourierdlem68  47387  fouriersw  47444  etransclem23  47470  etransclem35  47482  etransclem38  47485  etransclem39  47486  etransclem44  47491  etransclem45  47492  etransclem47  47494  rrxtopn0  47506  hoidmvlelem2  47809  vonicclem2  47897  fmtno4prmfac  48860  gpg5grlim  49394  gpg5grlic  49395  fuconuniqlem  50984  fuconuniqvalslem  50986  dvsec  51134  dvcsc  51135  dvcot  51136  veroquadgsumlem  51261