![]() |
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 4356 | . . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴 | |
2 | eliun 5000 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴) | |
3 | 1, 2 | mtbir 322 | . 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 |
4 | 3 | nel0 4349 | 1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 ∃wrex 3070 ∅c0 4321 ∪ ciun 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-ral 3062 df-rex 3071 df-v 3476 df-dif 3950 df-nul 4322 df-iun 4998 |
This theorem is referenced by: iinvdif 5082 iununi 5101 iunfi 9336 pwsdompw 10195 fsum2d 15713 fsumiun 15763 fprod2d 15921 prmreclem4 16848 prmreclem5 16849 fiuncmp 22899 ovolfiniun 25009 ovoliunnul 25015 finiunmbl 25052 volfiniun 25055 volsup 25064 gsumpart 32194 esum2dlem 33078 sigapildsyslem 33147 fiunelros 33160 mrsubvrs 34501 0totbnd 36629 totbndbnd 36645 fiiuncl 43737 sge0iunmptlemfi 45115 caragenfiiuncl 45217 carageniuncllem1 45223 |
Copyright terms: Public domain | W3C validator |