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. (Reproved without relying on ax-nul 5201 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.) |
Ref | Expression |
---|---|
uni0 | ⊢ ∪ ∅ = ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0ss 4347 | . 2 ⊢ ∅ ⊆ {∅} | |
2 | uni0b 4855 | . 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅}) | |
3 | 1, 2 | mpbir 232 | 1 ⊢ ∪ ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ⊆ wss 3933 ∅c0 4288 {csn 4557 ∪ cuni 4830 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-v 3494 df-dif 3936 df-in 3940 df-ss 3949 df-nul 4289 df-sn 4558 df-uni 4831 |
This theorem is referenced by: csbuni 4858 uniintsn 4904 iununi 5012 unisn2 5207 opswap 6079 unixp0 6127 unixpid 6128 unizlim 6300 iotanul 6326 funfv 6743 dffv2 6749 1stval 7680 2ndval 7681 1stnpr 7682 2ndnpr 7683 1st0 7684 2nd0 7685 1st2val 7706 2nd2val 7707 brtpos0 7888 tpostpos 7901 nnunifi 8757 supval2 8907 sup00 8916 infeq5 9088 rankuni 9280 rankxplim3 9298 iunfictbso 9528 cflim2 9673 fin1a2lem11 9820 itunisuc 9829 itunitc 9831 ttukeylem4 9922 incexclem 15179 arwval 17291 dprdsn 19087 zrhval 20583 0opn 21440 indistopon 21537 mretopd 21628 hauscmplem 21942 cmpfi 21944 comppfsc 22068 alexsublem 22580 alexsubALTlem2 22584 ptcmplem2 22589 lebnumlem3 23494 locfinref 31004 prsiga 31289 sigapildsys 31320 dya2iocuni 31440 fiunelcarsg 31473 carsgclctunlem1 31474 carsgclctunlem3 31477 unisnif 33283 limsucncmpi 33690 heicant 34808 ovoliunnfl 34815 voliunnfl 34817 volsupnfl 34818 mbfresfi 34819 stoweidlem35 42197 stoweidlem39 42201 prsal 42480 issalnnd 42505 ismeannd 42626 caragenunicl 42683 isomennd 42690 |
Copyright terms: Public domain | W3C validator |