Theorem noel 4331

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 2138, ax-11 2155, and ax-12 2172. (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 2105	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1556	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1800	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4325	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2826	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2711	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 488	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1803	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2812	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 397   = wceq 1542  ⊥wfal 1554  ∃wex 1782  [wsb 2068   ∈ wcel 2107  {cab 2710  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-dif 3952  df-nul 4324

This theorem is referenced by:  nel02  4333  n0i  4334  eq0f  4341  eq0ALT  4345  rex0  4358  rab0  4383  un0  4391  in0  4392  0ss  4397  sbcel12  4409  sbcel2  4416  disj  4448  disjOLD  4449  r19.2zb  4496  ral0OLD  4517  rabsnifsb  4727  iun0  5066  br0  5198  0xp  5775  csbxp  5776  dm0  5921  dm0rn0  5925  reldm0  5928  elimasni  6091  co02  6260  ord0eln0  6420  nlim0  6424  nsuceq0  6448  dffv3  6888  0fv  6936  elfv2ex  6938  mpo0  7494  el2mpocsbcl  8071  bropopvvv  8076  bropfvvvv  8078  tz7.44-2  8407  omordi  8566  nnmordi  8631  omabs  8650  omsmolem  8656  0er  8740  omxpenlem  9073  infn0  9307  en3lp  9609  cantnfle  9666  r1sdom  9769  r1pwss  9779  alephordi  10069  axdc3lem2  10446  zorn2lem7  10497  nlt1pi  10901  xrinf0  13317  elixx3g  13337  elfz2  13491  fzm1  13581  om2uzlti  13915  hashf1lem2  14417  sum0  15667  fsumsplit  15687  sumsplit  15714  fsum2dlem  15716  prod0  15887  fprod2dlem  15924  sadc0  16395  sadcp1  16396  saddisjlem  16405  smu01lem  16426  smu01  16427  smu02  16428  lcmf0  16571  prmreclem5  16853  vdwap0  16909  ram0  16955  0catg  17632  oduclatb  18460  0g0  18583  dfgrp2e  18848  cntzrcl  19191  pmtrfrn  19326  psgnunilem5  19362  gexdvds  19452  gsumzsplit  19795  dprdcntz2  19908  00lss  20552  dsmmfi  21293  mplcoe1  21592  mplcoe5  21595  00ply1bas  21762  maducoeval2  22142  madugsum  22145  0ntop  22407  haust1  22856  hauspwdom  23005  kqcldsat  23237  tsmssplit  23656  ustn0  23725  0met  23872  itg11  25208  itg0  25297  bddmulibl  25356  fsumharmonic  26516  ppiublem2  26706  lgsdir2lem3  26830  nulsslt  27298  nulssgt  27299  uvtx01vtx  28654  vtxdg0v  28730  0enwwlksnge1  29118  rusgr0edg  29227  clwwlk  29236  eupth2lem1  29471  helloworld  29718  topnfbey  29722  n0lpligALT  29737  ccatf1  32115  isarchi  32328  measvuni  33212  ddemeas  33234  sibf0  33333  signstfvneq0  33583  opelco3  34746  wsuclem  34797  unbdqndv1  35384  bj-projval  35877  bj-nuliota  35938  bj-0nmoore  35993  nlpineqsn  36289  poimirlem30  36518  pw2f1ocnv  41776  areaquad  41965  onexlimgt  41992  cantnfresb  42074  succlg  42078  oacl2g  42080  omabs2  42082  omcl2  42083  eu0  42271  ntrneikb  42845  r1rankcld  42990  en3lpVD  43606  supminfxr  44174  liminf0  44509  iblempty  44681  stoweidlem34  44750  sge00  45092  vonhoire  45388  prprelprb  46185  fpprbasnn  46397