Database SUPPLEMENTARY MATERIAL (USERS' MATHBOXES) Mathbox for Jonathan Ben-Naim
Table of Contents - 20.4. Mathbox for Jonathan Ben-Naim
Note: On 4-Sep-2016 and after, 745 unused theorems were deleted from this
mathbox, and 359 theorems used only once or twice were merged into their
referencing theorems. The originals can be recovered from set.mm versions
prior to this date.
w-bnj17
df-bnj17
c-bnj14
df-bnj14
w-bnj13
df-bnj13
w-bnj15
df-bnj15
c-bnj18
df-bnj18
w-bnj19
df-bnj19
First-order logic and set theory
bnj170 bnj240 bnj248 bnj250 bnj251 bnj252 bnj253 bnj255 bnj256 bnj257 bnj258 bnj268 bnj290 bnj291 bnj312 bnj334 bnj345 bnj422 bnj432 bnj446 bnj23 bnj31 bnj62 bnj89 bnj90 bnj101 bnj105 bnj115 bnj132 bnj133 bnj156 bnj158 bnj168 bnj206 bnj216 bnj219 bnj226 bnj228 bnj519 bnj521 bnj524 bnj525 bnj534 bnj538 bnj529 bnj551 bnj563 bnj564 bnj593 bnj596 bnj610 bnj642 bnj643 bnj645 bnj658 bnj667 bnj705 bnj706 bnj707 bnj708 bnj721 bnj832 bnj835 bnj836 bnj837 bnj769 bnj770 bnj771 bnj887 bnj918 bnj919 bnj923 bnj927 bnj930 bnj931 bnj937 bnj941 bnj945 bnj946 bnj951 bnj956 bnj976 bnj982 bnj1019 bnj1023 bnj1095 bnj1096 bnj1098 bnj1101 bnj1113 bnj1109 bnj1131 bnj1138 bnj1142 bnj1143 bnj1146 bnj1149 bnj1185 bnj1196 bnj1198 bnj1209 bnj1211 bnj1213 bnj1212 bnj1219 bnj1224 bnj1230 bnj1232 bnj1235 bnj1239 bnj1238 bnj1241 bnj1247 bnj1254 bnj1262 bnj1266 bnj1265 bnj1275 bnj1276 bnj1292 bnj1293 bnj1294 bnj1299 bnj1304 bnj1316 bnj1317 bnj1322 bnj1340 bnj1345 bnj1350 bnj1351 bnj1352 bnj1361 bnj1366 bnj1379 bnj1383 bnj1385 bnj1386 bnj1397 bnj1400 bnj1405 bnj1422 bnj1424 bnj1436 bnj1441 bnj1441g bnj1454 bnj1459 bnj1464 bnj1465 bnj1468 bnj1476 bnj1502 bnj1503 bnj1517 bnj1521 bnj1533 bnj1534 bnj1536 bnj1538 bnj1541 bnj1542
Well founded induction and recursion
bnj110 bnj157 bnj66 bnj91 bnj92 bnj93 bnj95 bnj96 bnj97 bnj98 bnj106 bnj118 bnj121 bnj124 bnj125 bnj126 bnj130 bnj149 bnj150 bnj151 bnj154 bnj155 bnj153 bnj207 bnj213 bnj222 bnj229 bnj517 bnj518 bnj523 bnj526 bnj528 bnj535 bnj539 bnj540 bnj543 bnj544 bnj545 bnj546 bnj548 bnj553 bnj554 bnj556 bnj557 bnj558 bnj561 bnj562 bnj570 bnj571 bnj605 bnj581 bnj589 bnj590 bnj591 bnj594 bnj580 bnj579 bnj602 bnj607 bnj609 bnj611 bnj600 bnj601 bnj852 bnj864 bnj865 bnj873 bnj849 bnj882 bnj18eq1 bnj893 bnj900 bnj906 bnj908 bnj911 bnj916 bnj917 bnj934 bnj929 bnj938 bnj944 bnj953 bnj958 bnj1000 bnj965 bnj964 bnj966 bnj967 bnj969 bnj970 bnj910 bnj978 bnj981 bnj983 bnj984 bnj985v bnj985 bnj986 bnj996 bnj998 bnj999 bnj1001 bnj1006 bnj1014 bnj1015 bnj1018g bnj1018 bnj1020 bnj1021 bnj907 bnj1029 bnj1033 bnj1034 bnj1039 bnj1040 bnj1047 bnj1049 bnj1052 bnj1053 bnj1071 bnj1083 bnj1090 bnj1093 bnj1097 bnj1110 bnj1112 bnj1118 bnj1121 bnj1123 bnj1030 bnj1124 bnj1133 bnj1128 bnj1127 bnj1125 bnj1145 bnj1147 bnj1137 bnj1148 bnj1136 bnj1152 bnj1154 bnj1171 bnj1172 bnj1173 bnj1174 bnj1175 bnj1176 bnj1177 bnj1186 bnj1190 bnj1189
The existence of a minimal element in certain classes
bnj69 bnj1228
Well-founded induction
bnj1204 bnj1234 bnj1245 bnj1256 bnj1259 bnj1253 bnj1279 bnj1286 bnj1280 bnj1296 bnj1309 bnj1307 bnj1311 bnj1318 bnj1326 bnj1321 bnj1364 bnj1371 bnj1373 bnj1374 bnj1384 bnj1388 bnj1398 bnj1413 bnj1408 bnj1414 bnj1415 bnj1416 bnj1418 bnj1417 bnj1421 bnj1444 bnj1445 bnj1446 bnj1447 bnj1448 bnj1449 bnj1442 bnj1450 bnj1423 bnj1452 bnj1466 bnj1467 bnj1463 bnj1489 bnj1491 bnj1312 bnj1493 bnj1497 bnj1498
Well-founded recursion, part 1 of 3
bnj60 bnj1514 bnj1518 bnj1519 bnj1520 bnj1501
Well-founded recursion, part 2 of 3
bnj1500 bnj1525 bnj1529 bnj1523
Well-founded recursion, part 3 of 3
bnj1522