Theorem reurmo 3346

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

Syntax hints:   → wi 4  ∃wrex 3062  ∃!wreu 3341  ∃*wrmo 3342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-eu 2570  df-rex 3063  df-rmo 3343  df-reu 3344

This theorem is referenced by:  reuimrmo  3692  reuxfr1d  3697  2reurmo  3706  2rexreu  3709  2reu2  3837  enqeq  10848  eqsqrtd  15321  efgred2  19719  0frgp  19745  frgpnabllem2  19840  frgpcyg  21563  lmieu  28866  poimirlem25  37980  poimirlem26  37981  addinvcom  42878  tfsconcatlem  43782  reuxfr1dd  49294  upeu  49658