Theorem eleqtri 2505

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

Syntax hints:   = wceq 1362   e. wcel 1755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429

This theorem is referenced by:  eleqtrri  2506  3eltr3i  2511  prid2  3972  seqp1i  11805  faclbnd4lem1  12052  bcn1  12072  bcpasc  12080  cats1fv  12469  ef0lem  13346  phi1  13830  dfphi2  13831  gsumws1  15496  efgsp1  16213  efgsres  16214  efgredlemd  16220  efgredlem  16223  lt6abl  16350  uvcvvcl  18053  smadiadetlem4  18316  indiscld  18536  cnrehmeo  20366  ovolicc1  20840  iblcnlem1  21106  dvcjbr  21264  c1lip2  21311  dvply1  21634  vieta1lem2  21661  dvtaylp  21719  taylthlem2  21723  dvloglem  21977  logdmopn  21978  efopnlem2  21986  logtayl  21989  cxpcn  22067  loglesqr  22080  leibpilem2  22220  log2ublem2  22226  efrlim  22247  basellem5  22306  ppiltx  22399  prmorcht  22400  chtlepsi  22429  chpub  22443  chebbnd1lem1  22602  chtppilimlem1  22606  axlowdimlem16  23025  axlowdimlem17  23026  axlowdim  23029  usgraexvlem  23135  konigsberg  23430  nlelchi  25287  hmopidmchi  25377  raddcn  26212  xrge0tmd  26229  indf  26325  ballotlemfrci  26757  ballotlemfrceq  26758  ballotlem1ri  26764  signsvfn  26830  bpoly2  28046  bpoly3  28047  bpoly4  28048  dvtanlem  28282  ftc1cnnc  28307  dvasin  28321  dvacos  28322  dvreasin  28323  dvreacos  28324  areacirclem2  28326  areacirclem4  28328  cncfres  28505  jm2.23  29187