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	⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) )
2	1	notbid	⊢ ( 𝐴 = 𝐵 → ( ¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵 ) )
3	2	rabbidv	⊢ ( 𝐴 = 𝐵 → { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴 } = { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵 } )
4		dfdif2	⊢ ( 𝐶 ∖ 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴 }
5		dfdif2	⊢ ( 𝐶 ∖ 𝐵 ) = { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵 }
6	3 4 5	3eqtr4g	⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) )