Theorem noel 4297

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 2142, ax-11 2158, and ax-12 2178. (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 2107	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1554	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1797	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4294	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2820	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2708	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1800	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2804	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540  ⊥wfal 1552  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2707  ∅c0 4292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-dif 3914  df-nul 4293

This theorem is referenced by:  nel02  4298  n0i  4299  eq0f  4306  eq0ALT  4310  rex0  4319  rab0  4345  un0  4353  in0  4354  0ss  4359  sbcel12  4370  sbcel2  4377  disj  4409  r19.2zb  4455  rabsnifsb  4682  iun0  5021  br0  5151  0xp  5729  csbxp  5730  dm0  5874  dm0rn0  5878  reldm0  5881  elimasni  6051  co02  6221  ord0eln0  6376  nlim0  6380  nsuceq0  6405  dffv3  6836  0fv  6884  elfv2ex  6886  mpo0  7454  el2mpocsbcl  8041  bropopvvv  8046  bropfvvvv  8048  tz7.44-2  8352  omordi  8507  nnmordi  8572  omabs  8592  omsmolem  8598  0er  8686  omxpenlem  9019  infn0  9227  en3lp  9543  cantnfle  9600  r1sdom  9703  r1pwss  9713  alephordi  10003  axdc3lem2  10380  zorn2lem7  10431  nlt1pi  10835  xrinf0  13275  elixx3g  13295  elfz2  13451  fzm1  13544  om2uzlti  13891  hashf1lem2  14397  sum0  15663  fsumsplit  15683  sumsplit  15710  fsum2dlem  15712  prod0  15885  fprod2dlem  15922  sadc0  16400  sadcp1  16401  saddisjlem  16410  smu01lem  16431  smu01  16432  smu02  16433  lcmf0  16580  prmreclem5  16867  vdwap0  16923  ram0  16969  0catg  17629  oduclatb  18448  0g0  18573  dfgrp2e  18877  cntzrcl  19241  pmtrfrn  19372  psgnunilem5  19408  gexdvds  19498  gsumzsplit  19841  dprdcntz2  19954  00lss  20879  dsmmfi  21680  mplcoe1  21977  mplcoe5  21980  00ply1bas  22157  maducoeval2  22560  madugsum  22563  0ntop  22825  haust1  23272  hauspwdom  23421  kqcldsat  23653  tsmssplit  24072  ustn0  24141  0met  24287  itg11  25625  itg0  25714  bddmulibl  25773  fsumharmonic  26955  ppiublem2  27147  lgsdir2lem3  27271  nulsslt  27743  nulssgt  27744  uvtx01vtx  29377  vtxdg0v  29454  dfpth2  29709  0enwwlksnge1  29844  rusgr0edg  29953  clwwlk  29962  eupth2lem1  30197  helloworld  30444  topnfbey  30448  n0lpligALT  30463  ccatf1  32920  chnccats1  32987  isarchi  33151  constrmon  33727  measvuni  34197  ddemeas  34219  sibf0  34318  signstfvneq0  34556  opelco3  35755  wsuclem  35806  unbdqndv1  36489  bj-projval  36977  bj-nuliota  37038  bj-0nmoore  37093  nlpineqsn  37389  poimirlem30  37637  pw2f1ocnv  43019  areaquad  43198  onexlimgt  43225  cantnfresb  43306  succlg  43310  oacl2g  43312  omabs2  43314  omcl2  43315  eu0  43502  ntrneikb  44076  r1rankcld  44213  en3lpVD  44827  0elaxnul  44966  omssaxinf2  44971  permaxnul  44991  permaxinf2lem  44995  supminfxr  45453  liminf0  45784  iblempty  45956  stoweidlem34  46025  sge00  46367  vonhoire  46663  prprelprb  47511  fpprbasnn  47723  stgr0  47952