Theorem 1ex 11307

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ℂcc 11202  1c1 11205

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11262

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  1elpr01  11308  1nn  12350  dfnn2  12352  nn1suc  12361  1eltp012  12417  nn0ind-raph  12803  fzprval  13723  fztpval  13724  expval  14210  m1expcl2  14232  1exp  14238  facnn  14423  fac0  14424  prhash2ex  14547  funcnvs2  15070  funcnvs3  15071  funcnvs4  15072  wrdlen2i  15099  wrd2pr2op  15100  wrd3tpop  15105  wwlktovf1  15116  relexp1g  15185  dfid6  15187  sgnval  15247  sgndm  15255  sgncl  15256  harmonic  16034  prodf1f  16067  fprodntriv  16115  prod1  16117  fprodss  16121  fprodn0f  16164  ege2le3  16262  ruclem8  16411  ruclem11  16414  1nprm  16860  pcmpt  17076  smndex2dnrinv  19120  mgmnsgrpex  19136  pmtrprfval  19707  pmtrprfvalrn  19708  psgnprfval  19741  psgnprfval1  19742  abvtrivd  21095  pzriprng1ALT  21808  cnmsgnsubg  21889  psdmplcl  22489  psdmul  22493  psdmvr  22496  m2detleiblem1  22945  m2detleiblem5  22946  m2detleiblem6  22947  m2detleiblem3  22950  m2detleiblem4  22951  m2detleib  22952  imasdsf1olem  24698  pcopt  25349  pcopt2  25350  pcoass  25351  ehl2eudis  25749  voliunlem1  25877  i1f1lem  26016  itg11  26018  iblcnlem1  26114  bddibl  26166  dvexp  26279  dvef  26306  mvth  26318  iaaOLD  26658  aalioulem2  26666  efrlim  27303  amgmlem  27323  amgm  27324  wilthlem2  27402  wilthlem3  27403  basellem7  27420  basellem9  27422  ppiublem2  27536  pclogsum  27548  bposlem5  27621  lgsfval  27635  lgsdir2lem3  27660  lgsdir  27665  lgsdilem2  27666  lgsdi  27667  lgsne0  27668  addsqnreup  27776  ostth1  27966  istrkg2ld  28928  axlowdimlem4  29529  axlowdimlem6  29531  axlowdimlem10  29535  axlowdimlem11  29536  axlowdimlem12  29537  axlowdimlem13  29538  axlowdim1  29543  umgr2v2eedg  30111  umgr2v2e  30112  umgr2v2evd2  30114  2wlklem  30252  usgr2trlncl  30352  2wlkdlem4  30523  2wlkdlem5  30524  2pthdlem1  30525  2wlkdlem10  30530  3wlkdlem4  30769  3wlkdlem5  30770  3pthdlem1  30771  3wlkdlem10  30776  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  konigsberglem4  30862  konigsberglem5  30863  ex-xp  31043  nmopun  32622  pjnmopi  32756  iuninc  33203  fprodex01  33463  psgnid  33705  cnmsgn0g  33754  cyc3evpm  33758  sgnsval  33769  sgnsf  33770  1fldgenq  33931  gsumind  33953  cntnevol  34908  ddeval1  34914  ddeval0  34915  eulerpartgbij  35051  coinfliprv  35162  hgt750lemg  35330  hgt750lemb  35332  tgoldbachgt  35339  subfacp1lem1  36031  subfacp1lem2a  36032  subfacp1lem3  36034  subfacp1lem5  36036  cvmliftlem10  36146  sinccvglem  36524  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem4  38636  poimirlem6  38638  poimirlem7  38639  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem23  38655  poimirlem24  38656  poimirlem25  38657  poimirlem28  38660  poimirlem29  38661  poimirlem31  38663  itg2addnclem  38683  sticksstones11  43300  readvrec  43507  rabren3dioph  43916  2nn0ind  44046  flcidc  44266  dfrcl4  44770  fvilbdRP  44784  iunrelexp0  44796  corclrcl  44801  cotrcltrcl  44819  trclfvdecomr  44822  corcltrcl  44833  cotrclrcl  44836  dvsid  45409  binomcxplemnotnn0  45434  refsum2cnlem1  46148  infleinf  46477  itgsin0pilem1  47054  fourierdlem29  47240  fourierdlem56  47266  fourierdlem62  47272  fourierswlem  47334  fouriersw  47335  numtowerdt  48010  lamberte  48032  cjnpoly  48033  fun2dmnopgexmpl  48448  sbgoldbo  48979  nnsum3primes4  48980  nnsum3primesgbe  48984  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  cycl3grtrilem  49138  stgr1  49153  usgrexmpl1lem  49213  usgrexmpl2lem  49218  usgrexmpl2nb0  49223  usgrexmpl2nb2  49225  usgrexmpl2trifr  49229  opgpgvtx  49247  gpgedgvtx1  49254  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedgiov  49257  gpgedg2iv  49259  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpg3nbgrvtx0  49268  gpg3nbgrvtx0ALT  49269  gpg3nbgrvtx1  49270  gpgcubic  49271  gpg5nbgr3star  49273  gpg3kgrtriex  49281  gpgprismgr4cycllem2  49288  gpgprismgr4cycllem7  49293  pgnioedg1  49300  pgnioedg2  49301  pgnioedg3  49302  pgnioedg4  49303  pgnioedg5  49304  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem2  49309  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5lem1  49312  pgnbgreunbgrlem5lem2  49313  pgnbgreunbgrlem5lem3  49314  pgnbgreunbgrlem6  49316  gpg5edgnedg  49322  zlmodzxzel  49561  zlmodzxz0  49562  zlmodzxzscm  49563  zlmodzxzadd  49564  blenval  49777  nn0sumshdiglemB  49826  fv2arycl  49854  2arymptfv  49856  2arymaptf1  49859  2arymaptfo  49860  fv1prop  49905  rrx2pnecoorneor  49922  ehl2eudisval0  49932  rrx2line  49946  rrx2linest  49948  line2ylem  49957  line2  49958