Theorem 1ex 11198

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ℂcc 11093  1c1 11096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  1elpr01  11199  1nn  12239  dfnn2  12241  nn1suc  12250  1eltp012  12306  nn0ind-raph  12691  fzprval  13609  fztpval  13610  expval  14095  m1expcl2  14117  1exp  14123  facnn  14307  fac0  14308  prhash2ex  14431  funcnvs2  14946  funcnvs3  14947  funcnvs4  14948  wrdlen2i  14975  wrd2pr2op  14976  wrd3tpop  14981  wwlktovf1  14990  relexp1g  15059  dfid6  15061  sgnval  15121  sgndm  15129  sgncl  15130  harmonic  15909  prodf1f  15942  fprodntriv  15992  prod1  15994  fprodss  15998  fprodn0f  16041  ege2le3  16139  ruclem8  16288  ruclem11  16291  1nprm  16732  pcmpt  16947  smndex2dnrinv  18972  mgmnsgrpex  18988  pmtrprfval  19552  pmtrprfvalrn  19553  psgnprfval  19586  psgnprfval1  19587  abvtrivd  20935  pzriprng1ALT  21646  cnmsgnsubg  21727  psdmplcl  22325  psdmul  22329  psdmvr  22332  m2detleiblem1  22781  m2detleiblem5  22782  m2detleiblem6  22783  m2detleiblem3  22786  m2detleiblem4  22787  m2detleib  22788  imasdsf1olem  24530  pcopt  25181  pcopt2  25182  pcoass  25183  ehl1eudis  25579  ehl2eudis  25581  voliunlem1  25709  i1f1lem  25848  itg11  25850  iblcnlem1  25947  bddibl  25999  dvexp  26112  dvef  26139  mvth  26151  iaa  26488  aalioulem2  26496  efrlim  27134  amgmlem  27154  amgm  27155  wilthlem2  27233  wilthlem3  27234  basellem7  27251  basellem9  27253  ppiublem2  27367  pclogsum  27379  bposlem5  27452  lgsfval  27466  lgsdir2lem3  27491  lgsdir  27496  lgsdilem2  27497  lgsdi  27498  lgsne0  27499  addsqnreup  27607  ostth1  27797  istrkg2ld  28729  axlowdimlem4  29295  axlowdimlem6  29297  axlowdimlem10  29301  axlowdimlem11  29302  axlowdimlem12  29303  axlowdimlem13  29304  axlowdim1  29309  umgr2v2eedg  29874  umgr2v2e  29875  umgr2v2evd2  29877  2wlklem  30015  usgr2trlncl  30109  2wlkdlem4  30277  2wlkdlem5  30278  2pthdlem1  30279  2wlkdlem10  30284  3wlkdlem4  30513  3wlkdlem5  30514  3pthdlem1  30515  3wlkdlem10  30520  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  konigsberglem4  30606  konigsberglem5  30607  ex-xp  30787  nmopun  32366  pjnmopi  32500  iuninc  32905  fprodex01  33169  s2rnOLD  33264  s3rnOLD  33266  psgnid  33417  cnmsgn0g  33466  cyc3evpm  33470  sgnsval  33481  sgnsf  33482  1fldgenq  33643  gsumind  33665  cntnevol  34618  ddeval1  34624  ddeval0  34625  eulerpartgbij  34762  coinfliprv  34873  hgt750lemg  35041  hgt750lemb  35043  tgoldbachgt  35050  subfacp1lem1  35671  subfacp1lem2a  35672  subfacp1lem3  35674  subfacp1lem5  35676  cvmliftlem10  35786  sinccvglem  36164  poimirlem1  38272  poimirlem2  38273  poimirlem3  38274  poimirlem4  38275  poimirlem6  38277  poimirlem7  38278  poimirlem10  38281  poimirlem11  38282  poimirlem12  38283  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem28  38299  poimirlem29  38300  poimirlem31  38302  itg2addnclem  38322  sticksstones11  42923  readvrec  43123  rabren3dioph  43542  2nn0ind  43672  flcidc  43897  dfrcl4  44402  fvilbdRP  44416  iunrelexp0  44428  corclrcl  44433  cotrcltrcl  44451  trclfvdecomr  44454  corcltrcl  44465  cotrclrcl  44468  dvsid  45041  binomcxplemnotnn0  45066  refsum2cnlem1  45757  infleinf  46087  itgsin0pilem1  46664  fourierdlem29  46850  fourierdlem56  46876  fourierdlem62  46882  fourierswlem  46944  fouriersw  46945  nthrucw  47607  lamberte  47625  cjnpoly  47626  fun2dmnopgexmpl  48021  sbgoldbo  48552  nnsum3primes4  48553  nnsum3primesgbe  48557  nnsum4primesodd  48561  nnsum4primesoddALTV  48562  cycl3grtrilem  48711  stgr1  48726  usgrexmpl1lem  48786  usgrexmpl2lem  48791  usgrexmpl2nb0  48796  usgrexmpl2nb2  48798  usgrexmpl2trifr  48802  opgpgvtx  48820  gpgedgvtx1  48827  gpgvtxedg0  48828  gpgvtxedg1  48829  gpgedgiov  48830  gpgedg2iv  48832  gpg5nbgrvtx03starlem1  48833  gpg5nbgrvtx03starlem3  48835  gpg5nbgrvtx13starlem1  48836  gpg5nbgrvtx13starlem2  48837  gpg5nbgrvtx13starlem3  48838  gpg3nbgrvtx0  48841  gpg3nbgrvtx0ALT  48842  gpg3nbgrvtx1  48843  gpgcubic  48844  gpg5nbgr3star  48846  gpg3kgrtriex  48854  gpgprismgr4cycllem2  48861  gpgprismgr4cycllem7  48866  pgnioedg1  48873  pgnioedg2  48874  pgnioedg3  48875  pgnioedg4  48876  pgnioedg5  48877  pgnbgreunbgrlem2lem1  48879  pgnbgreunbgrlem2lem2  48880  pgnbgreunbgrlem2lem3  48881  pgnbgreunbgrlem2  48882  pgnbgreunbgrlem3  48883  pgnbgreunbgrlem4  48884  pgnbgreunbgrlem5lem1  48885  pgnbgreunbgrlem5lem2  48886  pgnbgreunbgrlem5lem3  48887  pgnbgreunbgrlem6  48889  gpg5edgnedg  48895  zlmodzxzel  49135  zlmodzxz0  49136  zlmodzxzscm  49137  zlmodzxzadd  49138  blenval  49351  nn0sumshdiglemB  49400  fv2arycl  49428  2arymptfv  49430  2arymaptf1  49433  2arymaptfo  49434  fv1prop  49479  rrx2pxel  49491  prelrrx2  49493  prelrrx2b  49494  rrx2pnecoorneor  49495  rrx2xpref1o  49498  rrx2plordisom  49503  ehl2eudisval0  49505  rrx2line  49520  rrx2linest  49522  rrx2linesl  49523  2sphere0  49530  line2ylem  49531  line2  49532  line2xlem  49533  line2x  49534  line2y  49535  itscnhlinecirc02p  49565  inlinecirc02plem  49566