Theorem reurmo 3353

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

Syntax hints:   → wi 4  ∃wrex 3060  ∃!wreu 3348  ∃*wrmo 3349

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 2569  df-rex 3061  df-rmo 3350  df-reu 3351

This theorem is referenced by:  reuimrmo  3703  reuxfr1d  3708  2reurmo  3717  2rexreu  3720  2reu2  3848  enqeq  10845  eqsqrtd  15291  efgred2  19682  0frgp  19708  frgpnabllem2  19803  frgpcyg  21528  lmieu  28856  poimirlem25  37846  poimirlem26  37847  addinvcom  42687  tfsconcatlem  43578  reuxfr1dd  49052  upeu  49416