Theorem noel 4289

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 2142, ax-11 2158, and ax-12 2178. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.)

Assertion

Ref	Expression
noel	⊢ ¬ 𝐴 ∈ ∅

Proof of Theorem noel

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nsb 2107	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1554	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1797	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4286	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2820	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2708	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1800	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2804	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540  ⊥wfal 1552  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2707  ∅c0 4284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3906  df-nul 4285

This theorem is referenced by:  nel02  4290  n0i  4291  eq0f  4298  eq0ALT  4302  rex0  4311  rab0  4337  un0  4345  in0  4346  0ss  4351  sbcel12  4362  sbcel2  4369  disj  4401  r19.2zb  4447  rabsnifsb  4674  iun0  5011  br0  5141  0xp  5718  csbxp  5719  dm0  5863  dm0rn0  5867  reldm0  5870  elimasni  6042  co02  6209  ord0eln0  6363  nlim0  6367  nsuceq0  6392  dffv3  6818  0fv  6864  elfv2ex  6866  mpo0  7434  el2mpocsbcl  8018  bropopvvv  8023  bropfvvvv  8025  tz7.44-2  8329  omordi  8484  nnmordi  8549  omabs  8569  omsmolem  8575  0er  8663  omxpenlem  8995  infn0  9191  en3lp  9510  cantnfle  9567  r1sdom  9670  r1pwss  9680  alephordi  9968  axdc3lem2  10345  zorn2lem7  10396  nlt1pi  10800  xrinf0  13241  elixx3g  13261  elfz2  13417  fzm1  13510  om2uzlti  13857  hashf1lem2  14363  sum0  15628  fsumsplit  15648  sumsplit  15675  fsum2dlem  15677  prod0  15850  fprod2dlem  15887  sadc0  16365  sadcp1  16366  saddisjlem  16375  smu01lem  16396  smu01  16397  smu02  16398  lcmf0  16545  prmreclem5  16832  vdwap0  16888  ram0  16934  0catg  17594  oduclatb  18413  0g0  18538  dfgrp2e  18842  cntzrcl  19206  pmtrfrn  19337  psgnunilem5  19373  gexdvds  19463  gsumzsplit  19806  dprdcntz2  19919  00lss  20844  dsmmfi  21645  mplcoe1  21942  mplcoe5  21945  00ply1bas  22122  maducoeval2  22525  madugsum  22528  0ntop  22790  haust1  23237  hauspwdom  23386  kqcldsat  23618  tsmssplit  24037  ustn0  24106  0met  24252  itg11  25590  itg0  25679  bddmulibl  25738  fsumharmonic  26920  ppiublem2  27112  lgsdir2lem3  27236  nulsslt  27708  nulssgt  27709  uvtx01vtx  29342  vtxdg0v  29419  dfpth2  29674  0enwwlksnge1  29809  rusgr0edg  29918  clwwlk  29927  eupth2lem1  30162  helloworld  30409  topnfbey  30413  n0lpligALT  30428  ccatf1  32890  chnccats1  32957  isarchi  33124  constrmon  33711  measvuni  34181  ddemeas  34203  sibf0  34302  signstfvneq0  34540  opelco3  35748  wsuclem  35799  unbdqndv1  36482  bj-projval  36970  bj-nuliota  37031  bj-0nmoore  37086  nlpineqsn  37382  poimirlem30  37630  pw2f1ocnv  43010  areaquad  43189  onexlimgt  43216  cantnfresb  43297  succlg  43301  oacl2g  43303  omabs2  43305  omcl2  43306  eu0  43493  ntrneikb  44067  r1rankcld  44204  en3lpVD  44818  0elaxnul  44957  omssaxinf2  44962  permaxnul  44982  permaxinf2lem  44986  supminfxr  45443  liminf0  45774  iblempty  45946  stoweidlem34  46015  sge00  46357  vonhoire  46653  prprelprb  47501  fpprbasnn  47713  stgr0  47944