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  5677  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  mpo0  6091  nnsucelsuc  6659  nnsucuniel  6663  nnmordi  6684  nnaordex  6696  0er  6736  elssdc  7094  fidcenumlemrk  7153  nnnninfeq  7327  iftrueb01  7441  pw1if  7443  elni2  7534  nlt1pig  7561  0npr  7703  fzm1  10335  frec2uzltd  10665  0tonninf  10702  sum0  11950  fsumsplit  11969  sumsplitdc  11994  fsum2dlemstep  11996  prod0  12147  fprod2dlemstep  12184  ennnfonelem1  13029  0g0  13460  0ntop  14733  0met  15110  lgsdir2lem3  15761  vtxdg0v  16147  clwwlkn0  16261  clwwlknnn  16265  clwwlk0on0  16284  eupth2lem1  16311  if0ab  16404  bdcnul  16463  bj-nnelirr  16551  nnnninfex  16627