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 \ C ) = ( B \ D )

Proof

Step	Hyp	Ref	Expression
1		difeq1i.1	|- A = B
2		difeq12i.2	|- C = D
3	1	difeq1i	|- ( A \ C ) = ( B \ C )
4	2	difeq2i	|- ( B \ C ) = ( B \ D )
5	3 4	eqtri	|- ( A \ C ) = ( B \ D )