Theorem 1ex 8174

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

Syntax hints:   ∈ wcel 2202  Vcvv 2802  ℂcc 8030  1c1 8033

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 8125

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  9162  nn0ind-raph  9597  fzprval  10317  fztpval  10318  m1expcl2  10824  1exp  10831  facnn  10990  fac0  10991  prhash2ex  11074  prodf1f  12109  fprodntrivap  12150  prod1dc  12152  fprodssdc  12156  ege2le3  12237  1nprm  12691  pcmpt  12921  dvexp  15441  dvef  15457  lgsdir2lem3  15765  2wlklem  16233  2o01f  16619  iswomni0  16682