![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0ex | 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 3986. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Ref | Expression |
---|---|
0ex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-nul 3986 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eq0 3320 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | exbii 1548 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 145 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | issetri 2642 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-nul 3986 |
This theorem depends on definitions: df-bi 116 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-v 2635 df-dif 3015 df-nul 3303 |
This theorem is referenced by: 0elpw 4020 0nep0 4021 iin0r 4025 intv 4026 snexprc 4042 p0ex 4044 undifexmid 4049 exmidexmid 4052 exmid01 4053 exmidsssn 4055 exmidel 4057 exmidundif 4058 exmidundifim 4059 0elon 4243 onm 4252 ordtriexmidlem2 4365 ordtriexmid 4366 ordtri2orexmid 4367 ontr2exmid 4369 onsucsssucexmid 4371 onsucelsucexmidlem1 4372 onsucelsucexmid 4374 regexmidlem1 4377 reg2exmidlema 4378 ordsoexmid 4406 0elsucexmid 4409 ordpwsucexmid 4414 ordtri2or2exmid 4415 dcextest 4424 peano1 4437 finds 4443 finds2 4444 0elnn 4460 opthprc 4518 nfunv 5081 fun0 5106 acexmidlema 5681 acexmidlemb 5682 acexmidlemab 5684 ovprc 5722 1st0 5953 2nd0 5954 brtpos0 6055 reldmtpos 6056 tfr0dm 6125 rdg0 6190 frec0g 6200 1n0 6235 el1o 6239 0lt2o 6243 fnom 6251 omexg 6252 om0 6259 nnsucsssuc 6293 mapdm0 6460 map0e 6483 0elixp 6526 en0 6592 ensn1 6593 en1 6596 2dom 6602 map1 6609 xp1en 6619 endisj 6620 dom0 6634 php5dom 6659 ssfilem 6671 ssfiexmid 6672 domfiexmid 6674 diffitest 6683 ac6sfi 6694 exmidpw 6704 unfiexmid 6708 djulclr 6821 djulcl 6823 djulclb 6827 djulf1or 6828 djulf1o 6830 djur 6837 djuss 6841 1stinl 6845 2ndinl 6846 0ct 6869 finomni 6883 exmidomni 6885 exmidfodomrlemr 6925 exmidfodomrlemrALT 6926 indpi 6998 frecfzennn 9982 fihashen1 10338 hashunlem 10343 zfz1iso 10377 strsl0 11707 topgele 11895 en1top 11945 sn0topon 11956 sn0cld 12005 rest0 12047 restsn 12048 0met 12186 djulclALT 12425 bj-d0clsepcl 12544 bj-indint 12550 bj-bdfindis 12566 bj-inf2vnlem1 12589 pw1dom2 12611 0nninf 12614 nninfsellemdc 12623 |
Copyright terms: Public domain | W3C validator |