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

Proof

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