Theorem eleqtri 2834

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

Syntax hints:   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleqtrri  2835  3eltr3i  2848  prid2  4720  2eluzge0  12794  faclbnd4lem1  14216  cats1fv  14782  bpoly2  15980  bpoly3  15981  bpoly4  15982  ef0lem  16001  phi1  16700  gsumws1  18763  lt6abl  19824  uvcvvcl  21742  mhpvarcl  22091  smadiadetlem4  22613  indiscld  23035  cnrehmeo  24907  cnrehmeoOLD  24908  ovolicc1  25473  dvcjbr  25909  vieta1lem2  26275  dvloglem  26613  logdmopn  26614  efopnlem2  26622  cxpcn  26710  cxpcnOLD  26711  loglesqrt  26727  log2ublem2  26913  efrlim  26935  efrlimOLD  26936  precsexlem11  28213  tgcgr4  28603  axlowdimlem16  29030  axlowdimlem17  29031  nlelchi  32136  hmopidmchi  32226  indf  32934  evl1deg2  33658  evl1deg3  33659  raddcn  34086  xrge0tmd  34102  ballotlem1ri  34692  chtvalz  34786  circlemethhgt  34800  dvtanlem  37870  ftc1cnnc  37893  dvasin  37905  dvacos  37906  dvreasin  37907  dvreacos  37908  areacirclem2  37910  areacirclem4  37912  cncfres  37966  resuppsinopn  42618  jm2.23  43238  0finon  43689  1finon  43690  2finon  43691  3finon  43692  4finon  43693  fvnonrel  43838  frege54cor1c  44156  fourierdlem28  46379  fourierdlem57  46407  fourierdlem59  46409  fourierdlem62  46412  fourierdlem68  46418  fouriersw  46475  etransclem23  46501  etransclem35  46513  etransclem38  46516  etransclem39  46517  etransclem44  46522  etransclem45  46523  etransclem47  46525  rrxtopn0  46537  hoidmvlelem2  46840  vonicclem2  46928  fmtno4prmfac  47818  gpg5grlim  48339  gpg5grlic  48340