Theorem eleqtri 2827

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  eleqtrri  2828  3eltr3i  2841  prid2  4730  2eluzge0  12847  faclbnd4lem1  14265  cats1fv  14832  bpoly2  16030  bpoly3  16031  bpoly4  16032  ef0lem  16051  phi1  16750  gsumws1  18772  lt6abl  19832  uvcvvcl  21703  mhpvarcl  22042  smadiadetlem4  22563  indiscld  22985  cnrehmeo  24858  cnrehmeoOLD  24859  ovolicc1  25424  dvcjbr  25860  vieta1lem2  26226  dvloglem  26564  logdmopn  26565  efopnlem2  26573  cxpcn  26661  cxpcnOLD  26662  loglesqrt  26678  log2ublem2  26864  efrlim  26886  efrlimOLD  26887  precsexlem11  28126  tgcgr4  28465  axlowdimlem16  28891  axlowdimlem17  28892  nlelchi  31997  hmopidmchi  32087  indf  32785  evl1deg2  33553  evl1deg3  33554  raddcn  33926  xrge0tmd  33942  ballotlem1ri  34533  chtvalz  34627  circlemethhgt  34641  dvtanlem  37670  ftc1cnnc  37693  dvasin  37705  dvacos  37706  dvreasin  37707  dvreacos  37708  areacirclem2  37710  areacirclem4  37712  cncfres  37766  resuppsinopn  42358  jm2.23  42992  0finon  43444  1finon  43445  2finon  43446  3finon  43447  4finon  43448  fvnonrel  43593  frege54cor1c  43911  fourierdlem28  46140  fourierdlem57  46168  fourierdlem59  46170  fourierdlem62  46173  fourierdlem68  46179  fouriersw  46236  etransclem23  46262  etransclem35  46274  etransclem38  46277  etransclem39  46278  etransclem44  46283  etransclem45  46284  etransclem47  46286  rrxtopn0  46298  hoidmvlelem2  46601  vonicclem2  46689  fmtno4prmfac  47577  gpg5grlic  48088