MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleqtri Unicode version

Theorem eleqtri 2368
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
StepHypRef Expression
1 eleqtr.1 . 2  |-  A  e.  B
2 eleqtr.2 . . 3  |-  B  =  C
32eleq2i 2360 . 2  |-  ( A  e.  B  <->  A  e.  C )
41, 3mpbi 199 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696
This theorem is referenced by:  eleqtrri  2369  3eltr3i  2374  prid2  3748  seqp1i  11078  faclbnd4lem1  11322  bcn1  11341  bcpasc  11349  cats1fv  11525  ef0lem  12376  phi1  12857  dfphi2  12858  gsumws1  14478  efgsp1  15062  efgsres  15063  efgredlemd  15069  efgredlem  15072  lt6abl  15197  indiscld  16844  cnrehmeo  18467  ovolicc1  18891  iblcnlem1  19158  dvcjbr  19314  c1lip2  19361  dvply1  19680  vieta1lem2  19707  dvtaylp  19765  taylthlem2  19769  dvloglem  20011  logdmopn  20012  efopnlem2  20020  logtayl  20023  cxpcn  20101  loglesqr  20114  leibpilem2  20253  log2ublem2  20259  efrlim  20280  basellem5  20338  ppiltx  20431  prmorcht  20432  chtlepsi  20461  chpub  20475  chebbnd1lem1  20634  chtppilimlem1  20638  nlelchi  22657  hmopidmchi  22747  ballotlemfrci  23102  ballotlemfrceq  23103  ballotlem1ri  23109  raddcn  23317  xrge0tmd  23343  indf  23614  konigsberg  23926  axlowdimlem16  24657  axlowdimlem17  24658  axlowdim  24661  bpoly2  24864  bpoly3  24865  bpoly4  24866  ftc1cnnc  25025  areacirclem4  25030  areacirclem5  25032  cncfres  26588  jm2.23  27192  uvcvvcl  27339  usgraexvlem  28261
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator