Theorem eleqtri 2842

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

Syntax hints:   = wceq 1537   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleqtrri  2843  3eltr3i  2856  prid2  4788  2eluzge0  12958  faclbnd4lem1  14342  cats1fv  14908  bpoly2  16105  bpoly3  16106  bpoly4  16107  ef0lem  16126  phi1  16820  gsumws1  18873  lt6abl  19937  uvcvvcl  21830  mhpvarcl  22175  smadiadetlem4  22696  indiscld  23120  cnrehmeo  25003  cnrehmeoOLD  25004  ovolicc1  25570  dvcjbr  26007  vieta1lem2  26371  dvloglem  26708  logdmopn  26709  efopnlem2  26717  cxpcn  26805  cxpcnOLD  26806  loglesqrt  26822  log2ublem2  27008  efrlim  27030  efrlimOLD  27031  precsexlem11  28259  tgcgr4  28557  axlowdimlem16  28990  axlowdimlem17  28991  nlelchi  32093  hmopidmchi  32183  evl1deg2  33567  evl1deg3  33568  raddcn  33875  xrge0tmd  33891  indf  33979  ballotlem1ri  34499  chtvalz  34606  circlemethhgt  34620  dvtanlem  37629  ftc1cnnc  37652  dvasin  37664  dvacos  37665  dvreasin  37666  dvreacos  37667  areacirclem2  37669  areacirclem4  37671  cncfres  37725  jm2.23  42953  0finon  43410  1finon  43411  2finon  43412  3finon  43413  4finon  43414  fvnonrel  43559  frege54cor1c  43877  fourierdlem28  46056  fourierdlem57  46084  fourierdlem59  46086  fourierdlem62  46089  fourierdlem68  46095  fouriersw  46152  etransclem23  46178  etransclem35  46190  etransclem38  46193  etransclem39  46194  etransclem44  46199  etransclem45  46200  etransclem47  46202  rrxtopn0  46214  hoidmvlelem2  46517  vonicclem2  46605  fmtno4prmfac  47446