Theorem ralv

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

	Ref	Expression
Assertion	ralv	$$⊢\forall x\in \mathrm{V}\phi \leftrightarrow \forall x\phi$$

Proof

Step	Hyp	Ref	Expression
1		df-ral	$$⊢\forall x\in \mathrm{V}\phi \leftrightarrow \forall x\left(x\in \mathrm{V}\to \phi \right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	a1bi	$$⊢\phi \leftrightarrow \left(x\in \mathrm{V}\to \phi \right)$$
4	3	albii	$$⊢\forall x\phi \leftrightarrow \forall x\left(x\in \mathrm{V}\to \phi \right)$$
5	1 4	bitr4i	$$⊢\forall x\in \mathrm{V}\phi \leftrightarrow \forall x\phi$$