Theorem noel 3629

Description: The empty set has no elements. Theorem 6.14 of [Quine] p. 44. (Contributed by NM, 5-Aug-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 3466	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3467	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 173	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3626	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2497	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 299	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1755   _Vcvv 2962   \ cdif 3313   (/)c0 3625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-dif 3319  df-nul 3626

This theorem is referenced by:  n0i  3630  n0f  3633  rex0  3639  abvor0  3643  rab0  3646  un0  3650  in0  3651  0ss  3654  sbcel12  3663  sbcel2  3671  disj  3707  r19.2zb  3758  ral0  3772  rabsnifsb  3931  int0  4130  iun0  4214  0iun  4215  br0  4326  sbcbr123  4331  pwne0  4450  ord0eln0  4760  nlim0  4764  nsuceq0  4786  0xp  4904  csbxp  4905  dm0  5040  dm0rn0  5043  reldm0  5044  elimasni  5184  cnv0  5228  co02  5339  dffv3  5675  0fv  5711  mpt20  6145  bropopvvv  6642  tz7.44-2  6849  0we1  6934  omordi  6993  omeulem1  7009  nnmordi  7058  omabs  7074  omsmolem  7080  0er  7124  omxpenlem  7400  en3lp  7810  cantnfle  7867  cantnfleOLD  7897  r1sdom  7969  r1pwss  7979  alephordi  8232  axdc3lem2  8608  zorn2lem7  8659  brdom3  8683  canthwe  8806  nlt1pi  9063  xrinfm0  11287  elixx3g  11301  elfz2  11431  om2uzlti  11757  hashf1lem2  12193  swrd0  12311  sum0  13182  fsumsplit  13200  sumsplit  13219  fsum2dlem  13221  sadc0  13633  sadcp1  13634  saddisjlem  13643  smu01lem  13664  smu01  13665  smu02  13666  prmreclem5  13964  vdwap0  14020  ram0  14066  0catg  14608  oduclatb  15297  0g0  15417  cntzrcl  15825  pmtrfrn  15944  psgnunilem5  15980  gexdvds  16063  gsumzsplit  16398  gsumzsplitOLD  16399  dprdcntz2  16510  00lss  16945  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  mplrcl  17503  strov2rcl  17590  00ply1bas  17593  dsmmbas2  18004  dsmmfi  18005  maducoeval2  18288  madugsum  18291  0ntop  18360  haust1  18798  hauspwdom  18947  kqcldsat  19148  tsmssplit  19568  ustn0  19637  0met  19783  itg11  21011  itg0  21099  bddmulibl  21158  fsumharmonic  22290  ppiublem2  22427  lgsdir2lem3  22549  nbgra0edg  23166  uvtx01vtx  23223  eupath2lem1  23421  helloworld  23481  isarchi  26023  measvuni  26482  ddemeas  26506  sibf0  26568  signstfvneq0  26821  prod0  27303  fprod2dlem  27338  opelco3  27436  wsuclem  27609  pw2f1ocnv  29231  areaquad  29437  stoweidlem34  29675  2wlkonot3v  30240  2spthonot3v  30241  clwwlknprop  30281  rusgra0edg  30419  en3lpVD  31304  bj-projval  32093