Theorem rabdif

Description: Move difference in and out of a restricted class abstraction. (Contributed by Steven Nguyen, 6-Jun-2023)

	Ref	Expression
Assertion	rabdif	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ 𝐵 ) = { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		indif2	⊢ ( { 𝑥 ∣ 𝜑 } ∩ ( 𝐴 ∖ 𝐵 ) ) = ( ( { 𝑥 ∣ 𝜑 } ∩ 𝐴 ) ∖ 𝐵 )
2		dfrab2	⊢ { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 } = ( { 𝑥 ∣ 𝜑 } ∩ ( 𝐴 ∖ 𝐵 ) )
3		dfrab2	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = ( { 𝑥 ∣ 𝜑 } ∩ 𝐴 )
4	3	difeq1i	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ 𝐵 ) = ( ( { 𝑥 ∣ 𝜑 } ∩ 𝐴 ) ∖ 𝐵 )
5	1 2 4	3eqtr4ri	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∖ 𝐵 ) = { 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ∣ 𝜑 }