Theorem 1ex 8049

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

Syntax hints:   ∈ wcel 2175  Vcvv 2771  ℂcc 7905  1c1 7908

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 8000

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  9037  nn0ind-raph  9472  fzprval  10186  fztpval  10187  m1expcl2  10687  1exp  10694  facnn  10853  fac0  10854  prhash2ex  10935  prodf1f  11773  fprodntrivap  11814  prod1dc  11816  fprodssdc  11820  ege2le3  11901  1nprm  12355  pcmpt  12585  dvexp  15101  dvef  15117  lgsdir2lem3  15425  2o01f  15795  iswomni0  15854