Theorem noel 4279

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 4276	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2829	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2716	. . . . . 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 2813	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-dif 3893  df-nul 4275

This theorem is referenced by:  nel02  4280  eq0f  4288  eq0ALT  4292  rex0  4301  rab0  4327  un0  4335  in0  4336  0ss  4341  sbcel12  4352  sbcel2  4359  disj  4391  rabsnifsb  4667  uni0  4879  iun0  5005  br0  5135  0xp  5724  xp0  5725  csbxp  5726  dm0  5870  dm0rn0  5874  dm0rn0OLD  5875  reldm0  5878  elimasni  6051  co02  6220  ord0eln0  6374  nlim0  6378  nsuceq0  6403  dffv3  6831  0fv  6876  elfv2ex  6878  mpo0  7446  el2mpocsbcl  8029  bropopvvv  8034  bropfvvvv  8036  tz7.44-2  8340  omordi  8495  nnmordi  8561  omabs  8581  omsmolem  8587  0er  8676  omxpenlem  9010  infn0  9206  en3lp  9529  cantnfle  9586  r1sdom  9692  r1pwss  9702  alephordi  9990  axdc3lem2  10367  zorn2lem7  10418  nlt1pi  10823  xrinf0  13285  elixx3g  13305  elfz2  13462  fzm1  13555  om2uzlti  13906  hashf1lem2  14412  sum0  15677  fsumsplit  15697  sumsplit  15724  fsum2dlem  15726  prod0  15902  fprod2dlem  15939  sadc0  16417  sadcp1  16418  saddisjlem  16427  smu01lem  16448  smu01  16449  smu02  16450  lcmf0  16597  prmreclem5  16885  vdwap0  16941  ram0  16987  0catg  17648  oduclatb  18467  chnccats1  18585  chnccat  18586  0g0  18626  dfgrp2e  18933  cntzrcl  19296  pmtrfrn  19427  psgnunilem5  19463  gexdvds  19553  gsumzsplit  19896  dprdcntz2  20009  00lss  20930  dsmmfi  21731  mplcoe1  22028  mplcoe5  22031  00ply1bas  22216  maducoeval2  22618  madugsum  22621  0ntop  22883  haust1  23330  hauspwdom  23479  kqcldsat  23711  tsmssplit  24130  ustn0  24199  0met  24344  itg11  25671  itg0  25760  bddmulibl  25819  fsumharmonic  26992  ppiublem2  27183  lgsdir2lem3  27307  nulslts  27784  nulsgts  27785  uvtx01vtx  29483  vtxdg0v  29560  dfpth2  29815  0enwwlksnge1  29950  rusgr0edg  30062  clwwlk  30071  eupth2lem1  30306  helloworld  30553  topnfbey  30557  n0lpligALT  30573  ccatf1  33027  isarchi  33261  domnprodeq0  33355  constrmon  33907  measvuni  34377  ddemeas  34399  sibf0  34497  signstfvneq0  34735  opelco3  35976  wsuclem  36024  unbdqndv1  36787  bj-projval  37322  bj-nuliota  37383  bj-0nmoore  37443  nlpineqsn  37741  poimirlem30  37988  pw2f1ocnv  43486  areaquad  43665  onexlimgt  43692  cantnfresb  43773  succlg  43777  oacl2g  43779  omabs2  43781  omcl2  43782  eu0  43968  ntrneikb  44542  r1rankcld  44679  en3lpVD  45292  0elaxnul  45431  omssaxinf2  45436  permaxnul  45456  permaxinf2lem  45460  supminfxr  45913  liminf0  46242  iblempty  46414  stoweidlem34  46483  sge00  46825  vonhoire  47121  prprelprb  47992  fpprbasnn  48220  stgr0  48451