![]() |
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 4822 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 4005 | . 2 ⊢ ∅ ⊆ {∅} | |
2 | uni0b 4495 | . 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅}) | |
3 | 1, 2 | mpbir 221 | 1 ⊢ ∪ ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1523 ⊆ wss 3607 ∅c0 3948 {csn 4210 ∪ cuni 4468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-v 3233 df-dif 3610 df-in 3614 df-ss 3621 df-nul 3949 df-sn 4211 df-uni 4469 |
This theorem is referenced by: csbuni 4498 uniintsn 4546 iununi 4642 unisn2 4827 opswap 5660 unixp0 5707 unixpid 5708 unizlim 5882 iotanul 5904 funfv 6304 dffv2 6310 1stval 7212 2ndval 7213 1stnpr 7214 2ndnpr 7215 1st0 7216 2nd0 7217 1st2val 7238 2nd2val 7239 brtpos0 7404 tpostpos 7417 nnunifi 8252 supval2 8402 sup00 8411 infeq5 8572 rankuni 8764 rankxplim3 8782 iunfictbso 8975 cflim2 9123 fin1a2lem11 9270 itunisuc 9279 itunitc 9281 ttukeylem4 9372 incexclem 14612 arwval 16740 dprdsn 18481 zrhval 19904 0opn 20757 indistopon 20853 mretopd 20944 hauscmplem 21257 cmpfi 21259 comppfsc 21383 alexsublem 21895 alexsubALTlem2 21899 ptcmplem2 21904 lebnumlem3 22809 locfinref 30036 prsiga 30322 sigapildsys 30353 dya2iocuni 30473 fiunelcarsg 30506 carsgclctunlem1 30507 carsgclctunlem3 30510 unisnif 32157 limsucncmpi 32569 heicant 33574 ovoliunnfl 33581 voliunnfl 33583 volsupnfl 33584 mbfresfi 33586 stoweidlem35 40570 stoweidlem39 40574 prsal 40856 issalnnd 40881 ismeannd 41002 caragenunicl 41059 isomennd 41066 |
Copyright terms: Public domain | W3C validator |