Theorem 1ex 8173

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 8124	. 2 ⊢ 1 ∈ ℂ
2	1	elexi 2815	1 ⊢ 1 ∈ V

Syntax hints:   ∈ wcel 2202  Vcvv 2802  ℂcc 8029  1c1 8032

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213  ax-1cn 8124

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  nn1suc  9161  nn0ind-raph  9596  fzprval  10316  fztpval  10317  m1expcl2  10822  1exp  10829  facnn  10988  fac0  10989  prhash2ex  11072  prodf1f  12103  fprodntrivap  12144  prod1dc  12146  fprodssdc  12150  ege2le3  12231  1nprm  12685  pcmpt  12915  dvexp  15434  dvef  15450  lgsdir2lem3  15758  2wlklem  16226  2o01f  16593  iswomni0  16655