Theorem reurmo 3369

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

Syntax hints:   → wi 4  ∃wrex 3085  ∃!wreu 3364  ∃*wrmo 3365

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 209  df-an 400  df-eu 2595  df-rex 3086  df-rmo 3366  df-reu 3367

This theorem is referenced by:  reuimrmo  3706  reuxfr1d  3711  2reurmo  3720  2rexreu  3723  2reu2  3849  enqeq  10886  eqsqrtd  15386  efgred2  19784  0frgp  19810  frgpnabllem2  19905  frgpcyg  21613  lmieu  28941  poimirlem25  38105  poimirlem26  38106  addinvcom  43002  tfsconcatlem  43874  reuxfr1dd  49389  upeu  49753