Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 1ex | Unicode version |
Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
1ex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 7867 | . 2 | |
2 | 1 | elexi 2742 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2141 cvv 2730 cc 7772 c1 7775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1440 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-ext 2152 ax-1cn 7867 |
This theorem depends on definitions: df-bi 116 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-v 2732 |
This theorem is referenced by: nn1suc 8897 nn0ind-raph 9329 fzprval 10038 fztpval 10039 m1expcl2 10498 1exp 10505 facnn 10661 fac0 10662 prhash2ex 10744 prodf1f 11506 fprodntrivap 11547 prod1dc 11549 fprodssdc 11553 ege2le3 11634 1nprm 12068 pcmpt 12295 dvexp 13469 dvef 13482 lgsdir2lem3 13725 2o01f 14029 iswomni0 14083 |
Copyright terms: Public domain | W3C validator |