![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2ex | Structured version Visualization version GIF version |
Description: 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
2ex | ⊢ 2 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2cn 11172 | . 2 ⊢ 2 ∈ ℂ | |
2 | 1 | elexi 3285 | 1 ⊢ 2 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2071 Vcvv 3272 ℂcc 10015 2c2 11151 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1818 ax-5 1920 ax-6 1986 ax-7 2022 ax-9 2080 ax-10 2100 ax-11 2115 ax-12 2128 ax-13 2323 ax-ext 2672 ax-resscn 10074 ax-1cn 10075 ax-icn 10076 ax-addcl 10077 ax-addrcl 10078 ax-mulcl 10079 ax-mulrcl 10080 ax-i2m1 10085 ax-1ne0 10086 ax-rrecex 10089 ax-cnre 10090 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1567 df-ex 1786 df-nf 1791 df-sb 1979 df-clab 2679 df-cleq 2685 df-clel 2688 df-nfc 2823 df-ne 2865 df-ral 2987 df-rex 2988 df-rab 2991 df-v 3274 df-dif 3651 df-un 3653 df-in 3655 df-ss 3662 df-nul 3992 df-if 4163 df-sn 4254 df-pr 4256 df-op 4260 df-uni 4513 df-br 4729 df-iota 5932 df-fv 5977 df-ov 6736 df-2 11160 |
This theorem is referenced by: fzprval 12483 fztpval 12484 funcnvs3 13748 funcnvs4 13749 wrd3tpop 13781 wrdl3s3 13795 pmtrprfval 17996 m2detleiblem3 20526 m2detleiblem4 20527 iblcnlem1 23642 gausslemma2dlem4 25182 2lgslem4 25219 selberglem1 25322 axlowdimlem4 25913 2wlkdlem4 26937 2pthdlem1 26939 umgrwwlks2on 26967 3wlkdlem4 27203 3wlkdlem5 27204 3pthdlem1 27205 3wlkdlem10 27210 upgr3v3e3cycl 27221 upgr4cycl4dv4e 27226 eulerpathpr 27281 ex-ima 27499 prodfzo03 30879 circlevma 30918 circlemethhgt 30919 hgt750lemg 30930 hgt750lemb 30932 hgt750lema 30933 hgt750leme 30934 tgoldbachgtde 30936 tgoldbachgt 30939 rabren3dioph 37766 refsum2cnlem1 39580 nnsum3primes4 42071 nnsum3primesgbe 42075 nnsum4primesodd 42079 nnsum4primesoddALTV 42080 zlmodzxzldeplem3 42686 zlmodzxzldeplem4 42687 |
Copyright terms: Public domain | W3C validator |