Theorem reurmo 3354

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

Syntax hints:   → wi 4  ∃wrex 3053  ∃!wreu 3349  ∃*wrmo 3350

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

This theorem is referenced by:  reuimrmo  3713  reuxfr1d  3718  2reurmo  3727  2rexreu  3730  2reu2  3858  enqeq  10863  eqsqrtd  15310  efgred2  19659  0frgp  19685  frgpnabllem2  19780  frgpcyg  21459  lmieu  28687  poimirlem25  37612  poimirlem26  37613  addinvcom  42393  tfsconcatlem  43298  reuxfr1dd  48768  upeu  49133