Theorem noel 3592

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 3429	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3430	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 167	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3589	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2468	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 291	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1721   _Vcvv 2916   \ cdif 3277   (/)c0 3588

This theorem is referenced by:  n0i  3593  n0f  3596  rex0  3601  abvor0  3605  rab0  3608  un0  3612  in0  3613  0ss  3616  disj  3628  r19.2zb  3678  ral0  3692  int0  4024  iun0  4107  0iun  4108  ord0eln0  4595  nlim0  4599  nsuceq0  4621  xp0r  4915  dm0  5042  dm0rn0  5045  reldm0  5046  elimasni  5190  cnv0  5234  co02  5342  dffv3  5683  fv01  5722  bropopvvv  6385  mpt20  6386  tz7.44-2  6624  0we1  6709  omordi  6768  omeulem1  6784  nnmordi  6833  omabs  6849  omsmolem  6855  0er  6899  omxpenlem  7168  cantnfle  7582  en3lp  7628  r1sdom  7656  r1pwss  7666  alephordi  7911  axdc3lem2  8287  zorn2lem7  8338  brdom3  8362  canthwe  8482  nlt1pi  8739  xrinfm0  10871  elixx3g  10885  elfz2  11006  om2uzlti  11245  hashf1lem2  11660  sum0  12470  fsumsplit  12488  sumsplit  12507  fsum2dlem  12509  sadc0  12921  sadcp1  12922  saddisjlem  12931  smu01lem  12952  smu01  12953  smu02  12954  prmreclem5  13243  vdwap0  13299  ram0  13345  0catg  13867  oduclatb  14526  0g0  14664  cntzrcl  15081  gexdvds  15173  gsumzsplit  15484  dprdcntz2  15551  00lss  15973  mplcoe1  16483  mplcoe2  16485  mplrcl  16505  strov2rcl  16586  00ply1bas  16589  0ntop  16933  haust1  17370  hauspwdom  17517  kqcldsat  17718  tsmssplit  18134  ustn0  18203  0met  18349  itg11  19536  itg0  19624  bddmulibl  19683  fsumharmonic  20803  ppiublem2  20940  lgsdir2lem3  21062  nbgra0edg  21397  uvtx01vtx  21454  eupath2lem1  21652  helloworld  21712  isarchi  24205  measvuni  24521  sibf0  24602  prod0  25222  fprod2dlem  25257  pw2f1ocnv  26998  dsmmbas2  27071  dsmmfi  27072  pmtrfrn  27268  psgnunilem5  27285  stoweidlem34  27650  2wlkonot3v  28072  2spthonot3v  28073  en3lpVD  28666

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-dif 3283  df-nul 3589