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

Theorem noel 3911
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.)
Assertion
Ref Expression
noel ¬ 𝐴 ∈ ∅

Proof of Theorem noel
StepHypRef Expression
1 eldifi 3724 . . 3 (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2 eldifn 3725 . . 3 (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
31, 2pm2.65i 185 . 2 ¬ 𝐴 ∈ (V ∖ V)
4 df-nul 3908 . . 3 ∅ = (V ∖ V)
54eleq2i 2691 . 2 (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
63, 5mtbir 313 1 ¬ 𝐴 ∈ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1988  Vcvv 3195  cdif 3564  c0 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-nul 3908
This theorem is referenced by:  n0i  3912  eq0f  3917  n0fOLD  3920  rex0  3930  rab0  3946  rab0OLD  3947  un0  3958  in0  3959  0ss  3963  sbcel12  3974  sbcel2  3980  disj  4008  r19.2zb  4052  ral0  4067  rabsnifsb  4248  int0OLD  4482  iun0  4567  br0  4692  0xp  5189  csbxp  5190  dm0  5328  dm0rn0  5331  reldm0  5332  elimasni  5480  cnv0OLD  5524  co02  5637  ord0eln0  5767  nlim0  5771  nsuceq0  5793  dffv3  6174  0fv  6214  elfv2ex  6216  mpt20  6710  el2mpt2csbcl  7235  bropopvvv  7240  bropfvvvv  7242  tz7.44-2  7488  omordi  7631  omeulem1  7647  nnmordi  7696  omabs  7712  omsmolem  7718  0er  7765  0erOLD  7766  omxpenlem  8046  en3lp  8498  cantnfle  8553  r1sdom  8622  r1pwss  8632  alephordi  8882  axdc3lem2  9258  zorn2lem7  9309  nlt1pi  9713  xrinf0  12153  elixx3g  12173  elfz2  12318  fzm1  12404  om2uzlti  12732  hashf1lem2  13223  sum0  14433  fsumsplit  14452  sumsplit  14480  fsum2dlem  14482  prod0  14654  fprod2dlem  14691  sadc0  15157  sadcp1  15158  saddisjlem  15167  smu01lem  15188  smu01  15189  smu02  15190  lcmf0  15328  prmreclem5  15605  vdwap0  15661  ram0  15707  0catg  16329  oduclatb  17125  0g0  17244  dfgrp2e  17429  cntzrcl  17741  pmtrfrn  17859  psgnunilem5  17895  gexdvds  17980  gsumzsplit  18308  dprdcntz2  18418  00lss  18923  mplcoe1  19446  mplcoe5  19449  00ply1bas  19591  dsmmbas2  20062  dsmmfi  20063  maducoeval2  20427  madugsum  20430  0ntop  20691  haust1  21137  hauspwdom  21285  kqcldsat  21517  tsmssplit  21936  ustn0  22005  0met  22152  itg11  23439  itg0  23527  bddmulibl  23586  fsumharmonic  24719  ppiublem2  24909  lgsdir2lem3  25033  uvtxa01vtx0  26278  vtxdg0v  26350  0enwwlksnge1  26730  wwlks2onv  26828  rusgr0edg  26849  clwwlks  26860  eupth2lem1  27058  helloworld  27291  topnfbey  27295  n0lpligALT  27306  isarchi  29710  measvuni  30251  ddemeas  30273  sibf0  30370  signstfvneq0  30623  opelco3  31652  wsuclem  31747  wsuclemOLD  31748  unbdqndv1  32474  bj-projval  32959  bj-df-nul  32992  bj-nuliota  32994  bj-0nmoore  33042  poimirlem30  33410  pw2f1ocnv  37423  areaquad  37621  ntrneikb  38212  en3lpVD  38900  supminfxr  39507  liminf0  39819  iblempty  39944  stoweidlem34  40014  sge00  40356  vonhoire  40649
  Copyright terms: Public domain W3C validator