Theorem eleqtri 2537

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

Syntax hints:   = wceq 1454   e. wcel 1897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-cleq 2454  df-clel 2457

This theorem is referenced by:  eleqtrri  2538  3eltr3i  2551  prid2  4093  2eluzge0  11231  seqp1i  12260  faclbnd4lem1  12509  cats1fv  12991  bpoly2  14158  bpoly3  14159  bpoly4  14160  ef0lem  14181  phi1  14769  gsumws1  16671  lt6abl  17577  uvcvvcl  19393  smadiadetlem4  19742  indiscld  20155  cnrehmeo  22029  ovolicc1  22517  dvcjbr  22951  vieta1lem2  23312  dvloglem  23641  logdmopn  23642  efopnlem2  23650  cxpcn  23733  loglesqrt  23746  log2ublem2  23921  efrlim  23943  tgcgr4  24624  axlowdimlem16  25035  axlowdimlem17  25036  usgraexmplvtxlem  25170  konigsberg  25763  nlelchi  27762  hmopidmchi  27852  raddcn  28783  xrge0tmd  28800  indf  28885  ballotlem1ri  29415  ballotlem1riOLD  29453  dvtanlem  32034  dvtanlemOLD  32035  ftc1cnnc  32060  dvasin  32072  dvacos  32073  dvreasin  32074  dvreacos  32075  areacirclem2  32077  areacirclem4  32079  cncfres  32141  jm2.23  35895  fvnonrel  36247  frege54cor1c  36555  fourierdlem28  38034  fourierdlem57  38064  fourierdlem59  38066  fourierdlem62  38069  fourierdlem68  38075  fouriersw  38132  etransclem23  38159  etransclem35  38171  etransclem38  38174  etransclem39  38175  etransclem44  38180  etransclem45  38181  etransclem47  38183  rrxtopn0  38199  hoidmvlelem2  38455