Theorem 3ex 12465

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11237  3c3 12438

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-addcl 11299

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-2 12445  df-3 12446

This theorem is used by:  fztpval  13760  funcnvs4  15109  iblcnlem1  26163  basellem9  27473  lgsdir2lem3  27711  axlowdimlem7  29583  axlowdimlem8  29584  axlowdimlem9  29585  axlowdimlem13  29589  3wlkdlem4  30820  3pthdlem1  30822  upgr4cycl4dv4e  30843  konigsberglem4  30913  konigsberglem5  30914  ex-pss  31086  ex-fv  31101  ex-1st  31102  ex-2nd  31103  rabren3dioph  44088  lhe4.4ex1a  45574  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  usgrexmpl1lem  49392  usgrexmpl2lem  49397  usgrexmpl2nb0  49402  usgrexmpl2nb1  49403  usgrexmpl2nb2  49404  usgrexmpl2nb3  49405  usgrexmpl2nb4  49406  usgrexmpl2trifr  49408  zlmodzxzldeplem  49941