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

Theorem reurmo 3380
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 3379 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 498 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3071  ∃!wreu 3375  ∃*wrmo 3376
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 206  df-an 398  df-eu 2564  df-rex 3072  df-rmo 3377  df-reu 3378
This theorem is referenced by:  reuimrmo  3739  reuxfr1d  3744  2reurmo  3753  2rexreu  3756  2reu2  3890  enqeq  10924  eqsqrtd  15309  efgred2  19613  0frgp  19639  frgpnabllem2  19733  frgpcyg  21112  lmieu  28014  poimirlem25  36450  poimirlem26  36451  addinvcom  41247  tfsconcatlem  42018
  Copyright terms: Public domain W3C validator