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 496	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃*𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3053  ∃!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 2562  df-rex 3054  df-rmo 3343  df-reu 3344

This theorem is referenced by:  reuimrmo  3705  reuxfr1d  3710  2reurmo  3719  2rexreu  3722  2reu2  3850  enqeq  10828  eqsqrtd  15275  efgred2  19632  0frgp  19658  frgpnabllem2  19753  frgpcyg  21480  lmieu  28729  poimirlem25  37625  poimirlem26  37626  addinvcom  42405  tfsconcatlem  43309  reuxfr1dd  48791  upeu  49156