Theorem eleqtri 2839

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

Syntax hints:   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-clel 2816

This theorem is referenced by:  eleqtrri  2840  3eltr3i  2853  prid2  4763  2eluzge0  12935  faclbnd4lem1  14332  cats1fv  14898  bpoly2  16093  bpoly3  16094  bpoly4  16095  ef0lem  16114  phi1  16810  gsumws1  18851  lt6abl  19913  uvcvvcl  21807  mhpvarcl  22152  smadiadetlem4  22675  indiscld  23099  cnrehmeo  24984  cnrehmeoOLD  24985  ovolicc1  25551  dvcjbr  25987  vieta1lem2  26353  dvloglem  26690  logdmopn  26691  efopnlem2  26699  cxpcn  26787  cxpcnOLD  26788  loglesqrt  26804  log2ublem2  26990  efrlim  27012  efrlimOLD  27013  precsexlem11  28241  tgcgr4  28539  axlowdimlem16  28972  axlowdimlem17  28973  nlelchi  32080  hmopidmchi  32170  indf  32840  evl1deg2  33602  evl1deg3  33603  raddcn  33928  xrge0tmd  33944  ballotlem1ri  34537  chtvalz  34644  circlemethhgt  34658  dvtanlem  37676  ftc1cnnc  37699  dvasin  37711  dvacos  37712  dvreasin  37713  dvreacos  37714  areacirclem2  37716  areacirclem4  37718  cncfres  37772  resuppsinopn  42393  jm2.23  43008  0finon  43461  1finon  43462  2finon  43463  3finon  43464  4finon  43465  fvnonrel  43610  frege54cor1c  43928  fourierdlem28  46150  fourierdlem57  46178  fourierdlem59  46180  fourierdlem62  46183  fourierdlem68  46189  fouriersw  46246  etransclem23  46272  etransclem35  46284  etransclem38  46287  etransclem39  46288  etransclem44  46293  etransclem45  46294  etransclem47  46296  rrxtopn0  46308  hoidmvlelem2  46611  vonicclem2  46699  fmtno4prmfac  47559  gpg5grlic  48047