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

Theorem reurmo 3383
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 3382 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simprbi 496 1 (∃!𝑥𝐴 𝜑 → ∃*𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3070  ∃!wreu 3378  ∃*wrmo 3379
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 207  df-an 396  df-eu 2569  df-rex 3071  df-rmo 3380  df-reu 3381
This theorem is referenced by:  reuimrmo  3751  reuxfr1d  3756  2reurmo  3765  2rexreu  3768  2reu2  3898  enqeq  10974  eqsqrtd  15406  efgred2  19771  0frgp  19797  frgpnabllem2  19892  frgpcyg  21592  lmieu  28792  poimirlem25  37652  poimirlem26  37653  addinvcom  42461  tfsconcatlem  43349  reuxfr1dd  48726  upeu  48928
  Copyright terms: Public domain W3C validator