Theorem 3ex 12338

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

Assertion

Ref	Expression
3ex	⊢ 3 ∈ V

Proof of Theorem 3ex

Step	Hyp	Ref	Expression
1		3cn 12337	. 2 ⊢ 3 ∈ ℂ
2	1	elexi 3479	1 ⊢ 3 ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ℂcc 11113  3c3 12311

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11173  ax-addcl 11175

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-2 12318  df-3 12319

This theorem is used by:  fztpval  13631  funcnvs4  14976  iblcnlem1  25998  basellem9  27304  lgsdir2lem3  27542  axlowdimlem7  29353  axlowdimlem8  29354  axlowdimlem9  29355  axlowdimlem13  29359  3wlkdlem4  30584  3pthdlem1  30586  upgr4cycl4dv4e  30607  konigsberglem4  30677  konigsberglem5  30678  ex-pss  30850  ex-fv  30865  ex-1st  30866  ex-2nd  30867  rabren3dioph  43600  lhe4.4ex1a  45097  nnsum4primesodd  48619  nnsum4primesoddALTV  48620  usgrexmpl1lem  48844  usgrexmpl2lem  48849  usgrexmpl2nb0  48854  usgrexmpl2nb1  48855  usgrexmpl2nb2  48856  usgrexmpl2nb3  48857  usgrexmpl2nb4  48858  usgrexmpl2trifr  48860  zlmodzxzldeplem  49335