Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  noel Structured version   Visualization version   GIF version

Theorem noel 4269
 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 2145, ax-11 2161, and ax-12 2178. (Revised by Steven Nguyen, 3-May-2023.)
Assertion
Ref Expression
noel ¬ 𝐴 ∈ ∅

Proof of Theorem noel
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 pm3.24 406 . . . . . . 7 ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
21nex 1802 . . . . . 6 ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
3 df-clab 2801 . . . . . . 7 (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
4 spsbe 2088 . . . . . . 7 ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
53, 4sylbi 220 . . . . . 6 (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
62, 5mto 200 . . . . 5 ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
7 df-nul 4266 . . . . . . 7 ∅ = (V ∖ V)
8 df-dif 3911 . . . . . . 7 (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
97, 8eqtri 2845 . . . . . 6 ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
109eleq2i 2905 . . . . 5 (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)})
116, 10mtbir 326 . . . 4 ¬ 𝑥 ∈ ∅
1211intnan 490 . . 3 ¬ (𝑥 = 𝐴𝑥 ∈ ∅)
1312nex 1802 . 2 ¬ ∃𝑥(𝑥 = 𝐴𝑥 ∈ ∅)
14 dfclel 2895 . 2 (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ ∅))
1513, 14mtbir 326 1 ¬ 𝐴 ∈ ∅
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ∧ wa 399   = wceq 1538  ∃wex 1781  [wsb 2069   ∈ wcel 2114  {cab 2800  Vcvv 3469   ∖ cdif 3905  ∅c0 4265 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-dif 3911  df-nul 4266 This theorem is referenced by:  nel02  4270  n0i  4271  eq0f  4277  rex0  4289  rab0  4309  un0  4316  in0  4317  0ss  4322  sbcel12  4332  sbcel2  4339  disj  4371  r19.2zb  4413  ral0  4428  rabsnifsb  4632  iun0  4960  br0  5091  0xp  5626  csbxp  5627  dm0  5767  dm0rn0  5772  reldm0  5775  elimasni  5934  co02  6091  ord0eln0  6223  nlim0  6227  nsuceq0  6249  dffv3  6648  0fv  6691  elfv2ex  6693  mpo0  7223  el2mpocsbcl  7767  bropopvvv  7772  bropfvvvv  7774  tz7.44-2  8030  omordi  8179  nnmordi  8244  omabs  8261  omsmolem  8267  0er  8313  omxpenlem  8605  en3lp  9065  cantnfle  9122  r1sdom  9191  r1pwss  9201  alephordi  9489  axdc3lem2  9862  zorn2lem7  9913  nlt1pi  10317  xrinf0  12719  elixx3g  12739  elfz2  12892  fzm1  12982  om2uzlti  13313  hashf1lem2  13810  sum0  15069  fsumsplit  15088  sumsplit  15114  fsum2dlem  15116  prod0  15288  fprod2dlem  15325  sadc0  15792  sadcp1  15793  saddisjlem  15802  smu01lem  15823  smu01  15824  smu02  15825  lcmf0  15967  prmreclem5  16245  vdwap0  16301  ram0  16347  0catg  16949  oduclatb  17745  0g0  17865  dfgrp2e  18120  cntzrcl  18448  pmtrfrn  18577  psgnunilem5  18613  gexdvds  18700  gsumzsplit  19038  dprdcntz2  19151  00lss  19704  dsmmfi  20425  mplcoe1  20703  mplcoe5  20706  00ply1bas  20867  maducoeval2  21243  madugsum  21246  0ntop  21508  haust1  21955  hauspwdom  22104  kqcldsat  22336  tsmssplit  22755  ustn0  22824  0met  22971  itg11  24293  itg0  24381  bddmulibl  24440  fsumharmonic  25595  ppiublem2  25785  lgsdir2lem3  25909  uvtx01vtx  27185  vtxdg0v  27261  0enwwlksnge1  27648  rusgr0edg  27757  clwwlk  27766  eupth2lem1  28001  helloworld  28248  topnfbey  28252  n0lpligALT  28265  ccatf1  30635  isarchi  30842  measvuni  31547  ddemeas  31569  sibf0  31666  signstfvneq0  31916  opelco3  33092  wsuclem  33186  unbdqndv1  33921  bj-projval  34393  bj-df-nul  34433  bj-nuliota  34435  bj-0nmoore  34488  nlpineqsn  34786  poimirlem30  35045  pw2f1ocnv  39908  areaquad  40096  eu0  40158  ntrneikb  40730  r1rankcld  40873  en3lpVD  41485  supminfxr  42042  liminf0  42374  iblempty  42546  stoweidlem34  42615  sge00  42954  vonhoire  43250  prprelprb  43973  fpprbasnn  44186
 Copyright terms: Public domain W3C validator