| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iun0 | Structured version Visualization version GIF version | ||
| Description: An indexed union of the empty set is empty. (Contributed by NM, 26-Mar-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| Ref | Expression |
|---|---|
| iun0 | ⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noel 4338 | . . . . 5 ⊢ ¬ 𝑦 ∈ ∅ | |
| 2 | 1 | a1i 11 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝑦 ∈ ∅) |
| 3 | 2 | nrex 3074 | . . 3 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅ |
| 4 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅ ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ ∅) | |
| 5 | 3, 4 | mtbir 323 | . 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 ∅ |
| 6 | 5 | nel0 4354 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 ∅ = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 = wceq 1540 ∈ wcel 2108 ∃wrex 3070 ∅c0 4333 ∪ ciun 4991 |
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-rex 3071 df-v 3482 df-dif 3954 df-nul 4334 df-iun 4993 |
| This theorem is referenced by: iunxdif3 5095 iununi 5099 funiunfv 7268 om0r 8577 kmlem11 10201 ituniiun 10462 dfrtrclrec2 15097 voliunlem1 25585 ofpreima2 32676 ssdifidllem 33484 esum2dlem 34093 sigaclfu2 34122 measvunilem0 34214 measvuni 34215 cvmscld 35278 ovolval4lem1 46664 |
| Copyright terms: Public domain | W3C validator |