Theorem 1ex 11199

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ℂcc 11094  1c1 11097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-1cn 11154

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  1elpr01  11200  1nn  12240  dfnn2  12242  nn1suc  12251  1eltp012  12307  nn0ind-raph  12692  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  wrdl3s3  14995  relexp1g  15059  dfid6  15061  sgnval  15121  sgndm  15129  sgncl  15130  harmonic  15909  prodf1f  15942  fprodntriv  15992  prod1  15994  fprodss  15998  fprodn0f  16041  ege2le3  16140  ruclem8  16289  ruclem11  16292  1nprm  16733  pcmpt  16948  smndex2dnrinv  18973  mgmnsgrpex  18989  pmtrprfval  19553  pmtrprfvalrn  19554  psgnprfval  19587  psgnprfval1  19588  abvtrivd  20909  pzriprng1ALT  21611  cnmsgnsubg  21692  psdmplcl  22290  psdmul  22294  psdmvr  22297  m2detleiblem1  22746  m2detleiblem5  22747  m2detleiblem6  22748  m2detleiblem3  22751  m2detleiblem4  22752  m2detleib  22753  imasdsf1olem  24495  pcopt  25146  pcopt2  25147  pcoass  25148  ehl1eudis  25544  ehl2eudis  25546  voliunlem1  25674  i1f1lem  25813  i1f1  25814  itg11  25815  iblcnlem1  25912  bddibl  25964  dvexp  26077  dvef  26104  mvth  26116  iaa  26451  aalioulem2  26459  efrlim  27096  amgmlem  27116  amgm  27117  wilthlem2  27195  wilthlem3  27196  basellem7  27213  basellem9  27215  ppiublem2  27329  pclogsum  27341  bposlem5  27414  lgsfval  27428  lgsdir2lem3  27453  lgsdir  27458  lgsdilem2  27459  lgsdi  27460  lgsne0  27461  addsqnreup  27569  ostth1  27759  istrkg2ld  28691  axlowdimlem4  29232  axlowdimlem6  29234  axlowdimlem10  29238  axlowdimlem11  29239  axlowdimlem12  29240  axlowdimlem13  29241  axlowdim1  29246  umgr2v2eedg  29811  umgr2v2e  29812  umgr2v2evd2  29814  2wlklem  29952  usgr2trlncl  30046  2wlkdlem4  30214  2wlkdlem5  30215  2pthdlem1  30216  2wlkdlem10  30221  wwlks2onv  30239  elwwlks2ons3im  30240  usgrwwlks2on  30244  umgrwwlks2on  30245  3wlkdlem4  30450  3wlkdlem5  30451  3pthdlem1  30452  3wlkdlem10  30457  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  konigsberglem4  30543  konigsberglem5  30544  ex-xp  30724  nmopun  32303  pjnmopi  32437  iuninc  32842  fprodex01  33106  s2rnOLD  33201  s3rnOLD  33203  psgnid  33354  cyc3fv2  33395  cnmsgn0g  33403  cyc3evpm  33407  sgnsval  33418  sgnsf  33419  1fldgenq  33582  gsumind  33604  esplyfvaln  33905  nn0constr  34092  cntnevol  34559  ddeval1  34565  ddeval0  34566  eulerpartgbij  34703  coinfliprv  34814  prodfzo03  34931  circlevma  34970  circlemethhgt  34971  hgt750lemg  34982  hgt750lemb  34984  hgt750lema  34985  tgoldbachgtde  34988  tgoldbachgt  34991  subfacp1lem1  35566  subfacp1lem2a  35567  subfacp1lem3  35569  subfacp1lem5  35571  cvmliftlem10  35681  sinccvglem  36059  poimirlem1  38155  poimirlem2  38156  poimirlem3  38157  poimirlem4  38158  poimirlem6  38160  poimirlem7  38161  poimirlem10  38164  poimirlem11  38165  poimirlem12  38166  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem28  38182  poimirlem29  38183  poimirlem31  38185  itg2addnclem  38205  sticksstones11  42808  readvrec  43006  rabren3dioph  43427  2nn0ind  43557  flcidc  43782  dfrcl4  44287  fvilbdRP  44301  fvrcllb1d  44306  iunrelexp0  44313  corclrcl  44318  relexp1idm  44325  cotrcltrcl  44336  trclfvdecomr  44339  corcltrcl  44350  cotrclrcl  44353  dvsid  44926  binomcxplemnotnn0  44951  refsum2cnlem1  45642  infleinf  45972  itgsin0pilem1  46549  fourierdlem29  46735  fourierdlem56  46761  fourierdlem62  46767  fourierswlem  46829  fouriersw  46830  nthrucw  47487  lamberte  47507  cjnpoly  47508  fun2dmnopgexmpl  47903  sbgoldbo  48434  nnsum3primes4  48435  nnsum3primesgbe  48439  nnsum4primesodd  48443  nnsum4primesoddALTV  48444  cycl3grtrilem  48593  stgr1  48608  usgrexmpl1lem  48668  usgrexmpl1tri  48672  usgrexmpl2lem  48673  usgrexmpl2nb0  48678  usgrexmpl2nb1  48679  usgrexmpl2nb2  48680  usgrexmpl2trifr  48684  gpgiedgdmellem  48693  gpgvtx1  48701  opgpgvtx  48702  gpgedgvtx1  48709  gpgvtxedg0  48710  gpgvtxedg1  48711  gpgedgiov  48712  gpgedg2iv  48714  gpg5nbgrvtx03starlem1  48715  gpg5nbgrvtx03starlem3  48717  gpg5nbgrvtx13starlem1  48718  gpg5nbgrvtx13starlem2  48719  gpg5nbgrvtx13starlem3  48720  gpg3nbgrvtx0  48723  gpg3nbgrvtx0ALT  48724  gpg3nbgrvtx1  48725  gpgcubic  48726  gpg5nbgr3star  48728  gpg3kgrtriex  48736  gpgprismgr4cycllem2  48743  gpgprismgr4cycllem3  48744  gpgprismgr4cycllem7  48748  gpgprismgr4cycllem9  48750  pgnioedg1  48755  pgnioedg2  48756  pgnioedg3  48757  pgnioedg4  48758  pgnioedg5  48759  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgnbgreunbgrlem2lem3  48763  pgnbgreunbgrlem2  48764  pgnbgreunbgrlem3  48765  pgnbgreunbgrlem4  48766  pgnbgreunbgrlem5lem1  48767  pgnbgreunbgrlem5lem2  48768  pgnbgreunbgrlem5lem3  48769  pgnbgreunbgrlem6  48771  gpg5edgnedg  48777  zlmodzxzel  49013  zlmodzxz0  49014  zlmodzxzscm  49015  zlmodzxzadd  49016  blenval  49229  nn0sumshdiglemB  49278  fv2arycl  49306  2arympt  49307  2arymptfv  49308  2arymaptf1  49311  2arymaptfo  49312  fv1prop  49357  rrx2pxel  49369  prelrrx2  49371  prelrrx2b  49372  rrx2pnecoorneor  49373  rrx2xpref1o  49376  rrx2plordisom  49381  ehl2eudisval0  49383  rrx2line  49398  rrx2linest  49400  rrx2linesl  49401  2sphere0  49408  line2ylem  49409  line2  49410  line2xlem  49411  line2x  49412  line2y  49413  itscnhlinecirc02p  49443  inlinecirc02plem  49444