Metamath Proof Explorer

Theorem rexv

Description: An existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 26-Mar-2004)

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

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( 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 exbii 
 |-  ( E. x ph <-> E. x ( x e. _V /\ ph ) )
5 1 4 bitr4i 
 |-  ( E. x e. _V ph <-> E. x ph )