Theorem eleqtri 2909

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

Syntax hints:   = wceq 1531   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-cleq 2812  df-clel 2891

This theorem is referenced by:  eleqtrri  2910  3eltr3i  2923  prid2  4691  2eluzge0  12285  fz0to4untppr  13002  seqp1i  13378  faclbnd4lem1  13645  cats1fv  14213  bpoly2  15403  bpoly3  15404  bpoly4  15405  ef0lem  15424  phi1  16102  gsumws1  17994  lt6abl  19007  uvcvvcl  20923  smadiadetlem4  21270  indiscld  21691  cnrehmeo  23549  ovolicc1  24109  dvcjbr  24538  vieta1lem2  24892  dvloglem  25223  logdmopn  25224  efopnlem2  25232  cxpcn  25318  loglesqrt  25331  log2ublem2  25517  efrlim  25539  tgcgr4  26309  axlowdimlem16  26735  axlowdimlem17  26736  nlelchi  29830  hmopidmchi  29920  raddcn  31165  xrge0tmd  31181  indf  31267  ballotlem1ri  31785  chtvalz  31893  circlemethhgt  31907  dvtanlem  34933  ftc1cnnc  34958  dvasin  34970  dvacos  34971  dvreasin  34972  dvreacos  34973  areacirclem2  34975  areacirclem4  34977  cncfres  35035  jm2.23  39583  fvnonrel  39947  frege54cor1c  40251  fourierdlem28  42410  fourierdlem57  42438  fourierdlem59  42440  fourierdlem62  42443  fourierdlem68  42449  fouriersw  42506  etransclem23  42532  etransclem35  42544  etransclem38  42547  etransclem39  42548  etransclem44  42553  etransclem45  42554  etransclem47  42556  rrxtopn0  42568  hoidmvlelem2  42868  vonicclem2  42956  fmtno4prmfac  43724