Theorem reurmo 3379

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

Syntax hints:   → wi 4  ∃wrex 3095  ∃!wreu 3374  ∃*wrmo 3375

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 210  df-an 401  df-eu 2603  df-rex 3096  df-rmo 3376  df-reu 3377

This theorem is referenced by:  reuimrmo  3717  reuxfr1d  3722  2reurmo  3731  2rexreu  3734  2reu2  3860  enqeq  10915  eqsqrtd  15415  efgred2  19819  0frgp  19845  frgpnabllem2  19940  frgpcyg  21688  lmieu  29047  poimirlem25  38179  poimirlem26  38180  addinvcom  43078  tfsconcatlem  43950  reuxfr1dd  49465  upeu  49829