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  37866  ftc1cnnc  37889  dvasin  37901  dvacos  37902  dvreasin  37903  dvreacos  37904  areacirclem2  37906  areacirclem4  37908  cncfres  37962  resuppsinopn  42614  jm2.23  43234  0finon  43685  1finon  43686  2finon  43687  3finon  43688  4finon  43689  fvnonrel  43834  frege54cor1c  44152  fourierdlem28  46375  fourierdlem57  46403  fourierdlem59  46405  fourierdlem62  46408  fourierdlem68  46414  fouriersw  46471  etransclem23  46497  etransclem35  46509  etransclem38  46512  etransclem39  46513  etransclem44  46518  etransclem45  46519  etransclem47  46521  rrxtopn0  46533  hoidmvlelem2  46836  vonicclem2  46924  fmtno4prmfac  47814  gpg5grlim  48335  gpg5grlic  48336