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	|- { x e. _V | ph } = { x | ph }

Proof

Step	Hyp	Ref	Expression
1		df-rab	|- { x e. _V | ph } = { x | ( x e. _V /\ ph ) }
2		vex	|- x e. _V
3	2	biantrur	|- ( ph <-> ( x e. _V /\ ph ) )
4	3	abbii	|- { x | ph } = { x | ( x e. _V /\ ph ) }
5	1 4	eqtr4i	|- { x e. _V | ph } = { x | ph }