Theorem reurmo 3381

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

Syntax hints:   → wi 4  ∃wrex 3068  ∃!wreu 3376  ∃*wrmo 3377

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 2567  df-rex 3069  df-rmo 3378  df-reu 3379

This theorem is referenced by:  reuimrmo  3754  reuxfr1d  3759  2reurmo  3768  2rexreu  3771  2reu2  3907  enqeq  10972  eqsqrtd  15403  efgred2  19786  0frgp  19812  frgpnabllem2  19907  frgpcyg  21610  lmieu  28807  poimirlem25  37632  poimirlem26  37633  addinvcom  42438  tfsconcatlem  43326  reuxfr1dd  48655  upeu  48817