Theorem reurmo 3372

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3090  ∃!wreu 3367  ∃*wrmo 3368

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 2597  df-rex 3091  df-rmo 3369  df-reu 3370

This theorem is used by:  reuimrmo  3706  reuxfr1d  3711  2reurmo  3720  2rexreu  3723  2reu2  3850  enqeq  11058  eqsqrtd  15579  efgred2  20018  0frgp  20044  frgpnabllem2  20139  frgpcyg  21934  lmieu  29346  poimirlem25  38831  poimirlem26  38832  addinvcom  43749  tfsconcatlem  44599  reuxfr1dd  50248  upeu  50618