![]() |
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 4085 | . . 3 ⊢ ¬ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴 | |
2 | eliun 4658 | . . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 ↔ ∃𝑥 ∈ ∅ 𝑦 ∈ 𝐴) | |
3 | 1, 2 | mtbir 312 | . 2 ⊢ ¬ 𝑦 ∈ ∪ 𝑥 ∈ ∅ 𝐴 |
4 | 3 | nel0 4079 | 1 ⊢ ∪ 𝑥 ∈ ∅ 𝐴 = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1631 ∈ wcel 2145 ∃wrex 3062 ∅c0 4063 ∪ ciun 4654 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-v 3353 df-dif 3726 df-nul 4064 df-iun 4656 |
This theorem is referenced by: iinvdif 4726 iununi 4744 iunfi 8410 pwsdompw 9228 fsum2d 14710 fsumiun 14760 fprod2d 14918 prmreclem4 15830 prmreclem5 15831 fiuncmp 21428 ovolfiniun 23489 ovoliunnul 23495 finiunmbl 23532 volfiniun 23535 volsup 23544 esum2dlem 30494 sigapildsyslem 30564 fiunelros 30577 mrsubvrs 31757 0totbnd 33904 totbndbnd 33920 fiiuncl 39755 sge0iunmptlemfi 41147 caragenfiiuncl 41249 carageniuncllem1 41255 |
Copyright terms: Public domain | W3C validator |