Theorem eleqtri 2538

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

Hypotheses

Ref	Expression
eleqtr.1	|- A e. B
eleqtr.2	|- B = C

Assertion

Ref	Expression
eleqtri	|- A e. C

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtr.1	. 2 |- A e. B
2		eleqtr.2	. . 3 |- B = C
3	2	eleq2i 2530	. 2 |- ( A e. B <-> A e. C )
4	1, 3	mpbi 208	1 |- A e. C

Syntax hints:   = wceq 1370   e. wcel 1758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2444  df-clel 2447

This theorem is referenced by:  eleqtrri  2539  3eltr3i  2552  prid2  4087  seqp1i  11934  faclbnd4lem1  12181  bcn1  12201  bcpasc  12209  cats1fv  12599  ef0lem  13477  phi1  13961  dfphi2  13962  gsumws1  15631  efgsp1  16350  efgsres  16351  efgredlemd  16357  efgredlem  16360  lt6abl  16487  uvcvvcl  18332  smadiadetlem4  18602  indiscld  18822  cnrehmeo  20652  ovolicc1  21126  iblcnlem1  21393  dvcjbr  21551  c1lip2  21598  dvply1  21878  vieta1lem2  21905  dvtaylp  21963  taylthlem2  21967  dvloglem  22221  logdmopn  22222  efopnlem2  22230  logtayl  22233  cxpcn  22311  loglesqr  22324  leibpilem2  22464  log2ublem2  22470  efrlim  22491  basellem5  22550  ppiltx  22643  prmorcht  22644  chtlepsi  22673  chpub  22687  chebbnd1lem1  22846  chtppilimlem1  22850  axlowdimlem16  23350  axlowdimlem17  23351  axlowdim  23354  usgraexvlem  23460  konigsberg  23755  nlelchi  25612  hmopidmchi  25702  raddcn  26499  xrge0tmd  26516  indf  26612  ballotlemfrci  27049  ballotlemfrceq  27050  ballotlem1ri  27056  signsvfn  27122  bpoly2  28339  bpoly3  28340  bpoly4  28341  dvtanlem  28584  ftc1cnnc  28609  dvasin  28623  dvacos  28624  dvreasin  28625  dvreacos  28626  areacirclem2  28628  areacirclem4  28630  cncfres  28807  jm2.23  29488