![]() |
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 2129, ax-11 2146, and ax-12 2166. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) |
Ref | Expression |
---|---|
noel | ⊢ ¬ 𝐴 ∈ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nsb 2096 | . . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥) | |
2 | fal 1547 | . . . . . 6 ⊢ ¬ ⊥ | |
3 | 1, 2 | mpg 1791 | . . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥ |
4 | dfnul4 4324 | . . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥} | |
5 | 4 | eleq2i 2817 | . . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) |
6 | df-clab 2703 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
7 | 5, 6 | bitri 274 | . . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥) |
8 | 3, 7 | mtbir 322 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ |
9 | 8 | intnan 485 | . . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅) |
10 | 9 | nex 1794 | . 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅) |
11 | dfclel 2803 | . 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)) | |
12 | 10, 11 | mtbir 322 | 1 ⊢ ¬ 𝐴 ∈ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 394 = wceq 1533 ⊥wfal 1545 ∃wex 1773 [wsb 2059 ∈ wcel 2098 {cab 2702 ∅c0 4322 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-dif 3947 df-nul 4323 |
This theorem is referenced by: nel02 4332 n0i 4333 eq0f 4340 eq0ALT 4344 rex0 4357 rab0 4384 un0 4392 in0 4393 0ss 4398 sbcel12 4410 sbcel2 4417 disj 4449 disjOLD 4450 r19.2zb 4497 ral0OLD 4518 rabsnifsb 4728 iun0 5066 br0 5198 0xp 5776 csbxp 5777 dm0 5923 dm0rn0 5927 reldm0 5930 elimasni 6096 co02 6266 ord0eln0 6426 nlim0 6430 nsuceq0 6454 dffv3 6892 0fv 6940 elfv2ex 6942 mpo0 7505 el2mpocsbcl 8090 bropopvvv 8095 bropfvvvv 8097 tz7.44-2 8428 omordi 8587 nnmordi 8652 omabs 8672 omsmolem 8678 0er 8762 omxpenlem 9101 infn0 9335 en3lp 9644 cantnfle 9701 r1sdom 9804 r1pwss 9814 alephordi 10104 axdc3lem2 10481 zorn2lem7 10532 nlt1pi 10936 xrinf0 13357 elixx3g 13377 elfz2 13531 fzm1 13621 om2uzlti 13956 hashf1lem2 14458 sum0 15708 fsumsplit 15728 sumsplit 15755 fsum2dlem 15757 prod0 15928 fprod2dlem 15965 sadc0 16437 sadcp1 16438 saddisjlem 16447 smu01lem 16468 smu01 16469 smu02 16470 lcmf0 16613 prmreclem5 16897 vdwap0 16953 ram0 16999 0catg 17676 oduclatb 18507 0g0 18632 dfgrp2e 18933 cntzrcl 19295 pmtrfrn 19430 psgnunilem5 19466 gexdvds 19556 gsumzsplit 19899 dprdcntz2 20012 00lss 20842 dsmmfi 21694 mplcoe1 22002 mplcoe5 22005 00ply1bas 22187 maducoeval2 22591 madugsum 22594 0ntop 22856 haust1 23305 hauspwdom 23454 kqcldsat 23686 tsmssplit 24105 ustn0 24174 0met 24321 itg11 25669 itg0 25758 bddmulibl 25817 fsumharmonic 26994 ppiublem2 27186 lgsdir2lem3 27310 nulsslt 27781 nulssgt 27782 uvtx01vtx 29287 vtxdg0v 29364 0enwwlksnge1 29752 rusgr0edg 29861 clwwlk 29870 eupth2lem1 30105 helloworld 30352 topnfbey 30356 n0lpligALT 30371 ccatf1 32764 isarchi 32987 measvuni 33966 ddemeas 33988 sibf0 34087 signstfvneq0 34337 opelco3 35503 wsuclem 35554 unbdqndv1 36116 bj-projval 36608 bj-nuliota 36669 bj-0nmoore 36724 nlpineqsn 37020 poimirlem30 37256 pw2f1ocnv 42602 areaquad 42788 onexlimgt 42815 cantnfresb 42897 succlg 42901 oacl2g 42903 omabs2 42905 omcl2 42906 eu0 43094 ntrneikb 43668 r1rankcld 43812 en3lpVD 44428 supminfxr 44986 liminf0 45321 iblempty 45493 stoweidlem34 45562 sge00 45904 vonhoire 46200 prprelprb 46996 fpprbasnn 47208 |
Copyright terms: Public domain | W3C validator |