Metamath Proof Explorer

Theorem eumo

Description: Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995)

Ref Expression
Assertion eumo 
|- ( E! x ph -> E* x ph )

Proof

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