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 4717 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 3924 | . 2 ⊢ ∅ ⊆ {∅} | |
2 | uni0b 4399 | . 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅}) | |
3 | 1, 2 | mpbir 220 | 1 ⊢ ∪ ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ⊆ wss 3540 ∅c0 3874 {csn 4125 ∪ cuni 4372 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-v 3175 df-dif 3543 df-in 3547 df-ss 3554 df-nul 3875 df-sn 4126 df-uni 4373 |
This theorem is referenced by: csbuni 4402 uniintsn 4449 iununi 4546 unisn2 4722 opswap 5540 unixp0 5586 unixpid 5587 unizlim 5761 iotanul 5783 funfv 6175 dffv2 6181 1stval 7061 2ndval 7062 1stnpr 7063 2ndnpr 7064 1st0 7065 2nd0 7066 1st2val 7085 2nd2val 7086 brtpos0 7246 tpostpos 7259 nnunifi 8096 supval2 8244 sup00 8253 infeq5 8417 rankuni 8609 rankxplim3 8627 iunfictbso 8820 cflim2 8968 fin1a2lem11 9115 itunisuc 9124 itunitc 9126 ttukeylem4 9217 incexclem 14407 arwval 16516 dprdsn 18258 zrhval 19675 0opn 20534 indistopon 20615 mretopd 20706 hauscmplem 21019 cmpfi 21021 comppfsc 21145 alexsublem 21658 alexsubALTlem2 21662 ptcmplem2 21667 lebnumlem3 22570 locfinref 29236 prsiga 29521 sigapildsys 29552 dya2iocuni 29672 fiunelcarsg 29705 carsgclctunlem1 29706 carsgclctunlem3 29709 unisnif 31202 limsucncmpi 31614 heicant 32614 ovoliunnfl 32621 voliunnfl 32623 volsupnfl 32624 mbfresfi 32626 stoweidlem35 38928 stoweidlem39 38932 prsal 39214 issalnnd 39239 ismeannd 39360 caragenunicl 39414 isomennd 39421 |
Copyright terms: Public domain | W3C validator |