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

Theorem reurmo 3340
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 3337 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 500 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3062  ∃!wreu 3063  ∃*wrmo 3064
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 2568  df-rex 3067  df-reu 3068  df-rmo 3069
This theorem is referenced by:  reuimrmo  3658  reuxfr1d  3663  2reurmo  3672  2rexreu  3675  2reu2  3810  enqeq  10548  eqsqrtd  14931  efgred2  19143  0frgp  19169  frgpnabllem2  19259  frgpcyg  20538  lmieu  26875  poimirlem25  35539  poimirlem26  35540  addinvcom  40121
  Copyright terms: Public domain W3C validator