Theorem difin 4192

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 3899	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
4	3	imbi2i 335	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5		iman 401	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)))
6	2, 4, 5	3bitr2i 298	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	con2bii 357	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		eldif 3893	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
9	1, 7, 8	3bitr4i 302	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))
10	9	difeqri 4055	1 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ∖ cdif 3880   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890

This theorem is referenced by:  dfin4  4198  indif  4200  dfsymdif3  4227  notrab  4242  disjdif2  4410  dfsdom2  8836  hashdif  14056  isercolllem3  15306  iuncld  22104  llycmpkgen2  22609  1stckgen  22613  txkgen  22711  cmmbl  24603  indifbi  30769  disjdifprg2  30816  ldgenpisyslem1  32031  onint1  34565  nonrel  41081  nzprmdif  41826