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  3742  reuxfr1d  3747  2reurmo  3756  2rexreu  3759  2reu2  3893  enqeq  10929  eqsqrtd  15314  efgred2  19621  0frgp  19647  frgpnabllem2  19742  frgpcyg  21129  lmieu  28035  poimirlem25  36513  poimirlem26  36514  addinvcom  41304  tfsconcatlem  42086
  Copyright terms: Public domain W3C validator