Theorem difeq12i

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

	Ref	Expression
Hypotheses	difeq1i.1	⊢ 𝐴 = 𝐵
	difeq12i.2	⊢ 𝐶 = 𝐷
Assertion	difeq12i	⊢ ( 𝐴 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		difeq1i.1	⊢ 𝐴 = 𝐵
2		difeq12i.2	⊢ 𝐶 = 𝐷
3	1	difeq1i	⊢ ( 𝐴 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐶 )
4	2	difeq2i	⊢ ( 𝐵 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐷 )
5	3 4	eqtri	⊢ ( 𝐴 ∖ 𝐶 ) = ( 𝐵 ∖ 𝐷 )