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  17625  oduclatb  18442  0g0  18567  dfgrp2e  18871  cntzrcl  19235  pmtrfrn  19364  psgnunilem5  19400  gexdvds  19490  gsumzsplit  19833  dprdcntz2  19946  00lss  20823  dsmmfi  21623  mplcoe1  21920  mplcoe5  21923  00ply1bas  22100  maducoeval2  22503  madugsum  22506  0ntop  22768  haust1  23215  hauspwdom  23364  kqcldsat  23596  tsmssplit  24015  ustn0  24084  0met  24230  itg11  25568  itg0  25657  bddmulibl  25716  fsumharmonic  26898  ppiublem2  27090  lgsdir2lem3  27214  nulsslt  27685  nulssgt  27686  uvtx01vtx  29300  vtxdg0v  29377  dfpth2  29632  0enwwlksnge1  29767  rusgr0edg  29876  clwwlk  29885  eupth2lem1  30120  helloworld  30367  topnfbey  30371  n0lpligALT  30386  ccatf1  32843  chnccats1  32914  isarchi  33109  constrmon  33707  measvuni  34177  ddemeas  34199  sibf0  34298  signstfvneq0  34536  opelco3  35735  wsuclem  35786  unbdqndv1  36469  bj-projval  36957  bj-nuliota  37018  bj-0nmoore  37073  nlpineqsn  37369  poimirlem30  37617  pw2f1ocnv  42999  areaquad  43178  onexlimgt  43205  cantnfresb  43286  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  eu0  43482  ntrneikb  44056  r1rankcld  44193  en3lpVD  44807  0elaxnul  44946  omssaxinf2  44951  permaxnul  44971  permaxinf2lem  44975  supminfxr  45433  liminf0  45764  iblempty  45936  stoweidlem34  46005  sge00  46347  vonhoire  46643  prprelprb  47491  fpprbasnn  47703  stgr0  47932