Theorem reurmo 3347

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

Syntax hints:   → wi 4  ∃wrex 3063  ∃!wreu 3342  ∃*wrmo 3343

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 208  df-an 397  df-eu 2573  df-rex 3064  df-rmo 3344  df-reu 3345

This theorem is referenced by:  reuimrmo  3686  reuxfr1d  3691  2reurmo  3700  2rexreu  3703  2reu2  3830  enqeq  10848  eqsqrtd  15321  efgred2  19719  0frgp  19745  frgpnabllem2  19840  frgpcyg  21548  lmieu  28870  poimirlem25  38012  poimirlem26  38013  addinvcom  42909  tfsconcatlem  43781  reuxfr1dd  49297  upeu  49661