![]() |
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 5311. (Revised by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
uni0 | ⊢ ∪ ∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss 4401 | . 2 ⊢ ∅ ⊆ {∅} | |
2 | uni0b 4941 | . 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅}) | |
3 | 1, 2 | mpbir 230 | 1 ⊢ ∪ ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1534 ⊆ wss 3947 ∅c0 4325 {csn 4633 ∪ cuni 4913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-11 2147 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-v 3464 df-dif 3950 df-ss 3964 df-nul 4326 df-sn 4634 df-uni 4914 |
This theorem is referenced by: csbuni 4944 uniintsn 4995 iununi 5107 unisn2 5317 eqsnuniex 5365 opswap 6240 unixp0 6294 unixpid 6295 unizlim 6499 iotanul 6532 funfv 6989 dffv2 6997 1stval 8005 2ndval 8006 1stnpr 8007 2ndnpr 8008 1st0 8009 2nd0 8010 1st2val 8031 2nd2val 8032 brtpos0 8248 tpostpos 8261 nnunifi 9328 supval2 9498 sup00 9507 infeq5 9680 rankuni 9906 rankxplim3 9924 iunfictbso 10157 cflim2 10306 fin1a2lem11 10453 itunisuc 10462 itunitc 10464 ttukeylem4 10555 relexpfldd 15055 incexclem 15840 arwval 18065 dprdsn 20036 zrhval 21497 0opn 22897 indistopon 22995 mretopd 23087 hauscmplem 23401 cmpfi 23403 comppfsc 23527 alexsublem 24039 alexsubALTlem2 24043 ptcmplem2 24048 lebnumlem3 24980 old0 27883 made0 27897 locfinref 33656 prsiga 33964 sigapildsys 33995 dya2iocuni 34117 fiunelcarsg 34150 carsgclctunlem1 34151 carsgclctunlem3 34154 wevgblacfn 34936 nnuni 35549 unisnif 35749 limsucncmpi 36157 heicant 37356 ovoliunnfl 37363 voliunnfl 37365 volsupnfl 37366 mbfresfi 37367 onov0suclim 42940 stoweidlem35 45656 stoweidlem39 45660 prsal 45939 issalnnd 45966 ismeannd 46088 caragenunicl 46145 isomennd 46152 ipolub0 48318 |
Copyright terms: Public domain | W3C validator |