Theorem noel 4290

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 2175, ax-11 2191, and ax-12 2212. (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 2140	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1583	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1826	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4287	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2854	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2741	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 278	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 326	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 491	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1829	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2838	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 326	1 ⊢ ¬ 𝐴 ∈ ∅

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 400   = wceq 1569  ⊥wfal 1581  ∃wex 1808  [wsb 2095   ∈ wcel 2142  {cab 2740  ∅c0 4285

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3907  df-nul 4286

This theorem is used by:  nel02  4291  eq0f  4300  eq0ALT  4304  rex0  4314  rab0OLD  4342  un0  4350  in0  4351  0ss  4356  sbcel12  4375  sbcel2  4382  disj  4409  rabsnifsb  4687  uni0  4900  iun0  5025  br0  5159  0xp  5759  xp0  5760  csbxp  5761  dm0  5909  dm0rn0  5913  dm0rn0OLD  5914  reldm0  5917  elimasni  6092  co02  6261  ord0eln0  6417  nlim0  6421  nsuceq0  6446  dffv3  6877  0fv  6922  elfv2ex  6924  mpo0  7497  el2mpocsbcl  8078  bropopvvv  8083  bropfvvvv  8085  tz7.44-2  8392  omordi  8549  nnmordi  8615  omabs  8635  omsmolem  8641  0er  8731  omxpenlem  9064  infn0  9260  en3lp  9581  cantnfle  9638  r1sdom  9744  r1pwss  9754  alephordi  10065  axdc3lem2  10441  zorn2lem7  10492  nlt1pi  10897  xrinf0  13371  elixx3g  13391  elfz2  13548  fzm1  13642  om2uzlti  13993  hashf1lem2  14500  sum0  15779  fsumsplit  15799  sumsplit  15826  fsum2dlem  15828  prod0  16004  fprod2dlem  16041  sadc0  16518  sadcp1  16519  saddisjlem  16528  smu01lem  16549  smu01  16550  smu02  16551  lcmf0  16698  prmreclem5  16986  vdwap0  17042  ram0  17088  0catg  17750  oduclatb  18569  chnccats1  18687  chnccat  18688  0g0  18728  dfgrp2e  19036  cntzrcl  19403  pmtrfrn  19534  psgnunilem5  19570  gexdvds  19660  gsumzsplit  20003  dprdcntz2  20116  00lss  21073  dsmmfi  21899  mplcoe1  22199  mplcoe5  22202  00ply1bas  22410  maducoeval2  22808  madugsum  22811  0ntop  23073  haust1  23520  hauspwdom  23669  kqcldsat  23901  tsmssplit  24320  ustn0  24389  0met  24534  itg11  25861  itg0  25950  bddmulibl  26009  fsumharmonic  27187  ppiublem2  27378  lgsdir2lem3  27502  nulslts  27979  nulsgts  27980  uvtx01vtx  29758  vtxdg0v  29834  dfpth2  30089  0enwwlksnge1  30224  rusgr0edg  30336  clwwlk  30345  eupth2lem1  30580  helloworld  30827  topnfbey  30831  n0lpligALT  30847  ccatf1  33278  isarchi  33511  domnprodeq0  33608  0mplrim  33913  constrmon  34143  measvuni  34613  ddemeas  34635  sibf0  34733  signstfvneq0  34968  opelco3  36275  wsuclem  36323  unbdqndv1  37125  bj-projval  37660  bj-nuliota  37721  bj-0nmoore  37782  nlpineqsn  38082  poimirlem30  38329  pw2f1ocnv  43792  areaquad  43971  onexlimgt  43998  cantnfresb  44079  succlg  44083  oacl2g  44085  omabs2  44087  omcl2  44088  eu0  44274  ntrneikb  44848  r1rankcld  44983  en3lpVD  45581  0elaxnul  45720  omssaxinf2  45725  permaxnul  45745  permaxinf2lem  45749  supminfxr  46206  liminf0  46535  iblempty  46707  stoweidlem34  46776  sge00  47118  vonhoire  47414  prprelprb  48294  fpprbasnn  48522  stgr0  48753  prmringnzring  49130