Theorem 1ex 8038

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

Syntax hints:   ∈ wcel 2167  Vcvv 2763  ℂcc 7894  1c1 7897

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178  ax-1cn 7989

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  nn1suc  9026  nn0ind-raph  9460  fzprval  10174  fztpval  10175  m1expcl2  10670  1exp  10677  facnn  10836  fac0  10837  prhash2ex  10918  prodf1f  11725  fprodntrivap  11766  prod1dc  11768  fprodssdc  11772  ege2le3  11853  1nprm  12307  pcmpt  12537  dvexp  15031  dvef  15047  lgsdir2lem3  15355  2o01f  15725  iswomni0  15782