Theorem 3ex 12300

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 12299	. 2 ⊢ 3 ∈ ℂ
2	1	elexi 3476	1 ⊢ 3 ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  ℂcc 11071  3c3 12273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-addcl 11133

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-2 12280  df-3 12281

This theorem is referenced by:  fztpval  13591  funcnvs4  14928  iblcnlem1  25847  basellem9  27150  lgsdir2lem3  27388  axlowdimlem7  29146  axlowdimlem8  29147  axlowdimlem9  29148  axlowdimlem13  29152  3wlkdlem4  30361  3pthdlem1  30363  upgr4cycl4dv4e  30384  konigsberglem4  30454  konigsberglem5  30455  ex-pss  30627  ex-fv  30642  ex-1st  30643  ex-2nd  30644  rabren3dioph  43389  lhe4.4ex1a  44902  nnsum4primesodd  48415  nnsum4primesoddALTV  48416  usgrexmpl1lem  48640  usgrexmpl2lem  48645  usgrexmpl2nb0  48650  usgrexmpl2nb1  48651  usgrexmpl2nb2  48652  usgrexmpl2nb3  48653  usgrexmpl2nb4  48654  usgrexmpl2trifr  48656  zlmodzxzldeplem  49117