Theorem rabdif

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

	Ref	Expression
Assertion	rabdif	$$⊢\left\{x\in A|\phi \right\}\setminus B=\left\{x\in \left(A\setminus B\right)|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		indif2	$$⊢\left\{x|\phi \right\}\cap \left(A\setminus B\right)=\left(\left\{x|\phi \right\}\cap A\right)\setminus B$$
2		dfrab2	$$⊢\left\{x\in \left(A\setminus B\right)|\phi \right\}=\left\{x|\phi \right\}\cap \left(A\setminus B\right)$$
3		dfrab2	$$⊢\left\{x\in A|\phi \right\}=\left\{x|\phi \right\}\cap A$$
4	3	difeq1i	$$⊢\left\{x\in A|\phi \right\}\setminus B=\left(\left\{x|\phi \right\}\cap A\right)\setminus B$$
5	1 2 4	3eqtr4ri	$$⊢\left\{x\in A|\phi \right\}\setminus B=\left\{x\in \left(A\setminus B\right)|\phi \right\}$$