Theorem noel 3726

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 3544	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3545	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 178	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3723	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2541	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 306	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 1904   _Vcvv 3031   \ cdif 3387   (/)c0 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393  df-nul 3723

This theorem is referenced by:  n0i  3727  n0f  3731  rex0  3737  rab0  3756  un0  3762  in0  3763  0ss  3766  sbcel12  3776  sbcel2  3782  disj  3809  r19.2zb  3850  ral0  3865  rabsnifsb  4031  int0  4240  iun0  4325  0iun  4326  br0  4442  pwne0  4571  0xp  4920  csbxp  4921  dm0  5054  dm0rn0  5057  reldm0  5058  elimasni  5201  cnv0  5245  co02  5356  ord0eln0  5484  nlim0  5488  nsuceq0  5510  dffv3  5875  0fv  5912  mpt20  6380  bropopvvv  6893  bropfvvvv  6895  tz7.44-2  7143  omordi  7285  omeulem1  7301  nnmordi  7350  omabs  7366  omsmolem  7372  0er  7416  omxpenlem  7691  en3lp  8139  cantnfle  8194  r1sdom  8263  r1pwss  8273  alephordi  8523  axdc3lem2  8899  zorn2lem7  8950  nlt1pi  9349  xrinf0  11648  xrinfm0OLD  11652  elixx3g  11673  elfz2  11817  fzm1  11900  om2uzlti  12202  hashf1lem2  12660  sum0  13864  fsumsplit  13883  sumsplit  13906  fsum2dlem  13908  prod0  14074  fprod2dlem  14111  sadc0  14507  sadcp1  14508  saddisjlem  14517  smu01lem  14538  smu01  14539  smu02  14540  lcmf0  14686  prmreclem5  14943  vdwap0  15005  ram0  15059  0catg  15671  oduclatb  16468  0g0  16584  cntzrcl  17059  pmtrfrn  17177  psgnunilem5  17213  gexdvds  17313  gsumzsplit  17638  dprdcntz2  17749  00lss  18243  mplcoe1  18766  mplcoe5  18769  00ply1bas  18910  dsmmbas2  19377  dsmmfi  19378  maducoeval2  19742  madugsum  19745  0ntop  20012  haust1  20445  hauspwdom  20593  kqcldsat  20825  tsmssplit  21244  ustn0  21313  0met  21459  itg11  22728  itg0  22816  bddmulibl  22875  fsumharmonic  24016  ppiublem2  24210  lgsdir2lem3  24332  nbgra0edg  25239  uvtx01vtx  25299  clwwlknprop  25579  2wlkonot3v  25682  2spthonot3v  25683  rusgra0edg  25762  eupath2lem1  25784  helloworld  25981  topnfbey  25985  isarchi  28573  measvuni  29110  ddemeas  29132  sibf0  29240  signstfvneq0  29533  opelco3  30491  wsuclem  30579  bj-projval  31660  bj-df-nul  31691  bj-nuliota  31693  finxp0  31853  poimirlem30  32034  pw2f1ocnv  35963  areaquad  36172  en3lpVD  37304  iblempty  37939  stoweidlem34  38007  sge00  38332  uvtxa01vtx0  39633  vtxdg0v  39698  eupth2lem1  40130