Metamath Proof Explorer

Theorem reuv

Description: A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010)

Ref Expression
Assertion reuv 
|- ( E! x e. _V ph <-> E! x ph )

Proof

Step Hyp Ref Expression
1 df-reu 
 |-  ( E! x e. _V ph <-> E! x ( x e. _V /\ ph ) )
2 vex 
 |-  x e. _V
3 2 biantrur 
 |-  ( ph <-> ( x e. _V /\ ph ) )
4 3 eubii 
 |-  ( E! x ph <-> E! x ( x e. _V /\ ph ) )
5 1 4 bitr4i 
 |-  ( E! x e. _V ph <-> E! x ph )