Theorem reurmo 3350

Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.)

Assertion

Ref	Expression
reurmo	⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)

Proof of Theorem reurmo

Step	Hyp	Ref	Expression
1		reu5 3349	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2	1	simprbi 496	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3057  ∃!wreu 3345  ∃*wrmo 3346

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 2566  df-rex 3058  df-rmo 3347  df-reu 3348

This theorem is referenced by:  reuimrmo  3700  reuxfr1d  3705  2reurmo  3714  2rexreu  3717  2reu2  3845  enqeq  10836  eqsqrtd  15282  efgred2  19673  0frgp  19699  frgpnabllem2  19794  frgpcyg  21519  lmieu  28782  poimirlem25  37758  poimirlem26  37759  addinvcom  42602  tfsconcatlem  43493  reuxfr1dd  48968  upeu  49332