![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > velsn | Unicode version |
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
velsn |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 2740 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | elsn 3607 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-sn 3597 |
This theorem is referenced by: dfpr2 3610 mosn 3627 ralsnsg 3628 ralsns 3629 rexsns 3630 disjsn 3653 snprc 3656 euabsn2 3660 prmg 3712 snssOLD 3717 snssb 3724 difprsnss 3729 eqsnm 3753 snsssn 3759 snsspw 3762 dfnfc2 3825 uni0b 3832 uni0c 3833 sndisj 3996 unidif0 4164 exmid01 4195 rext 4211 exss 4223 frirrg 4346 ordsucim 4495 ordtriexmidlem 4514 ordtri2or2exmidlem 4521 onsucelsucexmidlem 4524 elirr 4536 sucprcreg 4544 fconstmpt 4669 opeliunxp 4677 restidsing 4958 dmsnopg 5095 dfmpt3 5333 nfunsn 5544 fsn 5683 fnasrn 5689 fnasrng 5691 fconstfvm 5729 eusvobj2 5854 opabex3d 6115 opabex3 6116 dcdifsnid 6498 ecexr 6533 ixp0x 6719 xpsnen 6814 fidifsnen 6863 difinfsn 7092 exmidonfinlem 7185 iccid 9899 fzsn 10039 fzpr 10050 fzdifsuc 10054 fsum2dlemstep 11413 prodsnf 11571 fprod1p 11578 fprodunsn 11583 fprod2dlemstep 11601 ef0lem 11639 1nprm 12084 mgmidsssn0 12682 mnd1id 12725 0subm 12748 restsn 13313 |
Copyright terms: Public domain | W3C validator |