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

Theorem noel 3877
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 3693 . . 3 (𝐴 ∈ (V ∖ V) → 𝐴 ∈ V)
2 eldifn 3694 . . 3 (𝐴 ∈ (V ∖ V) → ¬ 𝐴 ∈ V)
31, 2pm2.65i 183 . 2 ¬ 𝐴 ∈ (V ∖ V)
4 df-nul 3874 . . 3 ∅ = (V ∖ V)
54eleq2i 2679 . 2 (𝐴 ∈ ∅ ↔ 𝐴 ∈ (V ∖ V))
63, 5mtbir 311 1 ¬ 𝐴 ∈ ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wcel 1976  Vcvv 3172  cdif 3536  c0 3873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-nul 3874
This theorem is referenced by:  n0i  3878  eq0f  3883  n0fOLD  3886  rex0  3893  rab0  3908  rab0OLD  3909  un0  3918  in0  3919  0ss  3923  sbcel12  3934  sbcel2  3940  disj  3968  r19.2zb  4012  ral0  4027  rabsnifsb  4200  int0OLD  4420  iun0  4506  0iun  4507  br0  4625  0xp  5112  csbxp  5113  dm0  5247  dm0rn0  5250  reldm0  5251  elimasni  5398  cnv0  5441  co02  5552  ord0eln0  5682  nlim0  5686  nsuceq0  5708  dffv3  6084  0fv  6122  elfv2ex  6124  mpt20  6601  el2mpt2csbcl  7114  bropopvvv  7119  bropfvvvv  7121  tz7.44-2  7367  omordi  7510  omeulem1  7526  nnmordi  7575  omabs  7591  omsmolem  7597  0er  7644  0erOLD  7645  omxpenlem  7923  en3lp  8373  cantnfle  8428  r1sdom  8497  r1pwss  8507  alephordi  8757  axdc3lem2  9133  zorn2lem7  9184  nlt1pi  9584  xrinf0  11995  elixx3g  12015  elfz2  12159  fzm1  12244  om2uzlti  12566  hashf1lem2  13049  sum0  14245  fsumsplit  14264  sumsplit  14287  fsum2dlem  14289  prod0  14458  fprod2dlem  14495  sadc0  14960  sadcp1  14961  saddisjlem  14970  smu01lem  14991  smu01  14992  smu02  14993  lcmf0  15131  prmreclem5  15408  vdwap0  15464  ram0  15510  0catg  16117  oduclatb  16913  0g0  17032  dfgrp2e  17217  cntzrcl  17529  pmtrfrn  17647  psgnunilem5  17683  gexdvds  17768  gsumzsplit  18096  dprdcntz2  18206  00lss  18709  mplcoe1  19232  mplcoe5  19235  00ply1bas  19377  dsmmbas2  19842  dsmmfi  19843  maducoeval2  20207  madugsum  20210  0ntop  20477  haust1  20908  hauspwdom  21056  kqcldsat  21288  tsmssplit  21707  ustn0  21776  0met  21922  itg11  23181  itg0  23269  bddmulibl  23328  fsumharmonic  24455  ppiublem2  24645  lgsdir2lem3  24769  nbgra0edg  25727  uvtx01vtx  25786  clwwlknprop  26066  2wlkonot3v  26168  2spthonot3v  26169  rusgra0edg  26248  eupath2lem1  26270  helloworld  26479  topnfbey  26483  isarchi  28873  measvuni  29410  ddemeas  29432  sibf0  29529  signstfvneq0  29781  opelco3  30729  wsuclem  30823  wsuclemOLD  30824  unbdqndv1  31475  bj-projval  31980  bj-df-nul  32011  bj-nuliota  32013  finxp0  32207  poimirlem30  32412  pw2f1ocnv  36425  areaquad  36624  ntrneikb  37215  en3lpVD  37905  iblempty  38661  stoweidlem34  38731  sge00  39073  vonhoire  39367  uvtxa01vtx0  40625  vtxdg0v  40690  0enwwlksnge1  41062  wwlks2onv  41160  rusgr0edg  41178  clwwlks  41189  eupth2lem1  41388
  Copyright terms: Public domain W3C validator