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

Theorem reurmo 3300
 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 3298 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 483 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wrex 3051  ∃!wreu 3052  ∃*wrmo 3053 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-eu 2611  df-mo 2612  df-rex 3056  df-reu 3057  df-rmo 3058 This theorem is referenced by:  reuxfrd  5042  enqeq  9948  eqsqrtd  14306  efgred2  18366  0frgp  18392  frgpnabllem2  18477  frgpcyg  20124  lmieu  25875  reuxfr4d  29638  poimirlem25  33747  poimirlem26  33748  reuimrmo  41684  2reurmo  41688  2rexreu  41691  2reu2  41693
 Copyright terms: Public domain W3C validator