Theorem noel 4291

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 2179, ax-11 2195, and ax-12 2216. (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 2144	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1584	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1830	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4288	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2857	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2744	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 278	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 326	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 492	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1833	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2841	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 326	1 ⊢ ¬ 𝐴 ∈ ∅

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 401   = wceq 1570  ⊥wfal 1582  ∃wex 1812  [wsb 2099   ∈ wcel 2146  {cab 2743  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-dif 3909  df-nul 4287

This theorem is used by:  nel02  4292  eq0f  4301  eq0ALT  4305  rex0  4315  rab0OLD  4343  un0  4351  in0  4352  0ss  4357  sbcel12  4376  sbcel2  4383  disj  4410  rabsnifsb  4690  uni0  4903  iun0  5028  br0  5162  0xp  5762  xp0  5763  csbxp  5764  dm0  5912  dm0rn0  5916  dm0rn0OLD  5917  reldm0  5920  elimasni  6095  co02  6264  ord0eln0  6421  nlim0  6425  nsuceq0  6450  dffv3  6881  0fv  6926  elfv2ex  6928  mpo0  7504  el2mpocsbcl  8086  bropopvvv  8091  bropfvvvv  8093  tz7.44-2  8400  omordi  8557  nnmordi  8623  omabs  8643  omsmolem  8649  0er  8739  omxpenlem  9073  infn0  9269  en3lp  9590  cantnfle  9647  r1sdom  9753  r1pwss  9763  alephordi  10074  axdc3lem2  10450  zorn2lem7  10501  nlt1pi  10906  xrinf0  13381  elixx3g  13401  elfz2  13558  fzm1  13652  om2uzlti  14004  hashf1lem2  14511  ccatf1  14646  sum0  15795  fsumsplit  15815  sumsplit  15842  fsum2dlem  15844  prod0  16020  fprod2dlem  16057  sadc0  16534  sadcp1  16535  saddisjlem  16544  smu01lem  16565  smu01  16566  smu02  16567  lcmf0  16714  prmreclem5  17002  vdwap0  17058  ram0  17104  0catg  17766  oduclatb  18585  chnccats1  18703  chnccat  18704  0g0  18747  dfgrp2e  19074  cntzrcl  19441  pmtrfrn  19572  psgnunilem5  19608  gexdvds  19698  gsumzsplit  20041  dprdcntz2  20154  00lss  21112  dsmmfi  21938  mplcoe1  22238  mplcoe5  22241  00ply1bas  22449  maducoeval2  22847  madugsum  22850  0ntop  23112  haust1  23559  hauspwdom  23709  kqcldsat  23941  tsmssplit  24360  ustn0  24429  0met  24574  itg11  25901  itg0  25990  bddmulibl  26049  fsumharmonic  27227  ppiublem2  27418  lgsdir2lem3  27542  nulslts  28019  nulsgts  28020  uvtx01vtx  29805  vtxdg0v  29881  dfpth2  30141  0enwwlksnge1  30280  rusgr0edg  30392  clwwlk  30401  eupth2lem1  30640  helloworld  30887  topnfbey  30891  n0lpligALT  30907  isarchi  33566  domnprodeq0  33663  0mplrim  33968  constrmon  34198  measvuni  34669  ddemeas  34691  sibf0  34789  signstfvneq0  35024  opelco3  36304  wsuclem  36352  unbdqndv1  37154  bj-projval  37689  bj-nuliota  37750  bj-0nmoore  37811  nlpineqsn  38111  poimirlem30  38358  pw2f1ocnv  43822  areaquad  44001  onexlimgt  44028  cantnfresb  44109  succlg  44113  oacl2g  44115  omabs2  44117  omcl2  44118  eu0  44304  ntrneikb  44878  r1rankcld  45013  en3lpVD  45611  0elaxnul  45750  omssaxinf2  45755  permaxnul  45775  permaxinf2lem  45779  supminfxr  46236  liminf0  46565  iblempty  46737  stoweidlem34  46806  sge00  47148  vonhoire  47444  prprelprb  48324  fpprbasnn  48552  stgr0  48783  prmringnzring  49159