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

Theorem reurmo 3342
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 3340 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 491 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3088  ∃!wreu 3089  ∃*wrmo 3090
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 199  df-an 386  df-eu 2607  df-rex 3093  df-reu 3094  df-rmo 3095
This theorem is referenced by:  reuxfrd  5089  enqeq  10042  eqsqrtd  14445  efgred2  18478  0frgp  18504  frgpnabllem2  18589  frgpcyg  20240  lmieu  26025  reuxfr4d  29845  poimirlem25  33915  poimirlem26  33916  reuimrmo  41943  2reurmo  41947  2rexreu  41950  2reu2  41952
  Copyright terms: Public domain W3C validator