Theorem reurmo 3368

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3086  ∃!wreu 3363  ∃*wrmo 3364

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2594  df-rex 3087  df-rmo 3365  df-reu 3366

This theorem is used by:  reuimrmo  3702  reuxfr1d  3707  2reurmo  3716  2rexreu  3719  2reu2  3846  enqeq  11024  eqsqrtd  15542  efgred2  19974  0frgp  20000  frgpnabllem2  20095  frgpcyg  21886  lmieu  29296  poimirlem25  38670  poimirlem26  38671  addinvcom  43590  tfsconcatlem  44445  reuxfr1dd  50024  upeu  50394