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 3575 | . 2 | |
2 | 1 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1335 wcel 2128 csn 3560 |
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 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-v 2714 df-sn 3566 |
This theorem is referenced by: elsn2g 3593 nelsn 3595 disjsn2 3623 sssnm 3718 disjxsn 3964 pwntru 4161 opth1 4197 elsuci 4364 ordtri2orexmid 4483 onsucsssucexmid 4487 sosng 4660 ressn 5127 funcnvsn 5216 funinsn 5220 fvconst 5656 fmptap 5658 fmptapd 5659 fvunsng 5662 mposnif 5916 1stconst 6169 2ndconst 6170 reldmtpos 6201 tpostpos 6212 1domsn 6765 ac6sfi 6844 onunsnss 6862 snon0 6881 snexxph 6895 elfi2 6917 supsnti 6950 djuf1olem 6998 eldju2ndl 7017 eldju2ndr 7018 difinfsnlem 7044 pw1on 7162 elreal2 7751 ax1rid 7798 ltxrlt 7944 un0addcl 9124 un0mulcl 9125 elfzonlteqm1 10113 fxnn0nninf 10341 1exp 10452 hashinfuni 10655 hashennnuni 10657 hashprg 10686 zfz1isolemiso 10714 fisumss 11293 sumsnf 11310 fsumsplitsn 11311 fsum2dlemstep 11335 fisumcom2 11339 fprodssdc 11491 fprodunsn 11505 fprod2dlemstep 11523 fprodcom2fi 11527 fprodsplitsn 11534 divalgmod 11822 phi1 12098 dfphi2 12099 nnnn0modprm0 12134 exmidunben 12197 txdis1cn 12720 bj-nntrans 13568 bj-nnelirr 13570 pwtrufal 13611 sssneq 13616 exmidsbthrlem 13635 |
Copyright terms: Public domain | W3C validator |