Theorem 1ex 7902

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

Syntax hints:   ∈ wcel 2141  Vcvv 2730  ℂcc 7759  1c1 7762

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 7854

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:  nn1suc  8884  nn0ind-raph  9316  fzprval  10025  fztpval  10026  m1expcl2  10485  1exp  10492  facnn  10648  fac0  10649  prhash2ex  10731  prodf1f  11493  fprodntrivap  11534  prod1dc  11536  fprodssdc  11540  ege2le3  11621  1nprm  12055  pcmpt  12282  dvexp  13428  dvef  13441  lgsdir2lem3  13684  2o01f  13989  iswomni0  14043