Theorem reurmo 3362

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

Syntax hints:   → wi 4  ∃wrex 3066  ∃!wreu 3067  ∃*wrmo 3068

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 206  df-an 396  df-eu 2570  df-rex 3071  df-reu 3072  df-rmo 3073

This theorem is referenced by:  reuimrmo  3683  reuxfr1d  3688  2reurmo  3697  2rexreu  3700  2reu2  3835  enqeq  10674  eqsqrtd  15060  efgred2  19340  0frgp  19366  frgpnabllem2  19456  frgpcyg  20762  lmieu  27126  poimirlem25  35781  poimirlem26  35782  addinvcom  40393