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  3703  reuxfr1d  3708  2reurmo  3717  2rexreu  3720  2reu2  3846  enqeq  10943  eqsqrtd  15455  efgred2  19880  0frgp  19906  frgpnabllem2  20001  frgpcyg  21786  lmieu  29168  poimirlem25  38394  poimirlem26  38395  addinvcom  43307  tfsconcatlem  44177  reuxfr1dd  49735  upeu  50097