Theorem 1ex 11140

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  1c1 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  1nn  12185  dfnn2  12187  nn1suc  12196  nn0ind-raph  12629  fzprval  13539  fztpval  13540  expval  14025  m1expcl2  14047  1exp  14053  facnn  14237  fac0  14238  prhash2ex  14361  funcnvs2  14875  funcnvs3  14876  funcnvs4  14877  wrdlen2i  14904  wrd2pr2op  14905  wrd3tpop  14910  wwlktovf1  14919  wrdl3s3  14924  relexp1g  14988  dfid6  14990  sgnval  15050  harmonic  15824  prodf1f  15857  fprodntriv  15907  prod1  15909  fprodss  15913  fprodn0f  15956  ege2le3  16055  ruclem8  16204  ruclem11  16207  1nprm  16648  pcmpt  16863  smndex2dnrinv  18886  mgmnsgrpex  18902  pmtrprfval  19462  pmtrprfvalrn  19463  psgnprfval  19496  psgnprfval1  19497  abvtrivd  20809  pzriprng1ALT  21476  cnmsgnsubg  21557  psdmplcl  22128  psdmul  22132  psdmvr  22135  m2detleiblem1  22589  m2detleiblem5  22590  m2detleiblem6  22591  m2detleiblem3  22594  m2detleiblem4  22595  m2detleib  22596  imasdsf1olem  24338  pcopt  24989  pcopt2  24990  pcoass  24991  ehl1eudis  25387  ehl2eudis  25389  voliunlem1  25517  i1f1lem  25656  i1f1  25657  itg11  25658  iblcnlem1  25755  bddibl  25807  dvexp  25920  dvef  25947  mvth  25959  iaa  26291  aalioulem2  26299  efrlim  26933  amgmlem  26953  amgm  26954  wilthlem2  27032  wilthlem3  27033  basellem7  27050  basellem9  27052  ppiublem2  27166  pclogsum  27178  bposlem5  27251  lgsfval  27265  lgsdir2lem3  27290  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  addsqnreup  27406  ostth1  27596  istrkg2ld  28528  axlowdimlem4  29014  axlowdimlem6  29016  axlowdimlem10  29020  axlowdimlem11  29021  axlowdimlem12  29022  axlowdimlem13  29023  axlowdim1  29028  umgr2v2eedg  29593  umgr2v2e  29594  umgr2v2evd2  29596  2wlklem  29734  usgr2trlncl  29828  2wlkdlem4  29996  2wlkdlem5  29997  2pthdlem1  29998  2wlkdlem10  30003  wwlks2onv  30021  elwwlks2ons3im  30022  usgrwwlks2on  30026  umgrwwlks2on  30027  3wlkdlem4  30232  3wlkdlem5  30233  3pthdlem1  30234  3wlkdlem10  30239  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  konigsberglem4  30325  konigsberglem5  30326  ex-xp  30506  nmopun  32085  pjnmopi  32219  iuninc  32630  fprodex01  32898  sgncl  32904  s2rnOLD  33004  s3rnOLD  33006  psgnid  33158  cyc3fv2  33199  cnmsgn0g  33207  cyc3evpm  33211  sgnsval  33222  sgnsf  33223  1fldgenq  33383  gsumind  33405  esplyfvaln  33718  constrconj  33889  nn0constr  33905  cntnevol  34372  ddeval1  34378  ddeval0  34379  eulerpartgbij  34516  coinfliprv  34627  prodfzo03  34747  circlevma  34786  circlemethhgt  34787  hgt750lemg  34798  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgt  34807  subfacp1lem1  35361  subfacp1lem2a  35362  subfacp1lem3  35364  subfacp1lem5  35366  cvmliftlem10  35476  sinccvglem  35854  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  itg2addnclem  37992  sticksstones11  42595  readvrec  42794  rabren3dioph  43243  2nn0ind  43373  flcidc  43598  dfrcl4  44103  fvilbdRP  44117  fvrcllb1d  44122  iunrelexp0  44129  corclrcl  44134  relexp1idm  44141  cotrcltrcl  44152  trclfvdecomr  44155  corcltrcl  44166  cotrclrcl  44169  dvsid  44758  binomcxplemnotnn0  44783  refsum2cnlem1  45468  infleinf  45801  itgsin0pilem1  46378  fourierdlem29  46564  fourierdlem56  46590  fourierdlem62  46596  fourierswlem  46658  fouriersw  46659  nthrucw  47316  lamberte  47336  cjnpoly  47337  fun2dmnopgexmpl  47732  sbgoldbo  48263  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  cycl3grtrilem  48422  stgr1  48437  usgrexmpl1lem  48497  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2trifr  48513  gpgiedgdmellem  48522  gpgvtx1  48530  opgpgvtx  48531  gpgedgvtx1  48538  gpgvtxedg0  48539  gpgvtxedg1  48540  gpgedgiov  48541  gpgedg2iv  48543  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  gpgcubic  48555  gpg5nbgr3star  48557  gpg3kgrtriex  48565  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem9  48579  pgnioedg1  48584  pgnioedg2  48585  pgnioedg3  48586  pgnioedg4  48587  pgnioedg5  48588  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem2  48593  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgrlem6  48600  gpg5edgnedg  48606  grlimedgnedg  48607  zlmodzxzel  48831  zlmodzxz0  48832  zlmodzxzscm  48833  zlmodzxzadd  48834  blenval  49047  nn0sumshdiglemB  49096  fv2arycl  49124  2arympt  49125  2arymptfv  49126  2arymaptf1  49129  2arymaptfo  49130  fv1prop  49175  rrx2pxel  49187  prelrrx2  49189  prelrrx2b  49190  rrx2pnecoorneor  49191  rrx2xpref1o  49194  rrx2plordisom  49199  ehl2eudisval0  49201  rrx2line  49216  rrx2linest  49218  rrx2linesl  49219  2sphere0  49226  line2ylem  49227  line2  49228  line2xlem  49229  line2x  49230  line2y  49231  itscnhlinecirc02p  49261  inlinecirc02plem  49262