Metamath Proof Explorer

Theorem euabex

Description: The abstraction of a wff with existential uniqueness exists. (Contributed by NM, 25-Nov-1994)

Ref Expression
Assertion euabex 
|- ( E! x ph -> { x | ph } e. _V )

Proof

Step Hyp Ref Expression
1 eumo 
 |-  ( E! x ph -> E* x ph )
2 moabex 
 |-  ( E* x ph -> { x | ph } e. _V )
3 1 2 syl 
 |-  ( E! x ph -> { x | ph } e. _V )