Theorem reurmo 3383

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

Syntax hints:   → wi 4  ∃wrex 3070  ∃!wreu 3378  ∃*wrmo 3379

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 2569  df-rex 3071  df-rmo 3380  df-reu 3381

This theorem is referenced by:  reuimrmo  3751  reuxfr1d  3756  2reurmo  3765  2rexreu  3768  2reu2  3898  enqeq  10974  eqsqrtd  15406  efgred2  19771  0frgp  19797  frgpnabllem2  19892  frgpcyg  21592  lmieu  28792  poimirlem25  37652  poimirlem26  37653  addinvcom  42461  tfsconcatlem  43349  reuxfr1dd  48726  upeu  48928