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

Theorem c0ex 7950
Description: 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
c0ex 0 ∈ V

Proof of Theorem c0ex
StepHypRef Expression
1 0cn 7948 . 2 0 ∈ ℂ
21elexi 2749 1 0 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2148  Vcvv 2737  cc 7808  0cc0 7810
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-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159  ax-1cn 7903  ax-icn 7905  ax-addcl 7906  ax-mulcl 7908  ax-i2m1 7915
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739
This theorem is referenced by:  elnn0  9177  nn0ex  9181  un0mulcl  9209  nn0ssz  9270  nn0ind-raph  9369  ser0f  10514  fser0const  10515  facnn  10706  fac0  10707  prhash2ex  10788  iserge0  11350  sum0  11395  isumz  11396  fisumss  11399  bezoutlemmain  11998  lcmval  12062  dvef  14158  2o01f  14716  iswomni0  14769
  Copyright terms: Public domain W3C validator