Theorem 1ex 8321

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

This proof depends on syntax axioms:   ∈ wcel 2209  Vcvv 2821  ℂcc 8177  1c1 8180

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220  ax-1cn 8272

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  nn1suc  9323  nn0ind-raph  9763  fzprval  10489  fztpval  10490  m1expcl2  10998  1exp  11005  facnn  11165  fac0  11166  prhash2ex  11250  prodf1f  12310  fprodntrivap  12351  prod1dc  12353  fprodssdc  12357  ege2le3  12438  1nprm  12892  pcmpt  13122  ballotfilem2  13228  dvexp  15812  dvef  15828  lgsdir2lem3  16149  2wlklem  16617  konigsberglem4  16732  konigsberglem5  16733  2o01f  17024  iswomni0  17101