Theorem 1ex 8268

Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1ex	⊢ 1 ∈ V

Proof of Theorem 1ex

Step	Hyp	Ref	Expression
1		ax-1cn 8219	. 2 ⊢ 1 ∈ ℂ
2	1	elexi 2825	1 ⊢ 1 ∈ V

Syntax hints:   ∈ wcel 2203  Vcvv 2812  ℂcc 8124  1c1 8127

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-ext 2214  ax-1cn 8219

This theorem depends on definitions:  df-bi 117  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-v 2814

This theorem is referenced by:  nn1suc  9255  nn0ind-raph  9694  fzprval  10415  fztpval  10416  m1expcl2  10922  1exp  10929  facnn  11088  fac0  11089  prhash2ex  11172  prodf1f  12225  fprodntrivap  12266  prod1dc  12268  fprodssdc  12272  ege2le3  12353  1nprm  12807  pcmpt  13037  dvexp  15568  dvef  15584  lgsdir2lem3  15895  2wlklem  16363  konigsberglem4  16478  konigsberglem5  16479  2o01f  16760  iswomni0  16828