Theorem eleqtri 2829

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

Syntax hints:   = wceq 1539   ∈ wcel 2104

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  eleqtrri  2830  3eltr3i  2843  prid2  4766  2eluzge0  12881  fz0to4untppr  13608  faclbnd4lem1  14257  cats1fv  14814  bpoly2  16005  bpoly3  16006  bpoly4  16007  ef0lem  16026  phi1  16710  gsumws1  18755  lt6abl  19804  uvcvvcl  21561  mhpvarcl  21910  smadiadetlem4  22391  indiscld  22815  cnrehmeo  24698  cnrehmeoOLD  24699  ovolicc1  25265  dvcjbr  25701  vieta1lem2  26060  dvloglem  26392  logdmopn  26393  efopnlem2  26401  cxpcn  26489  loglesqrt  26502  log2ublem2  26688  efrlim  26710  precsexlem11  27902  tgcgr4  28049  axlowdimlem16  28482  axlowdimlem17  28483  nlelchi  31581  hmopidmchi  31671  raddcn  33207  xrge0tmd  33223  indf  33311  ballotlem1ri  33831  chtvalz  33939  circlemethhgt  33953  gg-cxpcn  35470  dvtanlem  36840  ftc1cnnc  36863  dvasin  36875  dvacos  36876  dvreasin  36877  dvreacos  36878  areacirclem2  36880  areacirclem4  36882  cncfres  36936  jm2.23  42037  0finon  42501  1finon  42502  2finon  42503  3finon  42504  4finon  42505  fvnonrel  42650  frege54cor1c  42968  fourierdlem28  45149  fourierdlem57  45177  fourierdlem59  45179  fourierdlem62  45182  fourierdlem68  45188  fouriersw  45245  etransclem23  45271  etransclem35  45283  etransclem38  45286  etransclem39  45287  etransclem44  45292  etransclem45  45293  etransclem47  45295  rrxtopn0  45307  hoidmvlelem2  45610  vonicclem2  45698  fmtno4prmfac  46538