Theorem reurmo 3355

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

Syntax hints:   → wi 4  ∃wrex 3062  ∃!wreu 3350  ∃*wrmo 3351

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 3352  df-reu 3353

This theorem is referenced by:  reuimrmo  3705  reuxfr1d  3710  2reurmo  3719  2rexreu  3722  2reu2  3850  enqeq  10857  eqsqrtd  15303  efgred2  19694  0frgp  19720  frgpnabllem2  19815  frgpcyg  21540  lmieu  28868  poimirlem25  37896  poimirlem26  37897  addinvcom  42802  tfsconcatlem  43693  reuxfr1dd  49166  upeu  49530