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

Theorem noel 3262
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 3095 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3096 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 601 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3259 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2146 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 629 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1434   _Vcvv 2602    \ cdif 2971   (/)c0 3258
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 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-dif 2976  df-nul 3259
This theorem is referenced by:  n0i  3263  n0rf  3267  rex0  3272  eq0  3273  abvor0dc  3276  rab0  3280  un0  3285  in0  3286  0ss  3289  disj  3299  ral0  3350  int0  3658  iun0  3742  0iun  3743  nlim0  4157  nsuceq0g  4181  ordtriexmidlem  4271  ordtriexmidlem2  4272  ordtriexmid  4273  ordtri2or2exmidlem  4277  onsucelsucexmidlem  4280  reg2exmidlema  4285  reg3exmidlemwe  4329  nn0eln0  4367  0xp  4446  dm0  4577  dm0rn0  4580  reldm0  4581  cnv0  4757  co02  4864  0fv  5240  acexmidlema  5534  acexmidlemb  5535  acexmidlemab  5537  mpt20  5605  nnsucelsuc  6135  nnsucuniel  6139  nnmordi  6155  nnaordex  6166  0er  6206  elni2  6566  nlt1pig  6593  0npr  6735  fzm1  9193  frec2uzltd  9485  bdcnul  10814  bj-nnelirr  10906
  Copyright terms: Public domain W3C validator