![]() |
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 2079, ax-11 2093, and ax-12 2106. (Revised by Steven Nguyen, 3-May-2023.) |
Ref | Expression |
---|---|
noel | ⊢ ¬ 𝐴 ∈ ∅ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.24 394 | . . . . . . 7 ⊢ ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) | |
2 | 1 | nex 1763 | . . . . . 6 ⊢ ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) |
3 | df-clab 2759 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)) | |
4 | spsbe 2033 | . . . . . . 7 ⊢ ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)) | |
5 | 3, 4 | sylbi 209 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)) |
6 | 2, 5 | mto 189 | . . . . 5 ⊢ ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} |
7 | df-nul 4181 | . . . . . . 7 ⊢ ∅ = (V ∖ V) | |
8 | df-dif 3834 | . . . . . . 7 ⊢ (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} | |
9 | 7, 8 | eqtri 2802 | . . . . . 6 ⊢ ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} |
10 | 9 | eleq2i 2857 | . . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}) |
11 | 6, 10 | mtbir 315 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ |
12 | 11 | intnan 479 | . . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅) |
13 | 12 | nex 1763 | . 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅) |
14 | dfclel 2847 | . 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)) | |
15 | 13, 14 | mtbir 315 | 1 ⊢ ¬ 𝐴 ∈ ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 387 = wceq 1507 ∃wex 1742 [wsb 2015 ∈ wcel 2050 {cab 2758 Vcvv 3415 ∖ cdif 3828 ∅c0 4180 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-ext 2750 |
This theorem depends on definitions: df-bi 199 df-an 388 df-ex 1743 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-dif 3834 df-nul 4181 |
This theorem is referenced by: n0i 4187 eq0f 4193 rex0 4205 rab0 4225 un0 4232 in0 4233 0ss 4237 sbcel12 4247 sbcel2 4254 disj 4283 r19.2zb 4325 ral0 4340 rabsnifsb 4533 iun0 4852 br0 4979 0xp 5500 csbxp 5501 dm0 5638 dm0rn0 5641 reldm0 5642 elimasni 5798 co02 5954 ord0eln0 6085 nlim0 6089 nsuceq0 6111 dffv3 6497 0fv 6541 elfv2ex 6543 mpo0 7057 el2mpocsbcl 7590 bropopvvv 7595 bropfvvvv 7597 tz7.44-2 7849 omordi 7995 nnmordi 8060 omabs 8076 omsmolem 8082 0er 8128 omxpenlem 8416 en3lp 8873 cantnfle 8930 r1sdom 8999 r1pwss 9009 alephordi 9296 axdc3lem2 9673 zorn2lem7 9724 nlt1pi 10128 xrinf0 12550 elixx3g 12570 elfz2 12718 fzm1 12806 om2uzlti 13136 hashf1lem2 13630 sum0 14941 fsumsplit 14960 sumsplit 14986 fsum2dlem 14988 prod0 15160 fprod2dlem 15197 sadc0 15666 sadcp1 15667 saddisjlem 15676 smu01lem 15697 smu01 15698 smu02 15699 lcmf0 15837 prmreclem5 16115 vdwap0 16171 ram0 16217 0catg 16819 oduclatb 17615 0g0 17734 dfgrp2e 17920 cntzrcl 18231 pmtrfrn 18350 psgnunilem5 18386 psgnunilem5OLD 18387 gexdvds 18473 gsumzsplit 18803 dprdcntz2 18913 00lss 19438 mplcoe1 19962 mplcoe5 19965 00ply1bas 20114 dsmmbas2 20586 dsmmfi 20587 maducoeval2 20956 madugsum 20959 0ntop 21220 haust1 21667 hauspwdom 21816 kqcldsat 22048 tsmssplit 22466 ustn0 22535 0met 22682 itg11 23998 itg0 24086 bddmulibl 24145 fsumharmonic 25294 ppiublem2 25484 lgsdir2lem3 25608 uvtx01vtx 26885 vtxdg0v 26961 0enwwlksnge1 27353 rusgr0edg 27482 clwwlk 27492 eupth2lem1 27751 helloworld 28024 topnfbey 28028 n0lpligALT 28041 isarchi 30477 measvuni 31118 ddemeas 31140 sibf0 31237 signstfvneq0 31489 opelco3 32538 wsuclem 32633 unbdqndv1 33367 bj-projval 33826 bj-df-nul 33859 bj-nuliota 33861 bj-0nmoore 33915 nlpineqsn 34130 poimirlem30 34363 nel02 35027 pw2f1ocnv 39030 areaquad 39219 ntrneikb 39807 r1rankcld 39942 en3lpVD 40598 supminfxr 41172 liminf0 41506 iblempty 41681 stoweidlem34 41751 sge00 42090 vonhoire 42386 prprelprb 43048 fpprbasnn 43263 |
Copyright terms: Public domain | W3C validator |