![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfun2 | Structured version Visualization version GIF version |
Description: An alternate definition of the union of two classes in terms of class difference, requiring no dummy variables. Along with dfin2 3893 and dfss4 3891 it shows we can express union, intersection, and subset directly in terms of the single "primitive" operation ∖ (class difference). (Contributed by NM, 10-Jun-2004.) |
Ref | Expression |
---|---|
dfun2 | ⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3234 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
2 | eldif 3617 | . . . . . . 7 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴)) | |
3 | 1, 2 | mpbiran 973 | . . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) |
4 | 3 | anbi1i 731 | . . . . 5 ⊢ ((𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
5 | eldif 3617 | . . . . 5 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ (𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵)) | |
6 | ioran 510 | . . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4i 292 | . . . 4 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
8 | 7 | con2bii 346 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵)) |
9 | eldif 3617 | . . . 4 ⊢ (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))) | |
10 | 1, 9 | mpbiran 973 | . . 3 ⊢ (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵)) |
11 | 8, 10 | bitr4i 267 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵))) |
12 | 11 | uneqri 3788 | 1 ⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 382 ∧ wa 383 = wceq 1523 ∈ wcel 2030 Vcvv 3231 ∖ cdif 3604 ∪ cun 3605 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-v 3233 df-dif 3610 df-un 3612 |
This theorem is referenced by: dfun3 3898 dfin3 3899 |
Copyright terms: Public domain | W3C validator |