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

Syntax hints:   → wi 4  ∃wrex 3060  ∃!wreu 3357  ∃*wrmo 3358

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 2568  df-rex 3061  df-rmo 3359  df-reu 3360

This theorem is referenced by:  reuimrmo  3728  reuxfr1d  3733  2reurmo  3742  2rexreu  3745  2reu2  3873  enqeq  10948  eqsqrtd  15386  efgred2  19734  0frgp  19760  frgpnabllem2  19855  frgpcyg  21534  lmieu  28763  poimirlem25  37669  poimirlem26  37670  addinvcom  42474  tfsconcatlem  43360  reuxfr1dd  48785  upeu  49106