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	⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
2		vex	⊢ 𝑥 ∈ V
3	2	biantrur	⊢ ( 𝜑 ↔ ( 𝑥 ∈ V ∧ 𝜑 ) )
4	3	abbii	⊢ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ V ∧ 𝜑 ) }
5	1 4	eqtr4i	⊢ { 𝑥 ∈ V ∣ 𝜑 } = { 𝑥 ∣ 𝜑 }