Theorem eleqtri 2832

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

Syntax hints:   = wceq 1542   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811

This theorem is referenced by:  eleqtrri  2833  3eltr3i  2846  prid2  4768  2eluzge0  12877  fz0to4untppr  13604  faclbnd4lem1  14253  cats1fv  14810  bpoly2  16001  bpoly3  16002  bpoly4  16003  ef0lem  16022  phi1  16706  gsumws1  18719  lt6abl  19763  uvcvvcl  21342  mhpvarcl  21691  smadiadetlem4  22171  indiscld  22595  cnrehmeo  24469  ovolicc1  25033  dvcjbr  25466  vieta1lem2  25824  dvloglem  26156  logdmopn  26157  efopnlem2  26165  cxpcn  26253  loglesqrt  26266  log2ublem2  26452  efrlim  26474  precsexlem11  27663  tgcgr4  27782  axlowdimlem16  28215  axlowdimlem17  28216  nlelchi  31314  hmopidmchi  31404  raddcn  32909  xrge0tmd  32925  indf  33013  ballotlem1ri  33533  chtvalz  33641  circlemethhgt  33655  gg-cnrehmeo  35171  gg-cxpcn  35184  dvtanlem  36537  ftc1cnnc  36560  dvasin  36572  dvacos  36573  dvreasin  36574  dvreacos  36575  areacirclem2  36577  areacirclem4  36579  cncfres  36633  jm2.23  41735  0finon  42199  1finon  42200  2finon  42201  3finon  42202  4finon  42203  fvnonrel  42348  frege54cor1c  42666  fourierdlem28  44851  fourierdlem57  44879  fourierdlem59  44881  fourierdlem62  44884  fourierdlem68  44890  fouriersw  44947  etransclem23  44973  etransclem35  44985  etransclem38  44988  etransclem39  44989  etransclem44  44994  etransclem45  44995  etransclem47  44997  rrxtopn0  45009  hoidmvlelem2  45312  vonicclem2  45400  fmtno4prmfac  46240