Theorem noel 3514

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 3343	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3344	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 644	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3511	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2301	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 678	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 2205   _Vcvv 2815   \ cdif 3210   (/)c0 3510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-dif 3215  df-nul 3511

This theorem is referenced by:  nel02  3515  n0i  3516  n0rf  3523  rex0  3528  eq0  3529  abvor0dc  3534  rab0  3539  un0  3544  in0  3545  0ss  3549  disj  3559  ral0  3613  rabsnifsb  3759  rabsnif  3760  int0  3965  iun0  4050  0iun  4051  br0  4160  exmid01  4313  nlim0  4517  nsuceq0g  4541  ordtriexmidlem  4643  ordtriexmidlem2  4644  ordtriexmid  4645  ontriexmidim  4646  ordtri2or2exmidlem  4650  onsucelsucexmidlem  4653  reg2exmidlema  4658  reg3exmidlemwe  4703  nn0eln0  4744  0xp  4832  dm0  4972  dm0rn0  4975  reldm0  4976  cnv0  5168  co02  5278  0fv  5710  acexmidlema  6043  acexmidlemb  6044  acexmidlemab  6046  mpo0  6125  nnsucelsuc  6726  nnsucuniel  6730  nnmordi  6751  nnaordex  6763  0er  6803  elssdc  7164  fissfi  7218  fidcenumlemrk  7226  nnnninfeq  7421  iftrueb01  7535  pw1if  7537  elni2  7631  nlt1pig  7658  0npr  7800  fzm1  10438  frec2uzltd  10769  0tonninf  10806  sum0  12078  fsumsplit  12097  sumsplitdc  12122  fsum2dlemstep  12124  prod0  12275  fprod2dlemstep  12312  ballotfilemcdc  13146  ennnfonelem1  13175  0g0  13606  0ntop  14889  0met  15266  lgsdir2lem3  15920  vtxdg0v  16306  clwwlkn0  16420  clwwlknnn  16424  clwwlk0on0  16443  eupth2lem1  16470  eupth2lem3lem4fi  16485  bdcnul  16652  bj-nnelirr  16740  nnnninfex  16817