Theorem 2ex 12048

Description: The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2ex	⊢ 2 ∈ V

Proof of Theorem 2ex

Step	Hyp	Ref	Expression
1		2cn 12046	. 2 ⊢ 2 ∈ ℂ
2	1	elexi 3450	1 ⊢ 2 ∈ V

Syntax hints:   ∈ wcel 2110  Vcvv 3431  ℂcc 10868  2c2 12026

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-1cn 10928  ax-addcl 10930

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-2 12034

This theorem is referenced by:  fzprval  13314  fztpval  13315  funcnvs3  14623  funcnvs4  14624  wrd3tpop  14657  wrdl3s3  14673  pmtrprfval  19091  m2detleiblem3  21774  m2detleiblem4  21775  ehl2eudis  24582  iblcnlem1  24948  gausslemma2dlem4  26513  2lgslem4  26550  addsqnreup  26587  selberglem1  26689  axlowdimlem4  27309  2wlkdlem4  28287  2pthdlem1  28289  umgrwwlks2on  28316  3wlkdlem4  28520  3wlkdlem5  28521  3pthdlem1  28522  3wlkdlem10  28527  upgr3v3e3cycl  28538  upgr4cycl4dv4e  28543  eulerpathpr  28598  ex-ima  28800  s3rn  31214  cyc3evpm  31411  prodfzo03  32577  circlevma  32616  circlemethhgt  32617  hgt750lemg  32628  hgt750lemb  32630  hgt750lema  32631  hgt750leme  32632  tgoldbachgtde  32634  tgoldbachgt  32637  rabren3dioph  40632  refsum2cnlem1  42548  nnsum3primes4  45207  nnsum3primesgbe  45211  nnsum4primesodd  45215  nnsum4primesoddALTV  45216  zlmodzxzldeplem3  45810  zlmodzxzldeplem4  45811  fv2prop  46013  rrx2pyel  46025  prelrrx2  46026  prelrrx2b  46027  rrx2pnecoorneor  46028  rrx2xpref1o  46031  rrx2plordisom  46036  ehl2eudisval0  46038  rrx2line  46053  rrx2linest  46055  rrx2linesl  46056  2sphere0  46063  line2ylem  46064  line2  46065  line2x  46067  line2y  46068  itscnhlinecirc02p  46098  inlinecirc02plem  46099