Theorem noel 4278

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 2147, ax-11 2163, and ax-12 2185. (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 2112	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1556	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1799	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4275	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2828	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2715	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1802	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2812	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1542  ⊥wfal 1554  ∃wex 1781  [wsb 2068   ∈ wcel 2114  {cab 2714  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3892  df-nul 4274

This theorem is referenced by:  nel02  4279  eq0f  4287  eq0ALT  4291  rex0  4300  rab0  4326  un0  4334  in0  4335  0ss  4340  sbcel12  4351  sbcel2  4358  disj  4390  rabsnifsb  4666  uni0  4878  iun0  5004  br0  5134  0xp  5730  xp0  5731  csbxp  5732  dm0  5875  dm0rn0  5879  dm0rn0OLD  5880  reldm0  5883  elimasni  6056  co02  6225  ord0eln0  6379  nlim0  6383  nsuceq0  6408  dffv3  6836  0fv  6881  elfv2ex  6883  mpo0  7452  el2mpocsbcl  8035  bropopvvv  8040  bropfvvvv  8042  tz7.44-2  8346  omordi  8501  nnmordi  8567  omabs  8587  omsmolem  8593  0er  8682  omxpenlem  9016  infn0  9212  en3lp  9535  cantnfle  9592  r1sdom  9698  r1pwss  9708  alephordi  9996  axdc3lem2  10373  zorn2lem7  10424  nlt1pi  10829  xrinf0  13291  elixx3g  13311  elfz2  13468  fzm1  13561  om2uzlti  13912  hashf1lem2  14418  sum0  15683  fsumsplit  15703  sumsplit  15730  fsum2dlem  15732  prod0  15908  fprod2dlem  15945  sadc0  16423  sadcp1  16424  saddisjlem  16433  smu01lem  16454  smu01  16455  smu02  16456  lcmf0  16603  prmreclem5  16891  vdwap0  16947  ram0  16993  0catg  17654  oduclatb  18473  chnccats1  18591  chnccat  18592  0g0  18632  dfgrp2e  18939  cntzrcl  19302  pmtrfrn  19433  psgnunilem5  19469  gexdvds  19559  gsumzsplit  19902  dprdcntz2  20015  00lss  20936  dsmmfi  21718  mplcoe1  22015  mplcoe5  22018  00ply1bas  22203  maducoeval2  22605  madugsum  22608  0ntop  22870  haust1  23317  hauspwdom  23466  kqcldsat  23698  tsmssplit  24117  ustn0  24186  0met  24331  itg11  25658  itg0  25747  bddmulibl  25806  fsumharmonic  26975  ppiublem2  27166  lgsdir2lem3  27290  nulslts  27767  nulsgts  27768  uvtx01vtx  29466  vtxdg0v  29542  dfpth2  29797  0enwwlksnge1  29932  rusgr0edg  30044  clwwlk  30053  eupth2lem1  30288  helloworld  30535  topnfbey  30539  n0lpligALT  30555  ccatf1  33009  isarchi  33243  domnprodeq0  33337  constrmon  33888  measvuni  34358  ddemeas  34380  sibf0  34478  signstfvneq0  34716  opelco3  35957  wsuclem  36005  unbdqndv1  36768  bj-projval  37303  bj-nuliota  37364  bj-0nmoore  37424  nlpineqsn  37724  poimirlem30  37971  pw2f1ocnv  43465  areaquad  43644  onexlimgt  43671  cantnfresb  43752  succlg  43756  oacl2g  43758  omabs2  43760  omcl2  43761  eu0  43947  ntrneikb  44521  r1rankcld  44658  en3lpVD  45271  0elaxnul  45410  omssaxinf2  45415  permaxnul  45435  permaxinf2lem  45439  supminfxr  45892  liminf0  46221  iblempty  46393  stoweidlem34  46462  sge00  46804  vonhoire  47100  prprelprb  47977  fpprbasnn  48205  stgr0  48436