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 3537 | . 2 | |
2 | 1 | ibi 175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wcel 1480 csn 3522 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-sn 3528 |
This theorem is referenced by: elsn2g 3553 disjsn2 3581 sssnm 3676 disjxsn 3922 pwntru 4117 opth1 4153 elsuci 4320 ordtri2orexmid 4433 onsucsssucexmid 4437 sosng 4607 ressn 5074 funcnvsn 5163 funinsn 5167 fvconst 5601 fmptap 5603 fmptapd 5604 fvunsng 5607 mposnif 5858 1stconst 6111 2ndconst 6112 reldmtpos 6143 tpostpos 6154 1domsn 6706 ac6sfi 6785 onunsnss 6798 snon0 6817 snexxph 6831 elfi2 6853 supsnti 6885 djuf1olem 6931 eldju2ndl 6950 eldju2ndr 6951 difinfsnlem 6977 elreal2 7631 ax1rid 7678 ltxrlt 7823 un0addcl 9003 un0mulcl 9004 elfzonlteqm1 9980 fxnn0nninf 10204 1exp 10315 hashinfuni 10516 hashennnuni 10518 hashprg 10547 zfz1isolemiso 10575 fisumss 11154 sumsnf 11171 fsumsplitsn 11172 fsum2dlemstep 11196 fisumcom2 11200 divalgmod 11613 phi1 11884 dfphi2 11885 exmidunben 11928 txdis1cn 12436 bj-nntrans 13138 bj-nnelirr 13140 pwtrufal 13181 exmidsbthrlem 13206 |
Copyright terms: Public domain | W3C validator |