Theorem noel 4284

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 2178, ax-11 2194, and ax-12 2213. (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 2143	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1584	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1830	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4281	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2852	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2739	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 278	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 326	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 492	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1833	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2836	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 326	1 ⊢ ¬ 𝐴 ∈ ∅

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ⊥wfal 1582  ∃wex 1812  [wsb 2099   ∈ wcel 2145  {cab 2738  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-dif 3902  df-nul 4280

This theorem is used by:  nel02  4285  eq0f  4294  eq0ALT  4298  rex0  4308  rab0OLD  4336  un0  4344  in0  4345  0ss  4350  sbcel12  4369  sbcel2  4376  disj  4403  rabsnifsb  4683  uni0  4896  iun0  5020  br0  5154  0xp  5754  xp0  5755  csbxp  5756  dm0  5904  dm0rn0  5908  dm0rn0OLD  5909  reldm0  5912  elimasni  6087  co02  6257  ord0eln0  6414  nlim0  6418  nsuceq0  6443  dffv3  6875  0fv  6920  elfv2ex  6922  mpo0  7499  el2mpocsbcl  8083  bropopvvv  8088  bropfvvvv  8090  tz7.44-2  8397  omordi  8554  nnmordi  8620  omabs  8640  omsmolem  8646  0er  8736  omxpenlem  9077  infn0  9273  en3lp  9594  cantnfle  9651  r1sdom  9757  r1pwss  9767  alephordi  10078  axdc3lem2  10454  zorn2lem7  10505  nlt1pi  10916  xrinf0  13392  elixx3g  13412  elfz2  13569  fzm1  13663  om2uzlti  14015  hashf1lem2  14522  ccatf1  14657  sum0  15808  fsumsplit  15828  sumsplit  15855  fsum2dlem  15857  prod0  16031  fprod2dlem  16068  sadc0  16545  sadcp1  16546  saddisjlem  16555  smu01lem  16576  smu01  16577  smu02  16578  lcmf0  16725  prmreclem5  17013  vdwap0  17069  ram0  17115  0catg  17777  oduclatb  18596  chnccats1  18714  chnccat  18715  0g0  18758  dfgrp2e  19088  cntzrcl  19455  pmtrfrn  19586  psgnunilem5  19622  gexdvds  19712  gsumzsplit  20055  dprdcntz2  20168  00lss  21126  dsmmfi  21952  mplcoe1  22254  mplcoe5  22257  00ply1bas  22465  maducoeval2  22863  madugsum  22866  0ntop  23131  haust1  23578  hauspwdom  23728  kqcldsat  23960  tsmssplit  24379  ustn0  24448  0met  24593  itg11  25920  itg0  26008  bddmulibl  26067  fsumharmonic  27249  ppiublem2  27440  lgsdir2lem3  27564  nulslts  28041  nulsgts  28042  uvtx01vtx  29858  vtxdg0v  29934  dfpth2  30194  0enwwlksnge1  30333  rusgr0edg  30445  clwwlk  30454  eupth2lem1  30699  helloworld  30946  topnfbey  30950  n0lpligALT  30966  isarchi  33623  domnprodeq0  33720  0mplrim  34025  constrmon  34255  measvuni  34726  ddemeas  34748  sibf0  34846  signstfvneq0  35081  opelco3  36355  wsuclem  36403  unbdqndv1  37206  bj-projval  37741  bj-nuliota  37802  bj-0nmoore  37863  nlpineqsn  38163  poimirlem30  38400  pw2f1ocnv  43879  areaquad  44058  onexlimgt  44085  cantnfresb  44166  succlg  44170  oacl2g  44172  omabs2  44174  omcl2  44175  eu0  44361  ntrneikb  44935  r1rankcld  45070  en3lpVD  45668  0elaxnul  45807  omssaxinf2  45812  permaxnul  45832  permaxinf2lem  45836  supminfxr  46293  liminf0  46622  iblempty  46794  stoweidlem34  46863  sge00  47205  vonhoire  47501  prprelprb  48418  fpprbasnn  48646  stgr0  48877  prmringnzring  49253