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

Ref | Expression | ||
---|---|---|---|

Assertion | difeq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eleq2 | ⊢ ( 𝐴 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵 ) ) | |

2 | 1 | notbid | ⊢ ( 𝐴 = 𝐵 → ( ¬ 𝑥 ∈ 𝐴 ↔ ¬ 𝑥 ∈ 𝐵 ) ) |

3 | 2 | rabbidv | ⊢ ( 𝐴 = 𝐵 → { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴 } = { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵 } ) |

4 | dfdif2 | ⊢ ( 𝐶 ∖ 𝐴 ) = { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐴 } | |

5 | dfdif2 | ⊢ ( 𝐶 ∖ 𝐵 ) = { 𝑥 ∈ 𝐶 ∣ ¬ 𝑥 ∈ 𝐵 } | |

6 | 3 4 5 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐶 ∖ 𝐴 ) = ( 𝐶 ∖ 𝐵 ) ) |