Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > noel | Structured version Visualization version GIF version |
Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Mario Carneiro, 1-Sep-2015.) Remove dependency on ax-10 2136, ax-11 2151, and ax-12 2167. (Revised by Steven Nguyen, 3-May-2023.) |
Ref | Expression |
---|---|
noel | ⊢ ¬ 𝐴 ∈ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.24 403 | . . . . . . 7 ⊢ ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) | |
2 | 1 | nex 1792 | . . . . . 6 ⊢ ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) |
3 | df-clab 2797 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)) | |
4 | spsbe 2079 | . . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)) | |
5 | 3, 4 | sylbi 218 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)) |
6 | 2, 5 | mto 198 | . . . . 5 ⊢ ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} |
7 | df-nul 4289 | . . . . . . 7 ⊢ ∅ = (V ∖ V) | |
8 | df-dif 3936 | . . . . . . 7 ⊢ (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} | |
9 | 7, 8 | eqtri 2841 | . . . . . 6 ⊢ ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} |
10 | 9 | eleq2i 2901 | . . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}) |
11 | 6, 10 | mtbir 324 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ |
12 | 11 | intnan 487 | . . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅) |
13 | 12 | nex 1792 | . 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅) |
14 | dfclel 2891 | . 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)) | |
15 | 13, 14 | mtbir 324 | 1 ⊢ ¬ 𝐴 ∈ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 396 = wceq 1528 ∃wex 1771 [wsb 2060 ∈ wcel 2105 {cab 2796 Vcvv 3492 ∖ cdif 3930 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-dif 3936 df-nul 4289 |
This theorem is referenced by: nel02 4295 n0i 4296 eq0f 4302 rex0 4314 rab0 4334 un0 4341 in0 4342 0ss 4347 sbcel12 4357 sbcel2 4364 disj 4395 r19.2zb 4437 ral0 4452 rabsnifsb 4650 iun0 4976 br0 5106 0xp 5642 csbxp 5643 dm0 5783 dm0rn0 5788 reldm0 5791 elimasni 5949 co02 6106 ord0eln0 6238 nlim0 6242 nsuceq0 6264 dffv3 6659 0fv 6702 elfv2ex 6704 mpo0 7228 el2mpocsbcl 7769 bropopvvv 7774 bropfvvvv 7776 tz7.44-2 8032 omordi 8181 nnmordi 8246 omabs 8263 omsmolem 8269 0er 8315 omxpenlem 8606 en3lp 9065 cantnfle 9122 r1sdom 9191 r1pwss 9201 alephordi 9488 axdc3lem2 9861 zorn2lem7 9912 nlt1pi 10316 xrinf0 12719 elixx3g 12739 elfz2 12887 fzm1 12975 om2uzlti 13306 hashf1lem2 13802 sum0 15066 fsumsplit 15085 sumsplit 15111 fsum2dlem 15113 prod0 15285 fprod2dlem 15322 sadc0 15791 sadcp1 15792 saddisjlem 15801 smu01lem 15822 smu01 15823 smu02 15824 lcmf0 15966 prmreclem5 16244 vdwap0 16300 ram0 16346 0catg 16946 oduclatb 17742 0g0 17862 dfgrp2e 18067 cntzrcl 18395 pmtrfrn 18515 psgnunilem5 18551 gexdvds 18638 gsumzsplit 18976 dprdcntz2 19089 00lss 19642 mplcoe1 20174 mplcoe5 20177 00ply1bas 20336 dsmmfi 20810 maducoeval2 21177 madugsum 21180 0ntop 21441 haust1 21888 hauspwdom 22037 kqcldsat 22269 tsmssplit 22687 ustn0 22756 0met 22903 itg11 24219 itg0 24307 bddmulibl 24366 fsumharmonic 25516 ppiublem2 25706 lgsdir2lem3 25830 uvtx01vtx 27106 vtxdg0v 27182 0enwwlksnge1 27569 rusgr0edg 27679 clwwlk 27688 eupth2lem1 27924 helloworld 28171 topnfbey 28175 n0lpligALT 28188 ccatf1 30552 isarchi 30738 measvuni 31372 ddemeas 31394 sibf0 31491 signstfvneq0 31741 opelco3 32915 wsuclem 33009 unbdqndv1 33744 bj-projval 34205 bj-df-nul 34242 bj-nuliota 34244 bj-0nmoore 34298 nlpineqsn 34571 poimirlem30 34803 pw2f1ocnv 39512 areaquad 39701 eu0 39764 ntrneikb 40322 r1rankcld 40444 en3lpVD 41056 supminfxr 41616 liminf0 41950 iblempty 42126 stoweidlem34 42196 sge00 42535 vonhoire 42831 prprelprb 43556 fpprbasnn 43771 |
Copyright terms: Public domain | W3C validator |