Theorem difin 4226

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 409	. . 3 ⊢ (¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
2		anclb 554	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
3		elin 3922	. . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
4	3	imbi2i 339	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)))
5		iman 406	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)))
6	2, 4, 5	3bitr2i 302	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)))
7	6	con2bii 360	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		eldif 3916	. . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
9	1, 7, 8	3bitr4i 306	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ 𝑥 ∈ (𝐴 ∖ 𝐵))
10	9	difeqri 4084	1 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ∖ cdif 3903   ∩ cin 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-in 3913

This theorem is referenced by:  dfin4  4232  indif  4234  dfsymdif3  4260  notrab  4276  disjdif2  4442  dfsdom2  9089  hashdif  14452  isercolllem3  15720  iuncld  23183  llycmpkgen2  23688  1stckgen  23692  txkgen  23790  cmmbl  25674  indifbi  32847  disjdifprg2  32902  ldgenpisyslem1  34534  onint1  36941  nonrel  44293  nzprmdif  45012