This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difdif

Description: Double class difference. Exercise 11 of TakeutiZaring p. 22. (Contributed by NM, 17-May-1998)

Ref Expression
Assertion difdif ⊢ A ∖ B ∖ A = A

Proof

Step Hyp Ref Expression
1 pm4.45im ⊢ x ∈ A ↔ x ∈ A ∧ x ∈ B → x ∈ A
2 iman ⊢ x ∈ B → x ∈ A ↔ ¬ x ∈ B ∧ ¬ x ∈ A
3 eldif ⊢ x ∈ B ∖ A ↔ x ∈ B ∧ ¬ x ∈ A
4 2 3 xchbinxr ⊢ x ∈ B → x ∈ A ↔ ¬ x ∈ B ∖ A
5 4 anbi2i ⊢ x ∈ A ∧ x ∈ B → x ∈ A ↔ x ∈ A ∧ ¬ x ∈ B ∖ A
6 1 5 bitr2i ⊢ x ∈ A ∧ ¬ x ∈ B ∖ A ↔ x ∈ A
7 6 difeqri ⊢ A ∖ B ∖ A = A