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 )