Theorem noel 3797

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 3622	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3623	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 173	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3794	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2535	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 299	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1819   _Vcvv 3109   \ cdif 3468   (/)c0 3793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3474  df-nul 3794

This theorem is referenced by:  n0i  3798  n0f  3802  rex0  3808  abvor0  3812  rab0  3815  un0  3819  in0  3820  0ss  3823  sbcel12  3832  sbcel2  3839  disj  3870  r19.2zb  3922  ral0  3937  rabsnifsb  4100  int0  4302  iun0  4388  0iun  4389  br0  4502  pwne0  4626  ord0eln0  4941  nlim0  4945  nsuceq0  4967  0xp  5089  csbxp  5090  dm0  5226  dm0rn0  5229  reldm0  5230  elimasni  5374  cnv0  5416  co02  5527  dffv3  5868  0fv  5905  mpt20  6366  bropopvvv  6879  tz7.44-2  7091  omordi  7233  omeulem1  7249  nnmordi  7298  omabs  7314  omsmolem  7320  0er  7364  omxpenlem  7637  en3lp  8050  cantnfle  8107  cantnfleOLD  8137  r1sdom  8209  r1pwss  8219  alephordi  8472  axdc3lem2  8848  zorn2lem7  8899  nlt1pi  9301  xrinfm0  11553  elixx3g  11567  elfz2  11704  fzm1  11784  om2uzlti  12064  hashf1lem2  12509  sum0  13555  fsumsplit  13574  sumsplit  13595  fsum2dlem  13597  prod0  13762  fprod2dlem  13796  sadc0  14116  sadcp1  14117  saddisjlem  14126  smu01lem  14147  smu01  14148  smu02  14149  prmreclem5  14450  vdwap0  14506  ram0  14552  0catg  15104  oduclatb  15901  0g0  16017  cntzrcl  16492  pmtrfrn  16610  psgnunilem5  16646  gexdvds  16731  gsumzsplit  17071  gsumzsplitOLD  17072  dprdcntz2  17213  00lss  17715  mplcoe1  18254  mplcoe5  18258  mplcoe2OLD  18260  00ply1bas  18408  dsmmbas2  18895  dsmmfi  18896  maducoeval2  19269  madugsum  19272  0ntop  19541  haust1  19980  hauspwdom  20128  kqcldsat  20360  tsmssplit  20780  ustn0  20849  0met  20995  itg11  22224  itg0  22312  bddmulibl  22371  fsumharmonic  23467  ppiublem2  23604  lgsdir2lem3  23726  nbgra0edg  24559  uvtx01vtx  24619  clwwlknprop  24899  2wlkonot3v  25002  2spthonot3v  25003  rusgra0edg  25082  eupath2lem1  25104  helloworld  25300  isarchi  27886  measvuni  28358  ddemeas  28381  sibf0  28473  signstfvneq0  28726  opelco3  29425  wsuclem  29598  pw2f1ocnv  31183  areaquad  31388  iblempty  31967  stoweidlem34  32019  en3lpVD  33788  bj-projval  34697  bj-df-nul  34727  bj-nuliota  34729