Theorem noel 3789

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	|- -. A e. (/)

Proof of Theorem noel

Step	Hyp	Ref	Expression
1		eldifi 3626	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3627	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 173	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3786	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2545	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 299	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1767   _Vcvv 3113   \ cdif 3473   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-nul 3786

This theorem is referenced by:  n0i  3790  n0f  3793  rex0  3799  abvor0  3803  rab0  3806  un0  3810  in0  3811  0ss  3814  sbcel12  3823  sbcel2  3831  disj  3867  r19.2zb  3918  ral0  3932  rabsnifsb  4095  int0  4296  iun0  4381  0iun  4382  br0  4493  sbcbr123  4498  pwne0  4617  ord0eln0  4932  nlim0  4936  nsuceq0  4958  0xp  5080  csbxp  5081  dm0  5216  dm0rn0  5219  reldm0  5220  elimasni  5364  cnv0  5409  co02  5521  dffv3  5862  0fv  5899  mpt20  6351  bropopvvv  6863  tz7.44-2  7073  0we1  7156  omordi  7215  omeulem1  7231  nnmordi  7280  omabs  7296  omsmolem  7302  0er  7346  omxpenlem  7618  en3lp  8033  cantnfle  8090  cantnfleOLD  8120  r1sdom  8192  r1pwss  8202  alephordi  8455  axdc3lem2  8831  zorn2lem7  8882  brdom3  8906  canthwe  9029  nlt1pi  9284  xrinfm0  11528  elixx3g  11542  elfz2  11679  om2uzlti  12029  hashf1lem2  12471  swrd0  12621  sum0  13506  fsumsplit  13525  sumsplit  13546  fsum2dlem  13548  sadc0  13963  sadcp1  13964  saddisjlem  13973  smu01lem  13994  smu01  13995  smu02  13996  prmreclem5  14297  vdwap0  14353  ram0  14399  0catg  14942  oduclatb  15631  0g0  15751  cntzrcl  16170  pmtrfrn  16289  psgnunilem5  16325  gexdvds  16410  gsumzsplit  16747  gsumzsplitOLD  16748  dprdcntz2  16888  00lss  17388  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  mplrcl  17953  00ply1bas  18080  dsmmbas2  18563  dsmmfi  18564  maducoeval2  18937  madugsum  18940  0ntop  19209  haust1  19647  hauspwdom  19796  kqcldsat  19997  tsmssplit  20417  ustn0  20486  0met  20632  itg11  21861  itg0  21949  bddmulibl  22008  fsumharmonic  23097  ppiublem2  23234  lgsdir2lem3  23356  nbgra0edg  24136  uvtx01vtx  24196  clwwlknprop  24476  2wlkonot3v  24579  2spthonot3v  24580  rusgra0edg  24659  eupath2lem1  24681  helloworld  24877  isarchi  27416  measvuni  27853  ddemeas  27876  sibf0  27944  signstfvneq0  28197  prod0  28680  fprod2dlem  28715  opelco3  28813  wsuclem  28986  pw2f1ocnv  30611  areaquad  30817  iblempty  31311  stoweidlem34  31362  en3lpVD  32743  bj-projval  33653  bj-df-nul  33683  bj-nuliota  33685