Theorem noel 3498

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 3329	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3330	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 644	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3495	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2298	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 677	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 2202   _Vcvv 2802   \ cdif 3197   (/)c0 3494

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-dif 3202  df-nul 3495

This theorem is referenced by:  nel02  3499  n0i  3500  n0rf  3507  rex0  3512  eq0  3513  abvor0dc  3518  rab0  3523  un0  3528  in0  3529  0ss  3533  disj  3543  ral0  3596  rabsnifsb  3737  rabsnif  3738  int0  3942  iun0  4027  0iun  4028  br0  4137  exmid01  4288  nlim0  4491  nsuceq0g  4515  ordtriexmidlem  4617  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2or2exmidlem  4624  onsucelsucexmidlem  4627  reg2exmidlema  4632  reg3exmidlemwe  4677  nn0eln0  4718  0xp  4806  dm0  4945  dm0rn0  4948  reldm0  4949  cnv0  5140  co02  5250  0fv  5678  acexmidlema  6012  acexmidlemb  6013  acexmidlemab  6015  mpo0  6094  nnsucelsuc  6662  nnsucuniel  6666  nnmordi  6687  nnaordex  6699  0er  6739  elssdc  7097  fidcenumlemrk  7156  nnnninfeq  7330  iftrueb01  7444  pw1if  7446  elni2  7537  nlt1pig  7564  0npr  7706  fzm1  10338  frec2uzltd  10669  0tonninf  10706  sum0  11970  fsumsplit  11989  sumsplitdc  12014  fsum2dlemstep  12016  prod0  12167  fprod2dlemstep  12204  ennnfonelem1  13049  0g0  13480  0ntop  14758  0met  15135  lgsdir2lem3  15786  vtxdg0v  16172  clwwlkn0  16286  clwwlknnn  16290  clwwlk0on0  16309  eupth2lem1  16336  eupth2lem3lem4fi  16351  if0ab  16460  bdcnul  16519  bj-nnelirr  16607  nnnninfex  16683