Theorem noel 3735

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 3555	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3556	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 177	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3732	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2521	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 301	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1887   _Vcvv 3045   \ cdif 3401   (/)c0 3731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-dif 3407  df-nul 3732

This theorem is referenced by:  n0i  3736  n0f  3740  rex0  3746  abvor0  3750  rab0  3753  un0  3759  in0  3760  0ss  3763  sbcel12  3772  sbcel2  3778  disj  3805  r19.2zb  3859  ral0  3874  rabsnifsb  4040  int0  4248  iun0  4334  0iun  4335  br0  4449  pwne0  4573  0xp  4915  csbxp  4916  dm0  5048  dm0rn0  5051  reldm0  5052  elimasni  5195  cnv0  5239  co02  5349  ord0eln0  5477  nlim0  5481  nsuceq0  5503  dffv3  5861  0fv  5898  mpt20  6361  bropopvvv  6874  bropfvvvv  6876  tz7.44-2  7125  omordi  7267  omeulem1  7283  nnmordi  7332  omabs  7348  omsmolem  7354  0er  7398  omxpenlem  7673  en3lp  8121  cantnfle  8176  r1sdom  8245  r1pwss  8255  alephordi  8505  axdc3lem2  8881  zorn2lem7  8932  nlt1pi  9331  xrinf0  11623  xrinfm0OLD  11627  elixx3g  11648  elfz2  11791  fzm1  11874  om2uzlti  12164  hashf1lem2  12619  sum0  13787  fsumsplit  13806  sumsplit  13829  fsum2dlem  13831  prod0  13997  fprod2dlem  14034  sadc0  14428  sadcp1  14429  saddisjlem  14438  smu01lem  14459  smu01  14460  smu02  14461  lcmf0  14607  prmreclem5  14864  vdwap0  14926  ram0  14980  0catg  15593  oduclatb  16390  0g0  16506  cntzrcl  16981  pmtrfrn  17099  psgnunilem5  17135  gexdvds  17235  gsumzsplit  17560  dprdcntz2  17671  00lss  18165  mplcoe1  18689  mplcoe5  18692  00ply1bas  18833  dsmmbas2  19300  dsmmfi  19301  maducoeval2  19665  madugsum  19668  0ntop  19935  haust1  20368  hauspwdom  20516  kqcldsat  20748  tsmssplit  21166  ustn0  21235  0met  21381  itg11  22649  itg0  22737  bddmulibl  22796  fsumharmonic  23937  ppiublem2  24131  lgsdir2lem3  24253  nbgra0edg  25160  uvtx01vtx  25220  clwwlknprop  25500  2wlkonot3v  25603  2spthonot3v  25604  rusgra0edg  25683  eupath2lem1  25705  helloworld  25902  topnfbey  25906  isarchi  28499  measvuni  29036  ddemeas  29059  sibf0  29167  signstfvneq0  29461  opelco3  30420  wsuclem  30508  bj-projval  31590  bj-df-nul  31621  bj-nuliota  31623  finxp0  31783  poimirlem30  31970  pw2f1ocnv  35892  areaquad  36101  en3lpVD  37241  iblempty  37842  stoweidlem34  37895  sge00  38218  uvtxa01vtx0  39469  vtxdg0v  39533