Theorem noel 4285

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 2144, ax-11 2160, and ax-12 2180. (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 2109	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1555	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1798	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4282	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2823	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2710	. . . . . 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 2807	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-dif 3900  df-nul 4281

This theorem is referenced by:  nel02  4286  n0i  4287  eq0f  4294  eq0ALT  4298  rex0  4307  rab0  4333  un0  4341  in0  4342  0ss  4347  sbcel12  4358  sbcel2  4365  disj  4397  r19.2zb  4443  rabsnifsb  4672  uni0  4884  iun0  5008  br0  5138  0xp  5713  xp0  5714  csbxp  5715  dm0  5859  dm0rn0  5863  dm0rn0OLD  5864  reldm0  5867  elimasni  6039  co02  6208  ord0eln0  6362  nlim0  6366  nsuceq0  6391  dffv3  6818  0fv  6863  elfv2ex  6865  mpo0  7431  el2mpocsbcl  8015  bropopvvv  8020  bropfvvvv  8022  tz7.44-2  8326  omordi  8481  nnmordi  8546  omabs  8566  omsmolem  8572  0er  8660  omxpenlem  8991  infn0  9186  en3lp  9504  cantnfle  9561  r1sdom  9667  r1pwss  9677  alephordi  9965  axdc3lem2  10342  zorn2lem7  10393  nlt1pi  10797  xrinf0  13238  elixx3g  13258  elfz2  13414  fzm1  13507  om2uzlti  13857  hashf1lem2  14363  sum0  15628  fsumsplit  15648  sumsplit  15675  fsum2dlem  15677  prod0  15850  fprod2dlem  15887  sadc0  16365  sadcp1  16366  saddisjlem  16375  smu01lem  16396  smu01  16397  smu02  16398  lcmf0  16545  prmreclem5  16832  vdwap0  16888  ram0  16934  0catg  17594  oduclatb  18413  chnccats1  18531  chnccat  18532  0g0  18572  dfgrp2e  18876  cntzrcl  19239  pmtrfrn  19370  psgnunilem5  19406  gexdvds  19496  gsumzsplit  19839  dprdcntz2  19952  00lss  20874  dsmmfi  21675  mplcoe1  21972  mplcoe5  21975  00ply1bas  22152  maducoeval2  22555  madugsum  22558  0ntop  22820  haust1  23267  hauspwdom  23416  kqcldsat  23648  tsmssplit  24067  ustn0  24136  0met  24281  itg11  25619  itg0  25708  bddmulibl  25767  fsumharmonic  26949  ppiublem2  27141  lgsdir2lem3  27265  nulsslt  27738  nulssgt  27739  uvtx01vtx  29375  vtxdg0v  29452  dfpth2  29707  0enwwlksnge1  29842  rusgr0edg  29954  clwwlk  29963  eupth2lem1  30198  helloworld  30445  topnfbey  30449  n0lpligALT  30464  ccatf1  32930  isarchi  33151  constrmon  33757  measvuni  34227  ddemeas  34249  sibf0  34347  signstfvneq0  34585  opelco3  35819  wsuclem  35867  unbdqndv1  36550  bj-projval  37038  bj-nuliota  37099  bj-0nmoore  37154  nlpineqsn  37450  poimirlem30  37698  pw2f1ocnv  43078  areaquad  43257  onexlimgt  43284  cantnfresb  43365  succlg  43369  oacl2g  43371  omabs2  43373  omcl2  43374  eu0  43561  ntrneikb  44135  r1rankcld  44272  en3lpVD  44885  0elaxnul  45024  omssaxinf2  45029  permaxnul  45049  permaxinf2lem  45053  supminfxr  45510  liminf0  45839  iblempty  46011  stoweidlem34  46080  sge00  46422  vonhoire  46718  prprelprb  47556  fpprbasnn  47768  stgr0  47999