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

Metamath Proof Explorer

Theorem difin

Description: Difference with intersection. Theorem 33 of Suppes p. 29. (Contributed by NM, 31-Mar-1998) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion difin ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )

Proof

Step Hyp Ref Expression
1 pm4.61 ⊢ ( ¬ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
2 anclb ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
3 elin ⊢ ( 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
4 3 imbi2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
5 iman ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
6 2 4 5 3bitr2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ¬ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) )
7 6 con2bii ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ ¬ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
8 eldif ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) )
9 1 7 8 3bitr4i ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ( 𝐴 ∩ 𝐵 ) ) ↔ 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) )
10 9 difeqri ⊢ ( 𝐴 ∖ ( 𝐴 ∩ 𝐵 ) ) = ( 𝐴 ∖ 𝐵 )