![]() |
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 403 | . . 3 ⊢ (¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
2 | anclb 544 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) | |
3 | elin 3965 | . . . . . 6 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
4 | 3 | imbi2i 335 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))) |
5 | iman 400 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))) | |
6 | 2, 4, 5 | 3bitr2i 298 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵))) |
7 | 6 | con2bii 356 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ ¬ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) |
8 | eldif 3959 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
9 | 1, 7, 8 | 3bitr4i 302 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ (𝐴 ∩ 𝐵)) ↔ 𝑥 ∈ (𝐴 ∖ 𝐵)) |
10 | 9 | difeqri 4125 | 1 ⊢ (𝐴 ∖ (𝐴 ∩ 𝐵)) = (𝐴 ∖ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 394 = wceq 1539 ∈ wcel 2104 ∖ cdif 3946 ∩ cin 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1542 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-v 3474 df-dif 3952 df-in 3956 |
This theorem is referenced by: dfin4 4268 indif 4270 dfsymdif3 4297 notrab 4312 disjdif2 4480 dfsdom2 9100 hashdif 14379 isercolllem3 15619 iuncld 22771 llycmpkgen2 23276 1stckgen 23280 txkgen 23378 cmmbl 25285 indifbi 32023 disjdifprg2 32072 ldgenpisyslem1 33457 onint1 35639 nonrel 42639 nzprmdif 43382 |
Copyright terms: Public domain | W3C validator |