![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > difin | Structured version Visualization version GIF version |
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 |
---|---|
difin | ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.61 406 | . . 3 ⊢ (¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
2 | anclb 547 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) | |
3 | elin 3962 | . . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 3 | imbi2i 336 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
5 | iman 403 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))) | |
6 | 2, 4, 5 | 3bitr2i 299 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))) |
7 | 6 | con2bii 358 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
8 | eldif 3956 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
9 | 1, 7, 8 | 3bitr4i 303 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
10 | 9 | difeqri 4122 | 1 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∖ cdif 3943 ∩ cin 3945 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-dif 3949 df-in 3953 |
This theorem is referenced by: dfin4 4265 indif 4267 dfsymdif3 4294 notrab 4309 disjdif2 4477 dfsdom2 9091 hashdif 14368 isercolllem3 15608 iuncld 22530 llycmpkgen2 23035 1stckgen 23039 txkgen 23137 cmmbl 25032 indifbi 31735 disjdifprg2 31784 ldgenpisyslem1 33098 onint1 35271 nonrel 42267 nzprmdif 43010 |
Copyright terms: Public domain | W3C validator |