![]() |
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 3991 and dfss4 3989 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 3331 | . . . . . . 7 ⊢ 𝑥 ∈ V | |
2 | eldif 3713 | . . . . . . 7 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ 𝐴)) | |
3 | 1, 2 | mpbiran 991 | . . . . . 6 ⊢ (𝑥 ∈ (V ∖ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴) |
4 | 3 | anbi1i 733 | . . . . 5 ⊢ ((𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) |
5 | eldif 3713 | . . . . 5 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ (𝑥 ∈ (V ∖ 𝐴) ∧ ¬ 𝑥 ∈ 𝐵)) | |
6 | ioran 512 | . . . . 5 ⊢ (¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ (¬ 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)) | |
7 | 4, 5, 6 | 3bitr4i 292 | . . . 4 ⊢ (𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵) ↔ ¬ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) |
8 | 7 | con2bii 346 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵)) |
9 | eldif 3713 | . . . 4 ⊢ (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵))) | |
10 | 1, 9 | mpbiran 991 | . . 3 ⊢ (𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) ↔ ¬ 𝑥 ∈ ((V ∖ 𝐴) ∖ 𝐵)) |
11 | 8, 10 | bitr4i 267 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ (V ∖ ((V ∖ 𝐴) ∖ 𝐵))) |
12 | 11 | uneqri 3886 | 1 ⊢ (𝐴 ∪ 𝐵) = (V ∖ ((V ∖ 𝐴) ∖ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∨ wo 382 ∧ wa 383 = wceq 1620 ∈ wcel 2127 Vcvv 3328 ∖ cdif 3700 ∪ cun 3701 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 df-sb 2035 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-v 3330 df-dif 3706 df-un 3708 |
This theorem is referenced by: dfun3 3996 dfin3 3997 |
Copyright terms: Public domain | W3C validator |