Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jonathan Ben-Naim
Metamath Proof Explorer
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
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