Theorem reurmo 3357

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

Syntax hints:   → wi 4  ∃wrex 3053  ∃!wreu 3352  ∃*wrmo 3353

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 3354  df-reu 3355

This theorem is referenced by:  reuimrmo  3716  reuxfr1d  3721  2reurmo  3730  2rexreu  3733  2reu2  3861  enqeq  10887  eqsqrtd  15334  efgred2  19683  0frgp  19709  frgpnabllem2  19804  frgpcyg  21483  lmieu  28711  poimirlem25  37639  poimirlem26  37640  addinvcom  42420  tfsconcatlem  43325  reuxfr1dd  48795  upeu  49160