Theorem reurmo 3345

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 3344	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2	1	simprbi 497	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3061  ∃!wreu 3340  ∃*wrmo 3341

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 3062  df-rmo 3342  df-reu 3343

This theorem is referenced by:  reuimrmo  3691  reuxfr1d  3696  2reurmo  3705  2rexreu  3708  2reu2  3836  enqeq  10857  eqsqrtd  15330  efgred2  19728  0frgp  19754  frgpnabllem2  19849  frgpcyg  21553  lmieu  28852  poimirlem25  37966  poimirlem26  37967  addinvcom  42864  tfsconcatlem  43764  reuxfr1dd  49282  upeu  49646