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

Theorem noel 3755
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 3592 . . 3
2 eldifn 3593 . . 3
31, 2pm2.65i 173 . 2
4 df-nul 3752 . . 3
54eleq2i 2532 . 2
63, 5mtbir 299 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  e.wcel 1758   cvv 3081  \cdif 3439   c0 3751
This theorem is referenced by:  n0i  3756  n0f  3759  rex0  3765  abvor0  3769  rab0  3772  un0  3776  in0  3777  0ss  3780  sbcel12  3789  sbcel2  3797  disj  3833  r19.2zb  3884  ral0  3898  rabsnifsb  4060  int0  4259  iun0  4343  0iun  4344  br0  4455  sbcbr123  4460  pwne0  4579  ord0eln0  4890  nlim0  4894  nsuceq0  4916  0xp  5034  csbxp  5035  dm0  5170  dm0rn0  5173  reldm0  5174  elimasni  5315  cnv0  5359  co02  5470  dffv3  5809  0fv  5846  mpt20  6288  bropopvvv  6786  tz7.44-2  6997  0we1  7080  omordi  7139  omeulem1  7155  nnmordi  7204  omabs  7220  omsmolem  7226  0er  7270  omxpenlem  7546  en3lp  7959  cantnfle  8016  cantnfleOLD  8046  r1sdom  8118  r1pwss  8128  alephordi  8381  axdc3lem2  8757  zorn2lem7  8808  brdom3  8832  canthwe  8955  nlt1pi  9212  xrinfm0  11438  elixx3g  11452  elfz2  11589  om2uzlti  11918  hashf1lem2  12367  swrd0  12485  sum0  13356  fsumsplit  13374  sumsplit  13393  fsum2dlem  13395  sadc0  13808  sadcp1  13809  saddisjlem  13818  smu01lem  13839  smu01  13840  smu02  13841  prmreclem5  14139  vdwap0  14195  ram0  14241  0catg  14784  oduclatb  15473  0g0  15593  cntzrcl  16004  pmtrfrn  16123  psgnunilem5  16159  gexdvds  16244  gsumzsplit  16579  gsumzsplitOLD  16580  dprdcntz2  16711  00lss  17199  mplcoe1  17721  mplcoe5  17725  mplcoe2OLD  17727  mplrcl  17748  00ply1bas  17875  dsmmbas2  18355  dsmmfi  18356  maducoeval2  18714  madugsum  18717  0ntop  18917  haust1  19355  hauspwdom  19504  kqcldsat  19705  tsmssplit  20125  ustn0  20194  0met  20340  itg11  21569  itg0  21657  bddmulibl  21716  fsumharmonic  22805  ppiublem2  22942  lgsdir2lem3  23064  nbgra0edg  23812  uvtx01vtx  23869  eupath2lem1  24067  helloworld  24127  isarchi  26660  measvuni  27085  ddemeas  27108  sibf0  27176  signstfvneq0  27429  prod0  27912  fprod2dlem  27947  opelco3  28045  wsuclem  28218  pw2f1ocnv  29846  areaquad  30052  iblempty  30512  stoweidlem34  30563  2wlkonot3v  31271  2spthonot3v  31272  clwwlknprop  31312  rusgra0edg  31450  en3lpVD  32424  bj-projval  33334  bj-df-nul  33364  bj-nuliota  33366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3083  df-dif 3445  df-nul 3752
  Copyright terms: Public domain W3C validator