Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > elsni | Unicode version |
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.) |
Ref | Expression |
---|---|
elsni |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elsng 3598 | . 2 | |
2 | 1 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1348 wcel 2141 csn 3583 |
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-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 df-sn 3589 |
This theorem is referenced by: elsn2g 3616 nelsn 3618 disjsn2 3646 sssnm 3741 disjxsn 3987 pwntru 4185 opth1 4221 elsuci 4388 ordtri2orexmid 4507 onsucsssucexmid 4511 sosng 4684 ressn 5151 funcnvsn 5243 funinsn 5247 fvconst 5684 fmptap 5686 fmptapd 5687 fvunsng 5690 mposnif 5947 1stconst 6200 2ndconst 6201 reldmtpos 6232 tpostpos 6243 1domsn 6797 ac6sfi 6876 onunsnss 6894 snon0 6913 snexxph 6927 elfi2 6949 supsnti 6982 djuf1olem 7030 eldju2ndl 7049 eldju2ndr 7050 difinfsnlem 7076 pw1on 7203 elreal2 7792 ax1rid 7839 ltxrlt 7985 un0addcl 9168 un0mulcl 9169 elfzonlteqm1 10166 fxnn0nninf 10394 1exp 10505 hashinfuni 10711 hashennnuni 10713 hashprg 10743 zfz1isolemiso 10774 fisumss 11355 sumsnf 11372 fsumsplitsn 11373 fsum2dlemstep 11397 fisumcom2 11401 fprodssdc 11553 fprodunsn 11567 fprod2dlemstep 11585 fprodcom2fi 11589 fprodsplitsn 11596 divalgmod 11886 phi1 12173 dfphi2 12174 nnnn0modprm0 12209 exmidunben 12381 txdis1cn 13072 bj-nntrans 13986 bj-nnelirr 13988 pwtrufal 14030 sssneq 14035 exmidsbthrlem 14054 |
Copyright terms: Public domain | W3C validator |