Theorem noel 4318

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 2142, ax-11 2158, and ax-12 2178. (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 2107	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1554	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1797	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4315	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2827	. . . . . 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 1800	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2811	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540  ⊥wfal 1552  ∃wex 1779  [wsb 2065   ∈ wcel 2109  {cab 2714  ∅c0 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-dif 3934  df-nul 4314

This theorem is referenced by:  nel02  4319  n0i  4320  eq0f  4327  eq0ALT  4331  rex0  4340  rab0  4366  un0  4374  in0  4375  0ss  4380  sbcel12  4391  sbcel2  4398  disj  4430  r19.2zb  4476  rabsnifsb  4703  iun0  5043  br0  5173  0xp  5758  csbxp  5759  dm0  5905  dm0rn0  5909  reldm0  5912  elimasni  6083  co02  6254  ord0eln0  6413  nlim0  6417  nsuceq0  6442  dffv3  6877  0fv  6925  elfv2ex  6927  mpo0  7497  el2mpocsbcl  8089  bropopvvv  8094  bropfvvvv  8096  tz7.44-2  8426  omordi  8583  nnmordi  8648  omabs  8668  omsmolem  8674  0er  8762  omxpenlem  9092  infn0  9317  en3lp  9633  cantnfle  9690  r1sdom  9793  r1pwss  9803  alephordi  10093  axdc3lem2  10470  zorn2lem7  10521  nlt1pi  10925  xrinf0  13360  elixx3g  13380  elfz2  13536  fzm1  13629  om2uzlti  13973  hashf1lem2  14479  sum0  15742  fsumsplit  15762  sumsplit  15789  fsum2dlem  15791  prod0  15964  fprod2dlem  16001  sadc0  16478  sadcp1  16479  saddisjlem  16488  smu01lem  16509  smu01  16510  smu02  16511  lcmf0  16658  prmreclem5  16945  vdwap0  17001  ram0  17047  0catg  17705  oduclatb  18522  0g0  18647  dfgrp2e  18951  cntzrcl  19315  pmtrfrn  19444  psgnunilem5  19480  gexdvds  19570  gsumzsplit  19913  dprdcntz2  20026  00lss  20903  dsmmfi  21703  mplcoe1  22000  mplcoe5  22003  00ply1bas  22180  maducoeval2  22583  madugsum  22586  0ntop  22848  haust1  23295  hauspwdom  23444  kqcldsat  23676  tsmssplit  24095  ustn0  24164  0met  24310  itg11  25649  itg0  25738  bddmulibl  25797  fsumharmonic  26979  ppiublem2  27171  lgsdir2lem3  27295  nulsslt  27766  nulssgt  27767  uvtx01vtx  29381  vtxdg0v  29458  dfpth2  29716  0enwwlksnge1  29851  rusgr0edg  29960  clwwlk  29969  eupth2lem1  30204  helloworld  30451  topnfbey  30455  n0lpligALT  30470  ccatf1  32929  chnccats1  33000  isarchi  33185  constrmon  33783  measvuni  34250  ddemeas  34272  sibf0  34371  signstfvneq0  34609  opelco3  35797  wsuclem  35848  unbdqndv1  36531  bj-projval  37019  bj-nuliota  37080  bj-0nmoore  37135  nlpineqsn  37431  poimirlem30  37679  pw2f1ocnv  43036  areaquad  43215  onexlimgt  43242  cantnfresb  43323  succlg  43327  oacl2g  43329  omabs2  43331  omcl2  43332  eu0  43519  ntrneikb  44093  r1rankcld  44230  en3lpVD  44844  0elaxnul  44983  omssaxinf2  44988  permaxnul  45008  permaxinf2lem  45012  supminfxr  45471  liminf0  45802  iblempty  45974  stoweidlem34  46043  sge00  46385  vonhoire  46681  prprelprb  47511  fpprbasnn  47723  stgr0  47952