Theorem noel 3765

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 3587	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3588	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 176	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3762	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2500	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 300	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1868   _Vcvv 3081   \ cdif 3433   (/)c0 3761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-dif 3439  df-nul 3762

This theorem is referenced by:  n0i  3766  n0f  3770  rex0  3776  abvor0  3780  rab0  3783  un0  3787  in0  3788  0ss  3791  sbcel12  3800  sbcel2  3806  disj  3833  r19.2zb  3887  ral0  3902  rabsnifsb  4065  int0  4266  iun0  4352  0iun  4353  br0  4467  pwne0  4591  0xp  4931  csbxp  4932  dm0  5064  dm0rn0  5067  reldm0  5068  elimasni  5211  cnv0  5255  co02  5365  ord0eln0  5493  nlim0  5497  nsuceq0  5519  dffv3  5874  0fv  5911  mpt20  6372  bropopvvv  6884  tz7.44-2  7130  omordi  7272  omeulem1  7288  nnmordi  7337  omabs  7353  omsmolem  7359  0er  7403  omxpenlem  7676  en3lp  8124  cantnfle  8178  r1sdom  8247  r1pwss  8257  alephordi  8506  axdc3lem2  8882  zorn2lem7  8933  nlt1pi  9332  xrinf0  11624  xrinfm0OLD  11628  elixx3g  11649  elfz2  11792  fzm1  11875  om2uzlti  12164  hashf1lem2  12617  sum0  13775  fsumsplit  13794  sumsplit  13817  fsum2dlem  13819  prod0  13985  fprod2dlem  14022  sadc0  14416  sadcp1  14417  saddisjlem  14426  smu01lem  14447  smu01  14448  smu02  14449  lcmf0  14595  prmreclem5  14852  vdwap0  14914  ram0  14968  0catg  15581  oduclatb  16378  0g0  16494  cntzrcl  16969  pmtrfrn  17087  psgnunilem5  17123  gexdvds  17223  gsumzsplit  17548  dprdcntz2  17659  00lss  18153  mplcoe1  18677  mplcoe5  18680  00ply1bas  18821  dsmmbas2  19287  dsmmfi  19288  maducoeval2  19652  madugsum  19655  0ntop  19922  haust1  20355  hauspwdom  20503  kqcldsat  20735  tsmssplit  21153  ustn0  21222  0met  21368  itg11  22636  itg0  22724  bddmulibl  22783  fsumharmonic  23924  ppiublem2  24118  lgsdir2lem3  24240  nbgra0edg  25146  uvtx01vtx  25206  clwwlknprop  25486  2wlkonot3v  25589  2spthonot3v  25590  rusgra0edg  25669  eupath2lem1  25691  helloworld  25888  topnfbey  25892  isarchi  28494  measvuni  29032  ddemeas  29055  sibf0  29163  signstfvneq0  29457  opelco3  30415  wsuclem  30503  bj-projval  31546  bj-df-nul  31576  bj-nuliota  31578  poimirlem30  31884  pw2f1ocnv  35812  areaquad  36021  en3lpVD  37102  iblempty  37662  stoweidlem34  37715  sge00  38006