| 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 2715. |
| Ref | Expression |
|---|---|
| 0ex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-nul 2715 |
. . . 4
| |
| 2 | 1 | zfnuleu 2712 |
. . 3
|
| 3 | eq0 2298 |
. . . 4
| |
| 4 | 3 | eubii 1389 |
. . 3
|
| 5 | 2, 4 | mpbir 190 |
. 2
|
| 6 | eueq 1919 |
. 2
| |
| 7 | 5, 6 | mpbir 190 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: class2set 2739 0elpw 2741 0nep0 2742 unidif0 2744 iin0 2745 notzfaus 2746 intv 2747 dtru 2778 zfpair 2783 opprc1b 2802 opprc3 2803 opthwiener 2813 unisn2 2881 onint0 3013 0elon 3028 nsuceq0 3059 onzsl 3123 snsn0non 3131 finds 3162 finds2 3164 tfinds2 3171 opthprc 3227 onnev 3248 xpexr 3485 fun0 3550 nfunv 3552 tz7.44-1 3934 1ne0 4148 el1o 4152 om0 4162 om0x 4164 map0e 4348 map0b 4349 map0 4350 0elixp 4366 en0 4429 ensn1 4430 en1 4432 2dom 4433 map1 4436 endisj 4443 pw2en 4452 0dom 4470 dom0 4471 0sdomg 4472 limensuci 4512 unifiOLD 4570 inf3lemb 4619 infeq5 4630 dfom3 4639 r10 4661 scottex 4726 brdom3 4811 cardeq0 4842 unxpdom2 4856 sucxpdom 4857 cf0 4922 cfeq0 4926 cfsuc 4927 uncdadom 4933 cdaun 4934 pm110.643 4935 cdaen 4936 cda0en 4937 cda1en 4938 xp1en 4939 cdacomen 4941 cdaassen 4942 mapcdaen 4944 cdadom1 4945 axpowndlem3 4963 indpi 5046 acdc3lem 7487 acdc2lem1 7489 acdclem 7495 alephadd 7584 sn0top 7644 indistop 7645 indistps 7650 0met 7822 bcth 8029 moec 10451 intprd 10461 vxveqv 10467 mapudiscn 10498 eqindhome 10527 top1 10533 top2ind 10534 top2usne 10535 homindlem2 10536 homindlem3 10537 efilcp 10556 fisub 10558 efilcp2 10561 cnfilca 10562 rcfpfillem2 10564 rcfpfillem3 10565 rcfpfillem5 10567 0alg 10660 0ded 10661 0cat 10662 hgrablkcard 10745 emhgrat 10746 0hgra 10747 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-10 968 ax-11 969 ax-12 970 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-nul 2715 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-v 1815 df-dif 2052 df-nul 2284 |