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  32891  chnccats1  32958  isarchi  33125  constrmon  33717  measvuni  34187  ddemeas  34209  sibf0  34308  signstfvneq0  34546  opelco3  35758  wsuclem  35809  unbdqndv1  36492  bj-projval  36980  bj-nuliota  37041  bj-0nmoore  37096  nlpineqsn  37392  poimirlem30  37640  pw2f1ocnv  43020  areaquad  43199  onexlimgt  43226  cantnfresb  43307  succlg  43311  oacl2g  43313  omabs2  43315  omcl2  43316  eu0  43503  ntrneikb  44077  r1rankcld  44214  en3lpVD  44828  0elaxnul  44967  omssaxinf2  44972  permaxnul  44992  permaxinf2lem  44996  supminfxr  45453  liminf0  45784  iblempty  45956  stoweidlem34  46025  sge00  46367  vonhoire  46663  prprelprb  47511  fpprbasnn  47723  stgr0  47954