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 503	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)

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

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 2595  df-rex 3088  df-rmo 3366  df-reu 3367

This theorem is used by:  reuimrmo  3703  reuxfr1d  3708  2reurmo  3717  2rexreu  3720  2reu2  3846  enqeq  11012  eqsqrtd  15528  efgred2  19960  0frgp  19986  frgpnabllem2  20081  frgpcyg  21872  lmieu  29282  poimirlem25  38543  poimirlem26  38544  addinvcom  43463  tfsconcatlem  44322  reuxfr1dd  49886  upeu  50248