Theorem 1ex 11131

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ℂcc 11027  1c1 11030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  1nn  12176  dfnn2  12178  nn1suc  12187  nn0ind-raph  12620  fzprval  13530  fztpval  13531  expval  14016  m1expcl2  14038  1exp  14044  facnn  14228  fac0  14229  prhash2ex  14352  funcnvs2  14866  funcnvs3  14867  funcnvs4  14868  wrdlen2i  14895  wrd2pr2op  14896  wrd3tpop  14901  wwlktovf1  14910  wrdl3s3  14915  relexp1g  14979  dfid6  14981  sgnval  15041  harmonic  15815  prodf1f  15848  fprodntriv  15898  prod1  15900  fprodss  15904  fprodn0f  15947  ege2le3  16046  ruclem8  16195  ruclem11  16198  1nprm  16639  pcmpt  16854  smndex2dnrinv  18877  mgmnsgrpex  18893  pmtrprfval  19453  pmtrprfvalrn  19454  psgnprfval  19487  psgnprfval1  19488  abvtrivd  20804  pzriprng1ALT  21471  cnmsgnsubg  21552  psdmplcl  22150  psdmul  22154  psdmvr  22157  m2detleiblem1  22607  m2detleiblem5  22608  m2detleiblem6  22609  m2detleiblem3  22612  m2detleiblem4  22613  m2detleib  22614  imasdsf1olem  24356  pcopt  25007  pcopt2  25008  pcoass  25009  ehl1eudis  25405  ehl2eudis  25407  voliunlem1  25535  i1f1lem  25674  i1f1  25675  itg11  25676  iblcnlem1  25773  bddibl  25825  dvexp  25938  dvef  25965  mvth  25977  iaa  26309  aalioulem2  26317  efrlim  26951  amgmlem  26971  amgm  26972  wilthlem2  27050  wilthlem3  27051  basellem7  27068  basellem9  27070  ppiublem2  27184  pclogsum  27196  bposlem5  27269  lgsfval  27283  lgsdir2lem3  27308  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  addsqnreup  27424  ostth1  27614  istrkg2ld  28546  axlowdimlem4  29032  axlowdimlem6  29034  axlowdimlem10  29038  axlowdimlem11  29039  axlowdimlem12  29040  axlowdimlem13  29041  axlowdim1  29046  umgr2v2eedg  29611  umgr2v2e  29612  umgr2v2evd2  29614  2wlklem  29752  usgr2trlncl  29846  2wlkdlem4  30014  2wlkdlem5  30015  2pthdlem1  30016  2wlkdlem10  30021  wwlks2onv  30039  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  3wlkdlem4  30250  3wlkdlem5  30251  3pthdlem1  30252  3wlkdlem10  30257  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  konigsberglem4  30343  konigsberglem5  30344  ex-xp  30524  nmopun  32103  pjnmopi  32237  iuninc  32649  fprodex01  32917  sgncl  32923  s2rnOLD  33023  s3rnOLD  33025  psgnid  33178  cyc3fv2  33219  cnmsgn0g  33227  cyc3evpm  33231  sgnsval  33242  sgnsf  33243  1fldgenq  33406  gsumind  33428  esplyfvaln  33758  constrconj  33929  nn0constr  33945  cntnevol  34412  ddeval1  34418  ddeval0  34419  eulerpartgbij  34556  coinfliprv  34667  prodfzo03  34787  circlevma  34826  circlemethhgt  34827  hgt750lemg  34838  hgt750lemb  34840  hgt750lema  34841  hgt750leme  34842  tgoldbachgtde  34844  tgoldbachgt  34847  subfacp1lem1  35407  subfacp1lem2a  35408  subfacp1lem3  35410  subfacp1lem5  35412  cvmliftlem10  35522  sinccvglem  35900  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem28  38015  poimirlem29  38016  poimirlem31  38018  itg2addnclem  38038  sticksstones11  42641  readvrec  42839  rabren3dioph  43260  2nn0ind  43390  flcidc  43615  dfrcl4  44120  fvilbdRP  44134  fvrcllb1d  44139  iunrelexp0  44146  corclrcl  44151  relexp1idm  44158  cotrcltrcl  44169  trclfvdecomr  44172  corcltrcl  44183  cotrclrcl  44186  dvsid  44775  binomcxplemnotnn0  44800  refsum2cnlem1  45485  infleinf  45816  itgsin0pilem1  46393  fourierdlem29  46579  fourierdlem56  46605  fourierdlem62  46611  fourierswlem  46673  fouriersw  46674  nthrucw  47331  lamberte  47351  cjnpoly  47352  fun2dmnopgexmpl  47747  sbgoldbo  48278  nnsum3primes4  48279  nnsum3primesgbe  48283  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  cycl3grtrilem  48437  stgr1  48452  usgrexmpl1lem  48512  usgrexmpl1tri  48516  usgrexmpl2lem  48517  usgrexmpl2nb0  48522  usgrexmpl2nb1  48523  usgrexmpl2nb2  48524  usgrexmpl2trifr  48528  gpgiedgdmellem  48537  gpgvtx1  48545  opgpgvtx  48546  gpgedgvtx1  48553  gpgvtxedg0  48554  gpgvtxedg1  48555  gpgedgiov  48556  gpgedg2iv  48558  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg3nbgrvtx0  48567  gpg3nbgrvtx0ALT  48568  gpg3nbgrvtx1  48569  gpgcubic  48570  gpg5nbgr3star  48572  gpg3kgrtriex  48580  gpgprismgr4cycllem2  48587  gpgprismgr4cycllem3  48588  gpgprismgr4cycllem7  48592  gpgprismgr4cycllem9  48594  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  pgnbgreunbgrlem2lem1  48605  pgnbgreunbgrlem2lem2  48606  pgnbgreunbgrlem2lem3  48607  pgnbgreunbgrlem2  48608  pgnbgreunbgrlem3  48609  pgnbgreunbgrlem4  48610  pgnbgreunbgrlem5lem1  48611  pgnbgreunbgrlem5lem2  48612  pgnbgreunbgrlem5lem3  48613  pgnbgreunbgrlem6  48615  gpg5edgnedg  48621  grlimedgnedg  48622  zlmodzxzel  48846  zlmodzxz0  48847  zlmodzxzscm  48848  zlmodzxzadd  48849  blenval  49062  nn0sumshdiglemB  49111  fv2arycl  49139  2arympt  49140  2arymptfv  49141  2arymaptf1  49144  2arymaptfo  49145  fv1prop  49190  rrx2pxel  49202  prelrrx2  49204  prelrrx2b  49205  rrx2pnecoorneor  49206  rrx2xpref1o  49209  rrx2plordisom  49214  ehl2eudisval0  49216  rrx2line  49231  rrx2linest  49233  rrx2linesl  49234  2sphere0  49241  line2ylem  49242  line2  49243  line2xlem  49244  line2x  49245  line2y  49246  itscnhlinecirc02p  49276  inlinecirc02plem  49277