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

Theorem noel 4293
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 2136, ax-11 2151, and ax-12 2167. (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 403 . . . . . . 7 ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
21nex 1792 . . . . . 6 ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
3 df-clab 2797 . . . . . . 7 (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
4 spsbe 2079 . . . . . . 7 ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
53, 4sylbi 218 . . . . . 6 (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
62, 5mto 198 . . . . 5 ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
7 df-nul 4289 . . . . . . 7 ∅ = (V ∖ V)
8 df-dif 3936 . . . . . . 7 (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
97, 8eqtri 2841 . . . . . 6 ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
109eleq2i 2901 . . . . 5 (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)})
116, 10mtbir 324 . . . 4 ¬ 𝑥 ∈ ∅
1211intnan 487 . . 3 ¬ (𝑥 = 𝐴𝑥 ∈ ∅)
1312nex 1792 . 2 ¬ ∃𝑥(𝑥 = 𝐴𝑥 ∈ ∅)
14 dfclel 2891 . 2 (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ ∅))
1513, 14mtbir 324 1 ¬ 𝐴 ∈ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 396   = wceq 1528  wex 1771  [wsb 2060  wcel 2105  {cab 2796  Vcvv 3492  cdif 3930  c0 4288
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-dif 3936  df-nul 4289
This theorem is referenced by:  nel02  4295  n0i  4296  eq0f  4302  rex0  4314  rab0  4334  un0  4341  in0  4342  0ss  4347  sbcel12  4357  sbcel2  4364  disj  4395  r19.2zb  4437  ral0  4452  rabsnifsb  4650  iun0  4976  br0  5106  0xp  5642  csbxp  5643  dm0  5783  dm0rn0  5788  reldm0  5791  elimasni  5949  co02  6106  ord0eln0  6238  nlim0  6242  nsuceq0  6264  dffv3  6659  0fv  6702  elfv2ex  6704  mpo0  7228  el2mpocsbcl  7769  bropopvvv  7774  bropfvvvv  7776  tz7.44-2  8032  omordi  8181  nnmordi  8246  omabs  8263  omsmolem  8269  0er  8315  omxpenlem  8606  en3lp  9065  cantnfle  9122  r1sdom  9191  r1pwss  9201  alephordi  9488  axdc3lem2  9861  zorn2lem7  9912  nlt1pi  10316  xrinf0  12719  elixx3g  12739  elfz2  12887  fzm1  12975  om2uzlti  13306  hashf1lem2  13802  sum0  15066  fsumsplit  15085  sumsplit  15111  fsum2dlem  15113  prod0  15285  fprod2dlem  15322  sadc0  15791  sadcp1  15792  saddisjlem  15801  smu01lem  15822  smu01  15823  smu02  15824  lcmf0  15966  prmreclem5  16244  vdwap0  16300  ram0  16346  0catg  16946  oduclatb  17742  0g0  17862  dfgrp2e  18067  cntzrcl  18395  pmtrfrn  18515  psgnunilem5  18551  gexdvds  18638  gsumzsplit  18976  dprdcntz2  19089  00lss  19642  mplcoe1  20174  mplcoe5  20177  00ply1bas  20336  dsmmfi  20810  maducoeval2  21177  madugsum  21180  0ntop  21441  haust1  21888  hauspwdom  22037  kqcldsat  22269  tsmssplit  22687  ustn0  22756  0met  22903  itg11  24219  itg0  24307  bddmulibl  24366  fsumharmonic  25516  ppiublem2  25706  lgsdir2lem3  25830  uvtx01vtx  27106  vtxdg0v  27182  0enwwlksnge1  27569  rusgr0edg  27679  clwwlk  27688  eupth2lem1  27924  helloworld  28171  topnfbey  28175  n0lpligALT  28188  ccatf1  30552  isarchi  30738  measvuni  31372  ddemeas  31394  sibf0  31491  signstfvneq0  31741  opelco3  32915  wsuclem  33009  unbdqndv1  33744  bj-projval  34205  bj-df-nul  34242  bj-nuliota  34244  bj-0nmoore  34298  nlpineqsn  34571  poimirlem30  34803  pw2f1ocnv  39512  areaquad  39701  eu0  39764  ntrneikb  40322  r1rankcld  40444  en3lpVD  41056  supminfxr  41616  liminf0  41950  iblempty  42126  stoweidlem34  42196  sge00  42535  vonhoire  42831  prprelprb  43556  fpprbasnn  43771
  Copyright terms: Public domain W3C validator