Theorem noel 4266

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 2152, ax-11 2168, and ax-12 2189. (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 2117	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1561	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1804	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4263	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2831	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2718	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 276	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 324	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 487	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1807	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2815	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 324	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1547  ⊥wfal 1559  ∃wex 1786  [wsb 2073   ∈ wcel 2119  {cab 2717  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-dif 3886  df-nul 4262

This theorem is referenced by:  nel02  4267  eq0f  4275  eq0ALT  4279  rex0  4288  rab0  4314  un0  4322  in0  4323  0ss  4328  sbcel12  4339  sbcel2  4346  disj  4378  rabsnifsb  4654  uni0  4866  iun0  4991  br0  5121  0xp  5717  xp0  5718  csbxp  5719  dm0  5862  dm0rn0  5866  dm0rn0OLD  5867  reldm0  5870  elimasni  6043  co02  6212  ord0eln0  6366  nlim0  6370  nsuceq0  6395  dffv3  6823  0fv  6868  elfv2ex  6870  mpo0  7441  el2mpocsbcl  8024  bropopvvv  8029  bropfvvvv  8031  tz7.44-2  8336  omordi  8491  nnmordi  8557  omabs  8577  omsmolem  8583  0er  8672  omxpenlem  9006  infn0  9202  en3lp  9526  cantnfle  9583  r1sdom  9689  r1pwss  9699  alephordi  9987  axdc3lem2  10364  zorn2lem7  10415  nlt1pi  10820  xrinf0  13282  elixx3g  13302  elfz2  13459  fzm1  13552  om2uzlti  13903  hashf1lem2  14409  sum0  15674  fsumsplit  15694  sumsplit  15721  fsum2dlem  15723  prod0  15899  fprod2dlem  15936  sadc0  16414  sadcp1  16415  saddisjlem  16424  smu01lem  16445  smu01  16446  smu02  16447  lcmf0  16594  prmreclem5  16882  vdwap0  16938  ram0  16984  0catg  17645  oduclatb  18464  chnccats1  18582  chnccat  18583  0g0  18623  dfgrp2e  18930  cntzrcl  19293  pmtrfrn  19424  psgnunilem5  19460  gexdvds  19550  gsumzsplit  19893  dprdcntz2  20006  00lss  20931  dsmmfi  21713  mplcoe1  22013  mplcoe5  22016  00ply1bas  22224  maducoeval2  22623  madugsum  22626  0ntop  22888  haust1  23335  hauspwdom  23484  kqcldsat  23716  tsmssplit  24135  ustn0  24204  0met  24349  itg11  25676  itg0  25765  bddmulibl  25824  fsumharmonic  26993  ppiublem2  27184  lgsdir2lem3  27308  nulslts  27785  nulsgts  27786  uvtx01vtx  29484  vtxdg0v  29560  dfpth2  29815  0enwwlksnge1  29950  rusgr0edg  30062  clwwlk  30071  eupth2lem1  30306  helloworld  30553  topnfbey  30557  n0lpligALT  30573  ccatf1  33028  isarchi  33263  domnprodeq0  33357  0mplrim  33698  constrmon  33928  measvuni  34398  ddemeas  34420  sibf0  34518  signstfvneq0  34756  opelco3  36003  wsuclem  36051  unbdqndv1  36814  bj-projval  37349  bj-nuliota  37410  bj-0nmoore  37470  nlpineqsn  37770  poimirlem30  38017  pw2f1ocnv  43482  areaquad  43661  onexlimgt  43688  cantnfresb  43769  succlg  43773  oacl2g  43775  omabs2  43777  omcl2  43778  eu0  43964  ntrneikb  44538  r1rankcld  44675  en3lpVD  45288  0elaxnul  45427  omssaxinf2  45432  permaxnul  45452  permaxinf2lem  45456  supminfxr  45907  liminf0  46236  iblempty  46408  stoweidlem34  46477  sge00  46819  vonhoire  47115  prprelprb  47992  fpprbasnn  48220  stgr0  48451