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

Theorem c0ex 7632
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 7630 . 2 0 ∈ ℂ
21elexi 2653 1 0 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1448  Vcvv 2641  cc 7498  0cc0 7500
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-ext 2082  ax-1cn 7588  ax-icn 7590  ax-addcl 7591  ax-mulcl 7593  ax-i2m1 7600
This theorem depends on definitions:  df-bi 116  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-v 2643
This theorem is referenced by:  elnn0  8831  nn0ex  8835  un0mulcl  8863  nn0ssz  8924  nn0ind-raph  9020  ser0f  10129  fser0const  10130  facnn  10314  fac0  10315  prhash2ex  10396  iserge0  10951  sum0  10996  isumz  10997  fisumss  11000  bezoutlemmain  11479  lcmval  11537  isomninnlem  12809
  Copyright terms: Public domain W3C validator