![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 0ex | GIF 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 3994. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Ref | Expression |
---|---|
0ex | ⊢ ∅ ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-nul 3994 | . . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | |
2 | eq0 3328 | . . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥) | |
3 | 2 | exbii 1552 | . . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) |
4 | 1, 3 | mpbir 145 | . 2 ⊢ ∃𝑥 𝑥 = ∅ |
5 | 4 | issetri 2650 | 1 ⊢ ∅ ∈ V |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∀wal 1297 = wceq 1299 ∃wex 1436 ∈ wcel 1448 Vcvv 2641 ∅c0 3310 |
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 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-nul 3994 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-v 2643 df-dif 3023 df-nul 3311 |
This theorem is referenced by: 0elpw 4028 0nep0 4029 iin0r 4033 intv 4034 snexprc 4050 p0ex 4052 undifexmid 4057 exmidexmid 4060 exmid01 4061 exmidsssn 4063 exmidel 4066 exmidundif 4067 exmidundifim 4068 0elon 4252 onm 4261 ordtriexmidlem2 4374 ordtriexmid 4375 ordtri2orexmid 4376 ontr2exmid 4378 onsucsssucexmid 4380 onsucelsucexmidlem1 4381 onsucelsucexmid 4383 regexmidlem1 4386 reg2exmidlema 4387 ordsoexmid 4415 0elsucexmid 4418 ordpwsucexmid 4423 ordtri2or2exmid 4424 dcextest 4433 peano1 4446 finds 4452 finds2 4453 0elnn 4470 opthprc 4528 nfunv 5092 fun0 5117 acexmidlema 5697 acexmidlemb 5698 acexmidlemab 5700 ovprc 5738 1st0 5973 2nd0 5974 brtpos0 6079 reldmtpos 6080 tfr0dm 6149 rdg0 6214 frec0g 6224 1n0 6259 el1o 6264 0lt2o 6268 fnom 6276 omexg 6277 om0 6284 nnsucsssuc 6318 mapdm0 6487 map0e 6510 0elixp 6553 en0 6619 ensn1 6620 en1 6623 2dom 6629 map1 6636 xp1en 6646 endisj 6647 dom0 6661 php5dom 6686 ssfilem 6698 ssfiexmid 6699 domfiexmid 6701 diffitest 6710 ac6sfi 6721 exmidpw 6731 unfiexmid 6735 djuexb 6844 djulclr 6849 djulcl 6851 djulclb 6855 djulf1or 6856 djulf1o 6858 inl11 6865 djuss 6870 1stinl 6874 2ndinl 6875 0ct 6907 finomni 6924 exmidomni 6926 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 dju0en 6974 djucomen 6976 djuassen 6977 xpdjuen 6978 indpi 7051 frecfzennn 10040 fihashen1 10386 hashunlem 10391 zfz1iso 10425 ennnfonelemj0 11706 ennnfonelem0 11710 ennnfonelemhom 11720 strsl0 11789 topgele 11978 en1top 12028 sn0topon 12039 sn0cld 12088 rest0 12130 restsn 12131 0met 12312 djulclALT 12589 bj-d0clsepcl 12708 bj-indint 12714 bj-bdfindis 12730 bj-inf2vnlem1 12753 pw1dom2 12775 pwle2 12779 0nninf 12781 nninfsellemdc 12790 |
Copyright terms: Public domain | W3C validator |