Theorem noel 4291

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 2176, ax-11 2192, and ax-12 2213. (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 2141	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1584	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1827	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4288	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2855	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2742	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 278	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 326	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 491	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1830	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2839	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 326	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 400   = wceq 1570  ⊥wfal 1582  ∃wex 1809  [wsb 2096   ∈ wcel 2143  {cab 2741  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-dif 3908  df-nul 4287

This theorem is referenced by:  nel02  4292  eq0f  4301  eq0ALT  4305  rex0  4315  rab0OLD  4343  un0  4351  in0  4352  0ss  4357  sbcel12  4376  sbcel2  4383  disj  4410  rabsnifsb  4688  uni0  4901  iun0  5026  br0  5160  0xp  5760  xp0  5761  csbxp  5762  dm0  5910  dm0rn0  5914  dm0rn0OLD  5915  reldm0  5918  elimasni  6093  co02  6262  ord0eln0  6417  nlim0  6421  nsuceq0  6446  dffv3  6877  0fv  6922  elfv2ex  6924  mpo0  7495  el2mpocsbcl  8076  bropopvvv  8081  bropfvvvv  8083  tz7.44-2  8390  omordi  8547  nnmordi  8613  omabs  8633  omsmolem  8639  0er  8729  omxpenlem  9062  infn0  9258  en3lp  9579  cantnfle  9636  r1sdom  9742  r1pwss  9752  alephordi  10054  axdc3lem2  10430  zorn2lem7  10481  nlt1pi  10886  xrinf0  13360  elixx3g  13380  elfz2  13537  fzm1  13631  om2uzlti  13982  hashf1lem2  14489  sum0  15768  fsumsplit  15788  sumsplit  15815  fsum2dlem  15817  prod0  15993  fprod2dlem  16030  sadc0  16507  sadcp1  16508  saddisjlem  16517  smu01lem  16538  smu01  16539  smu02  16540  lcmf0  16687  prmreclem5  16975  vdwap0  17031  ram0  17077  0catg  17739  oduclatb  18558  chnccats1  18676  chnccat  18677  0g0  18717  dfgrp2e  19025  cntzrcl  19392  pmtrfrn  19523  psgnunilem5  19559  gexdvds  19649  gsumzsplit  19992  dprdcntz2  20105  00lss  21062  dsmmfi  21888  mplcoe1  22188  mplcoe5  22191  00ply1bas  22399  maducoeval2  22797  madugsum  22800  0ntop  23062  haust1  23509  hauspwdom  23658  kqcldsat  23890  tsmssplit  24309  ustn0  24378  0met  24523  itg11  25850  itg0  25939  bddmulibl  25998  fsumharmonic  27176  ppiublem2  27367  lgsdir2lem3  27491  nulslts  27968  nulsgts  27969  uvtx01vtx  29747  vtxdg0v  29823  dfpth2  30078  0enwwlksnge1  30213  rusgr0edg  30325  clwwlk  30334  eupth2lem1  30569  helloworld  30816  topnfbey  30820  n0lpligALT  30836  ccatf1  33269  isarchi  33502  domnprodeq0  33599  0mplrim  33904  constrmon  34134  measvuni  34604  ddemeas  34626  sibf0  34724  signstfvneq0  34959  opelco3  36267  wsuclem  36315  unbdqndv1  37097  bj-projval  37632  bj-nuliota  37693  bj-0nmoore  37754  nlpineqsn  38054  poimirlem30  38301  pw2f1ocnv  43764  areaquad  43943  onexlimgt  43970  cantnfresb  44051  succlg  44055  oacl2g  44057  omabs2  44059  omcl2  44060  eu0  44246  ntrneikb  44820  r1rankcld  44955  en3lpVD  45553  0elaxnul  45692  omssaxinf2  45697  permaxnul  45717  permaxinf2lem  45721  supminfxr  46178  liminf0  46507  iblempty  46679  stoweidlem34  46748  sge00  47090  vonhoire  47386  prprelprb  48266  fpprbasnn  48494  stgr0  48725  prmringnzring  49102