Theorem reurmo 3374

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3091  ∃!wreu 3369  ∃*wrmo 3370

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 2599  df-rex 3092  df-rmo 3371  df-reu 3372

This theorem is used by:  reuimrmo  3710  reuxfr1d  3715  2reurmo  3724  2rexreu  3727  2reu2  3853  enqeq  10934  eqsqrtd  15443  efgred2  19867  0frgp  19893  frgpnabllem2  19988  frgpcyg  21773  lmieu  29144  poimirlem25  38353  poimirlem26  38354  addinvcom  43251  tfsconcatlem  44121  reuxfr1dd  49642  upeu  50006