Theorem difeq2

Description: Equality theorem for class difference. (Contributed by NM, 10-Feb-1997) (Proof shortened by Andrew Salmon, 26-Jun-2011)

	Ref	Expression
Assertion	difeq2	$$⊢A=B\to C\setminus A=C\setminus B$$

Proof

Step	Hyp	Ref	Expression
1		eleq2	$$⊢A=B\to \left(x\in A\leftrightarrow x\in B\right)$$
2	1	notbid	$$⊢A=B\to \left(\neg x\in A\leftrightarrow \neg x\in B\right)$$
3	2	rabbidv	$$⊢A=B\to \left\{x\in C|\neg x\in A\right\}=\left\{x\in C|\neg x\in B\right\}$$
4		dfdif2	$$⊢C\setminus A=\left\{x\in C|\neg x\in A\right\}$$
5		dfdif2	$$⊢C\setminus B=\left\{x\in C|\neg x\in B\right\}$$
6	3 4 5	3eqtr4g	$$⊢A=B\to C\setminus A=C\setminus B$$