Theorem noel 3741

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 3564	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3565	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 173	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3738	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2480	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 297	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1842   _Vcvv 3058   \ cdif 3410   (/)c0 3737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3060  df-dif 3416  df-nul 3738

This theorem is referenced by:  n0i  3742  n0f  3746  rex0  3752  abvor0  3756  rab0  3759  un0  3763  in0  3764  0ss  3767  sbcel12  3776  sbcel2  3782  disj  3809  r19.2zb  3862  ral0  3877  rabsnifsb  4039  int0  4240  iun0  4326  0iun  4327  br0  4440  pwne0  4563  0xp  4903  csbxp  4904  dm0  5036  dm0rn0  5039  reldm0  5040  elimasni  5183  cnv0  5226  co02  5336  ord0eln0  5463  nlim0  5467  nsuceq0  5489  dffv3  5844  0fv  5881  mpt20  6347  bropopvvv  6863  tz7.44-2  7109  omordi  7251  omeulem1  7267  nnmordi  7316  omabs  7332  omsmolem  7338  0er  7382  omxpenlem  7655  en3lp  8065  cantnfle  8121  cantnfleOLD  8151  r1sdom  8223  r1pwss  8233  alephordi  8486  axdc3lem2  8862  zorn2lem7  8913  nlt1pi  9313  xrinfm0  11580  elixx3g  11594  elfz2  11731  fzm1  11811  om2uzlti  12100  hashf1lem2  12552  sum0  13690  fsumsplit  13709  sumsplit  13732  fsum2dlem  13734  prod0  13900  fprod2dlem  13934  sadc0  14311  sadcp1  14312  saddisjlem  14321  smu01lem  14342  smu01  14343  smu02  14344  prmreclem5  14645  vdwap0  14701  ram0  14747  0catg  15299  oduclatb  16096  0g0  16212  cntzrcl  16687  pmtrfrn  16805  psgnunilem5  16841  gexdvds  16926  gsumzsplit  17266  gsumzsplitOLD  17267  dprdcntz2  17404  00lss  17906  mplcoe1  18445  mplcoe5  18449  mplcoe2OLD  18451  00ply1bas  18599  dsmmbas2  19064  dsmmfi  19065  maducoeval2  19432  madugsum  19435  0ntop  19704  haust1  20144  hauspwdom  20292  kqcldsat  20524  tsmssplit  20944  ustn0  21013  0met  21159  itg11  22388  itg0  22476  bddmulibl  22535  fsumharmonic  23665  ppiublem2  23857  lgsdir2lem3  23979  nbgra0edg  24836  uvtx01vtx  24896  clwwlknprop  25176  2wlkonot3v  25279  2spthonot3v  25280  rusgra0edg  25359  eupath2lem1  25381  helloworld  25577  isarchi  28164  measvuni  28648  ddemeas  28671  sibf0  28768  signstfvneq0  29021  topnfbey  29051  opelco3  29980  wsuclem  30068  bj-projval  31106  bj-df-nul  31136  bj-nuliota  31138  pw2f1ocnv  35321  areaquad  35528  en3lpVD  36655  iblempty  37113  stoweidlem34  37165