Theorem noel 3495

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 3326	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3327	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 642	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3492	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2296	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 675	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 2200   _Vcvv 2799   \ cdif 3194   (/)c0 3491

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492

This theorem is referenced by:  nel02  3496  n0i  3497  n0rf  3504  rex0  3509  eq0  3510  abvor0dc  3515  rab0  3520  un0  3525  in0  3526  0ss  3530  disj  3540  ral0  3593  int0  3937  iun0  4022  0iun  4023  br0  4132  exmid01  4282  nlim0  4485  nsuceq0g  4509  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2or2exmidlem  4618  onsucelsucexmidlem  4621  reg2exmidlema  4626  reg3exmidlemwe  4671  nn0eln0  4712  0xp  4799  dm0  4937  dm0rn0  4940  reldm0  4941  cnv0  5132  co02  5242  0fv  5665  acexmidlema  5992  acexmidlemb  5993  acexmidlemab  5995  mpo0  6074  nnsucelsuc  6637  nnsucuniel  6641  nnmordi  6662  nnaordex  6674  0er  6714  fidcenumlemrk  7121  nnnninfeq  7295  iftrueb01  7408  pw1if  7410  elni2  7501  nlt1pig  7528  0npr  7670  fzm1  10296  frec2uzltd  10625  0tonninf  10662  sum0  11899  fsumsplit  11918  sumsplitdc  11943  fsum2dlemstep  11945  prod0  12096  fprod2dlemstep  12133  ennnfonelem1  12978  0g0  13409  0ntop  14681  0met  15058  lgsdir2lem3  15709  if0ab  16169  bdcnul  16228  bj-nnelirr  16316  nnnninfex  16388