Theorem difin 4291

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

Assertion

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

Proof of Theorem difin

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		pm4.61 404	. . 3 ⊢ (¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		anclb 545	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
3		elin 3992	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
4	3	imbi2i 336	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5		iman 401	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)))
6	2, 4, 5	3bitr2i 299	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	con2bii 357	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		eldif 3986	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
9	1, 7, 8	3bitr4i 303	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))
10	9	difeqri 4151	1 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ∖ cdif 3973   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-in 3983

This theorem is referenced by:  dfin4  4297  indif  4299  dfsymdif3  4325  notrab  4341  disjdif2  4503  dfsdom2  9162  hashdif  14462  isercolllem3  15715  iuncld  23074  llycmpkgen2  23579  1stckgen  23583  txkgen  23681  cmmbl  25588  indifbi  32550  disjdifprg2  32598  ldgenpisyslem1  34127  onint1  36415  nonrel  43546  nzprmdif  44288