![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uni0 | Structured version Visualization version Unicode 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 4506 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 3731 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | uni0b 4193 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpbir 214 |
1
![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1673 ax-4 1686 ax-5 1762 ax-6 1809 ax-7 1855 ax-10 1919 ax-11 1924 ax-12 1937 ax-13 2092 ax-ext 2432 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-tru 1451 df-ex 1668 df-nf 1672 df-sb 1802 df-clab 2439 df-cleq 2445 df-clel 2448 df-nfc 2582 df-ne 2624 df-ral 2742 df-rex 2743 df-v 3015 df-dif 3375 df-in 3379 df-ss 3386 df-nul 3700 df-sn 3937 df-uni 4169 |
This theorem is referenced by: csbuni 4196 uniintsn 4242 iununi 4338 unisn2 4511 opswap 5302 unixp0 5349 unixpid 5350 unizlim 5518 iotanul 5540 funfv 5916 dffv2 5922 1stval 6783 2ndval 6784 1stnpr 6785 2ndnpr 6786 1st0 6787 2nd0 6788 1st2val 6807 2nd2val 6808 brtpos0 6967 tpostpos 6980 nnunifi 7809 supval2 7956 sup00 7965 infeq5 8129 rankuni 8321 rankxplim3 8339 iunfictbso 8532 cflim2 8680 fin1a2lem11 8827 itunisuc 8836 itunitc 8838 ttukeylem4 8929 incexclem 13905 arwval 15949 dprdsn 17680 zrhval 19090 0opn 19945 indistopon 20027 mretopd 20119 hauscmplem 20432 cmpfi 20434 comppfsc 20558 alexsublem 21070 alexsubALTlem2 21074 ptcmplem2 21079 lebnumlem3 22002 lebnumlem3OLD 22005 locfinref 28675 prsiga 28960 sigapildsys 28991 dya2iocuni 29111 fiunelcarsg 29154 carsgclctunlem1 29155 carsgclctunlem3 29158 unisnif 30698 limsucncmpi 31111 heicant 31977 ovoliunnfl 31984 voliunnfl 31986 volsupnfl 31987 mbfresfi 31989 stoweidlem35 37953 stoweidlem39 37957 prsal 38236 issalnnd 38261 ismeannd 38366 caragenunicl 38409 isomennd 38416 |
Copyright terms: Public domain | W3C validator |