| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > uni0 | Structured version Visualization version GIF version | ||
| Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Contributed by NM, 16-Sep-1993.) Remove use of ax-nul 5306. (Revised by Eric Schmidt, 4-Apr-2007.) |
| Ref | Expression |
|---|---|
| uni0 | ⊢ ∪ ∅ = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ss 4400 | . 2 ⊢ ∅ ⊆ {∅} | |
| 2 | uni0b 4933 | . 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅}) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ ∪ ∅ = ∅ |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ⊆ wss 3951 ∅c0 4333 {csn 4626 ∪ cuni 4907 |
| 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-11 2157 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-ss 3968 df-nul 4334 df-sn 4627 df-uni 4908 |
| This theorem is referenced by: csbuni 4936 uniintsn 4985 iununi 5099 unisn2 5312 eqsnuniex 5361 opswap 6249 unixp0 6303 unixpid 6304 unizlim 6507 iotanul 6539 funfv 6996 dffv2 7004 1stval 8016 2ndval 8017 1stnpr 8018 2ndnpr 8019 1st0 8020 2nd0 8021 1st2val 8042 2nd2val 8043 brtpos0 8258 tpostpos 8271 nnunifi 9327 supval2 9495 sup00 9504 infeq5 9677 rankuni 9903 rankxplim3 9921 iunfictbso 10154 cflim2 10303 fin1a2lem11 10450 itunisuc 10459 itunitc 10461 ttukeylem4 10552 relexpfldd 15089 incexclem 15872 arwval 18088 dprdsn 20056 zrhval 21518 0opn 22910 indistopon 23008 mretopd 23100 hauscmplem 23414 cmpfi 23416 comppfsc 23540 alexsublem 24052 alexsubALTlem2 24056 ptcmplem2 24061 lebnumlem3 24995 old0 27898 made0 27912 locfinref 33840 prsiga 34132 sigapildsys 34163 dya2iocuni 34285 fiunelcarsg 34318 carsgclctunlem1 34319 carsgclctunlem3 34322 wevgblacfn 35114 nnuni 35727 unisnif 35926 limsucncmpi 36446 heicant 37662 ovoliunnfl 37669 voliunnfl 37671 volsupnfl 37672 mbfresfi 37673 onov0suclim 43287 stoweidlem35 46050 stoweidlem39 46054 prsal 46333 issalnnd 46360 ismeannd 46482 caragenunicl 46539 isomennd 46546 dftpos5 48774 ipolub0 48881 |
| Copyright terms: Public domain | W3C validator |