Theorem noel 3748

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

Syntax hints:   -. wn 3   e. wcel 1758   _Vcvv 3076   \ cdif 3432   (/)c0 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3078  df-dif 3438  df-nul 3745

This theorem is referenced by:  n0i  3749  n0f  3752  rex0  3758  abvor0  3762  rab0  3765  un0  3769  in0  3770  0ss  3773  sbcel12  3782  sbcel2  3790  disj  3826  r19.2zb  3877  ral0  3891  rabsnifsb  4050  int0  4249  iun0  4333  0iun  4334  br0  4445  sbcbr123  4450  pwne0  4569  ord0eln0  4880  nlim0  4884  nsuceq0  4906  0xp  5024  csbxp  5025  dm0  5160  dm0rn0  5163  reldm0  5164  elimasni  5303  cnv0  5347  co02  5458  dffv3  5794  0fv  5831  mpt20  6264  bropopvvv  6762  tz7.44-2  6972  0we1  7055  omordi  7114  omeulem1  7130  nnmordi  7179  omabs  7195  omsmolem  7201  0er  7245  omxpenlem  7521  en3lp  7932  cantnfle  7989  cantnfleOLD  8019  r1sdom  8091  r1pwss  8101  alephordi  8354  axdc3lem2  8730  zorn2lem7  8781  brdom3  8805  canthwe  8928  nlt1pi  9185  xrinfm0  11409  elixx3g  11423  elfz2  11560  om2uzlti  11889  hashf1lem2  12326  swrd0  12444  sum0  13315  fsumsplit  13333  sumsplit  13352  fsum2dlem  13354  sadc0  13767  sadcp1  13768  saddisjlem  13777  smu01lem  13798  smu01  13799  smu02  13800  prmreclem5  14098  vdwap0  14154  ram0  14200  0catg  14743  oduclatb  15432  0g0  15552  cntzrcl  15963  pmtrfrn  16082  psgnunilem5  16118  gexdvds  16203  gsumzsplit  16538  gsumzsplitOLD  16539  dprdcntz2  16657  00lss  17145  mplcoe1  17667  mplcoe5  17671  mplcoe2OLD  17673  mplrcl  17694  00ply1bas  17817  dsmmbas2  18286  dsmmfi  18287  maducoeval2  18577  madugsum  18580  0ntop  18649  haust1  19087  hauspwdom  19236  kqcldsat  19437  tsmssplit  19857  ustn0  19926  0met  20072  itg11  21301  itg0  21389  bddmulibl  21448  fsumharmonic  22537  ppiublem2  22674  lgsdir2lem3  22796  nbgra0edg  23494  uvtx01vtx  23551  eupath2lem1  23749  helloworld  23809  isarchi  26343  measvuni  26772  ddemeas  26795  sibf0  26863  signstfvneq0  27116  prod0  27599  fprod2dlem  27634  opelco3  27732  wsuclem  27905  pw2f1ocnv  29533  areaquad  29739  stoweidlem34  29976  2wlkonot3v  30541  2spthonot3v  30542  clwwlknprop  30582  rusgra0edg  30720  en3lpVD  31898  bj-projval  32806  bj-df-nul  32836  bj-nuliota  32838