Theorem eleqtri 2888

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

Syntax hints:   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eleqtrri  2889  3eltr3i  2902  prid2  4659  2eluzge0  12281  fz0to4untppr  13005  faclbnd4lem1  13649  cats1fv  14212  bpoly2  15403  bpoly3  15404  bpoly4  15405  ef0lem  15424  phi1  16100  gsumws1  17994  lt6abl  19008  uvcvvcl  20476  mhpvarcl  20798  smadiadetlem4  21274  indiscld  21696  cnrehmeo  23558  ovolicc1  24120  dvcjbr  24552  vieta1lem2  24907  dvloglem  25239  logdmopn  25240  efopnlem2  25248  cxpcn  25334  loglesqrt  25347  log2ublem2  25533  efrlim  25555  tgcgr4  26325  axlowdimlem16  26751  axlowdimlem17  26752  nlelchi  29844  hmopidmchi  29934  raddcn  31282  xrge0tmd  31298  indf  31384  ballotlem1ri  31902  chtvalz  32010  circlemethhgt  32024  dvtanlem  35106  ftc1cnnc  35129  dvasin  35141  dvacos  35142  dvreasin  35143  dvreacos  35144  areacirclem2  35146  areacirclem4  35148  cncfres  35203  jm2.23  39937  fvnonrel  40297  frege54cor1c  40616  fourierdlem28  42777  fourierdlem57  42805  fourierdlem59  42807  fourierdlem62  42810  fourierdlem68  42816  fouriersw  42873  etransclem23  42899  etransclem35  42911  etransclem38  42914  etransclem39  42915  etransclem44  42920  etransclem45  42921  etransclem47  42923  rrxtopn0  42935  hoidmvlelem2  43235  vonicclem2  43323  fmtno4prmfac  44089