Theorem difeq1

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

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

Proof

Step	Hyp	Ref	Expression
1		rabeq	$$⊢A=B\to \left\{x\in A|\neg x\in C\right\}=\left\{x\in B|\neg x\in C\right\}$$
2		dfdif2	$$⊢A\setminus C=\left\{x\in A|\neg x\in C\right\}$$
3		dfdif2	$$⊢B\setminus C=\left\{x\in B|\neg x\in C\right\}$$
4	1 2 3	3eqtr4g	$$⊢A=B\to A\setminus C=B\setminus C$$