Theorem noel 3472

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 3303	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3304	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 640	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3469	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2274	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 673	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 2178   _Vcvv 2776   \ cdif 3171   (/)c0 3468

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 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-v 2778  df-dif 3176  df-nul 3469

This theorem is referenced by:  nel02  3473  n0i  3474  n0rf  3481  rex0  3486  eq0  3487  abvor0dc  3492  rab0  3497  un0  3502  in0  3503  0ss  3507  disj  3517  ral0  3570  int0  3913  iun0  3998  0iun  3999  br0  4108  exmid01  4258  nlim0  4459  nsuceq0g  4483  ordtriexmidlem  4585  ordtriexmidlem2  4586  ordtriexmid  4587  ontriexmidim  4588  ordtri2or2exmidlem  4592  onsucelsucexmidlem  4595  reg2exmidlema  4600  reg3exmidlemwe  4645  nn0eln0  4686  0xp  4773  dm0  4911  dm0rn0  4914  reldm0  4915  cnv0  5105  co02  5215  0fv  5635  acexmidlema  5958  acexmidlemb  5959  acexmidlemab  5961  mpo0  6038  nnsucelsuc  6600  nnsucuniel  6604  nnmordi  6625  nnaordex  6637  0er  6677  fidcenumlemrk  7082  nnnninfeq  7256  iftrueb01  7369  pw1if  7371  elni2  7462  nlt1pig  7489  0npr  7631  fzm1  10257  frec2uzltd  10585  0tonninf  10622  sum0  11814  fsumsplit  11833  sumsplitdc  11858  fsum2dlemstep  11860  prod0  12011  fprod2dlemstep  12048  ennnfonelem1  12893  0g0  13323  0ntop  14594  0met  14971  lgsdir2lem3  15622  if0ab  15941  bdcnul  16000  bj-nnelirr  16088  nnnninfex  16161