Metamath Proof Explorer

Theorem ralv

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

Ref Expression
Assertion ralv 
|- ( A. x e. _V ph <-> A. x ph )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. _V ph <-> A. x ( x e. _V -> ph ) )
2 vex 
 |-  x e. _V
3 2 a1bi 
 |-  ( ph <-> ( x e. _V -> ph ) )
4 3 albii 
 |-  ( A. x ph <-> A. x ( x e. _V -> ph ) )
5 1 4 bitr4i 
 |-  ( A. x e. _V ph <-> A. x ph )