Theorem 3ex 11877

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

Syntax hints:   ∈ wcel 2112  Vcvv 3398  ℂcc 10692  3c3 11851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-addcl 10754

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-2 11858  df-3 11859

This theorem is referenced by:  fztpval  13139  funcnvs4  14445  iblcnlem1  24639  basellem9  25925  lgsdir2lem3  26162  axlowdimlem7  26993  axlowdimlem8  26994  axlowdimlem9  26995  axlowdimlem13  26999  3wlkdlem4  28199  3pthdlem1  28201  upgr4cycl4dv4e  28222  konigsberglem4  28292  konigsberglem5  28293  ex-pss  28465  ex-fv  28480  ex-1st  28481  ex-2nd  28482  rabren3dioph  40281  lhe4.4ex1a  41561  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  zlmodzxzldeplem  45455