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

Theorem reurmo 2923
Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
Assertion
Ref Expression
reurmo  |-  ( E! x  e.  A  ph  ->  E* x  e.  A ph )

Proof of Theorem reurmo
StepHypRef Expression
1 reu5 2921 . 2  |-  ( E! x  e.  A  ph  <->  ( E. x  e.  A  ph 
/\  E* x  e.  A ph ) )
21simprbi 451 1  |-  ( E! x  e.  A  ph  ->  E* x  e.  A ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wrex 2706   E!wreu 2707   E*wrmo 2708
This theorem is referenced by:  reuxfrd  4748  enqeq  8811  eqsqrd  12171  efgred2  15385  0frgp  15411  frgpnabllem2  15485  frgpcyg  16854  qtophmeo  17849  reuxfr4d  23977  reuimrmo  27932  2reurmo  27936  2rexreu  27939  2reu2  27941
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-rex 2711  df-reu 2712  df-rmo 2713
  Copyright terms: Public domain W3C validator