Theorem noel 4320

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 2140, ax-11 2156, and ax-12 2176. (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 2105	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1553	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1796	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4317	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2825	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2713	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1799	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2809	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1539  ⊥wfal 1551  ∃wex 1778  [wsb 2063   ∈ wcel 2107  {cab 2712  ∅c0 4315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-dif 3936  df-nul 4316

This theorem is referenced by:  nel02  4321  n0i  4322  eq0f  4329  eq0ALT  4333  rex0  4342  rab0  4368  un0  4376  in0  4377  0ss  4382  sbcel12  4393  sbcel2  4400  disj  4432  r19.2zb  4478  rabsnifsb  4704  iun0  5044  br0  5174  0xp  5766  csbxp  5767  dm0  5913  dm0rn0  5917  reldm0  5920  elimasni  6091  co02  6262  ord0eln0  6420  nlim0  6424  nsuceq0  6448  dffv3  6883  0fv  6931  elfv2ex  6933  mpo0  7501  el2mpocsbcl  8093  bropopvvv  8098  bropfvvvv  8100  tz7.44-2  8430  omordi  8587  nnmordi  8652  omabs  8672  omsmolem  8678  0er  8766  omxpenlem  9096  infn0  9323  en3lp  9637  cantnfle  9694  r1sdom  9797  r1pwss  9807  alephordi  10097  axdc3lem2  10474  zorn2lem7  10525  nlt1pi  10929  xrinf0  13363  elixx3g  13383  elfz2  13537  fzm1  13630  om2uzlti  13974  hashf1lem2  14478  sum0  15740  fsumsplit  15760  sumsplit  15787  fsum2dlem  15789  prod0  15962  fprod2dlem  15999  sadc0  16474  sadcp1  16475  saddisjlem  16484  smu01lem  16505  smu01  16506  smu02  16507  lcmf0  16654  prmreclem5  16941  vdwap0  16997  ram0  17043  0catg  17707  oduclatb  18526  0g0  18651  dfgrp2e  18955  cntzrcl  19319  pmtrfrn  19449  psgnunilem5  19485  gexdvds  19575  gsumzsplit  19918  dprdcntz2  20031  00lss  20912  dsmmfi  21725  mplcoe1  22022  mplcoe5  22025  00ply1bas  22208  maducoeval2  22613  madugsum  22616  0ntop  22878  haust1  23325  hauspwdom  23474  kqcldsat  23706  tsmssplit  24125  ustn0  24194  0met  24340  itg11  25681  itg0  25770  bddmulibl  25829  fsumharmonic  27010  ppiublem2  27202  lgsdir2lem3  27326  nulsslt  27797  nulssgt  27798  uvtx01vtx  29361  vtxdg0v  29438  dfpth2  29696  0enwwlksnge1  29831  rusgr0edg  29940  clwwlk  29949  eupth2lem1  30184  helloworld  30431  topnfbey  30435  n0lpligALT  30450  ccatf1  32880  chnccats1  32951  isarchi  33135  constrmon  33726  measvuni  34156  ddemeas  34178  sibf0  34277  signstfvneq0  34528  opelco3  35716  wsuclem  35767  unbdqndv1  36450  bj-projval  36938  bj-nuliota  36999  bj-0nmoore  37054  nlpineqsn  37350  poimirlem30  37598  pw2f1ocnv  42994  areaquad  43173  onexlimgt  43200  cantnfresb  43282  succlg  43286  oacl2g  43288  omabs2  43290  omcl2  43291  eu0  43478  ntrneikb  44052  r1rankcld  44195  en3lpVD  44810  0elaxnul  44945  omssaxinf2  44950  supminfxr  45420  liminf0  45753  iblempty  45925  stoweidlem34  45994  sge00  46336  vonhoire  46632  prprelprb  47450  fpprbasnn  47662  stgr0  47873