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 2853	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2740	. . . . . 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 2837	. 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 2739  ∅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 2733

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 2740  df-cleq 2753  df-clel 2836  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  5750  xp0  5751  csbxp  5752  dm0  5902  dm0rn0  5906  dm0rn0OLD  5907  reldm0  5910  elimasni  6089  co02  6262  ord0eln0  6419  nlim0  6423  nsuceq0  6448  dffv3  6881  0fv  6926  elfv2ex  6928  mpo0  7505  el2mpocsbcl  8096  bropopvvv  8101  bropfvvvv  8103  tz7.44-2  8415  omordi  8574  nnmordi  8640  omabs  8660  omsmolem  8666  0er  8756  omxpenlem  9097  infn0  9294  en3lp  9615  cantnfle  9672  r1sdom  9781  r1pwss  9791  alephordi  10153  axdc3lem2  10529  zorn2lem7  10580  nlt1pi  10991  xrinf0  13469  elixx3g  13489  elfz2  13646  fzm1  13741  om2uzlti  14093  hashf1lem2  14601  ccatf1  14736  sum0  15887  fsumsplit  15907  sumsplit  15934  fsum2dlem  15936  prod0  16110  fprod2dlem  16147  sadc0  16624  sadcp1  16625  saddisjlem  16634  smu01lem  16655  smu01  16656  smu02  16657  lcmf0  16809  prmreclem5  17098  vdwap0  17154  ram0  17200  0catg  17862  oduclatb  18681  chnccats1  18799  chnccat  18800  0g0  18844  dfgrp2e  19174  cntzrcl  19541  pmtrfrn  19672  psgnunilem5  19708  gexdvds  19798  gsumzsplit  20141  dprdcntz2  20254  00lss  21216  dsmmfi  22044  mplcoe1  22346  mplcoe5  22349  00ply1bas  22557  maducoeval2  22955  madugsum  22958  0ntop  23223  haust1  23670  hauspwdom  23820  kqcldsat  24052  tsmssplit  24471  ustn0  24540  0met  24685  itg11  26012  itg0  26100  bddmulibl  26159  fsumharmonic  27339  ppiublem2  27530  lgsdir2lem3  27654  nulslts  28161  nulsgts  28162  uvtx01vtx  29978  vtxdg0v  30054  dfpth2  30314  0enwwlksnge1  30453  rusgr0edg  30565  clwwlk  30574  eupth2lem1  30819  helloworld  31066  topnfbey  31070  n0lpligALT  31086  isarchi  33743  domnprodeq0  33840  0mplrim  34146  constrmon  34376  measvuni  34847  ddemeas  34869  sibf0  34966  signstfvneq0  35201  opelco3  36539  wsuclem  36587  unbdqndv1  37374  bj-projval  37909  bj-nuliota  37972  bj-0nmoore  38033  nlpineqsn  38331  poimirlem30  38568  pw2f1ocnv  44043  areaquad  44217  onexlimgt  44244  cantnfresb  44325  succlg  44329  oacl2g  44331  omabs2  44333  omcl2  44334  eu0  44520  ntrneikb  45093  r1rankcld  45228  en3lpVD  45826  0elaxnul  45972  omssaxinf2  45977  permaxnul  45997  permaxinf2lem  46001  supminfxr  46473  liminf0  46802  iblempty  46974  stoweidlem34  47043  sge00  47385  vonhoire  47681  prprelprb  48598  fpprbasnn  48826  stgr0  49057  prmringnzring  49433