Metamath Proof Explorer

Theorem reurex

Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999)

Ref Expression
Assertion reurex 
|- ( E! x e. A ph -> E. x e. A ph )

Proof

Step Hyp Ref Expression
1 reu5 
 |-  ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) )
2 1 simplbi 
 |-  ( E! x e. A ph -> E. x e. A ph )