Theorem eleqtri 2540

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

Syntax hints:   = wceq 1398   e. wcel 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-cleq 2446  df-clel 2449

This theorem is referenced by:  eleqtrri  2541  3eltr3i  2554  prid2  4125  2eluzge0  11126  seqp1i  12108  faclbnd4lem1  12356  cats1fv  12818  ef0lem  13899  phi1  14390  gsumws1  16209  lt6abl  17099  uvcvvcl  18992  smadiadetlem4  19341  indiscld  19762  cnrehmeo  21622  ovolicc1  22096  dvcjbr  22521  vieta1lem2  22876  dvloglem  23200  logdmopn  23201  efopnlem2  23209  cxpcn  23290  loglesqrt  23303  log2ublem2  23478  efrlim  23500  axlowdimlem16  24465  axlowdimlem17  24466  usgraexvlem  24600  konigsberg  25192  nlelchi  27181  hmopidmchi  27271  raddcn  28149  xrge0tmd  28166  indf  28248  ballotlem1ri  28740  bpoly2  30050  bpoly3  30051  bpoly4  30052  dvtanlem  30307  ftc1cnnc  30332  dvasin  30346  dvacos  30347  dvreasin  30348  dvreacos  30349  areacirclem2  30351  areacirclem4  30353  cncfres  30504  jm2.23  31180  fourierdlem28  32159  fourierdlem57  32188  fourierdlem59  32190  fourierdlem62  32193  fourierdlem68  32199  fouriersw  32256  etransclem23  32282  etransclem35  32294  etransclem38  32297  etransclem39  32298  etransclem44  32303  etransclem45  32304  etransclem47  32306  frege54cor1c  38416