Theorem eleqtri 2686

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtr.1	⊢ 𝐴 ∈ 𝐵
eleqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtr.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eleq2i 2680	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)
4	1, 3	mpbi 219	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  eleqtrri  2687  3eltr3i  2700  prid2  4242  2eluzge0  11609  fz0to4untppr  12311  seqp1i  12679  faclbnd4lem1  12942  cats1fv  13455  bpoly2  14627  bpoly3  14628  bpoly4  14629  ef0lem  14648  phi1  15316  gsumws1  17199  lt6abl  18119  uvcvvcl  19945  smadiadetlem4  20294  indiscld  20705  cnrehmeo  22560  ovolicc1  23091  dvcjbr  23518  vieta1lem2  23870  dvloglem  24194  logdmopn  24195  efopnlem2  24203  cxpcn  24286  loglesqrt  24299  log2ublem2  24474  efrlim  24496  tgcgr4  25226  axlowdimlem16  25637  axlowdimlem17  25638  konigsberg  26514  nlelchi  28304  hmopidmchi  28394  raddcn  29303  xrge0tmd  29320  indf  29405  ballotlem1ri  29923  dvtanlem  32629  ftc1cnnc  32654  dvasin  32666  dvacos  32667  dvreasin  32668  dvreacos  32669  areacirclem2  32671  areacirclem4  32673  cncfres  32734  jm2.23  36581  fvnonrel  36922  frege54cor1c  37229  fourierdlem28  39028  fourierdlem57  39056  fourierdlem59  39058  fourierdlem62  39061  fourierdlem68  39067  fouriersw  39124  etransclem23  39150  etransclem35  39162  etransclem38  39165  etransclem39  39166  etransclem44  39171  etransclem45  39172  etransclem47  39174  rrxtopn0  39189  hoidmvlelem2  39486  vonicclem2  39575  fmtno4prmfac  40022