Theorem reurmo 3391

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

Syntax hints:   → wi 4  ∃wrex 3076  ∃!wreu 3386  ∃*wrmo 3387

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 2572  df-rex 3077  df-rmo 3388  df-reu 3389

This theorem is referenced by:  reuimrmo  3767  reuxfr1d  3772  2reurmo  3781  2rexreu  3784  2reu2  3920  enqeq  11003  eqsqrtd  15416  efgred2  19795  0frgp  19821  frgpnabllem2  19916  frgpcyg  21615  lmieu  28810  poimirlem25  37605  poimirlem26  37606  addinvcom  42407  tfsconcatlem  43298