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

Theorem reurmo 3378
 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 3375 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 500 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wrex 3107  ∃!wreu 3108  ∃*wrmo 3109 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 210  df-an 400  df-eu 2629  df-rex 3112  df-reu 3113  df-rmo 3114 This theorem is referenced by:  reuimrmo  3684  reuxfr1d  3689  2reurmo  3699  2rexreu  3701  2reu2  3827  enqeq  10352  eqsqrtd  14726  efgred2  18879  0frgp  18905  frgpnabllem2  18995  frgpcyg  20274  lmieu  26592  poimirlem25  35122  poimirlem26  35123  addinvcom  39632
 Copyright terms: Public domain W3C validator