Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sneqd | Unicode version |
Description: Equality deduction for singletons. (Contributed by NM, 22-Jan-2004.) |
Ref | Expression |
---|---|
sneqd.1 |
Ref | Expression |
---|---|
sneqd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneqd.1 | . 2 | |
2 | sneq 3581 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 csn 3570 |
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-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-sn 3576 |
This theorem is referenced by: dmsnsnsng 5075 cnvsng 5083 ressn 5138 f1osng 5467 fsng 5652 fnressn 5665 fvsng 5675 2nd1st 6140 dfmpo 6182 cnvf1olem 6183 tpostpos 6223 tfrlemi1 6291 tfr1onlemaccex 6307 tfrcllemaccex 6320 elixpsn 6692 ixpsnf1o 6693 en1bg 6757 mapsnen 6768 xpassen 6787 fztp 10003 fzsuc2 10004 fseq1p1m1 10019 fseq1m1p1 10020 zfz1isolemsplit 10737 zfz1isolem1 10739 fsumm1 11343 fprodm1 11525 divalgmod 11849 ennnfonelemg 12279 ennnfonelemp1 12282 ennnfonelem1 12283 ennnfonelemnn0 12298 setsvalg 12367 strsetsid 12370 txdis 12824 |
Copyright terms: Public domain | W3C validator |