Theorem reurmo 3349

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

Syntax hints:   → wi 4  ∃wrex 3056  ∃!wreu 3344  ∃*wrmo 3345

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 2564  df-rex 3057  df-rmo 3346  df-reu 3347

This theorem is referenced by:  reuimrmo  3699  reuxfr1d  3704  2reurmo  3713  2rexreu  3716  2reu2  3844  enqeq  10820  eqsqrtd  15270  efgred2  19660  0frgp  19686  frgpnabllem2  19781  frgpcyg  21505  lmieu  28757  poimirlem25  37685  poimirlem26  37686  addinvcom  42465  tfsconcatlem  43369  reuxfr1dd  48838  upeu  49203