Theorem dfrab3

Description: Alternate definition of restricted class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	dfrab3	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )

Proof

Step	Hyp	Ref	Expression
1		df-rab	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
2		inab	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∩ { 𝑥 ∣ 𝜑 } ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) }
3		abid2	⊢ { 𝑥 ∣ 𝑥 ∈ 𝐴 } = 𝐴
4	3	ineq1i	⊢ ( { 𝑥 ∣ 𝑥 ∈ 𝐴 } ∩ { 𝑥 ∣ 𝜑 } ) = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )
5	1 2 4	3eqtr2i	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )