![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1ex | GIF version |
Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
1ex | ⊢ 1 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 7632 | . 2 ⊢ 1 ∈ ℂ | |
2 | 1 | elexi 2667 | 1 ⊢ 1 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 1461 Vcvv 2655 ℂcc 7539 1c1 7542 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-ext 2095 ax-1cn 7632 |
This theorem depends on definitions: df-bi 116 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-v 2657 |
This theorem is referenced by: nn1suc 8643 nn0ind-raph 9066 fzprval 9749 fztpval 9750 m1expcl2 10202 1exp 10209 facnn 10360 fac0 10361 prhash2ex 10442 ege2le3 11222 1nprm 11635 isomninnlem 12906 |
Copyright terms: Public domain | W3C validator |