Metamath Proof Explorer

Theorem euimmo

Description: Existential uniqueness implies uniqueness through reverse implication. (Contributed by NM, 22-Apr-1995)

Ref Expression
Assertion euimmo 
|- ( A. x ( ph -> ps ) -> ( E! x ps -> E* x ph ) )

Proof

Step Hyp Ref Expression
1 eumo 
 |-  ( E! x ps -> E* x ps )
2 moim 
 |-  ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )
3 1 2 syl5 
 |-  ( A. x ( ph -> ps ) -> ( E! x ps -> E* x ph ) )