![]() |
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 3912. (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 3912 | . . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥 | |
2 | eq0 3273 | . . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥) | |
3 | 2 | exbii 1537 | . . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥) |
4 | 1, 3 | mpbir 144 | . 2 ⊢ ∃𝑥 𝑥 = ∅ |
5 | 4 | issetri 2609 | 1 ⊢ ∅ ∈ V |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 ∀wal 1283 = wceq 1285 ∃wex 1422 ∈ wcel 1434 Vcvv 2602 ∅c0 3258 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-nul 3912 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1687 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-v 2604 df-dif 2976 df-nul 3259 |
This theorem is referenced by: 0elpw 3946 0nep0 3947 iin0r 3951 intv 3952 snexprc 3966 p0ex 3967 0elon 4155 onm 4164 ordtriexmidlem2 4272 ordtriexmid 4273 ordtri2orexmid 4274 ontr2exmid 4276 onsucsssucexmid 4278 onsucelsucexmidlem1 4279 onsucelsucexmid 4281 regexmidlem1 4284 reg2exmidlema 4285 ordsoexmid 4313 0elsucexmid 4316 ordpwsucexmid 4321 ordtri2or2exmid 4322 peano1 4343 finds 4349 finds2 4350 0elnn 4366 opthprc 4417 nfunv 4963 fun0 4988 acexmidlema 5534 acexmidlemb 5535 acexmidlemab 5537 ovprc 5571 1st0 5802 2nd0 5803 brtpos0 5901 reldmtpos 5902 tfr0dm 5971 rdg0 6036 frec0g 6046 1n0 6080 el1o 6084 fnom 6094 omexg 6095 om0 6102 nnsucsssuc 6136 en0 6342 ensn1 6343 en1 6346 2dom 6352 xp1en 6367 endisj 6368 php5dom 6398 ssfilem 6410 ssfiexmid 6411 domfiexmid 6413 diffitest 6421 ac6sfi 6431 unfiexmid 6438 indpi 6594 frecfzennn 9508 sizeen1 9823 sizeunlem 9828 bj-d0clsepcl 10878 bj-indint 10884 bj-bdfindis 10900 bj-inf2vnlem1 10923 |
Copyright terms: Public domain | W3C validator |