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 11719 | . 2 ⊢ 3 ∈ ℂ | |
2 | 1 | elexi 3513 | 1 ⊢ 3 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 Vcvv 3494 ℂcc 10535 3c3 11694 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2793 ax-1cn 10595 ax-addcl 10597 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-v 3496 df-2 11701 df-3 11702 |
This theorem is referenced by: fztpval 12970 funcnvs4 14277 iblcnlem1 24388 basellem9 25666 lgsdir2lem3 25903 axlowdimlem7 26734 axlowdimlem8 26735 axlowdimlem9 26736 axlowdimlem13 26740 3wlkdlem4 27941 3pthdlem1 27943 upgr4cycl4dv4e 27964 konigsberglem4 28034 konigsberglem5 28035 ex-pss 28207 ex-fv 28222 ex-1st 28223 ex-2nd 28224 rabren3dioph 39432 lhe4.4ex1a 40681 nnsum4primesodd 43981 nnsum4primesoddALTV 43982 zlmodzxzldeplem 44573 |
Copyright terms: Public domain | W3C validator |