Theorem 3ex 11041

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

Assertion

Ref	Expression
3ex	⊢ 3 ∈ V

Proof of Theorem 3ex

Step	Hyp	Ref	Expression
1		3cn 11040	. 2 ⊢ 3 ∈ ℂ
2	1	elexi 3204	1 ⊢ 3 ∈ V

Syntax hints:   ∈ wcel 1992  Vcvv 3191  ℂcc 9879  3c3 11016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-i2m1 9949  ax-1ne0 9950  ax-rrecex 9953  ax-cnre 9954

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-2 11024  df-3 11025

This theorem is referenced by:  fztpval  12341  funcnvs4  13591  iblcnlem1  23455  basellem9  24710  lgsdir2lem3  24947  axlowdimlem7  25723  axlowdimlem13  25729  3wlkdlem4  26882  3pthdlem1  26884  upgr4cycl4dv4e  26905  konigsberglem4  26977  konigsberglem5  26978  ex-pss  27133  ex-fv  27148  rabren3dioph  36845  lhe4.4ex1a  37996  nnsum4primesodd  40961  nnsum4primesoddALTV  40962  zlmodzxzldeplem  41549