Theorem noel 4288

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 2146, ax-11 2162, and ax-12 2182. (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 2111	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1555	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1798	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4285	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2826	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2713	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1801	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2810	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1541  ⊥wfal 1553  ∃wex 1780  [wsb 2067   ∈ wcel 2113  {cab 2712  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-dif 3902  df-nul 4284

This theorem is referenced by:  nel02  4289  n0i  4290  eq0f  4297  eq0ALT  4301  rex0  4310  rab0  4336  un0  4344  in0  4345  0ss  4350  sbcel12  4361  sbcel2  4368  disj  4400  rabsnifsb  4677  uni0  4889  iun0  5015  br0  5145  0xp  5721  xp0  5722  csbxp  5723  dm0  5867  dm0rn0  5871  dm0rn0OLD  5872  reldm0  5875  elimasni  6048  co02  6217  ord0eln0  6371  nlim0  6375  nsuceq0  6400  dffv3  6828  0fv  6873  elfv2ex  6875  mpo0  7441  el2mpocsbcl  8025  bropopvvv  8030  bropfvvvv  8032  tz7.44-2  8336  omordi  8491  nnmordi  8557  omabs  8577  omsmolem  8583  0er  8671  omxpenlem  9004  infn0  9200  en3lp  9521  cantnfle  9578  r1sdom  9684  r1pwss  9694  alephordi  9982  axdc3lem2  10359  zorn2lem7  10410  nlt1pi  10815  xrinf0  13252  elixx3g  13272  elfz2  13428  fzm1  13521  om2uzlti  13871  hashf1lem2  14377  sum0  15642  fsumsplit  15662  sumsplit  15689  fsum2dlem  15691  prod0  15864  fprod2dlem  15901  sadc0  16379  sadcp1  16380  saddisjlem  16389  smu01lem  16410  smu01  16411  smu02  16412  lcmf0  16559  prmreclem5  16846  vdwap0  16902  ram0  16948  0catg  17609  oduclatb  18428  chnccats1  18546  chnccat  18547  0g0  18587  dfgrp2e  18891  cntzrcl  19254  pmtrfrn  19385  psgnunilem5  19421  gexdvds  19511  gsumzsplit  19854  dprdcntz2  19967  00lss  20890  dsmmfi  21691  mplcoe1  21990  mplcoe5  21993  00ply1bas  22178  maducoeval2  22582  madugsum  22585  0ntop  22847  haust1  23294  hauspwdom  23443  kqcldsat  23675  tsmssplit  24094  ustn0  24163  0met  24308  itg11  25646  itg0  25735  bddmulibl  25794  fsumharmonic  26976  ppiublem2  27168  lgsdir2lem3  27292  nulsslt  27765  nulssgt  27766  uvtx01vtx  29419  vtxdg0v  29496  dfpth2  29751  0enwwlksnge1  29886  rusgr0edg  29998  clwwlk  30007  eupth2lem1  30242  helloworld  30489  topnfbey  30493  n0lpligALT  30508  ccatf1  32980  isarchi  33213  domnprodeq0  33307  constrmon  33850  measvuni  34320  ddemeas  34342  sibf0  34440  signstfvneq0  34678  opelco3  35918  wsuclem  35966  unbdqndv1  36651  bj-projval  37140  bj-nuliota  37201  bj-0nmoore  37256  nlpineqsn  37552  poimirlem30  37790  pw2f1ocnv  43221  areaquad  43400  onexlimgt  43427  cantnfresb  43508  succlg  43512  oacl2g  43514  omabs2  43516  omcl2  43517  eu0  43703  ntrneikb  44277  r1rankcld  44414  en3lpVD  45027  0elaxnul  45166  omssaxinf2  45171  permaxnul  45191  permaxinf2lem  45195  supminfxr  45650  liminf0  45979  iblempty  46151  stoweidlem34  46220  sge00  46562  vonhoire  46858  prprelprb  47705  fpprbasnn  47917  stgr0  48148