Theorem noel 4360

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 2141, 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 2106	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1551	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1795	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4354	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2836	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2718	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1798	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2820	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1537  ⊥wfal 1549  ∃wex 1777  [wsb 2064   ∈ wcel 2108  {cab 2717  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-dif 3979  df-nul 4353

This theorem is referenced by:  nel02  4362  n0i  4363  eq0f  4370  eq0ALT  4374  rex0  4383  rab0  4409  un0  4417  in0  4418  0ss  4423  sbcel12  4434  sbcel2  4441  disj  4473  r19.2zb  4519  rabsnifsb  4747  iun0  5085  br0  5215  0xp  5798  csbxp  5799  dm0  5945  dm0rn0  5949  reldm0  5952  elimasni  6121  co02  6291  ord0eln0  6450  nlim0  6454  nsuceq0  6478  dffv3  6916  0fv  6964  elfv2ex  6966  mpo0  7535  el2mpocsbcl  8126  bropopvvv  8131  bropfvvvv  8133  tz7.44-2  8463  omordi  8622  nnmordi  8687  omabs  8707  omsmolem  8713  0er  8801  omxpenlem  9139  infn0  9368  en3lp  9683  cantnfle  9740  r1sdom  9843  r1pwss  9853  alephordi  10143  axdc3lem2  10520  zorn2lem7  10571  nlt1pi  10975  xrinf0  13400  elixx3g  13420  elfz2  13574  fzm1  13664  om2uzlti  14001  hashf1lem2  14505  sum0  15769  fsumsplit  15789  sumsplit  15816  fsum2dlem  15818  prod0  15991  fprod2dlem  16028  sadc0  16500  sadcp1  16501  saddisjlem  16510  smu01lem  16531  smu01  16532  smu02  16533  lcmf0  16681  prmreclem5  16967  vdwap0  17023  ram0  17069  0catg  17746  oduclatb  18577  0g0  18702  dfgrp2e  19003  cntzrcl  19367  pmtrfrn  19500  psgnunilem5  19536  gexdvds  19626  gsumzsplit  19969  dprdcntz2  20082  00lss  20962  dsmmfi  21781  mplcoe1  22078  mplcoe5  22081  00ply1bas  22262  maducoeval2  22667  madugsum  22670  0ntop  22932  haust1  23381  hauspwdom  23530  kqcldsat  23762  tsmssplit  24181  ustn0  24250  0met  24397  itg11  25745  itg0  25835  bddmulibl  25894  fsumharmonic  27073  ppiublem2  27265  lgsdir2lem3  27389  nulsslt  27860  nulssgt  27861  uvtx01vtx  29432  vtxdg0v  29509  0enwwlksnge1  29897  rusgr0edg  30006  clwwlk  30015  eupth2lem1  30250  helloworld  30497  topnfbey  30501  n0lpligALT  30516  ccatf1  32915  isarchi  33162  constrmon  33734  measvuni  34178  ddemeas  34200  sibf0  34299  signstfvneq0  34549  opelco3  35738  wsuclem  35789  unbdqndv1  36474  bj-projval  36962  bj-nuliota  37023  bj-0nmoore  37078  nlpineqsn  37374  poimirlem30  37610  pw2f1ocnv  42994  areaquad  43177  onexlimgt  43204  cantnfresb  43286  succlg  43290  oacl2g  43292  omabs2  43294  omcl2  43295  eu0  43482  ntrneikb  44056  r1rankcld  44200  en3lpVD  44816  supminfxr  45379  liminf0  45714  iblempty  45886  stoweidlem34  45955  sge00  46297  vonhoire  46593  prprelprb  47391  fpprbasnn  47603