Metamath Proof Explorer

Theorem reurmo

Description: Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017)

Ref Expression
Assertion reurmo 
|- ( E! x e. A ph -> E* x e. A ph )

Proof

Step Hyp Ref Expression
1 reu5 
 |-  ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
2 1 simprbi 
 |-  ( E! x e. A ph -> E* x e. A ph )