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

Theorem eleqtri 2461
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 2453 . 2  |-  ( A  e.  B  <->  A  e.  C )
41, 3mpbi 200 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1717
This theorem is referenced by:  eleqtrri  2462  3eltr3i  2467  prid2  3858  seqp1i  11268  faclbnd4lem1  11513  bcn1  11533  bcpasc  11541  cats1fv  11752  ef0lem  12610  phi1  13091  dfphi2  13092  gsumws1  14714  efgsp1  15298  efgsres  15299  efgredlemd  15305  efgredlem  15308  lt6abl  15433  indiscld  17080  cnrehmeo  18851  ovolicc1  19281  iblcnlem1  19548  dvcjbr  19704  c1lip2  19751  dvply1  20070  vieta1lem2  20097  dvtaylp  20155  taylthlem2  20159  dvloglem  20408  logdmopn  20409  efopnlem2  20417  logtayl  20420  cxpcn  20498  loglesqr  20511  leibpilem2  20650  log2ublem2  20656  efrlim  20677  basellem5  20736  ppiltx  20829  prmorcht  20830  chtlepsi  20859  chpub  20873  chebbnd1lem1  21032  chtppilimlem1  21036  usgraexvlem  21282  konigsberg  21559  nlelchi  23414  hmopidmchi  23504  raddcn  24121  xrge0tmd  24138  indf  24211  ballotlemfrci  24566  ballotlemfrceq  24567  ballotlem1ri  24573  axlowdimlem16  25612  axlowdimlem17  25613  axlowdim  25616  bpoly2  25819  bpoly3  25820  bpoly4  25821  ftc1cnnc  25981  areacirclem4  25986  areacirclem5  25988  cncfres  26167  jm2.23  26760  uvcvvcl  26907
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 1661  ax-8 1682  ax-11 1753  ax-ext 2370
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2382  df-clel 2385
  Copyright terms: Public domain W3C validator