![]() |
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 4166 | . . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴 | |
2 | eliun 4757 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴) | |
3 | 1, 2 | mtbir 315 | . 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 |
4 | 3 | nel0 4160 | 1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∈ wcel 2107 ∃wrex 3091 ∅c0 4141 ∪ ciun 4753 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-v 3400 df-dif 3795 df-nul 4142 df-iun 4755 |
This theorem is referenced by: iinvdif 4825 iununi 4844 iunfi 8542 pwsdompw 9361 fsum2d 14907 fsumiun 14957 fprod2d 15114 prmreclem4 16027 prmreclem5 16028 fiuncmp 21616 ovolfiniun 23705 ovoliunnul 23711 finiunmbl 23748 volfiniun 23751 volsup 23760 esum2dlem 30752 sigapildsyslem 30822 fiunelros 30835 mrsubvrs 32018 0totbnd 34196 totbndbnd 34212 fiiuncl 40165 sge0iunmptlemfi 41554 caragenfiiuncl 41656 carageniuncllem1 41662 |
Copyright terms: Public domain | W3C validator |