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 2129, ax-11 2146, and ax-12 2166. (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 2096	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1547	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1791	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4324	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2817	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2703	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 274	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 322	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 485	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1794	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2803	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 322	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 394   = wceq 1533  ⊥wfal 1545  ∃wex 1773  [wsb 2059   ∈ wcel 2098  {cab 2702  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-dif 3947  df-nul 4323

This theorem is referenced by:  nel02  4332  n0i  4333  eq0f  4340  eq0ALT  4344  rex0  4357  rab0  4384  un0  4392  in0  4393  0ss  4398  sbcel12  4410  sbcel2  4417  disj  4449  disjOLD  4450  r19.2zb  4497  ral0OLD  4518  rabsnifsb  4728  iun0  5066  br0  5198  0xp  5776  csbxp  5777  dm0  5923  dm0rn0  5927  reldm0  5930  elimasni  6096  co02  6266  ord0eln0  6426  nlim0  6430  nsuceq0  6454  dffv3  6892  0fv  6940  elfv2ex  6942  mpo0  7505  el2mpocsbcl  8090  bropopvvv  8095  bropfvvvv  8097  tz7.44-2  8428  omordi  8587  nnmordi  8652  omabs  8672  omsmolem  8678  0er  8762  omxpenlem  9101  infn0  9335  en3lp  9644  cantnfle  9701  r1sdom  9804  r1pwss  9814  alephordi  10104  axdc3lem2  10481  zorn2lem7  10532  nlt1pi  10936  xrinf0  13357  elixx3g  13377  elfz2  13531  fzm1  13621  om2uzlti  13956  hashf1lem2  14458  sum0  15708  fsumsplit  15728  sumsplit  15755  fsum2dlem  15757  prod0  15928  fprod2dlem  15965  sadc0  16437  sadcp1  16438  saddisjlem  16447  smu01lem  16468  smu01  16469  smu02  16470  lcmf0  16613  prmreclem5  16897  vdwap0  16953  ram0  16999  0catg  17676  oduclatb  18507  0g0  18632  dfgrp2e  18933  cntzrcl  19295  pmtrfrn  19430  psgnunilem5  19466  gexdvds  19556  gsumzsplit  19899  dprdcntz2  20012  00lss  20842  dsmmfi  21694  mplcoe1  22002  mplcoe5  22005  00ply1bas  22187  maducoeval2  22591  madugsum  22594  0ntop  22856  haust1  23305  hauspwdom  23454  kqcldsat  23686  tsmssplit  24105  ustn0  24174  0met  24321  itg11  25669  itg0  25758  bddmulibl  25817  fsumharmonic  26994  ppiublem2  27186  lgsdir2lem3  27310  nulsslt  27781  nulssgt  27782  uvtx01vtx  29287  vtxdg0v  29364  0enwwlksnge1  29752  rusgr0edg  29861  clwwlk  29870  eupth2lem1  30105  helloworld  30352  topnfbey  30356  n0lpligALT  30371  ccatf1  32764  isarchi  32987  measvuni  33966  ddemeas  33988  sibf0  34087  signstfvneq0  34337  opelco3  35503  wsuclem  35554  unbdqndv1  36116  bj-projval  36608  bj-nuliota  36669  bj-0nmoore  36724  nlpineqsn  37020  poimirlem30  37256  pw2f1ocnv  42602  areaquad  42788  onexlimgt  42815  cantnfresb  42897  succlg  42901  oacl2g  42903  omabs2  42905  omcl2  42906  eu0  43094  ntrneikb  43668  r1rankcld  43812  en3lpVD  44428  supminfxr  44986  liminf0  45321  iblempty  45493  stoweidlem34  45562  sge00  45904  vonhoire  46200  prprelprb  46996  fpprbasnn  47208