Theorem rabab

Description: A class abstraction restricted to the universe is unrestricted. (Contributed by NM, 27-Dec-2004) (Proof shortened by Andrew Salmon, 8-Jun-2011)

	Ref	Expression
Assertion	rabab	$$⊢\left\{x\in \mathrm{V}|\phi \right\}=\left\{x|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-rab	$$⊢\left\{x\in \mathrm{V}|\phi \right\}=\left\{x|\left(x\in \mathrm{V}\wedge \phi \right)\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	biantrur	$$⊢\phi \leftrightarrow \left(x\in \mathrm{V}\wedge \phi \right)$$
4	3	abbii	$$⊢\left\{x|\phi \right\}=\left\{x|\left(x\in \mathrm{V}\wedge \phi \right)\right\}$$
5	1 4	eqtr4i	$$⊢\left\{x\in \mathrm{V}|\phi \right\}=\left\{x|\phi \right\}$$