Theorem noel 4290

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 2175, ax-11 2191, and ax-12 2212. (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 2140	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1574	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1817	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4287	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2854	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2741	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 277	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 325	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 490	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1820	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2838	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 325	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1560  ⊥wfal 1572  ∃wex 1799  [wsb 2090   ∈ wcel 2142  {cab 2740  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-dif 3907  df-nul 4286

This theorem is referenced by:  nel02  4291  eq0f  4299  eq0ALT  4303  rex0  4313  rab0OLD  4340  un0  4348  in0  4349  0ss  4354  sbcel12  4365  sbcel2  4372  disj  4404  rabsnifsb  4681  uni0  4894  iun0  5019  br0  5149  0xp  5746  xp0  5747  csbxp  5748  dm0  5896  dm0rn0  5900  dm0rn0OLD  5901  reldm0  5904  elimasni  6080  co02  6248  ord0eln0  6402  nlim0  6406  nsuceq0  6431  dffv3  6863  0fv  6908  elfv2ex  6910  mpo0  7481  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvv  8071  tz7.44-2  8378  omordi  8535  nnmordi  8601  omabs  8621  omsmolem  8627  0er  8717  omxpenlem  9050  infn0  9246  en3lp  9569  cantnfle  9626  r1sdom  9732  r1pwss  9742  alephordi  10030  axdc3lem2  10408  zorn2lem7  10459  nlt1pi  10864  xrinf0  13342  elixx3g  13362  elfz2  13519  fzm1  13612  om2uzlti  13963  hashf1lem2  14469  sum0  15748  fsumsplit  15768  sumsplit  15795  fsum2dlem  15797  prod0  15973  fprod2dlem  16010  sadc0  16488  sadcp1  16489  saddisjlem  16498  smu01lem  16519  smu01  16520  smu02  16521  lcmf0  16668  prmreclem5  16956  vdwap0  17012  ram0  17058  0catg  17720  oduclatb  18539  chnccats1  18657  chnccat  18658  0g0  18698  dfgrp2e  19005  cntzrcl  19367  pmtrfrn  19498  psgnunilem5  19534  gexdvds  19624  gsumzsplit  19967  dprdcntz2  20080  00lss  21008  dsmmfi  21790  mplcoe1  22090  mplcoe5  22093  00ply1bas  22301  maducoeval2  22700  madugsum  22703  0ntop  22965  haust1  23412  hauspwdom  23561  kqcldsat  23793  tsmssplit  24212  ustn0  24281  0met  24426  itg11  25753  itg0  25842  bddmulibl  25901  fsumharmonic  27076  ppiublem2  27267  lgsdir2lem3  27391  nulslts  27868  nulsgts  27869  uvtx01vtx  29598  vtxdg0v  29674  dfpth2  29929  0enwwlksnge1  30064  rusgr0edg  30176  clwwlk  30185  eupth2lem1  30420  helloworld  30667  topnfbey  30671  n0lpligALT  30687  ccatf1  33127  isarchi  33362  domnprodeq0  33460  0mplrim  33811  constrmon  34041  measvuni  34511  ddemeas  34533  sibf0  34631  signstfvneq0  34866  opelco3  36125  wsuclem  36173  unbdqndv1  36946  bj-projval  37481  bj-nuliota  37542  bj-0nmoore  37602  nlpineqsn  37902  poimirlem30  38149  pw2f1ocnv  43614  areaquad  43793  onexlimgt  43820  cantnfresb  43901  succlg  43905  oacl2g  43907  omabs2  43909  omcl2  43910  eu0  44096  ntrneikb  44670  r1rankcld  44807  en3lpVD  45420  0elaxnul  45559  omssaxinf2  45564  permaxnul  45584  permaxinf2lem  45588  supminfxr  46038  liminf0  46367  iblempty  46539  stoweidlem34  46608  sge00  46950  vonhoire  47246  prprelprb  48123  fpprbasnn  48351  stgr0  48582