Theorem eleqtri 2476

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-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 2468	. 2 |- ( A e. B <-> A e. C )
4	1, 3	mpbi 200	1 |- A e. C

Syntax hints:   = wceq 1649   e. wcel 1721

This theorem is referenced by:  eleqtrri  2477  3eltr3i  2482  prid2  3873  seqp1i  11294  faclbnd4lem1  11539  bcn1  11559  bcpasc  11567  cats1fv  11778  ef0lem  12636  phi1  13117  dfphi2  13118  gsumws1  14740  efgsp1  15324  efgsres  15325  efgredlemd  15331  efgredlem  15334  lt6abl  15459  indiscld  17110  cnrehmeo  18931  ovolicc1  19365  iblcnlem1  19632  dvcjbr  19788  c1lip2  19835  dvply1  20154  vieta1lem2  20181  dvtaylp  20239  taylthlem2  20243  dvloglem  20492  logdmopn  20493  efopnlem2  20501  logtayl  20504  cxpcn  20582  loglesqr  20595  leibpilem2  20734  log2ublem2  20740  efrlim  20761  basellem5  20820  ppiltx  20913  prmorcht  20914  chtlepsi  20943  chpub  20957  chebbnd1lem1  21116  chtppilimlem1  21120  usgraexvlem  21367  konigsberg  21662  nlelchi  23517  hmopidmchi  23607  raddcn  24268  xrge0tmd  24285  indf  24366  ballotlemfrci  24738  ballotlemfrceq  24739  ballotlem1ri  24745  binomfallfaclem2  25307  axlowdimlem16  25800  axlowdimlem17  25801  axlowdim  25804  bpoly2  26007  bpoly3  26008  bpoly4  26009  ftc1cnnc  26178  areacirclem4  26183  areacirclem5  26185  cncfres  26364  jm2.23  26957  uvcvvcl  27104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400