| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 2710. |
| Ref | Expression |
|---|---|
| 0ex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-nul 2710 |
. . . 4
| |
| 2 | 1 | zfnuleu 2707 |
. . 3
|
| 3 | eq0 2294 |
. . . 4
| |
| 4 | 3 | eubii 1387 |
. . 3
|
| 5 | 2, 4 | mpbir 190 |
. 2
|
| 6 | eueq 1916 |
. 2
| |
| 7 | 5, 6 | mpbir 190 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: class2set 2734 0elpw 2736 0nep0 2737 unidif0 2739 iin0 2740 notzfaus 2741 dtru 2772 zfpair 2777 opprc1b 2796 opprc3 2797 opthwiener 2807 unisn2 2875 onint0 3007 0elon 3022 nsuceq0 3053 onzsl 3117 snsn0non 3125 finds 3156 finds2 3158 tfinds2 3165 opthprc 3221 onnev 3242 xpexr 3479 fun0 3544 nfunv 3546 tz7.44-1 3928 1ne0 4142 el1o 4146 om0 4156 om0x 4158 map0e 4342 map0b 4343 map0 4344 0elixp 4360 en0 4423 ensn1 4424 en1 4426 2dom 4427 map1 4430 endisj 4437 pw2en 4446 0dom 4464 dom0 4465 0sdomg 4466 limensuci 4506 unifiOLD 4557 inf3lemb 4610 infeq5 4621 dfom3 4630 r10 4651 scottex 4716 brdom3 4801 cardeq0 4832 unxpdom2 4845 sucxpdom 4846 cf0 4910 cfeq0 4914 cfsuc 4915 uncdadom 4921 cdaun 4922 pm110.643 4923 cdaen 4924 cda0en 4925 cda1en 4926 xp1en 4927 cdacomen 4929 cdaassen 4930 mapcdaen 4932 cdadom1 4933 axpowndlem3 4951 indpi 5034 acdc3lem 7486 acdc2lem1 7488 acdclem 7494 alephadd 7582 sn0top 7647 indistop 7648 indistps 7653 0met 7825 bcth 8032 moec 10461 intprd 10471 mapudiscn 10512 eqindhome 10541 top1 10547 top2ind 10548 top2usne 10549 homindlem2 10550 homindlem3 10551 efilcp 10572 efilcpOLD 10573 fisub 10576 fisubOLD 10577 efilcp2 10581 efilcp2OLD 10582 cnfilca 10583 cnfilcaOLD 10584 rcfpfillem2 10587 rcfpfillem2OLD 10588 rcfpfillem3 10589 rcfpfillem3OLD 10590 rcfpfillem5 10593 rcfpfillem5OLD 10594 relrded 10675 0alg 10689 0ded 10690 0cat 10691 relrcat 10696 hgrablkcard 10774 emhgrat 10775 0hgra 10776 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-10 966 ax-11 967 ax-12 968 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-nul 2710 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-v 1812 df-dif 2049 df-nul 2281 |