Theorem noel 4264

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 2137, ax-11 2154, and ax-12 2171. (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 2104	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1553	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1800	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4258	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2830	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2716	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 274	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 487	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1803	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2817	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1539  ⊥wfal 1551  ∃wex 1782  [wsb 2067   ∈ wcel 2106  {cab 2715  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-dif 3890  df-nul 4257

This theorem is referenced by:  nel02  4266  n0i  4267  eq0f  4274  eq0ALT  4278  rex0  4291  rab0  4316  un0  4324  in0  4325  0ss  4330  sbcel12  4342  sbcel2  4349  disj  4381  disjOLD  4382  r19.2zb  4426  ral0OLD  4447  rabsnifsb  4658  dfopif  4800  iun0  4991  br0  5123  0xp  5685  csbxp  5686  dm0  5829  dm0rn0  5834  reldm0  5837  elimasni  5999  co02  6164  ord0eln0  6320  nlim0  6324  nsuceq0  6346  dffv3  6770  0fv  6813  elfv2ex  6815  mpo0  7360  el2mpocsbcl  7925  bropopvvv  7930  bropfvvvv  7932  tz7.44-2  8238  omordi  8397  nnmordi  8462  omabs  8481  omsmolem  8487  0er  8535  omxpenlem  8860  en3lp  9372  cantnfle  9429  r1sdom  9532  r1pwss  9542  alephordi  9830  axdc3lem2  10207  zorn2lem7  10258  nlt1pi  10662  xrinf0  13072  elixx3g  13092  elfz2  13246  fzm1  13336  om2uzlti  13670  hashf1lem2  14170  sum0  15433  fsumsplit  15453  sumsplit  15480  fsum2dlem  15482  prod0  15653  fprod2dlem  15690  sadc0  16161  sadcp1  16162  saddisjlem  16171  smu01lem  16192  smu01  16193  smu02  16194  lcmf0  16339  prmreclem5  16621  vdwap0  16677  ram0  16723  0catg  17397  oduclatb  18225  0g0  18348  dfgrp2e  18605  cntzrcl  18933  pmtrfrn  19066  psgnunilem5  19102  gexdvds  19189  gsumzsplit  19528  dprdcntz2  19641  00lss  20203  dsmmfi  20945  mplcoe1  21238  mplcoe5  21241  00ply1bas  21411  maducoeval2  21789  madugsum  21792  0ntop  22054  haust1  22503  hauspwdom  22652  kqcldsat  22884  tsmssplit  23303  ustn0  23372  0met  23519  itg11  24855  itg0  24944  bddmulibl  25003  fsumharmonic  26161  ppiublem2  26351  lgsdir2lem3  26475  uvtx01vtx  27764  vtxdg0v  27840  0enwwlksnge1  28229  rusgr0edg  28338  clwwlk  28347  eupth2lem1  28582  helloworld  28829  topnfbey  28833  n0lpligALT  28846  ccatf1  31223  isarchi  31436  measvuni  32182  ddemeas  32204  sibf0  32301  signstfvneq0  32551  opelco3  33749  wsuclem  33819  nulsslt  33991  nulssgt  33992  unbdqndv1  34688  bj-projval  35186  bj-nuliota  35228  bj-0nmoore  35283  nlpineqsn  35579  poimirlem30  35807  pw2f1ocnv  40859  areaquad  41047  eu0  41127  ntrneikb  41704  r1rankcld  41849  en3lpVD  42465  supminfxr  43004  liminf0  43334  iblempty  43506  stoweidlem34  43575  sge00  43914  vonhoire  44210  prprelprb  44969  fpprbasnn  45181