Theorem noel 4261

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 2139, ax-11 2156, and ax-12 2173. (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 1553	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1801	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4255	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2830	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2716	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 274	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 322	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1804	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2818	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 322	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1539  ⊥wfal 1551  ∃wex 1783  [wsb 2068   ∈ wcel 2108  {cab 2715  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-dif 3886  df-nul 4254

This theorem is referenced by:  nel02  4263  n0i  4264  eq0f  4271  eq0ALT  4275  rex0  4288  rab0  4313  un0  4321  in0  4322  0ss  4327  sbcel12  4339  sbcel2  4346  disj  4378  disjOLD  4379  r19.2zb  4423  ral0OLD  4444  rabsnifsb  4655  dfopif  4797  iun0  4987  br0  5119  0xp  5675  csbxp  5676  dm0  5818  dm0rn0  5823  reldm0  5826  elimasni  5988  co02  6153  ord0eln0  6305  nlim0  6309  nsuceq0  6331  dffv3  6752  0fv  6795  elfv2ex  6797  mpo0  7338  el2mpocsbcl  7896  bropopvvv  7901  bropfvvvv  7903  tz7.44-2  8209  omordi  8359  nnmordi  8424  omabs  8441  omsmolem  8447  0er  8493  omxpenlem  8813  en3lp  9302  cantnfle  9359  r1sdom  9463  r1pwss  9473  alephordi  9761  axdc3lem2  10138  zorn2lem7  10189  nlt1pi  10593  xrinf0  13001  elixx3g  13021  elfz2  13175  fzm1  13265  om2uzlti  13598  hashf1lem2  14098  sum0  15361  fsumsplit  15381  sumsplit  15408  fsum2dlem  15410  prod0  15581  fprod2dlem  15618  sadc0  16089  sadcp1  16090  saddisjlem  16099  smu01lem  16120  smu01  16121  smu02  16122  lcmf0  16267  prmreclem5  16549  vdwap0  16605  ram0  16651  0catg  17314  oduclatb  18140  0g0  18263  dfgrp2e  18520  cntzrcl  18848  pmtrfrn  18981  psgnunilem5  19017  gexdvds  19104  gsumzsplit  19443  dprdcntz2  19556  00lss  20118  dsmmfi  20855  mplcoe1  21148  mplcoe5  21151  00ply1bas  21321  maducoeval2  21697  madugsum  21700  0ntop  21962  haust1  22411  hauspwdom  22560  kqcldsat  22792  tsmssplit  23211  ustn0  23280  0met  23427  itg11  24760  itg0  24849  bddmulibl  24908  fsumharmonic  26066  ppiublem2  26256  lgsdir2lem3  26380  uvtx01vtx  27667  vtxdg0v  27743  0enwwlksnge1  28130  rusgr0edg  28239  clwwlk  28248  eupth2lem1  28483  helloworld  28730  topnfbey  28734  n0lpligALT  28747  ccatf1  31125  isarchi  31338  measvuni  32082  ddemeas  32104  sibf0  32201  signstfvneq0  32451  opelco3  33655  wsuclem  33746  nulsslt  33918  nulssgt  33919  unbdqndv1  34615  bj-projval  35113  bj-nuliota  35155  bj-0nmoore  35210  nlpineqsn  35506  poimirlem30  35734  pw2f1ocnv  40775  areaquad  40963  eu0  41025  ntrneikb  41593  r1rankcld  41738  en3lpVD  42354  supminfxr  42894  liminf0  43224  iblempty  43396  stoweidlem34  43465  sge00  43804  vonhoire  44100  prprelprb  44857  fpprbasnn  45069