Theorem noel 4299

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 2182, ax-11 2198, and ax-12 2219. (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 2147	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1581	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1824	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4296	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2861	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2748	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 278	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 326	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 491	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1827	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2845	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 326	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 400   = wceq 1567  ⊥wfal 1579  ∃wex 1806  [wsb 2097   ∈ wcel 2149  {cab 2747  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-dif 3916  df-nul 4295

This theorem is referenced by:  nel02  4300  eq0f  4309  eq0ALT  4313  rex0  4323  rab0OLD  4350  un0  4358  in0  4359  0ss  4364  sbcel12  4382  sbcel2  4389  disj  4416  rabsnifsb  4693  uni0  4905  iun0  5030  br0  5164  0xp  5761  xp0  5762  csbxp  5763  dm0  5911  dm0rn0  5915  dm0rn0OLD  5916  reldm0  5919  elimasni  6094  co02  6263  ord0eln0  6418  nlim0  6422  nsuceq0  6447  dffv3  6878  0fv  6923  elfv2ex  6925  mpo0  7496  el2mpocsbcl  8079  bropopvvv  8084  bropfvvvv  8086  tz7.44-2  8393  omordi  8550  nnmordi  8616  omabs  8636  omsmolem  8642  0er  8732  omxpenlem  9065  infn0  9261  en3lp  9582  cantnfle  9639  r1sdom  9745  r1pwss  9755  alephordi  10057  axdc3lem2  10434  zorn2lem7  10485  nlt1pi  10890  xrinf0  13364  elixx3g  13384  elfz2  13541  fzm1  13634  om2uzlti  13985  hashf1lem2  14492  sum0  15771  fsumsplit  15791  sumsplit  15818  fsum2dlem  15820  prod0  15996  fprod2dlem  16033  sadc0  16511  sadcp1  16512  saddisjlem  16521  smu01lem  16542  smu01  16543  smu02  16544  lcmf0  16691  prmreclem5  16979  vdwap0  17035  ram0  17081  0catg  17743  oduclatb  18562  chnccats1  18680  chnccat  18681  0g0  18721  dfgrp2e  19029  cntzrcl  19396  pmtrfrn  19527  psgnunilem5  19563  gexdvds  19653  gsumzsplit  19996  dprdcntz2  20109  00lss  21039  dsmmfi  21856  mplcoe1  22156  mplcoe5  22159  00ply1bas  22367  maducoeval2  22765  madugsum  22768  0ntop  23030  haust1  23477  hauspwdom  23626  kqcldsat  23858  tsmssplit  24277  ustn0  24346  0met  24491  itg11  25818  itg0  25907  bddmulibl  25966  fsumharmonic  27141  ppiublem2  27332  lgsdir2lem3  27456  nulslts  27933  nulsgts  27934  uvtx01vtx  29687  vtxdg0v  29763  dfpth2  30018  0enwwlksnge1  30153  rusgr0edg  30265  clwwlk  30274  eupth2lem1  30509  helloworld  30756  topnfbey  30760  n0lpligALT  30776  ccatf1  33209  isarchi  33442  domnprodeq0  33539  0mplrim  33848  constrmon  34078  measvuni  34548  ddemeas  34570  sibf0  34668  signstfvneq0  34903  opelco3  36165  wsuclem  36213  unbdqndv1  36985  bj-projval  37519  bj-nuliota  37580  bj-0nmoore  37641  nlpineqsn  37941  poimirlem30  38188  pw2f1ocnv  43655  areaquad  43834  onexlimgt  43861  cantnfresb  43942  succlg  43946  oacl2g  43948  omabs2  43950  omcl2  43951  eu0  44137  ntrneikb  44711  r1rankcld  44846  en3lpVD  45444  0elaxnul  45583  omssaxinf2  45588  permaxnul  45608  permaxinf2lem  45612  supminfxr  46069  liminf0  46398  iblempty  46570  stoweidlem34  46639  sge00  46981  vonhoire  47277  prprelprb  48154  fpprbasnn  48382  stgr0  48613  prmringnzring  48990