![]() |
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 2755 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | elsn 3623 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-sn 3613 |
This theorem is referenced by: dfpr2 3626 mosn 3643 ralsnsg 3644 ralsns 3645 rexsns 3646 disjsn 3669 snprc 3672 euabsn2 3676 prmg 3728 snssOLD 3733 snssb 3740 difprsnss 3745 eqsnm 3770 snsssn 3776 snsspw 3779 dfnfc2 3842 uni0b 3849 uni0c 3850 sndisj 4014 unidif0 4185 exmid01 4216 rext 4233 exss 4245 frirrg 4368 ordsucim 4517 ordtriexmidlem 4536 ordtri2or2exmidlem 4543 onsucelsucexmidlem 4546 elirr 4558 sucprcreg 4566 fconstmpt 4691 opeliunxp 4699 restidsing 4981 dmsnopg 5118 dfmpt3 5357 nfunsn 5569 fsn 5709 fnasrn 5715 fnasrng 5717 fconstfvm 5755 eusvobj2 5882 opabex3d 6146 opabex3 6147 dcdifsnid 6529 ecexr 6564 ixp0x 6752 xpsnen 6847 fidifsnen 6898 difinfsn 7129 exmidonfinlem 7222 iccid 9955 fzsn 10096 fzpr 10107 fzdifsuc 10111 fsum2dlemstep 11474 prodsnf 11632 fprod1p 11639 fprodunsn 11644 fprod2dlemstep 11662 ef0lem 11700 1nprm 12146 mgmidsssn0 12860 mnd1id 12908 0subm 12936 trivsubgsnd 13140 kerf1ghm 13213 mulgrhm2 13908 restsn 14140 |
Copyright terms: Public domain | W3C validator |