Theorem noel 4301

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 4298	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2820	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2708	. . . . . 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 2804	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-dif 3917  df-nul 4297

This theorem is referenced by:  nel02  4302  n0i  4303  eq0f  4310  eq0ALT  4314  rex0  4323  rab0  4349  un0  4357  in0  4358  0ss  4363  sbcel12  4374  sbcel2  4381  disj  4413  r19.2zb  4459  rabsnifsb  4686  iun0  5026  br0  5156  0xp  5737  csbxp  5738  dm0  5884  dm0rn0  5888  reldm0  5891  elimasni  6062  co02  6233  ord0eln0  6388  nlim0  6392  nsuceq0  6417  dffv3  6854  0fv  6902  elfv2ex  6904  mpo0  7474  el2mpocsbcl  8064  bropopvvv  8069  bropfvvvv  8071  tz7.44-2  8375  omordi  8530  nnmordi  8595  omabs  8615  omsmolem  8621  0er  8709  omxpenlem  9042  infn0  9251  en3lp  9567  cantnfle  9624  r1sdom  9727  r1pwss  9737  alephordi  10027  axdc3lem2  10404  zorn2lem7  10455  nlt1pi  10859  xrinf0  13299  elixx3g  13319  elfz2  13475  fzm1  13568  om2uzlti  13915  hashf1lem2  14421  sum0  15687  fsumsplit  15707  sumsplit  15734  fsum2dlem  15736  prod0  15909  fprod2dlem  15946  sadc0  16424  sadcp1  16425  saddisjlem  16434  smu01lem  16455  smu01  16456  smu02  16457  lcmf0  16604  prmreclem5  16891  vdwap0  16947  ram0  16993  0catg  17649  oduclatb  18466  0g0  18591  dfgrp2e  18895  cntzrcl  19259  pmtrfrn  19388  psgnunilem5  19424  gexdvds  19514  gsumzsplit  19857  dprdcntz2  19970  00lss  20847  dsmmfi  21647  mplcoe1  21944  mplcoe5  21947  00ply1bas  22124  maducoeval2  22527  madugsum  22530  0ntop  22792  haust1  23239  hauspwdom  23388  kqcldsat  23620  tsmssplit  24039  ustn0  24108  0met  24254  itg11  25592  itg0  25681  bddmulibl  25740  fsumharmonic  26922  ppiublem2  27114  lgsdir2lem3  27238  nulsslt  27709  nulssgt  27710  uvtx01vtx  29324  vtxdg0v  29401  dfpth2  29659  0enwwlksnge1  29794  rusgr0edg  29903  clwwlk  29912  eupth2lem1  30147  helloworld  30394  topnfbey  30398  n0lpligALT  30413  ccatf1  32870  chnccats1  32941  isarchi  33136  constrmon  33734  measvuni  34204  ddemeas  34226  sibf0  34325  signstfvneq0  34563  opelco3  35762  wsuclem  35813  unbdqndv1  36496  bj-projval  36984  bj-nuliota  37045  bj-0nmoore  37100  nlpineqsn  37396  poimirlem30  37644  pw2f1ocnv  43026  areaquad  43205  onexlimgt  43232  cantnfresb  43313  succlg  43317  oacl2g  43319  omabs2  43321  omcl2  43322  eu0  43509  ntrneikb  44083  r1rankcld  44220  en3lpVD  44834  0elaxnul  44973  omssaxinf2  44978  permaxnul  44998  permaxinf2lem  45002  supminfxr  45460  liminf0  45791  iblempty  45963  stoweidlem34  46032  sge00  46374  vonhoire  46670  prprelprb  47518  fpprbasnn  47730  stgr0  47959