Theorem noel 4290

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 2146, ax-11 2162, and ax-12 2184. (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 2111	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1555	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1798	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4287	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2828	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2715	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1801	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2812	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1541  ⊥wfal 1553  ∃wex 1780  [wsb 2067   ∈ wcel 2113  {cab 2714  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-dif 3904  df-nul 4286

This theorem is referenced by:  nel02  4291  n0i  4292  eq0f  4299  eq0ALT  4303  rex0  4312  rab0  4338  un0  4346  in0  4347  0ss  4352  sbcel12  4363  sbcel2  4370  disj  4402  rabsnifsb  4679  uni0  4891  iun0  5017  br0  5147  0xp  5723  xp0  5724  csbxp  5725  dm0  5869  dm0rn0  5873  dm0rn0OLD  5874  reldm0  5877  elimasni  6050  co02  6219  ord0eln0  6373  nlim0  6377  nsuceq0  6402  dffv3  6830  0fv  6875  elfv2ex  6877  mpo0  7443  el2mpocsbcl  8027  bropopvvv  8032  bropfvvvv  8034  tz7.44-2  8338  omordi  8493  nnmordi  8559  omabs  8579  omsmolem  8585  0er  8673  omxpenlem  9006  infn0  9202  en3lp  9523  cantnfle  9580  r1sdom  9686  r1pwss  9696  alephordi  9984  axdc3lem2  10361  zorn2lem7  10412  nlt1pi  10817  xrinf0  13254  elixx3g  13274  elfz2  13430  fzm1  13523  om2uzlti  13873  hashf1lem2  14379  sum0  15644  fsumsplit  15664  sumsplit  15691  fsum2dlem  15693  prod0  15866  fprod2dlem  15903  sadc0  16381  sadcp1  16382  saddisjlem  16391  smu01lem  16412  smu01  16413  smu02  16414  lcmf0  16561  prmreclem5  16848  vdwap0  16904  ram0  16950  0catg  17611  oduclatb  18430  chnccats1  18548  chnccat  18549  0g0  18589  dfgrp2e  18893  cntzrcl  19256  pmtrfrn  19387  psgnunilem5  19423  gexdvds  19513  gsumzsplit  19856  dprdcntz2  19969  00lss  20892  dsmmfi  21693  mplcoe1  21992  mplcoe5  21995  00ply1bas  22180  maducoeval2  22584  madugsum  22587  0ntop  22849  haust1  23296  hauspwdom  23445  kqcldsat  23677  tsmssplit  24096  ustn0  24165  0met  24310  itg11  25648  itg0  25737  bddmulibl  25796  fsumharmonic  26978  ppiublem2  27170  lgsdir2lem3  27294  nulslts  27771  nulsgts  27772  uvtx01vtx  29470  vtxdg0v  29547  dfpth2  29802  0enwwlksnge1  29937  rusgr0edg  30049  clwwlk  30058  eupth2lem1  30293  helloworld  30540  topnfbey  30544  n0lpligALT  30559  ccatf1  33031  isarchi  33264  domnprodeq0  33358  constrmon  33901  measvuni  34371  ddemeas  34393  sibf0  34491  signstfvneq0  34729  opelco3  35969  wsuclem  36017  unbdqndv1  36708  bj-projval  37197  bj-nuliota  37258  bj-0nmoore  37317  nlpineqsn  37613  poimirlem30  37851  pw2f1ocnv  43279  areaquad  43458  onexlimgt  43485  cantnfresb  43566  succlg  43570  oacl2g  43572  omabs2  43574  omcl2  43575  eu0  43761  ntrneikb  44335  r1rankcld  44472  en3lpVD  45085  0elaxnul  45224  omssaxinf2  45229  permaxnul  45249  permaxinf2lem  45253  supminfxr  45708  liminf0  46037  iblempty  46209  stoweidlem34  46278  sge00  46620  vonhoire  46916  prprelprb  47763  fpprbasnn  47975  stgr0  48206