Theorem reurmo 3380

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

Syntax hints:   → wi 4  ∃wrex 3071  ∃!wreu 3375  ∃*wrmo 3376

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 398  df-eu 2564  df-rex 3072  df-rmo 3377  df-reu 3378

This theorem is referenced by:  reuimrmo  3739  reuxfr1d  3744  2reurmo  3753  2rexreu  3756  2reu2  3890  enqeq  10924  eqsqrtd  15309  efgred2  19613  0frgp  19639  frgpnabllem2  19733  frgpcyg  21112  lmieu  28014  poimirlem25  36450  poimirlem26  36451  addinvcom  41247  tfsconcatlem  42018