Theorem 1ex 11254

Description: One is a set. (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 11210	. 2 ⊢ 1 ∈ ℂ
2	1	elexi 3500	1 ⊢ 1 ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ℂcc 11150  1c1 11153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  1nn  12274  dfnn2  12276  nn1suc  12285  nn0ind-raph  12715  fzprval  13621  fztpval  13622  expval  14100  m1expcl2  14122  1exp  14128  facnn  14310  fac0  14311  prhash2ex  14434  funcnvs2  14948  funcnvs3  14949  funcnvs4  14950  wrdlen2i  14977  wrd2pr2op  14978  wrd3tpop  14983  wwlktovf1  14992  wrdl3s3  14997  relexp1g  15061  dfid6  15063  sgnval  15123  harmonic  15891  prodf1f  15924  fprodntriv  15974  prod1  15976  fprodss  15980  fprodn0f  16023  ege2le3  16122  ruclem8  16269  ruclem11  16272  1nprm  16712  pcmpt  16925  smndex2dnrinv  18940  mgmnsgrpex  18956  pmtrprfval  19519  pmtrprfvalrn  19520  psgnprfval  19553  psgnprfval1  19554  abvtrivd  20849  pzriprng1ALT  21524  cnmsgnsubg  21612  psdmplcl  22183  psdmul  22187  m2detleiblem1  22645  m2detleiblem5  22646  m2detleiblem6  22647  m2detleiblem3  22650  m2detleiblem4  22651  m2detleib  22652  imasdsf1olem  24398  pcopt  25068  pcopt2  25069  pcoass  25070  ehl1eudis  25467  ehl2eudis  25469  voliunlem1  25598  i1f1lem  25737  i1f1  25738  itg11  25739  iblcnlem1  25837  bddibl  25889  dvexp  26005  dvef  26032  mvth  26045  iaa  26381  aalioulem2  26389  efrlim  27026  efrlimOLD  27027  amgmlem  27047  amgm  27048  wilthlem2  27126  wilthlem3  27127  basellem7  27144  basellem9  27146  ppiublem2  27261  pclogsum  27273  bposlem5  27346  lgsfval  27360  lgsdir2lem3  27385  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  addsqnreup  27501  ostth1  27691  istrkg2ld  28482  axlowdimlem4  28974  axlowdimlem6  28976  axlowdimlem10  28980  axlowdimlem11  28981  axlowdimlem12  28982  axlowdimlem13  28983  axlowdim1  28988  umgr2v2eedg  29556  umgr2v2e  29557  umgr2v2evd2  29559  2wlklem  29699  usgr2trlncl  29792  2wlkdlem4  29957  2wlkdlem5  29958  2pthdlem1  29959  2wlkdlem10  29964  wwlks2onv  29982  elwwlks2ons3im  29983  umgrwwlks2on  29986  3wlkdlem4  30190  3wlkdlem5  30191  3pthdlem1  30192  3wlkdlem10  30197  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  konigsberglem4  30283  konigsberglem5  30284  ex-xp  30464  nmopun  32042  pjnmopi  32176  iuninc  32580  fprodex01  32831  s2rnOLD  32912  s3rnOLD  32914  psgnid  33099  cyc3fv2  33140  cnmsgn0g  33148  cyc3evpm  33152  sgnsval  33163  sgnsf  33164  1fldgenq  33303  constrconj  33749  cntnevol  34208  ddeval1  34214  ddeval0  34215  eulerpartgbij  34353  coinfliprv  34463  sgncl  34519  prodfzo03  34596  circlevma  34635  circlemethhgt  34636  hgt750lemg  34647  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgt  34656  subfacp1lem1  35163  subfacp1lem2a  35164  subfacp1lem3  35166  subfacp1lem5  35168  cvmliftlem10  35278  sinccvglem  35656  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  itg2addnclem  37657  sticksstones11  42137  readvrec  42370  rabren3dioph  42802  2nn0ind  42933  flcidc  43158  dfrcl4  43665  fvilbdRP  43679  fvrcllb1d  43684  iunrelexp0  43691  corclrcl  43696  relexp1idm  43703  cotrcltrcl  43714  trclfvdecomr  43717  corcltrcl  43728  cotrclrcl  43731  dvsid  44326  binomcxplemnotnn0  44351  refsum2cnlem1  44974  infleinf  45321  itgsin0pilem1  45905  fourierdlem29  46091  fourierdlem56  46117  fourierdlem62  46123  fourierswlem  46185  fouriersw  46186  fun2dmnopgexmpl  47233  sbgoldbo  47711  nnsum3primes4  47712  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  stgr1  47863  usgrexmpl1lem  47915  usgrexmpl1tri  47919  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2trifr  47931  gpgedgel  47942  gpgvtx1  47944  gpgedgvtx1  47954  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  gpgcubic  47969  gpg5nbgr3star  47971  zlmodzxzel  48199  zlmodzxz0  48200  zlmodzxzscm  48201  zlmodzxzadd  48202  blenval  48420  nn0sumshdiglemB  48469  fv2arycl  48497  2arympt  48498  2arymptfv  48499  2arymaptf1  48502  2arymaptfo  48503  fv1prop  48548  rrx2pxel  48560  prelrrx2  48562  prelrrx2b  48563  rrx2pnecoorneor  48564  rrx2xpref1o  48567  rrx2plordisom  48572  ehl2eudisval0  48574  rrx2line  48589  rrx2linest  48591  rrx2linesl  48592  2sphere0  48599  line2ylem  48600  line2  48601  line2xlem  48602  line2x  48603  line2y  48604  itscnhlinecirc02p  48634  inlinecirc02plem  48635