Theorem 1ex 8087

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

Syntax hints:   ∈ wcel 2177  Vcvv 2773  ℂcc 7943  1c1 7946

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188  ax-1cn 8038

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-v 2775

This theorem is referenced by:  nn1suc  9075  nn0ind-raph  9510  fzprval  10224  fztpval  10225  m1expcl2  10728  1exp  10735  facnn  10894  fac0  10895  prhash2ex  10976  prodf1f  11929  fprodntrivap  11970  prod1dc  11972  fprodssdc  11976  ege2le3  12057  1nprm  12511  pcmpt  12741  dvexp  15258  dvef  15274  lgsdir2lem3  15582  2o01f  16070  iswomni0  16131