Theorem reurmo 3359

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

Syntax hints:   → wi 4  ∃wrex 3054  ∃!wreu 3354  ∃*wrmo 3355

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 2563  df-rex 3055  df-rmo 3356  df-reu 3357

This theorem is referenced by:  reuimrmo  3719  reuxfr1d  3724  2reurmo  3733  2rexreu  3736  2reu2  3864  enqeq  10894  eqsqrtd  15341  efgred2  19690  0frgp  19716  frgpnabllem2  19811  frgpcyg  21490  lmieu  28718  poimirlem25  37646  poimirlem26  37647  addinvcom  42427  tfsconcatlem  43332  reuxfr1dd  48799  upeu  49164