Theorem noel 4330

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 2138, ax-11 2155, and ax-12 2172. (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 2105	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1556	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1800	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4324	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2826	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2711	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 488	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1803	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2812	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 397   = wceq 1542  ⊥wfal 1554  ∃wex 1782  [wsb 2068   ∈ wcel 2107  {cab 2710  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-dif 3951  df-nul 4323

This theorem is referenced by:  nel02  4332  n0i  4333  eq0f  4340  eq0ALT  4344  rex0  4357  rab0  4382  un0  4390  in0  4391  0ss  4396  sbcel12  4408  sbcel2  4415  disj  4447  disjOLD  4448  r19.2zb  4495  ral0OLD  4516  rabsnifsb  4726  iun0  5065  br0  5197  0xp  5773  csbxp  5774  dm0  5919  dm0rn0  5923  reldm0  5926  elimasni  6088  co02  6257  ord0eln0  6417  nlim0  6421  nsuceq0  6445  dffv3  6885  0fv  6933  elfv2ex  6935  mpo0  7491  el2mpocsbcl  8068  bropopvvv  8073  bropfvvvv  8075  tz7.44-2  8404  omordi  8563  nnmordi  8628  omabs  8647  omsmolem  8653  0er  8737  omxpenlem  9070  infn0  9304  en3lp  9606  cantnfle  9663  r1sdom  9766  r1pwss  9776  alephordi  10066  axdc3lem2  10443  zorn2lem7  10494  nlt1pi  10898  xrinf0  13314  elixx3g  13334  elfz2  13488  fzm1  13578  om2uzlti  13912  hashf1lem2  14414  sum0  15664  fsumsplit  15684  sumsplit  15711  fsum2dlem  15713  prod0  15884  fprod2dlem  15921  sadc0  16392  sadcp1  16393  saddisjlem  16402  smu01lem  16423  smu01  16424  smu02  16425  lcmf0  16568  prmreclem5  16850  vdwap0  16906  ram0  16952  0catg  17629  oduclatb  18457  0g0  18580  dfgrp2e  18845  cntzrcl  19186  pmtrfrn  19321  psgnunilem5  19357  gexdvds  19447  gsumzsplit  19790  dprdcntz2  19903  00lss  20545  dsmmfi  21285  mplcoe1  21584  mplcoe5  21587  00ply1bas  21754  maducoeval2  22134  madugsum  22137  0ntop  22399  haust1  22848  hauspwdom  22997  kqcldsat  23229  tsmssplit  23648  ustn0  23717  0met  23864  itg11  25200  itg0  25289  bddmulibl  25348  fsumharmonic  26506  ppiublem2  26696  lgsdir2lem3  26820  nulsslt  27288  nulssgt  27289  uvtx01vtx  28644  vtxdg0v  28720  0enwwlksnge1  29108  rusgr0edg  29217  clwwlk  29226  eupth2lem1  29461  helloworld  29708  topnfbey  29712  n0lpligALT  29725  ccatf1  32103  isarchi  32316  measvuni  33201  ddemeas  33223  sibf0  33322  signstfvneq0  33572  opelco3  34735  wsuclem  34786  unbdqndv1  35373  bj-projval  35866  bj-nuliota  35927  bj-0nmoore  35982  nlpineqsn  36278  poimirlem30  36507  pw2f1ocnv  41762  areaquad  41951  onexlimgt  41978  cantnfresb  42060  succlg  42064  oacl2g  42066  omabs2  42068  omcl2  42069  eu0  42257  ntrneikb  42831  r1rankcld  42976  en3lpVD  43592  supminfxr  44161  liminf0  44496  iblempty  44668  stoweidlem34  44737  sge00  45079  vonhoire  45375  prprelprb  46172  fpprbasnn  46384