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

Theorem reurmo 3138
Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)
Assertion
Ref Expression
reurmo (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)

Proof of Theorem reurmo
StepHypRef Expression
1 reu5 3136 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 479 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 2897  ∃!wreu 2898  ∃*wrmo 2899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-eu 2462  df-mo 2463  df-rex 2902  df-reu 2903  df-rmo 2904
This theorem is referenced by:  reuxfrd  4819  enqeq  9635  eqsqrtd  13955  efgred2  17989  0frgp  18015  frgpnabllem2  18100  frgpcyg  19741  lmieu  25476  reuxfr4d  28714  poimirlem25  32604  poimirlem26  32605  reuimrmo  39827  2reurmo  39831  2rexreu  39834  2reu2  39836
  Copyright terms: Public domain W3C validator