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

Theorem noel 3253
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 3091 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  A  e. 
_V )
2 eldifn 3092 . . 3  |-  ( A  e.  ( _V  \  _V )  ->  -.  A  e.  _V )
31, 2pm2.65i 576 . 2  |-  -.  A  e.  ( _V  \  _V )
4 df-nul 3250 . . 3  |-  (/)  =  ( _V  \  _V )
54eleq2i 2118 . 2  |-  ( A  e.  (/)  <->  A  e.  ( _V  \  _V ) )
63, 5mtbir 604 1  |-  -.  A  e.  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3    e. wcel 1407   _Vcvv 2572    \ cdif 2939   (/)c0 3249
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574  df-dif 2945  df-nul 3250
This theorem is referenced by:  n0i  3254  n0rf  3258  rex0  3263  eq0  3264  abvor0dc  3267  rab0  3271  un0  3276  in0  3277  0ss  3280  disj  3293  ral0  3347  int0  3654  iun0  3738  0iun  3739  nlim0  4156  nsuceq0g  4180  ordtriexmidlem  4270  ordtriexmidlem2  4271  ordtriexmid  4272  ordtri2or2exmidlem  4276  onsucelsucexmidlem  4279  reg2exmidlema  4284  reg3exmidlemwe  4328  nn0eln0  4366  0xp  4445  dm0  4574  dm0rn0  4577  reldm0  4578  cnv0  4752  co02  4859  0fv  5233  acexmidlema  5528  acexmidlemb  5529  acexmidlemab  5531  mpt20  5599  nnsucelsuc  6098  nnmordi  6117  nnaordex  6128  0er  6168  elni2  6440  nlt1pig  6467  0npr  6609  fzm1  9034  frec2uzltd  9318  bdcnul  10315  bj-nnelirr  10408
  Copyright terms: Public domain W3C validator