Theorem 1ex 8066

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

Syntax hints:   ∈ wcel 2175  Vcvv 2771  ℂcc 7922  1c1 7925

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-ext 2186  ax-1cn 8017

This theorem depends on definitions:  df-bi 117  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-v 2773

This theorem is referenced by:  nn1suc  9054  nn0ind-raph  9489  fzprval  10203  fztpval  10204  m1expcl2  10704  1exp  10711  facnn  10870  fac0  10871  prhash2ex  10952  prodf1f  11796  fprodntrivap  11837  prod1dc  11839  fprodssdc  11843  ege2le3  11924  1nprm  12378  pcmpt  12608  dvexp  15125  dvef  15141  lgsdir2lem3  15449  2o01f  15864  iswomni0  15923