Theorem dfrab2

Description: Alternate definition of restricted class abstraction. (Contributed by NM, 20-Sep-2003) (Proof shortened by BJ, 22-Apr-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dfrab3	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } )
2		incom	⊢ ( 𝐴 ∩ { 𝑥 ∣ 𝜑 } ) = ( { 𝑥 ∣ 𝜑 } ∩ 𝐴 )
3	1 2	eqtri	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( { 𝑥 ∣ 𝜑 } ∩ 𝐴 )