![]() |
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 5063 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 4230 | . 2 ⊢ ∅ ⊆ {∅} | |
2 | uni0b 4733 | . 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅}) | |
3 | 1, 2 | mpbir 223 | 1 ⊢ ∪ ∅ = ∅ |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1507 ⊆ wss 3823 ∅c0 4172 {csn 4435 ∪ cuni 4708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2744 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-v 3411 df-dif 3826 df-in 3830 df-ss 3837 df-nul 4173 df-sn 4436 df-uni 4709 |
This theorem is referenced by: csbuni 4736 uniintsn 4782 iununi 4883 unisn2 5069 opswap 5922 unixp0 5969 unixpid 5970 unizlim 6142 iotanul 6164 funfv 6576 dffv2 6582 1stval 7501 2ndval 7502 1stnpr 7503 2ndnpr 7504 1st0 7505 2nd0 7506 1st2val 7527 2nd2val 7528 brtpos0 7700 tpostpos 7713 nnunifi 8562 supval2 8712 sup00 8721 infeq5 8892 rankuni 9084 rankxplim3 9102 iunfictbso 9332 cflim2 9481 fin1a2lem11 9628 itunisuc 9637 itunitc 9639 ttukeylem4 9730 incexclem 15049 arwval 17173 dprdsn 18920 zrhval 20369 0opn 21228 indistopon 21325 mretopd 21416 hauscmplem 21730 cmpfi 21732 comppfsc 21856 alexsublem 22368 alexsubALTlem2 22372 ptcmplem2 22377 lebnumlem3 23282 locfinref 30778 prsiga 31064 sigapildsys 31095 dya2iocuni 31215 fiunelcarsg 31248 carsgclctunlem1 31249 carsgclctunlem3 31252 unisnif 32936 limsucncmpi 33342 heicant 34397 ovoliunnfl 34404 voliunnfl 34406 volsupnfl 34407 mbfresfi 34408 stoweidlem35 41776 stoweidlem39 41780 prsal 42059 issalnnd 42084 ismeannd 42205 caragenunicl 42262 isomennd 42269 |
Copyright terms: Public domain | W3C validator |