Theorem reurmo 3380

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

Syntax hints:   → wi 4  ∃wrex 3071  ∃!wreu 3375  ∃*wrmo 3376

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 398  df-eu 2564  df-rex 3072  df-rmo 3377  df-reu 3378

This theorem is referenced by:  reuimrmo  3742  reuxfr1d  3747  2reurmo  3756  2rexreu  3759  2reu2  3893  enqeq  10929  eqsqrtd  15314  efgred2  19621  0frgp  19647  frgpnabllem2  19742  frgpcyg  21129  lmieu  28066  poimirlem25  36561  poimirlem26  36562  addinvcom  41352  tfsconcatlem  42134