Theorem noel 4286

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 2180, ax-11 2197, and ax-12 2216. (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 1584	. . . 4 ⊢ ¬ ⊥
2		dfnul4 4283	. . . . . 6 ⊢ ∅ = {𝑦 ∣ ⊥}
3	2	eleq2i 2856	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
4		df-clab 2742	. . . . 5 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
5		sbv 2127	. . . . 5 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥)
6	3, 4, 5	3bitri 300	. . . 4 ⊢ (𝑥 ∈ ∅ ↔ ⊥)
7	1, 6	mtbir 326	. . 3 ⊢ ¬ 𝑥 ∈ ∅
8	7	nex 1833	. 2 ⊢ ¬ ∃𝑥 𝑥 ∈ ∅
9		elex2 2841	. 2 ⊢ (𝐴 ∈ ∅ → ∃𝑥 𝑥 ∈ ∅)
10	8, 9	mto 200	1 ⊢ ¬ 𝐴 ∈ ∅

This proof depends on syntax axioms:  ¬ wn 3  ⊥wfal 1582  ∃wex 1812  [wsb 2101   ∈ wcel 2147  {cab 2741  ∅c0 4281

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-dif 4050  df-nul 4282

This theorem is used by:  nel02  4288  eq0f  4297  eq0ALT  4301  rex0  4311  rab0OLD  4339  un0  4347  in0  4348  0ss  4353  sbcel12  4372  sbcel2  4379  disj  4406  rabsnifsb  4685  uni0  4901  iun0  5025  br0  5160  0xp  5758  xp0  5759  csbxp  5760  dm0  5914  dm0rn0  5918  dm0rn0OLD  5919  reldm0  5922  elimasni  6107  co02  6283  ord0eln0  6445  nlim0  6449  nsuceq0  6474  dffv3  6912  0fv  6957  elfv2ex  6959  mpo0  7536  el2mpocsbcl  8131  bropopvvv  8136  bropfvvvv  8138  tz7.44-2  8453  omordi  8612  nnmordi  8678  omabs  8698  omsmolem  8704  0er  8794  omxpenlem  9135  infn0  9332  en3lp  9652  cantnfle  9709  r1sdom  9818  r1pwss  9828  alephordi  10192  axdc3lem2  10568  zorn2lem7  10619  nlt1pi  11030  xrinf0  13509  elixx3g  13529  elfz2  13686  fzm1  13781  om2uzlti  14133  hashf1lem2  14642  ccatf1  14777  sum0  15931  fsumsplit  15951  sumsplit  15978  fsum2dlem  15980  prod0  16154  fprod2dlem  16191  sadc0  16668  sadcp1  16669  saddisjlem  16678  smu01lem  16699  smu01  16700  smu02  16701  lcmf0  16853  prmreclem5  17142  vdwap0  17198  ram0  17244  0catg  17912  oduclatb  18731  chnccats1  18849  chnccat  18850  0g0  18894  dfgrp2e  19224  cntzrcl  19592  pmtrfrn  19723  psgnunilem5  19759  gexdvds  19849  gsumzsplit  20192  dprdcntz2  20305  00lss  21267  dsmmfi  22099  mplcoe1  22401  mplcoe5  22404  00ply1bas  22612  maducoeval2  23010  madugsum  23013  0ntop  23278  haust1  23725  hauspwdom  23875  kqcldsat  24107  tsmssplit  24526  ustn0  24595  0met  24740  itg11  26067  itg0  26155  bddmulibl  26214  fsumharmonic  27396  ppiublem2  27587  lgsdir2lem3  27711  nulslts  28218  nulsgts  28219  uvtx01vtx  30035  vtxdg0v  30111  dfpth2  30371  0enwwlksnge1  30510  rusgr0edg  30622  clwwlk  30631  eupth2lem1  30876  helloworld  31123  topnfbey  31127  n0lpligALT  31143  isarchi  33842  domnprodeq0  33939  0mplrim  34257  constrmon  34487  measvuni  34958  ddemeas  34980  sibf0  35077  signstfvneq0  35312  elpssmo  36673  opelco3  36754  wsuclem  36802  unbdqndv1  37589  bj-projval  38124  bj-nuliota  38242  bj-0nmoore  38303  nlpineqsn  38599  poimirlem30  38836  pw2f1ocnv  44310  areaquad  44479  onexlimgt  44506  cantnfresb  44587  succlg  44591  oacl2g  44593  omabs2  44595  omcl2  44596  eu0  44782  ntrneikb  45355  r1rankcld  45490  en3lpVD  46087  0elaxnul  46237  omssaxinf2  46242  permaxnul  46262  permaxinf2lem  46266  supminfxr  46747  liminf0  47076  iblempty  47248  stoweidlem34  47317  sge00  47659  vonhoire  47955  prprelprb  48872  fpprbasnn  49100  stgr0  49331  prmringnzring  49765  elif0  50253