Theorem difeq12i

Description: Equality inference for class difference. (Contributed by NM, 29-Aug-2004)

	Ref	Expression
Hypotheses	difeq1i.1	$$⊢A=B$$
	difeq12i.2	$$⊢C=D$$
Assertion	difeq12i	$$⊢A\setminus C=B\setminus D$$

Proof

Step	Hyp	Ref	Expression
1		difeq1i.1	$$⊢A=B$$
2		difeq12i.2	$$⊢C=D$$
3	1	difeq1i	$$⊢A\setminus C=B\setminus C$$
4	2	difeq2i	$$⊢B\setminus C=B\setminus D$$
5	3 4	eqtri	$$⊢A\setminus C=B\setminus D$$