Theorem noel 4292

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 2147, ax-11 2163, and ax-12 2185. (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 2112	. . . . . 6 ⊢ (∀𝑦 ¬ ⊥ → ¬ [𝑥 / 𝑦]⊥)
2		fal 1556	. . . . . 6 ⊢ ¬ ⊥
3	1, 2	mpg 1799	. . . . 5 ⊢ ¬ [𝑥 / 𝑦]⊥
4		dfnul4 4289	. . . . . . 7 ⊢ ∅ = {𝑦 ∣ ⊥}
5	4	eleq2i 2829	. . . . . 6 ⊢ (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ ⊥})
6		df-clab 2716	. . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥)
7	5, 6	bitri 275	. . . . 5 ⊢ (𝑥 ∈ ∅ ↔ [𝑥 / 𝑦]⊥)
8	3, 7	mtbir 323	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
9	8	intnan 486	. . 3 ⊢ ¬ (𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
10	9	nex 1802	. 2 ⊢ ¬ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅)
11		dfclel 2813	. 2 ⊢ (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ ∅))
12	10, 11	mtbir 323	1 ⊢ ¬ 𝐴 ∈ ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1542  ⊥wfal 1554  ∃wex 1781  [wsb 2068   ∈ wcel 2114  {cab 2715  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-dif 3906  df-nul 4288

This theorem is referenced by:  nel02  4293  n0i  4294  eq0f  4301  eq0ALT  4305  rex0  4314  rab0  4340  un0  4348  in0  4349  0ss  4354  sbcel12  4365  sbcel2  4372  disj  4404  rabsnifsb  4681  uni0  4893  iun0  5019  br0  5149  0xp  5731  xp0  5732  csbxp  5733  dm0  5877  dm0rn0  5881  dm0rn0OLD  5882  reldm0  5885  elimasni  6058  co02  6227  ord0eln0  6381  nlim0  6385  nsuceq0  6410  dffv3  6838  0fv  6883  elfv2ex  6885  mpo0  7453  el2mpocsbcl  8037  bropopvvv  8042  bropfvvvv  8044  tz7.44-2  8348  omordi  8503  nnmordi  8569  omabs  8589  omsmolem  8595  0er  8684  omxpenlem  9018  infn0  9214  en3lp  9535  cantnfle  9592  r1sdom  9698  r1pwss  9708  alephordi  9996  axdc3lem2  10373  zorn2lem7  10424  nlt1pi  10829  xrinf0  13266  elixx3g  13286  elfz2  13442  fzm1  13535  om2uzlti  13885  hashf1lem2  14391  sum0  15656  fsumsplit  15676  sumsplit  15703  fsum2dlem  15705  prod0  15878  fprod2dlem  15915  sadc0  16393  sadcp1  16394  saddisjlem  16403  smu01lem  16424  smu01  16425  smu02  16426  lcmf0  16573  prmreclem5  16860  vdwap0  16916  ram0  16962  0catg  17623  oduclatb  18442  chnccats1  18560  chnccat  18561  0g0  18601  dfgrp2e  18905  cntzrcl  19268  pmtrfrn  19399  psgnunilem5  19435  gexdvds  19525  gsumzsplit  19868  dprdcntz2  19981  00lss  20904  dsmmfi  21705  mplcoe1  22004  mplcoe5  22007  00ply1bas  22192  maducoeval2  22596  madugsum  22599  0ntop  22861  haust1  23308  hauspwdom  23457  kqcldsat  23689  tsmssplit  24108  ustn0  24177  0met  24322  itg11  25660  itg0  25749  bddmulibl  25808  fsumharmonic  26990  ppiublem2  27182  lgsdir2lem3  27306  nulslts  27783  nulsgts  27784  uvtx01vtx  29482  vtxdg0v  29559  dfpth2  29814  0enwwlksnge1  29949  rusgr0edg  30061  clwwlk  30070  eupth2lem1  30305  helloworld  30552  topnfbey  30556  n0lpligALT  30572  ccatf1  33042  isarchi  33276  domnprodeq0  33370  constrmon  33922  measvuni  34392  ddemeas  34414  sibf0  34512  signstfvneq0  34750  opelco3  35991  wsuclem  36039  unbdqndv1  36730  bj-projval  37244  bj-nuliota  37305  bj-0nmoore  37365  nlpineqsn  37663  poimirlem30  37901  pw2f1ocnv  43394  areaquad  43573  onexlimgt  43600  cantnfresb  43681  succlg  43685  oacl2g  43687  omabs2  43689  omcl2  43690  eu0  43876  ntrneikb  44450  r1rankcld  44587  en3lpVD  45200  0elaxnul  45339  omssaxinf2  45344  permaxnul  45364  permaxinf2lem  45368  supminfxr  45822  liminf0  46151  iblempty  46323  stoweidlem34  46392  sge00  46734  vonhoire  47030  prprelprb  47877  fpprbasnn  48089  stgr0  48320