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