Theorem 3ex 12263

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  3c3 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-2 12244  df-3 12245

This theorem is referenced by:  fztpval  13540  funcnvs4  14877  iblcnlem1  25755  basellem9  27052  lgsdir2lem3  27290  axlowdimlem7  29017  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem13  29023  3wlkdlem4  30232  3pthdlem1  30234  upgr4cycl4dv4e  30255  konigsberglem4  30325  konigsberglem5  30326  ex-pss  30498  ex-fv  30513  ex-1st  30514  ex-2nd  30515  rabren3dioph  43243  lhe4.4ex1a  44756  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2trifr  48513  zlmodzxzldeplem  48974