![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ex | Structured version Visualization version GIF version |
Description: The number 3 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
3ex | ⊢ 3 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3cn 12345 | . 2 ⊢ 3 ∈ ℂ | |
2 | 1 | elexi 3501 | 1 ⊢ 3 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3478 ℂcc 11151 3c3 12320 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-1cn 11211 ax-addcl 11213 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-v 3480 df-2 12327 df-3 12328 |
This theorem is referenced by: fztpval 13623 funcnvs4 14951 iblcnlem1 25838 basellem9 27147 lgsdir2lem3 27386 axlowdimlem7 28978 axlowdimlem8 28979 axlowdimlem9 28980 axlowdimlem13 28984 3wlkdlem4 30191 3pthdlem1 30193 upgr4cycl4dv4e 30214 konigsberglem4 30284 konigsberglem5 30285 ex-pss 30457 ex-fv 30472 ex-1st 30473 ex-2nd 30474 rabren3dioph 42803 lhe4.4ex1a 44325 nnsum4primesodd 47721 nnsum4primesoddALTV 47722 usgrexmpl1lem 47916 usgrexmpl2lem 47921 usgrexmpl2nb0 47926 usgrexmpl2nb1 47927 usgrexmpl2nb2 47928 usgrexmpl2nb3 47929 usgrexmpl2nb4 47930 usgrexmpl2trifr 47932 zlmodzxzldeplem 48344 |
Copyright terms: Public domain | W3C validator |