![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sneqd | GIF 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 3618 | . 2 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → {𝐴} = {𝐵}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 {csn 3607 |
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-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-sn 3613 |
This theorem is referenced by: dmsnsnsng 5124 cnvsng 5132 ressn 5187 f1osng 5521 fsng 5710 fnressn 5723 fvsng 5733 2nd1st 6205 dfmpo 6248 cnvf1olem 6249 tpostpos 6289 tfrlemi1 6357 tfr1onlemaccex 6373 tfrcllemaccex 6386 elixpsn 6761 ixpsnf1o 6762 en1bg 6826 mapsnen 6837 xpassen 6856 fztp 10108 fzsuc2 10109 fseq1p1m1 10124 fseq1m1p1 10125 zfz1isolemsplit 10850 zfz1isolem1 10852 fsumm1 11456 fprodm1 11638 divalgmod 11964 ennnfonelemg 12454 ennnfonelemp1 12457 ennnfonelem1 12458 ennnfonelemnn0 12473 setsvalg 12542 strsetsid 12545 imasex 12782 imasival 12783 imasaddvallemg 12792 mulgval 13064 isunitd 13456 lspsnneg 13736 lspsnsub 13737 lmodindp1 13744 lidl0 13805 rsp0 13809 ridl0 13825 zrhrhmb 13919 znval 13932 psrval 13944 txdis 14237 |
Copyright terms: Public domain | W3C validator |