ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  noel Unicode version

Theorem noel 3288
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
StepHypRef Expression
1 eldifi 3120 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3121 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 603 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3285 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2154 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 631 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1438   _Vcvv 2619    \ cdif 2994   (/)c0 3284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-v 2621  df-dif 2999  df-nul 3285
This theorem is referenced by:  n0i  3289  n0rf  3293  rex0  3298  eq0  3299  abvor0dc  3304  rab0  3309  un0  3314  in0  3315  0ss  3318  disj  3328  ral0  3379  int0  3697  iun0  3781  0iun  3782  exmid01  4023  nlim0  4212  nsuceq0g  4236  ordtriexmidlem  4326  ordtriexmidlem2  4327  ordtriexmid  4328  ordtri2or2exmidlem  4332  onsucelsucexmidlem  4335  reg2exmidlema  4340  reg3exmidlemwe  4384  nn0eln0  4423  0xp  4506  dm0  4638  dm0rn0  4641  reldm0  4642  cnv0  4822  co02  4931  0fv  5323  acexmidlema  5625  acexmidlemb  5626  acexmidlemab  5628  mpt20  5700  nnsucelsuc  6234  nnsucuniel  6238  nnmordi  6255  nnaordex  6266  0er  6306  fidcenumlemrk  6642  elni2  6852  nlt1pig  6879  0npr  7021  fzm1  9481  frec2uzltd  9775  0tonninf  9810  sum0  10744  fsumsplit  10764  sumsplitdc  10789  fsum2dlemstep  10791  bdcnul  11413  bj-nnelirr  11505  nninfalllemn  11555
  Copyright terms: Public domain W3C validator