Theorem eleqtri 2553

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 2545	. 2 |- ( A e. B <-> A e. C )
4	1, 3	mpbi 208	1 |- A e. C

Syntax hints:   = wceq 1379   e. wcel 1767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462

This theorem is referenced by:  eleqtrri  2554  3eltr3i  2567  prid2  4136  seqp1i  12087  faclbnd4lem1  12335  bcn1  12355  bcpasc  12363  cats1fv  12783  ef0lem  13672  phi1  14158  dfphi2  14159  gsumws1  15830  efgsp1  16551  efgsres  16552  efgredlemd  16558  efgredlem  16561  lt6abl  16688  uvcvvcl  18585  smadiadetlem4  18938  indiscld  19358  cnrehmeo  21188  ovolicc1  21662  iblcnlem1  21929  dvcjbr  22087  c1lip2  22134  dvply1  22414  vieta1lem2  22441  dvtaylp  22499  taylthlem2  22503  dvloglem  22757  logdmopn  22758  efopnlem2  22766  logtayl  22769  cxpcn  22847  loglesqrt  22860  leibpilem2  23000  log2ublem2  23006  efrlim  23027  basellem5  23086  ppiltx  23179  prmorcht  23180  chtlepsi  23209  chpub  23223  chebbnd1lem1  23382  chtppilimlem1  23386  axlowdimlem16  23936  axlowdimlem17  23937  axlowdim  23940  usgraexvlem  24071  konigsberg  24663  nlelchi  26656  hmopidmchi  26746  raddcn  27547  xrge0tmd  27564  indf  27669  ballotlemfrci  28106  ballotlemfrceq  28107  ballotlem1ri  28113  signsvfn  28179  bpoly2  29396  bpoly3  29397  bpoly4  29398  dvtanlem  29641  ftc1cnnc  29666  dvasin  29680  dvacos  29681  dvreasin  29682  dvreacos  29683  areacirclem2  29685  areacirclem4  29687  cncfres  29864  jm2.23  30542  dvasinbx  31250  dvcosax  31256  fourierdlem28  31435  fourierdlem57  31464  fourierdlem59  31466  fourierdlem62  31469  fourierdlem68  31475  fourierdlem103  31510  fourierdlem104  31511  fouriersw  31532