Theorem noel 4285

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 2196, and ax-12 2215. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) (Proof shortened by BJ, 11-Oct-2026.)

Assertion

Ref	Expression
noel	⊢ ¬ 𝐴 ∈ ∅

Proof of Theorem noel

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fal 1583	. . . 4 ⊢ ¬ ⊥
2		dfnul4 4282	. . . . . 6 ⊢ ∅ = {𝑦 ∣ ⊥}
3	2	eleq2i 2855	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
4		df-clab 2742	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
5		sbv 2126	. . . . 5 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
6	3, 4, 5	3bitri 300	. . . 4 ⊢ (𝑥 ∈ ∅ ↔ ⊥)
7	1, 6	mtbir 326	. . 3 ⊢ ¬ 𝑥 ∈ ∅
8	7	nex 1832	. 2 ⊢ ¬ ∃𝑥 𝑥 ∈ ∅
9		elex2 2840	. 2 ⊢ (𝐴 ∈ ∅ → ∃𝑥 𝑥 ∈ ∅)
10	8, 9	mto 200	1 ⊢ ¬ 𝐴 ∈ ∅

This proof depends on syntax axioms:  ¬ wn 3  ⊥wfal 1581  ∃wex 1811  [wsb 2100   ∈ wcel 2146  {cab 2741  ∅c0 4280

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 4049  df-nul 4281

This theorem is used by:  nel02  4287  eq0f  4296  eq0ALT  4300  rex0  4310  rab0OLD  4338  un0  4346  in0  4347  0ss  4352  sbcel12  4371  sbcel2  4378  disj  4405  rabsnifsb  4682  uni0  4898  iun0  5022  br0  5156  0xp  5754  xp0  5755  csbxp  5756  dm0  5906  dm0rn0  5910  dm0rn0OLD  5911  reldm0  5914  elimasni  6094  co02  6268  ord0eln0  6425  nlim0  6429  nsuceq0  6454  dffv3  6889  0fv  6934  elfv2ex  6936  mpo0  7512  el2mpocsbcl  8104  bropopvvv  8109  bropfvvvv  8111  tz7.44-2  8426  omordi  8585  nnmordi  8651  omabs  8671  omsmolem  8677  0er  8767  omxpenlem  9108  infn0  9305  en3lp  9625  cantnfle  9682  r1sdom  9791  r1pwss  9801  alephordi  10163  axdc3lem2  10539  zorn2lem7  10590  nlt1pi  11001  xrinf0  13479  elixx3g  13499  elfz2  13656  fzm1  13751  om2uzlti  14103  hashf1lem2  14611  ccatf1  14746  sum0  15899  fsumsplit  15919  sumsplit  15946  fsum2dlem  15948  prod0  16122  fprod2dlem  16159  sadc0  16636  sadcp1  16637  saddisjlem  16646  smu01lem  16667  smu01  16668  smu02  16669  lcmf0  16821  prmreclem5  17110  vdwap0  17166  ram0  17212  0catg  17874  oduclatb  18693  chnccats1  18811  chnccat  18812  0g0  18856  dfgrp2e  19186  cntzrcl  19553  pmtrfrn  19684  psgnunilem5  19720  gexdvds  19810  gsumzsplit  20153  dprdcntz2  20266  00lss  21228  dsmmfi  22056  mplcoe1  22358  mplcoe5  22361  00ply1bas  22569  maducoeval2  22967  madugsum  22970  0ntop  23235  haust1  23682  hauspwdom  23832  kqcldsat  24064  tsmssplit  24483  ustn0  24552  0met  24697  itg11  26024  itg0  26112  bddmulibl  26171  fsumharmonic  27351  ppiublem2  27542  lgsdir2lem3  27666  nulslts  28173  nulsgts  28174  uvtx01vtx  29990  vtxdg0v  30066  dfpth2  30326  0enwwlksnge1  30465  rusgr0edg  30577  clwwlk  30586  eupth2lem1  30831  helloworld  31078  topnfbey  31082  n0lpligALT  31098  isarchi  33796  domnprodeq0  33893  0mplrim  34199  constrmon  34429  measvuni  34900  ddemeas  34922  sibf0  35019  signstfvneq0  35254  opelco3  36666  wsuclem  36714  unbdqndv1  37501  bj-projval  38036  bj-nuliota  38111  bj-0nmoore  38172  nlpineqsn  38471  poimirlem30  38708  pw2f1ocnv  44184  areaquad  44358  onexlimgt  44385  cantnfresb  44466  succlg  44470  oacl2g  44472  omabs2  44474  omcl2  44475  eu0  44661  ntrneikb  45234  r1rankcld  45369  en3lpVD  45966  0elaxnul  46112  omssaxinf2  46117  permaxnul  46137  permaxinf2lem  46141  supminfxr  46613  liminf0  46942  iblempty  47114  stoweidlem34  47183  sge00  47525  vonhoire  47821  prprelprb  48738  fpprbasnn  48966  stgr0  49197  prmringnzring  49573  elif0  50061