Theorem reurmo 3354

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

Syntax hints:   → wi 4  ∃wrex 3069  ∃!wreu 3349  ∃*wrmo 3350

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 397  df-eu 2562  df-rex 3070  df-rmo 3351  df-reu 3352

This theorem is referenced by:  reuimrmo  3706  reuxfr1d  3711  2reurmo  3720  2rexreu  3723  2reu2  3857  enqeq  10879  eqsqrtd  15264  efgred2  19549  0frgp  19575  frgpnabllem2  19666  frgpcyg  21017  lmieu  27789  poimirlem25  36176  poimirlem26  36177  addinvcom  40958  tfsconcatlem  41729