New Foundations Explorer Home New Foundations Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  NFE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the New Foundations Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular reference, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Higher-Order Logic Explorer
Bibliographic Reference DescriptionHigher-Order Logic Explorer Page(s)
[BellMachover] p. 36Lemma 10.3id1 19
[BellMachover] p. 97Definition 10.1df-eu 1795
[BellMachover] p. 460Notationdf-mo 1796
[BellMachover] p. 460Definitionmo3 1816
[BellMachover] p. 461Axiom Extax-ext 1877
[BellMachover] p. 462Theorem 1.1bm1.1 1881
[ChoquetDD] p. 2Definition of mappingdf-mpt 4895
[Eisenberg] p. 125Definition 8.21df-map 5213
[Enderton] p. 19Definitiondf-tp 2809
[Enderton] p. 26Exercise 5unissb 3065
[Enderton] p. 30Theorem "Distributive laws"iinun2 3918  iunin2 3917
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 3921  iundif2 3919
[Enderton] p. 32Exercise 20unineq 2716
[Enderton] p. 33Exercise 23iinuni 3927
[Enderton] p. 33Exercise 25iununi 3928
[Enderton] p. 33Exercise 24(a)iinpw 3932
[Enderton] p. 33Exercise 24(b)iunpwss 3933
[Enderton] p. 38Exercise 6(a)unipw 3219
[Enderton] p. 41Lemma 3Drnex 4317  rnexg 4314
[Enderton] p. 41Exercise 8dmuni 4105  rnuni 4234
[Enderton] p. 42Definition of a functiondffun7 4344  dffun8 4345
[Enderton] p. 43Definition of function valuefunfv2 4594
[Enderton] p. 43Definition of single-rootedfuncnv 4367
[Enderton] p. 44Definition (d)dfima4 4144
[Enderton] p. 47Theorem 3Hfvco2 4600
[Enderton] p. 50Theorem 3K(a)imauni 4705
[Enderton] p. 52Definitiondf-map 5213
[Enderton] p. 53Exercise 21coass 4304
[Enderton] p. 53Exercise 27dmco 4293
[Enderton] p. 53Exercise 14(a)funin 4376
[Enderton] p. 53Exercise 22(a)imass2 4218
[Enderton] p. 56Theorem 3Merref 5170
[Enderton] p. 57Lemma 3Nerthi 5181
[Enderton] p. 57Definitiondf-ec 5158
[Enderton] p. 58Definitiondf-qs 5162
[Enderton] p. 61Exercise 35df-ec 5158
[Enderton] p. 65Exercise 56(a)dmun 4103
[Enderton] p. 79Definition of operation valuedf-ov 4768
[Enderton] p. 129Definitiondf-en 5241
[Enderton] p. 144Corollary 6Kundif2 2778
[Enderton] p. 145Figure 38ffoss 4530
[Gleason] p. 119Proposition 9-2.4caovmo 4889
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)id1 19
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1326
[Jech] p. 4Definition of classcv 1397  cvjust 1890
[KalishMontague] p. 81Axiom B7' in footnote 1ax-9 1424
[Kunen] p. 10Axiom 0a9e 1521
[Kunen] p. 24Definition 10.24mapval 5223  mapvalg 5221
[Kunen] p. 31Definition 10.24mapex 5218  mapexi 5215
[Margaris] p. 40Rule Cexlimiv 1695
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 357  df-ex 1328  df-or 356  dfbi2 599
[Margaris] p. 51Theorem 1id1 19
[Margaris] p. 56Theorem 3syld 39
[Margaris] p. 60Theorem 8mth8 135
[Margaris] p. 89Theorem 19.219.2 1468  r19.2z 2783
[Margaris] p. 89Theorem 19.319.3 1469  rr19.3v 2408
[Margaris] p. 89Theorem 19.5alcom 1347
[Margaris] p. 89Theorem 19.6alex 1349
[Margaris] p. 89Theorem 19.7alnex 1348
[Margaris] p. 89Theorem 19.819.8a 1467
[Margaris] p. 89Theorem 19.919.9 1471  19.9v 1683
[Margaris] p. 89Theorem 19.11excom 1474  excomim 1473
[Margaris] p. 89Theorem 19.1219.12 1475  r19.12 2207
[Margaris] p. 90Theorem 19.14exnal 1351
[Margaris] p. 90Theorem 19.15albi 1340  ralbi 2227
[Margaris] p. 90Theorem 19.1619.16 1476
[Margaris] p. 90Theorem 19.1719.17 1477
[Margaris] p. 90Theorem 19.18exbi 1358
[Margaris] p. 90Theorem 19.1919.19 1478
[Margaris] p. 90Theorem 19.20alim 1336  alimd 1339  alimdv 1689  ralimdaa 2171  ralimdv 2173  ralimdva 2172  sbcimdv 2525
[Margaris] p. 90Theorem 19.2119.21-2 1480  19.21 1479  19.21bi 1482  19.21t 1513  19.21v 1684  alrimd 1364  alrimdv 1687  alrimi 1341  alrimiv 1685  alrimivv 1686  r19.21 2180  r19.21be 2195  r19.21bi 2192  r19.21t 2179  r19.21v 2181  ralrimd 2182  ralrimdv 2183  ralrimdva 2184  ralrimdvv 2188  ralrimdvva 2189  ralrimi 2175  ralrimiv 2176  ralrimiva 2177  ralrimivv 2185  ralrimivva 2186  ralrimivvva 2187  ralrimivw 2178  rexlimi 2211
[Margaris] p. 90Theorem 19.222alimdv 1691  2eximdv 1692  exim 1352  eximd 1365  eximdv 1690  rexim 2198  reximdai 2202  reximdv 2205  reximdv2 2203  reximdva 2206  reximdvai 2204  reximi2 2200
[Margaris] p. 90Theorem 19.2319.23 1484  19.23bi 1486  19.23t 1514  19.23v 1693  19.23vv 1694  exlimd 1487  exlimdv 1612  exlimdvv 1698  exlimi 1485  exlimiv 1695  exlimivv 1697  r19.23 2209  r19.23v 2210  rexlimd 2215  rexlimdv 2217  rexlimdva 2218  rexlimdvv 2221  rexlimdvva 2222  rexlimdvw 2219  rexlimiv 2212  rexlimiva 2213  rexlimivv 2220
[Margaris] p. 90Theorem 19.2419.24 1495
[Margaris] p. 90Theorem 19.2519.25 1381
[Margaris] p. 90Theorem 19.2619.26-2 1372  19.26-3an 1373  19.26 1371  r19.26-2 2224  r19.26-3 2225  r19.26 2223  r19.26m 2226
[Margaris] p. 90Theorem 19.2719.27 1488  19.27v 1699  r19.27av 2229  r19.27z 2792  r19.27zv 2793
[Margaris] p. 90Theorem 19.2819.28 1489  19.28v 1700  r19.28av 2230  r19.28z 2786  r19.28zv 2789  rr19.28v 2409
[Margaris] p. 90Theorem 19.2919.29 1374  19.29r 1375  19.29r2 1376  19.29x 1377  r19.29 2231  r19.29r 2232
[Margaris] p. 90Theorem 19.3019.30 1382  r19.30 2233
[Margaris] p. 90Theorem 19.3119.31 1497
[Margaris] p. 90Theorem 19.3219.32 1496  r19.32v 2234
[Margaris] p. 90Theorem 19.3319.33 1384  19.33b 1385
[Margaris] p. 90Theorem 19.3419.34 1500
[Margaris] p. 90Theorem 19.3519.35 1378  19.35i 1379  19.35ri 1380  r19.35 2235
[Margaris] p. 90Theorem 19.3619.36 1490  19.36aiv 1702  19.36i 1491  19.36v 1701  r19.36av 2236  r19.36zv 2794
[Margaris] p. 90Theorem 19.3719.37 1492  19.37aiv 1705  19.37v 1704  r19.37av 2237  r19.37zv 2790
[Margaris] p. 90Theorem 19.3819.38 1493
[Margaris] p. 90Theorem 19.3919.39 1494
[Margaris] p. 90Theorem 19.4019.40-2 1387  19.40 1386  r19.40 2238
[Margaris] p. 90Theorem 19.4119.41 1501  19.41v 1706  19.41vv 1707  19.41vvv 1708  19.41vvvv 1709  r19.41 2239  r19.41v 2240
[Margaris] p. 90Theorem 19.4219.42 1502  19.42v 1710  19.42vv 1712  19.42vvv 1713  r19.42v 2241
[Margaris] p. 90Theorem 19.4319.43 1383  r19.43 2242
[Margaris] p. 90Theorem 19.4419.44 1498  r19.44av 2243
[Margaris] p. 90Theorem 19.4519.45 1499  r19.45av 2244  r19.45zv 2791
[Margaris] p. 110Exercise 2(b)eu1 1806
[Megill] p. 444Axiom C5ax-17 1413
[Megill] p. 445Lemma L12alequcom 1409  ax-10 1403
[Megill] p. 446Lemma L17equtrr 1530
[Megill] p. 446Lemma L18ax9 1520
[Megill] p. 446Lemma L19hbnae 1542
[Megill] p. 447Remark 9.1df-sb 1568  sbid 1580
[Megill] p. 448Remark 9.6ax15 1768
[Megill] p. 448Scheme C4'ax-5o 1431
[Megill] p. 448Scheme C5'ax-4 1429
[Megill] p. 448Scheme C6'ax-7 1325
[Megill] p. 448Scheme C7'ax-6o 1434
[Megill] p. 448Scheme C8'ax-8 1402
[Megill] p. 448Scheme C9'ax-12 1405
[Megill] p. 448Scheme C10'ax-9 1424  ax-9o 1519
[Megill] p. 448Scheme C11'ax-10o 1538
[Megill] p. 448Scheme C12'ax-13 1406
[Megill] p. 448Scheme C13'ax-14 1407
[Megill] p. 448Scheme C14'ax-15 1769
[Megill] p. 448Scheme C15'ax-11o 1616
[Megill] p. 448Scheme C16'ax-16 1606
[Megill] p. 448Theorem 9.4dral1 1548  dral2 1549  drex1 1550  drex2 1551  drsb1 1571  drsb2 1628
[Megill] p. 449Theorem 9.7sbcom2 1744  sbequ 1627  sbid2v 1752
[Megill] p. 450Example in Appendixhba1 1441
[Mendelson] p. 36Lemma 1.8id1 19
[Mendelson] p. 69Axiom 4ra4sbc 2543  ra4sbca 2544  stdpc4 1581
[Mendelson] p. 69Axiom 5ax-5o 1431  ra5 2546  stdpc5 1481
[Mendelson] p. 81Rule Cexlimiv 1695
[Mendelson] p. 95Axiom 6stdpc6 1525
[Mendelson] p. 95Axiom 7stdpc7 1576
[Mendelson] p. 231Exercise 4.10(k)inv1 2752
[Mendelson] p. 231Exercise 4.10(l)unv 2753
[Mendelson] p. 231Exercise 4.10(o)df-nul 2727
[Mendelson] p. 231Exercise 4.10(q)dfin4 3032
[Mendelson] p. 235Exercise 4.12(n)uniin 3057
[Mendelson] p. 235Exercise 4.12(p)reli 4051
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 4306
[Mendelson] p. 254Proposition 4.22(b)xpen 5268
[Mendelson] p. 254Proposition 4.22(c)xpsnen 5262  xpsneng 5263
[Mendelson] p. 254Proposition 4.22(d)xpcomen 5265  xpcomeng 5266
[Mendelson] p. 254Proposition 4.22(e)xpassen 5269
[Mendelson] p. 255Exercise 4.39endisj 5264
[Mendelson] p. 255Exercise 4.41mapprc 5216
[Monk1] p. 26Theorem 2.8(vii)ssin 3008
[Monk1] p. 33Theorem 3.2(i)ssrel 4018
[Monk1] p. 33Theorem 3.2(ii)eqrel 4019
[Monk1] p. 34Definition 3.3df-opab 3723
[Monk1] p. 36Theorem 3.7(i)coi1 4300  coi2 4301
[Monk1] p. 36Theorem 3.8(v)dm0 4109  rn0 4161
[Monk1] p. 36Theorem 3.7(ii)cnvi 4228
[Monk1] p. 37Theorem 3.13(i)relxp 4034
[Monk1] p. 37Theorem 3.13(x)dmxp 4114  rnxp 4247
[Monk1] p. 37Theorem 3.13(ii)xp0 4240  xp0r 4012
[Monk1] p. 38Theorem 3.16(ii)ima0 4206
[Monk1] p. 38Theorem 3.16(viii)imai 4203
[Monk1] p. 39Theorem 3.16(xi)imassrn 4202
[Monk1] p. 41Theorem 4.3(i)fnopfv 4644  funfvop 4632
[Monk1] p. 42Theorem 4.3(ii)funopfvb 4579
[Monk1] p. 42Theorem 4.4(iii)fvelima 4587
[Monk1] p. 43Theorem 4.6funun 4357
[Monk1] p. 43Theorem 4.8(iv)dff13 4711  dff13f 4712
[Monk1] p. 50Definition 5.4fniunfv 4706
[Monk1] p. 52Theorem 5.11(viii)ssint 3087
[Monk2] p. 105Axiom C4ax-5 1323
[Monk2] p. 105Axiom C7ax-8 1402
[Monk2] p. 105Axiom C8ax-11 1404  ax-11o 1616
[Monk2] p. 105Axiom (C8)ax11v 1665
[Monk2] p. 108Lemma 5ax-5o 1431
[Monk2] p. 109Lemma 12ax-7 1325
[Monk2] p. 109Lemma 15equvin 1674  equvini 1564  eqvinop 3712
[Monk2] p. 113Axiom C5-1ax-17 1413
[Monk2] p. 113Axiom C5-2ax-6 1324
[Monk2] p. 113Axiom C5-3ax-7 1325
[Monk2] p. 114Lemma 21ax4 1428
[Monk2] p. 114Lemma 22ax5o 1430  hba1 1441
[Monk2] p. 114Lemma 23hbia1 1452
[Monk2] p. 114Lemma 24hba2 1451  hbra2 2147
[Quine] p. 16Definition 2.1df-clab 1883  rabid 2256
[Quine] p. 17Definition 2.1''dfsb7 1749
[Quine] p. 18Definition 2.7df-cleq 1888
[Quine] p. 34Theorem 5.1abeq2 1994
[Quine] p. 35Theorem 5.2abid2 2006  abid2f 2007
[Quine] p. 40Theorem 6.1sb5 1668
[Quine] p. 40Theorem 6.2sb56 1666  sb6 1667
[Quine] p. 41Theorem 6.3df-clel 1891
[Quine] p. 41Theorem 6.4eqid 1895
[Quine] p. 41Theorem 6.5eqcom 1897
[Quine] p. 42Theorem 6.6df-sbc 2469
[Quine] p. 42Theorem 6.7dfsbcq 2470
[Quine] p. 43Theorem 6.8vex 2303
[Quine] p. 43Theorem 6.9isset 2304
[Quine] p. 44Theorem 7.3cla4gf 2368  cla4gv 2370
[Quine] p. 44Theorem 6.11a4sbc 2472
[Quine] p. 44Theorem 6.12elex 2308
[Quine] p. 44Theorem 6.13elab 2412  elabg 2414  elabgf 2413  elabs2 2500
[Quine] p. 44Theorem 6.14noel 2731
[Quine] p. 48Definition 7.1df-pr 2808  df-sn 2807
[Quine] p. 49Theorem 7.4snss 2997  snssg 2999
[Quine] p. 49Theorem 7.5prss 3005  prssg 3016
[Quine] p. 53Theorem 8.2unisn 3053  unisng 3054
[Quine] p. 53Theorem 8.3uniun 3056
[Quine] p. 54Theorem 8.6elssuni 3063
[Quine] p. 54Theorem 8.7uni0 3062
[Quine] p. 56Theorem 8.17uniabio 3460
[Quine] p. 56Definition 8.18dfiota2 3451
[Quine] p. 57Theorem 8.19iotaval 3461
[Quine] p. 57Theorem 8.22iotanul 3463
[Quine] p. 58Theorem 8.23iotaex 3464
[Quine] p. 61Theorem 9.5opabid 3790  opelopab 3806  opelopaba 3801  opelopabaf 3808  opelopabf 3809  opelopabg 3803  opelopabga 3798  oprabid 4787
[Quine] p. 64Definition 9.11df-xp 3957
[Quine] p. 64Definition 9.12df-cnv 3959
[Quine] p. 64Definition 9.15df-id 3939
[Quine] p. 65Theorem 10.3fun0 4364
[Quine] p. 65Theorem 10.4funi 4348
[Quine] p. 65Theorem 10.5funsn 4358  funsng 4359
[Quine] p. 65Definition 10.1df-fun 3963
[Quine] p. 65Definition 10.2args 4213
[Quine] p. 68Definition 10.11fv2 4540
[Schechter] p. 51Definition of antisymmetryintasym 4224
[Schechter] p. 51Definition of irreflexivityintirr 4225
[Schechter] p. 51Definition of symmetrycnvsym 4223
[Schechter] p. 51Definition of transitivitycotr 4222
[Stoll] p. 16Exercise 4.40dif 2773  dif0 2772
[Stoll] p. 16Exercise 4.8difdifdir 2782
[Stoll] p. 17Theorem 5.1(5)undifv 2776
[Stoll] p. 43Definitionuniiun 3906
[Stoll] p. 44Definitionintiin 3907
[Stoll] p. 45Definitiondf-iin 3863
[Stoll] p. 45Definition indexed uniondf-iun 3862
[Stoll] p. 176Theorem 3.4(27)iman 407
[Suppes] p. 22Theorem 2eq0 2741
[Suppes] p. 22Theorem 4eqss 2902  eqssd 2904  eqssi 2903
[Suppes] p. 23Theorem 5ss0 3023  ss0b 3022
[Suppes] p. 23Theorem 6sstr 2895
[Suppes] p. 23Theorem 7pssirr 2973
[Suppes] p. 23Theorem 8pssn2lp 2974
[Suppes] p. 23Theorem 9psstr 2977
[Suppes] p. 23Theorem 10pssss 2970
[Suppes] p. 26Theorem 16in0 2751
[Suppes] p. 27Theorem 24un0 2750
[Suppes] p. 27Theorem 25ssun1 2985
[Suppes] p. 27Theorem 26ssequn1 2990
[Suppes] p. 27Theorem 27unss 2994
[Suppes] p. 27Theorem 28indir 2714
[Suppes] p. 27Theorem 29undir 2715
[Suppes] p. 28Theorem 32difid 2770
[Suppes] p. 29Theorem 33difin 3031
[Suppes] p. 29Theorem 35undif1 2777
[Suppes] p. 29Theorem 36difun2 2781
[Suppes] p. 29Theorem 37difin0 2775
[Suppes] p. 29Theorem 38disjdif 2774
[Suppes] p. 39Theorem 61uniss 3058
[Suppes] p. 41Theorem 70intsn 3105
[Suppes] p. 42Theorem 71intpr 3103  intprg 3104
[Suppes] p. 42Theorem 78intun 3102
[Suppes] p. 44Definition 15(a)dfiun2 3887  dfiun2g 3886
[Suppes] p. 44Definition 15(b)dfiin2 3889
[Suppes] p. 47Theorem 86elpw 3171  elpwg 3172
[Suppes] p. 47Theorem 87pwid 3176
[Suppes] p. 47Theorem 89pw0 3264
[Suppes] p. 52Theorem 101xpss12 4032
[Suppes] p. 52Theorem 102xpindi 4056  xpindir 4057
[Suppes] p. 52Theorem 103xpundi 3998  xpundir 3999
[Suppes] p. 58Theorem 2relss 4017
[Suppes] p. 59Theorem 4eldm 4089  eldm2 4090
[Suppes] p. 60Theorem 6dmin 4104
[Suppes] p. 60Theorem 8rnun 4232
[Suppes] p. 60Theorem 9rnin 4233
[Suppes] p. 60Definition 4dfrn2 4093
[Suppes] p. 61Theorem 11brcnv 4083
[Suppes] p. 62Equation 5elcnv 4080  elcnv2 4081
[Suppes] p. 62Theorem 12relcnv 4220
[Suppes] p. 62Theorem 15cnvin 4231
[Suppes] p. 62Theorem 16cnvun 4229
[Suppes] p. 63Theorem 20co02 4298
[Suppes] p. 63Theorem 21dmcoss 4163
[Suppes] p. 64Theorem 26cnvco 4085
[Suppes] p. 64Theorem 27coass 4304
[Suppes] p. 65Theorem 31resundi 4173
[Suppes] p. 65Theorem 34elima 3852  elima2 3853  elima3 3854
[Suppes] p. 65Theorem 35imaundi 4235
[Suppes] p. 66Theorem 40dminss 4237
[Suppes] p. 66Theorem 41imainss 4238
[Suppes] p. 67Exercise 11cnvxp 4239
[Suppes] p. 81Definition 34dfec2 5159
[Suppes] p. 82Theorem 72elec 5175
[Suppes] p. 82Theorem 73erth 5179  erth2 5180
[Suppes] p. 83Theorem 74erdisj 5184
[Suppes] p. 89Theorem 96map0b 5236
[Suppes] p. 89Theorem 97map0 5237
[Suppes] p. 89Theorem 98mapsn 5238
[Suppes] p. 89Theorem 99mapss 5239
[Suppes] p. 92Theorem 4unen 5261
[Suppes] p. 98Exercise 4fundmen 5256  fundmeng 5257
[TakeutiZaring] p. 8Axiom 1ax-ext 1877
[TakeutiZaring] p. 13Definition 4.5df-cleq 1888
[TakeutiZaring] p. 13Proposition 4.6df-clel 1891
[TakeutiZaring] p. 13Proposition 4.9cvjust 1890
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 1912
[TakeutiZaring] p. 14Definition 4.16df-oprab 4769
[TakeutiZaring] p. 14Proposition 4.14ru 2468
[TakeutiZaring] p. 15Exercise 1elpr 2844  elpr2 2845
[TakeutiZaring] p. 15Exercise 4sneq 2810
[TakeutiZaring] p. 15Definition 5.1dfpr2 2841
[TakeutiZaring] p. 16Definition 5.3dftp2 2849
[TakeutiZaring] p. 16Definition 5.5df-uni 3038
[TakeutiZaring] p. 16Proposition 5.7unipr 3051  uniprg 3052
[TakeutiZaring] p. 17Exercise 1eltp 2848
[TakeutiZaring] p. 17Exercise 5sstr2 2894
[TakeutiZaring] p. 17Exercise 10indi 2712
[TakeutiZaring] p. 17Exercise 11undi 2713
[TakeutiZaring] p. 17Definition 5.9df-pss 2878  dfss2 2879
[TakeutiZaring] p. 17Definition 5.10df-pw 3167
[TakeutiZaring] p. 18Exercise 7unss2 2991
[TakeutiZaring] p. 18Exercise 9df-ss 2876  sseqin2 3029
[TakeutiZaring] p. 18Exercise 10ssid 2905
[TakeutiZaring] p. 18Exercise 12inss1 3003  inss2 3006
[TakeutiZaring] p. 18Exercise 13nss 2940
[TakeutiZaring] p. 18Exercise 15unieq 3046
[TakeutiZaring] p. 18Exercise 18sspwb 3220
[TakeutiZaring] p. 20Definitiondf-rab 2110
[TakeutiZaring] p. 20Definition 5.14dfnul2 2728
[TakeutiZaring] p. 20Proposition 5.15difid 2770
[TakeutiZaring] p. 20Proposition 5.17(1)n0 2736  n0f 2735  neq0 2737
[TakeutiZaring] p. 21Definition 5.20df-v 2302
[TakeutiZaring] p. 22Exercise 7ssdif0 3015
[TakeutiZaring] p. 22Exercise 14difss 2980
[TakeutiZaring] p. 22Exercise 15sscon 2983
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2107
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2108
[TakeutiZaring] p. 23Proposition 6.2xpex 4325  xpexg 4324
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 3958
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 4369
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 4478  fun11 4372
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 4331  svrelfun 4370
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4092
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4094
[TakeutiZaring] p. 24Definition 6.6(1)df-res 3962
[TakeutiZaring] p. 25Exercise 2cnvcnvss 4262  dfrel2 4258
[TakeutiZaring] p. 25Exercise 3xpss 4033
[TakeutiZaring] p. 25Exercise 5relun 4040
[TakeutiZaring] p. 25Exercise 6reluni 4046
[TakeutiZaring] p. 25Exercise 9inxp 4055
[TakeutiZaring] p. 25Exercise 12relres 4184
[TakeutiZaring] p. 25Exercise 13opelres 4142
[TakeutiZaring] p. 25Exercise 14dmres 4178
[TakeutiZaring] p. 25Exercise 15resss 4180
[TakeutiZaring] p. 25Exercise 17resabs1 4185
[TakeutiZaring] p. 25Exercise 18funres 4354
[TakeutiZaring] p. 25Exercise 24relco 4221
[TakeutiZaring] p. 25Exercise 29funco 4353
[TakeutiZaring] p. 25Exercise 30f1co 4479
[TakeutiZaring] p. 26Definition 6.10eu2 1810
[TakeutiZaring] p. 26Definition 6.11fv3 4558
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 4312  cnvexg 4311
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4316  dmexg 4315
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4317  rnexg 4314
[TakeutiZaring] p. 27Corollary 6.13fvex 4556
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 4561  tz6.12 4562  tz6.12c 4565
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 4564  tz6.12i 4566
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 3964
[TakeutiZaring] p. 27Definition 6.15(3)df-f 3965
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 3967  wfo 3952
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 3966  wf1 3951
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 3968  wf1o 3953
[TakeutiZaring] p. 28Exercise 4eqfnfv 4622  eqfnfv2 4623  eqfnfv2f 4626
[TakeutiZaring] p. 28Exercise 5fvco 4601
[TakeutiZaring] p. 29Definition 6.18df-br 3737
[TakeutiZaring] p. 30Definition 6.21eliniseg 4214  iniseg 4216
[TakeutiZaring] p. 30Definition 6.22df-eprel 3936
[TakeutiZaring] p. 32Definition 6.28df-iso 3970
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 4732
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 4733
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 4737
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 4738
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 4739
[TakeutiZaring] p. 34Proposition 6.33f1oiso 4741
[TakeutiZaring] p. 40Proposition 7.20elssuni 3063
[TakeutiZaring] p. 44Exercise 2int0 3085
[TakeutiZaring] p. 44Exercise 4intss1 3086
[TakeutiZaring] p. 44Definition 7.35df-int 3072
[TakeutiZaring] p. 53Proposition 7.532eu5 1870
[TakeutiZaring] p. 59Proposition 8.6iunss2 3898  uniss2 3066
[TakeutiZaring] p. 88Exercise 1en0 5255
[TakeutiZaring] p. 95Definition 10.42df-map 5213
[Tarski] p. 67Axiom B5ax-4 1429
[Tarski] p. 68Lemma 6equid 1522  equid1 1524  equidALT 1523
[Tarski] p. 69Lemma 7equcomi 1526
[Tarski] p. 70Lemma 14a4im 1554  a4ime 1555
[Tarski] p. 70Lemma 16ax-11 1404  ax-11o 1616  ax11i 1536
[Tarski] p. 70Lemmas 16 and 17sb6 1667
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1413
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1406  ax-14 1407
[WhiteheadRussell] p. 96Axiom *1.3olc 369
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 371
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 490
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 499
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 768
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 157
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 105
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 75
[WhiteheadRussell] p. 100Theorem *2.05imim2 48
[WhiteheadRussell] p. 100Theorem *2.06imim1 69
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 401
[WhiteheadRussell] p. 101Theorem *2.06syl 14
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 381
[WhiteheadRussell] p. 101Theorem *2.08id 18  id1 19
[WhiteheadRussell] p. 101Theorem *2.11exmid 400
[WhiteheadRussell] p. 101Theorem *2.12notnot1 111
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 402
[WhiteheadRussell] p. 102Theorem *2.14notnot2 102
[WhiteheadRussell] p. 102Theorem *2.15con1 117
[WhiteheadRussell] p. 103Theorem *2.16con3 123  con3th 874
[WhiteheadRussell] p. 103Theorem *2.17ax-3 7
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 100
[WhiteheadRussell] p. 104Theorem *2.2orc 370
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 545
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 98
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 99
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 389
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 807
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 34
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 502
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 503
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 770
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 771
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 769
[WhiteheadRussell] p. 105Definition *2.33df-3or 885
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 548
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 546
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 547
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 46
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 382
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 383
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 141
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 159
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 384
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 385
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 386
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 142
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 144
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 359
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 360
[WhiteheadRussell] p. 107Theorem *2.55orel1 367
[WhiteheadRussell] p. 107Theorem *2.56orel2 368
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 160
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 394
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 718
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 719
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 161
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 387  pm2.67 388
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 143
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 393
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 777
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 395
[WhiteheadRussell] p. 108Theorem *2.69looinv 171
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 772
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 773
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 776
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 775
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 778
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 779
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 70
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 780
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 93
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 475
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 425  pm3.2im 134
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 476
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 477
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 478
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 479
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 426
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 427
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 806
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 560
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 422
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 423
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 434  simplim 140
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 438  simprim 139
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 558
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 559
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 552
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 535
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 533
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 534
[WhiteheadRussell] p. 113Theorem *3.44jao 489  pm3.44 488
[WhiteheadRussell] p. 113Theorem *3.47prth 544
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 786
[WhiteheadRussell] p. 113Theorem *3.45 (Fact)pm3.45 761
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 760
[WhiteheadRussell] p. 116Theorem *4.1con34b 280
[WhiteheadRussell] p. 117Theorem *4.2biid 224
[WhiteheadRussell] p. 117Theorem *4.11notbi 283
[WhiteheadRussell] p. 117Theorem *4.12con2bi 315
[WhiteheadRussell] p. 117Theorem *4.13notnot 279
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 551
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 554
[WhiteheadRussell] p. 117Theorem *4.21bicom 188
[WhiteheadRussell] p. 117Theorem *4.22biantr 847  bitr 676
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 613
[WhiteheadRussell] p. 117Theorem *4.25oridm 491  pm4.25 492
[WhiteheadRussell] p. 118Theorem *4.3ancom 428
[WhiteheadRussell] p. 118Theorem *4.4andi 791
[WhiteheadRussell] p. 118Theorem *4.31orcom 372
[WhiteheadRussell] p. 118Theorem *4.32anass 619
[WhiteheadRussell] p. 118Theorem *4.33orass 501
[WhiteheadRussell] p. 118Theorem *4.36anbi1 674
[WhiteheadRussell] p. 118Theorem *4.37orbi1 673
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 796
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 795
[WhiteheadRussell] p. 118Definition *4.34df-3an 886
[WhiteheadRussell] p. 119Theorem *4.41ordi 788
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 876
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 843
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 550
[WhiteheadRussell] p. 119Theorem *4.45orabs 782  pm4.45 658  pm4.45im 536
[WhiteheadRussell] p. 119Theorem *10.2219.26 1371
[WhiteheadRussell] p. 120Theorem *4.5anor 466
[WhiteheadRussell] p. 120Theorem *4.6imor 397
[WhiteheadRussell] p. 120Theorem *4.7anclb 521
[WhiteheadRussell] p. 120Theorem *4.51ianor 465
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 468
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 469
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 470
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 471
[WhiteheadRussell] p. 120Theorem *4.56ioran 467  pm4.56 472
[WhiteheadRussell] p. 120Theorem *4.57oran 473  pm4.57 474
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 409
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 403
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 405
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 358
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 410
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 404
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 411
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 601  pm4.71i 603  pm4.71r 602  pm4.71rd 605  pm4.71ri 604
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 800
[WhiteheadRussell] p. 121Theorem *4.73iba 480
[WhiteheadRussell] p. 121Theorem *4.74biorf 390
[WhiteheadRussell] p. 121Theorem *4.76jcab 787  pm4.76 790
[WhiteheadRussell] p. 121Theorem *4.77jaob 714  pm4.77 717
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 555
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 556
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 351
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 352
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 844
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 845
[WhiteheadRussell] p. 122Theorem *4.84imbi1 310
[WhiteheadRussell] p. 122Theorem *4.85imbi2 311
[WhiteheadRussell] p. 122Theorem *4.86bibi1 314
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 347  impexp 424  pm4.87 557
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 784
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 808
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 809
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 811
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 810
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 813
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 814
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 812
[WhiteheadRussell] p. 124Theorem *5.18nbbn 344  pm5.18 342
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 346
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 785
[WhiteheadRussell] p. 124Theorem *5.22xor 815
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 817
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 818
[WhiteheadRussell] p. 124Theorem *5.25dfor2 396
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 679
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 348
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 323
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 828
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 850
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 561
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 606
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 802
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 823
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 803
[WhiteheadRussell] p. 125Theorem *5.41imdi 349  pm5.41 350
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 522
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 827
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 726
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 824
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 821
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 680
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 839
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 840
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 852
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 327
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 232
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 853
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 1745
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1388
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1387
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1350
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1357
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1696
[WhiteheadRussell] p. 175Definition *14.02df-eu 1795
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2081
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2082
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2512
[WhiteheadRussell] p. 190Theorem *14.22iota4 3465
[WhiteheadRussell] p. 191Theorem *14.23iota4an 3466
[WhiteheadRussell] p. 192Theorem *14.26eupick 1849  eupickbi 1852

  This page was last updated on 14-Aug-2016.
Copyright terms: Public domain
W3C HTML validation [external]