Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sneq | Unicode version |
Description: Equality theorem for singletons. Part of Exercise 4 of [TakeutiZaring] p. 15. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sneq |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2167 | . . 3 | |
2 | 1 | abbidv 2275 | . 2 |
3 | df-sn 3566 | . 2 | |
4 | df-sn 3566 | . 2 | |
5 | 2, 3, 4 | 3eqtr4g 2215 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1335 cab 2143 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-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-11 1486 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-sn 3566 |
This theorem is referenced by: sneqi 3572 sneqd 3573 euabsn 3629 absneu 3631 preq1 3636 tpeq3 3647 snssg 3692 sneqrg 3725 sneqbg 3726 opeq1 3741 unisng 3789 exmidsssn 4163 exmidsssnc 4164 suceq 4362 snnex 4408 opeliunxp 4641 relop 4736 elimasng 4954 dmsnsnsng 5063 elxp4 5073 elxp5 5074 iotajust 5134 fconstg 5366 f1osng 5455 nfvres 5501 fsng 5640 fnressn 5653 fressnfv 5654 funfvima3 5700 isoselem 5770 1stvalg 6090 2ndvalg 6091 2ndval2 6104 fo1st 6105 fo2nd 6106 f1stres 6107 f2ndres 6108 mpomptsx 6145 dmmpossx 6147 fmpox 6148 brtpos2 6198 dftpos4 6210 tpostpos 6211 eceq1 6515 fvdiagfn 6638 mapsncnv 6640 elixpsn 6680 ixpsnf1o 6681 ensn1g 6742 en1 6744 xpsneng 6767 xpcomco 6771 xpassen 6775 xpdom2 6776 phplem3 6799 phplem3g 6801 fidifsnen 6815 xpfi 6874 pm54.43 7125 cc2lem 7186 cc2 7187 exp3val 10421 fsum2dlemstep 11331 fsumcnv 11334 fisumcom2 11335 fprod2dlemstep 11519 fprodcnv 11522 fprodcom2fi 11523 txswaphmeolem 12731 |
Copyright terms: Public domain | W3C validator |