| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 0iun | Structured version Visualization version GIF version | ||
| Description: An empty indexed union is empty. (Contributed by NM, 4-Dec-2004.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| Ref | Expression |
|---|---|
| 0iun | ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rex0 4360 | . . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴 | |
| 2 | eliun 4995 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴) | |
| 3 | 1, 2 | mtbir 323 | . 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 |
| 4 | 3 | nel0 4354 | 1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: = 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: iinvdif 5080 iununi 5099 iunfi 9383 pwsdompw 10243 fsum2d 15807 fsumiun 15857 fprod2d 16017 prmreclem4 16957 prmreclem5 16958 fiuncmp 23412 ovolfiniun 25536 ovoliunnul 25542 finiunmbl 25579 volfiniun 25582 volsup 25591 gsumpart 33060 esum2dlem 34093 sigapildsyslem 34162 fiunelros 34175 mrsubvrs 35527 0totbnd 37780 totbndbnd 37796 fiiuncl 45070 sge0iunmptlemfi 46428 caragenfiiuncl 46530 carageniuncllem1 46536 |
| Copyright terms: Public domain | W3C validator |