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

Theorem c0ex 7907
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 7905 . 2 0 ∈ ℂ
21elexi 2742 1 0 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2141  Vcvv 2730  cc 7765  0cc0 7767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152  ax-1cn 7860  ax-icn 7862  ax-addcl 7863  ax-mulcl 7865  ax-i2m1 7872
This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-v 2732
This theorem is referenced by:  elnn0  9130  nn0ex  9134  un0mulcl  9162  nn0ssz  9223  nn0ind-raph  9322  ser0f  10464  fser0const  10465  facnn  10654  fac0  10655  prhash2ex  10737  iserge0  11299  sum0  11344  isumz  11345  fisumss  11348  bezoutlemmain  11946  lcmval  12010  dvef  13447  2o01f  13994  iswomni0  14048
  Copyright terms: Public domain W3C validator