Theorem eleqtri 2699

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtr.1	⊢ 𝐴 ∈ 𝐵
eleqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eleq2i 2693	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)
4	1, 3	mpbi 220	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  eleqtrri  2700  3eltr3i  2713  prid2  4298  2eluzge0  11733  fz0to4untppr  12442  seqp1i  12817  faclbnd4lem1  13080  cats1fv  13604  bpoly2  14788  bpoly3  14789  bpoly4  14790  ef0lem  14809  phi1  15478  gsumws1  17376  lt6abl  18296  uvcvvcl  20126  smadiadetlem4  20475  indiscld  20895  cnrehmeo  22752  ovolicc1  23284  dvcjbr  23712  vieta1lem2  24066  dvloglem  24394  logdmopn  24395  efopnlem2  24403  cxpcn  24486  loglesqrt  24499  log2ublem2  24674  efrlim  24696  tgcgr4  25426  axlowdimlem16  25837  axlowdimlem17  25838  nlelchi  28920  hmopidmchi  29010  raddcn  29975  xrge0tmd  29992  indf  30077  ballotlem1ri  30596  chtvalz  30707  circlemethhgt  30721  dvtanlem  33459  ftc1cnnc  33484  dvasin  33496  dvacos  33497  dvreasin  33498  dvreacos  33499  areacirclem2  33501  areacirclem4  33503  cncfres  33564  jm2.23  37563  fvnonrel  37903  frege54cor1c  38209  fourierdlem28  40352  fourierdlem57  40380  fourierdlem59  40382  fourierdlem62  40385  fourierdlem68  40391  fouriersw  40448  etransclem23  40474  etransclem35  40486  etransclem38  40489  etransclem39  40490  etransclem44  40495  etransclem45  40496  etransclem47  40498  rrxtopn0  40513  hoidmvlelem2  40810  vonicclem2  40898  fmtno4prmfac  41484