![]() |
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 3607 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ibi 176 |
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 3598 |
This theorem is referenced by: elsn2g 3625 nelsn 3627 disjsn2 3655 sssnm 3754 disjxsn 4001 pwntru 4199 opth1 4236 elsuci 4403 ordtri2orexmid 4522 onsucsssucexmid 4526 sosng 4699 elrelimasn 4994 ressn 5169 funcnvsn 5261 funinsn 5265 fvconst 5704 fmptap 5706 fmptapd 5707 fvunsng 5710 mposnif 5968 1stconst 6221 2ndconst 6222 reldmtpos 6253 tpostpos 6264 1domsn 6818 ac6sfi 6897 onunsnss 6915 snon0 6934 snexxph 6948 elfi2 6970 supsnti 7003 djuf1olem 7051 eldju2ndl 7070 eldju2ndr 7071 difinfsnlem 7097 pw1on 7224 elreal2 7828 ax1rid 7875 ltxrlt 8021 un0addcl 9207 un0mulcl 9208 elfzonlteqm1 10207 fxnn0nninf 10435 1exp 10546 hashinfuni 10752 hashennnuni 10754 hashprg 10783 zfz1isolemiso 10814 fisumss 11395 sumsnf 11412 fsumsplitsn 11413 fsum2dlemstep 11437 fisumcom2 11441 fprodssdc 11593 fprodunsn 11607 fprod2dlemstep 11625 fprodcom2fi 11629 fprodsplitsn 11636 divalgmod 11926 phi1 12213 dfphi2 12214 nnnn0modprm0 12249 exmidunben 12421 0nsg 13027 txdis1cn 13671 bj-nntrans 14585 bj-nnelirr 14587 pwtrufal 14629 sssneq 14633 exmidsbthrlem 14652 |
Copyright terms: Public domain | W3C validator |