Description: Double class difference. Exercise 11 of TakeutiZaring p. 22. (Contributed by NM, 17-May-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | difdif | ⊢ ( 𝐴 ∖ ( 𝐵 ∖ 𝐴 ) ) = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.45im | ⊢ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ) ) | |
2 | iman | ⊢ ( ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ↔ ¬ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) ) | |
3 | eldif | ⊢ ( 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ¬ 𝑥 ∈ 𝐴 ) ) | |
4 | 2 3 | xchbinxr | ⊢ ( ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ↔ ¬ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) |
5 | 4 | anbi2i | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) ) |
6 | 1 5 | bitr2i | ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) ↔ 𝑥 ∈ 𝐴 ) |
7 | 6 | difeqri | ⊢ ( 𝐴 ∖ ( 𝐵 ∖ 𝐴 ) ) = 𝐴 |