Theorem noel 4330

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 2137, ax-11 2154, and ax-12 2171. (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 2104	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1555	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1799	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4324	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2825	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2710	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 274	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 322	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 487	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1802	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2811	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 322	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1541  ⊥wfal 1553  ∃wex 1781  [wsb 2067   ∈ wcel 2106  {cab 2709  ∅c0 4322

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-dif 3951  df-nul 4323

This theorem is referenced by:  nel02  4332  n0i  4333  eq0f  4340  eq0ALT  4344  rex0  4357  rab0  4382  un0  4390  in0  4391  0ss  4396  sbcel12  4408  sbcel2  4415  disj  4447  disjOLD  4448  r19.2zb  4495  ral0OLD  4516  rabsnifsb  4726  iun0  5065  br0  5197  0xp  5774  csbxp  5775  dm0  5920  dm0rn0  5924  reldm0  5927  elimasni  6090  co02  6259  ord0eln0  6419  nlim0  6423  nsuceq0  6447  dffv3  6887  0fv  6935  elfv2ex  6937  mpo0  7496  el2mpocsbcl  8073  bropopvvv  8078  bropfvvvv  8080  tz7.44-2  8409  omordi  8568  nnmordi  8633  omabs  8652  omsmolem  8658  0er  8742  omxpenlem  9075  infn0  9309  en3lp  9611  cantnfle  9668  r1sdom  9771  r1pwss  9781  alephordi  10071  axdc3lem2  10448  zorn2lem7  10499  nlt1pi  10903  xrinf0  13319  elixx3g  13339  elfz2  13493  fzm1  13583  om2uzlti  13917  hashf1lem2  14419  sum0  15669  fsumsplit  15689  sumsplit  15716  fsum2dlem  15718  prod0  15889  fprod2dlem  15926  sadc0  16397  sadcp1  16398  saddisjlem  16407  smu01lem  16428  smu01  16429  smu02  16430  lcmf0  16573  prmreclem5  16855  vdwap0  16911  ram0  16957  0catg  17634  oduclatb  18462  0g0  18585  dfgrp2e  18850  cntzrcl  19193  pmtrfrn  19328  psgnunilem5  19364  gexdvds  19454  gsumzsplit  19797  dprdcntz2  19910  00lss  20557  dsmmfi  21299  mplcoe1  21598  mplcoe5  21601  00ply1bas  21769  maducoeval2  22149  madugsum  22152  0ntop  22414  haust1  22863  hauspwdom  23012  kqcldsat  23244  tsmssplit  23663  ustn0  23732  0met  23879  itg11  25215  itg0  25304  bddmulibl  25363  fsumharmonic  26523  ppiublem2  26713  lgsdir2lem3  26837  nulsslt  27306  nulssgt  27307  uvtx01vtx  28692  vtxdg0v  28768  0enwwlksnge1  29156  rusgr0edg  29265  clwwlk  29274  eupth2lem1  29509  helloworld  29756  topnfbey  29760  n0lpligALT  29775  ccatf1  32153  isarchi  32369  measvuni  33281  ddemeas  33303  sibf0  33402  signstfvneq0  33652  opelco3  34821  wsuclem  34872  unbdqndv1  35476  bj-projval  35969  bj-nuliota  36030  bj-0nmoore  36085  nlpineqsn  36381  poimirlem30  36610  pw2f1ocnv  41864  areaquad  42053  onexlimgt  42080  cantnfresb  42162  succlg  42166  oacl2g  42168  omabs2  42170  omcl2  42171  eu0  42359  ntrneikb  42933  r1rankcld  43078  en3lpVD  43694  supminfxr  44259  liminf0  44594  iblempty  44766  stoweidlem34  44835  sge00  45177  vonhoire  45473  prprelprb  46270  fpprbasnn  46482