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

Theorem noel 4185
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 2079, ax-11 2093, and ax-12 2106. (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 394 . . . . . . 7 ¬ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
21nex 1763 . . . . . 6 ¬ ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)
3 df-clab 2759 . . . . . . 7 (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} ↔ [𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
4 spsbe 2033 . . . . . . 7 ([𝑥 / 𝑦](𝑦 ∈ V ∧ ¬ 𝑦 ∈ V) → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
53, 4sylbi 209 . . . . . 6 (𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)} → ∃𝑦(𝑦 ∈ V ∧ ¬ 𝑦 ∈ V))
62, 5mto 189 . . . . 5 ¬ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
7 df-nul 4181 . . . . . . 7 ∅ = (V ∖ V)
8 df-dif 3834 . . . . . . 7 (V ∖ V) = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
97, 8eqtri 2802 . . . . . 6 ∅ = {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)}
109eleq2i 2857 . . . . 5 (𝑥 ∈ ∅ ↔ 𝑥 ∈ {𝑦 ∣ (𝑦 ∈ V ∧ ¬ 𝑦 ∈ V)})
116, 10mtbir 315 . . . 4 ¬ 𝑥 ∈ ∅
1211intnan 479 . . 3 ¬ (𝑥 = 𝐴𝑥 ∈ ∅)
1312nex 1763 . 2 ¬ ∃𝑥(𝑥 = 𝐴𝑥 ∈ ∅)
14 dfclel 2847 . 2 (𝐴 ∈ ∅ ↔ ∃𝑥(𝑥 = 𝐴𝑥 ∈ ∅))
1513, 14mtbir 315 1 ¬ 𝐴 ∈ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 387   = wceq 1507  wex 1742  [wsb 2015  wcel 2050  {cab 2758  Vcvv 3415  cdif 3828  c0 4180
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2750
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-dif 3834  df-nul 4181
This theorem is referenced by:  n0i  4187  eq0f  4193  rex0  4205  rab0  4225  un0  4232  in0  4233  0ss  4237  sbcel12  4247  sbcel2  4254  disj  4283  r19.2zb  4325  ral0  4340  rabsnifsb  4533  iun0  4852  br0  4979  0xp  5500  csbxp  5501  dm0  5638  dm0rn0  5641  reldm0  5642  elimasni  5798  co02  5954  ord0eln0  6085  nlim0  6089  nsuceq0  6111  dffv3  6497  0fv  6541  elfv2ex  6543  mpo0  7057  el2mpocsbcl  7590  bropopvvv  7595  bropfvvvv  7597  tz7.44-2  7849  omordi  7995  nnmordi  8060  omabs  8076  omsmolem  8082  0er  8128  omxpenlem  8416  en3lp  8873  cantnfle  8930  r1sdom  8999  r1pwss  9009  alephordi  9296  axdc3lem2  9673  zorn2lem7  9724  nlt1pi  10128  xrinf0  12550  elixx3g  12570  elfz2  12718  fzm1  12806  om2uzlti  13136  hashf1lem2  13630  sum0  14941  fsumsplit  14960  sumsplit  14986  fsum2dlem  14988  prod0  15160  fprod2dlem  15197  sadc0  15666  sadcp1  15667  saddisjlem  15676  smu01lem  15697  smu01  15698  smu02  15699  lcmf0  15837  prmreclem5  16115  vdwap0  16171  ram0  16217  0catg  16819  oduclatb  17615  0g0  17734  dfgrp2e  17920  cntzrcl  18231  pmtrfrn  18350  psgnunilem5  18386  psgnunilem5OLD  18387  gexdvds  18473  gsumzsplit  18803  dprdcntz2  18913  00lss  19438  mplcoe1  19962  mplcoe5  19965  00ply1bas  20114  dsmmbas2  20586  dsmmfi  20587  maducoeval2  20956  madugsum  20959  0ntop  21220  haust1  21667  hauspwdom  21816  kqcldsat  22048  tsmssplit  22466  ustn0  22535  0met  22682  itg11  23998  itg0  24086  bddmulibl  24145  fsumharmonic  25294  ppiublem2  25484  lgsdir2lem3  25608  uvtx01vtx  26885  vtxdg0v  26961  0enwwlksnge1  27353  rusgr0edg  27482  clwwlk  27492  eupth2lem1  27751  helloworld  28024  topnfbey  28028  n0lpligALT  28041  isarchi  30477  measvuni  31118  ddemeas  31140  sibf0  31237  signstfvneq0  31489  opelco3  32538  wsuclem  32633  unbdqndv1  33367  bj-projval  33826  bj-df-nul  33859  bj-nuliota  33861  bj-0nmoore  33915  nlpineqsn  34130  poimirlem30  34363  nel02  35027  pw2f1ocnv  39030  areaquad  39219  ntrneikb  39807  r1rankcld  39942  en3lpVD  40598  supminfxr  41172  liminf0  41506  iblempty  41681  stoweidlem34  41751  sge00  42090  vonhoire  42386  prprelprb  43048  fpprbasnn  43263
  Copyright terms: Public domain W3C validator