Theorem reurmo 3372

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

Syntax hints:   → wi 4  ∃wrex 3089  ∃!wreu 3367  ∃*wrmo 3368

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 2597  df-rex 3090  df-rmo 3369  df-reu 3370

This theorem is referenced by:  reuimrmo  3708  reuxfr1d  3713  2reurmo  3722  2rexreu  3725  2reu2  3852  enqeq  10914  eqsqrtd  15415  efgred2  19818  0frgp  19844  frgpnabllem2  19939  frgpcyg  21723  lmieu  29093  poimirlem25  38296  poimirlem26  38297  addinvcom  43193  tfsconcatlem  44063  reuxfr1dd  49585  upeu  49949