Theorem noel 3426

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 3257	. . 3 |- ( A e. ( _V \ _V ) -> A e. _V )
2		eldifn 3258	. . 3 |- ( A e. ( _V \ _V ) -> -. A e. _V )
3	1, 2	pm2.65i 639	. 2 |- -. A e. ( _V \ _V )
4		df-nul 3423	. . 3 |- (/) = ( _V \ _V )
5	4	eleq2i 2244	. 2 |- ( A e. (/) <-> A e. ( _V \ _V ) )
6	3, 5	mtbir 671	1 |- -. A e. (/)

Syntax hints:   -. wn 3   e. wcel 2148   _Vcvv 2737   \ cdif 3126   (/)c0 3422

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-dif 3131  df-nul 3423

This theorem is referenced by:  nel02  3427  n0i  3428  n0rf  3435  rex0  3440  eq0  3441  abvor0dc  3446  rab0  3451  un0  3456  in0  3457  0ss  3461  disj  3471  ral0  3524  int0  3858  iun0  3943  0iun  3944  br0  4051  exmid01  4198  nlim0  4394  nsuceq0g  4418  ordtriexmidlem  4518  ordtriexmidlem2  4519  ordtriexmid  4520  ontriexmidim  4521  ordtri2or2exmidlem  4525  onsucelsucexmidlem  4528  reg2exmidlema  4533  reg3exmidlemwe  4578  nn0eln0  4619  0xp  4706  dm0  4841  dm0rn0  4844  reldm0  4845  cnv0  5032  co02  5142  0fv  5550  acexmidlema  5865  acexmidlemb  5866  acexmidlemab  5868  mpo0  5944  nnsucelsuc  6491  nnsucuniel  6495  nnmordi  6516  nnaordex  6528  0er  6568  fidcenumlemrk  6952  nnnninfeq  7125  elni2  7312  nlt1pig  7339  0npr  7481  fzm1  10097  frec2uzltd  10400  0tonninf  10436  sum0  11391  fsumsplit  11410  sumsplitdc  11435  fsum2dlemstep  11437  prod0  11588  fprod2dlemstep  11625  ennnfonelem1  12402  0g0  12749  0ntop  13398  0met  13777  lgsdir2lem3  14324  if0ab  14439  bdcnul  14499  bj-nnelirr  14587