Metamath Proof Explorer

Theorem eumoi

Description: Uniqueness inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995)

Ref Expression
Hypothesis eumoi.1 
|- E! x ph
Assertion eumoi 
|- E* x ph

Proof

Step Hyp Ref Expression
1 eumoi.1 
 |-  E! x ph
2 eumo 
 |-  ( E! x ph -> E* x ph )
3 1 2 ax-mp 
 |-  E* x ph