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.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 2208
[BellMachover] p. 460Notationdf-mo 2209
[BellMachover] p. 460Definitionmo3 2235
[BellMachover] p. 461Axiom Extax-ext 2334
[BellMachover] p. 462Theorem 1.1bm1.1 2338
[ChoquetDD] p. 2Definition of mappingdf-mpt 5693
[Eisenberg] p. 125Definition 8.21df-map 6038
[Enderton] p. 19Definitiondf-tp 3743
[Enderton] p. 26Exercise 5unissb 3921
[Enderton] p. 30Theorem "Distributive laws"iinin1 4037  iinin2 4036  iinun2 4032  iunin1 4031  iunin2 4030
[Enderton] p. 31Theorem "De Morgan's laws"iindif2 4035  iundif2 4033
[Enderton] p. 32Exercise 20unineq 3505
[Enderton] p. 33Exercise 23iinuni 4049
[Enderton] p. 33Exercise 25iununi 4050
[Enderton] p. 33Exercise 24(a)iinpw 4054
[Enderton] p. 33Exercise 24(b)iunpwss 4055
[Enderton] p. 38Exercise 6(a)unipw 4117
[Enderton] p. 41Lemma 3Drnex 5141  rnexg 5138
[Enderton] p. 41Exercise 8dmuni 4927  rnuni 5056
[Enderton] p. 42Definition of a functiondffun7 5168  dffun8 5169
[Enderton] p. 43Definition of function valuefunfv2 5417
[Enderton] p. 43Definition of single-rootedfuncnv 5191
[Enderton] p. 44Definition (d)dfima4 4967
[Enderton] p. 47Theorem 3Hfvco2 5423
[Enderton] p. 50Theorem 3K(a)imauni 5506
[Enderton] p. 52Definitiondf-map 6038
[Enderton] p. 53Exercise 21coass 5128
[Enderton] p. 53Exercise 27dmco 5117
[Enderton] p. 53Exercise 14(a)funin 5200
[Enderton] p. 53Exercise 22(a)imass2 5040
[Enderton] p. 56Theorem 3Merref 5996
[Enderton] p. 57Lemma 3Nerthi 6007
[Enderton] p. 57Definitiondf-ec 5984
[Enderton] p. 58Definitiondf-qs 5988
[Enderton] p. 61Exercise 35df-ec 5984
[Enderton] p. 65Exercise 56(a)dmun 4925
[Enderton] p. 79Definition of operation valuedf-ov 5566
[Enderton] p. 129Definitiondf-en 6066
[Enderton] p. 144Corollary 6Kundif2 3626
[Enderton] p. 145Figure 38ffoss 5355
[Gleason] p. 119Proposition 9-2.4caovmo 5688
[Hailperin] p. 6Axiom P1ax-nin 4078  df-nin 3211
[Hailperin] p. 10Axiom P2ax-si 4083
[Hailperin] p. 10Axiom P3ax-ins2 4084
[Hailperin] p. 10Axiom P4ax-ins3 4085
[Hailperin] p. 10Axiom P5ax-xp 4079
[Hailperin] p. 10Axiom P6ax-typlower 4086
[Hailperin] p. 10Axiom P7ax-cnv 4080
[Hailperin] p. 10Axiom P8ax-1c 4081
[Hailperin] p. 10Axiom P9ax-sset 4082
[Hamilton] p. 28Definition 2.1ax-1 5
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 8
[Hamilton] p. 74Rule 2ax-gen 1546
[Hitchcock] p. 5Rule A3mpto1 1533
[Hitchcock] p. 5Rule A4mpto2 1534
[Hitchcock] p. 5Rule A5mtp-xor 1536
[Holmes] p. 40Definitiondf-txp 5773
[Jech] p. 4Definition of classcv 1641  cvjust 2348
[KalishMontague] p. 81Note 1ax-9 1654
[KalishMontague] p. 85Lemma 2equid 1676
[KalishMontague] p. 85Lemma 3equcomi 1679
[KalishMontague] p. 86Lemma 7cbvalivw 1674  cbvaliw 1673
[KalishMontague] p. 87Lemma 8spimvw 1669  spimw 1668
[KalishMontague] p. 87Lemma 9spfw 1691  spw 1694
[Kunen] p. 10Axiom 0a9e 1951
[Kunen] p. 24Definition 10.24mapval 6048  mapvalg 6046
[Kunen] p. 31Definition 10.24mapex 6043  mapexi 6040
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3979
[Levy] p. 338Axiomdf-clab 2340  df-clel 2349  df-cleq 2346
[Lopez-Astorga] p. 12Rule 1mpto1 1533
[Lopez-Astorga] p. 12Rule 2mpto2 1534
[Lopez-Astorga] p. 12Rule 3mtp-xor 1536
[Margaris] p. 40Rule Cexlimiv 1634
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3ax-3 7
[Margaris] p. 49Definitiondf-an 360  df-ex 1542  df-or 359  dfbi2 609
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 40
[Margaris] p. 60Theorem 8mth8 138
[Margaris] p. 89Theorem 19.219.2 1659  19.2g 1757  r19.2z 3639
[Margaris] p. 89Theorem 19.319.3 1785  19.3v 1665  rr19.3v 2980
[Margaris] p. 89Theorem 19.5alcom 1737
[Margaris] p. 89Theorem 19.6alex 1572
[Margaris] p. 89Theorem 19.7alnex 1543
[Margaris] p. 89Theorem 19.819.8a 1756
[Margaris] p. 89Theorem 19.919.9 1783  19.9h 1780  19.9v 1664
[Margaris] p. 89Theorem 19.11excom 1741  excomim 1742
[Margaris] p. 89Theorem 19.1219.12 1847  r19.12 2727
[Margaris] p. 90Theorem 19.14exnal 1574
[Margaris] p. 90Theorem 19.15albi 1564  ralbi 2750
[Margaris] p. 90Theorem 19.1619.16 1860
[Margaris] p. 90Theorem 19.1719.17 1861
[Margaris] p. 90Theorem 19.18exbi 1581
[Margaris] p. 90Theorem 19.1919.19 1862
[Margaris] p. 90Theorem 19.20alim 1558  alimd 1764  alimdh 1563  alimdv 1621  ralimdaa 2691  ralimdv 2693  ralimdva 2692  sbcimdv 3107
[Margaris] p. 90Theorem 19.2119.21-2 1864  19.21 1796  19.21bi 1758  19.21h 1797  19.21t 1795  19.21v 1890  alrimd 1769  alrimdd 1768  alrimdh 1587  alrimdv 1633  alrimi 1765  alrimih 1565  alrimiv 1631  alrimivv 1632  r19.21 2700  r19.21be 2715  r19.21bi 2712  r19.21t 2699  r19.21v 2701  ralrimd 2702  ralrimdv 2703  ralrimdva 2704  ralrimdvv 2708  ralrimdvva 2709  ralrimi 2695  ralrimiv 2696  ralrimiva 2697  ralrimivv 2705  ralrimivva 2706  ralrimivvva 2707  ralrimivw 2698  rexlimi 2731
[Margaris] p. 90Theorem 19.222alimdv 1623  2eximdv 1624  exim 1575  eximd 1770  eximdh 1588  eximdv 1622  rexim 2718  reximdai 2722  reximdv 2725  reximdv2 2723  reximdva 2726  reximdvai 2724  reximi2 2720
[Margaris] p. 90Theorem 19.2319.23 1801  19.23bi 1759  19.23h 1802  19.23t 1800  19.23v 1891  19.23vv 1892  exlimd 1806  exlimdh 1807  exlimdv 1636  exlimdvv 1637  exlimi 1803  exlimih 1804  exlimiv 1634  exlimivv 1635  r19.23 2729  r19.23v 2730  rexlimd 2735  rexlimdv 2737  rexlimdv3a 2740  rexlimdva 2738  rexlimdvaa 2739  rexlimdvv 2744  rexlimdvva 2745  rexlimdvw 2741  rexlimiv 2732  rexlimiva 2733  rexlimivv 2743
[Margaris] p. 90Theorem 19.2419.24 1662
[Margaris] p. 90Theorem 19.2519.25 1603
[Margaris] p. 90Theorem 19.2619.26-2 1594  19.26-3an 1595  19.26 1593  r19.26-2 2747  r19.26-3 2748  r19.26 2746  r19.26m 2749
[Margaris] p. 90Theorem 19.2719.27 1869  19.27v 1894  r19.27av 2752  r19.27z 3648  r19.27zv 3649
[Margaris] p. 90Theorem 19.2819.28 1870  19.28v 1895  r19.28av 2753  r19.28z 3642  r19.28zv 3645  rr19.28v 2981
[Margaris] p. 90Theorem 19.2919.29 1596  19.29r 1597  19.29r2 1598  19.29x 1599  r19.29 2754  r19.29r 2755
[Margaris] p. 90Theorem 19.3019.30 1604  r19.30 2756
[Margaris] p. 90Theorem 19.3119.31 1876
[Margaris] p. 90Theorem 19.3219.32 1875  r19.32v 2757
[Margaris] p. 90Theorem 19.3319.33 1607  19.33b 1608
[Margaris] p. 90Theorem 19.3419.34 1663
[Margaris] p. 90Theorem 19.3519.35 1600  19.35i 1601  19.35ri 1602  r19.35 2758
[Margaris] p. 90Theorem 19.3619.36 1871  19.36aiv 1897  19.36i 1872  19.36v 1896  r19.36av 2759  r19.36zv 3650
[Margaris] p. 90Theorem 19.3719.37 1873  19.37aiv 1900  19.37v 1899  r19.37 2760  r19.37av 2761  r19.37zv 3646
[Margaris] p. 90Theorem 19.3819.38 1794
[Margaris] p. 90Theorem 19.3919.39 1661
[Margaris] p. 90Theorem 19.4019.40-2 1610  19.40 1609  r19.40 2762
[Margaris] p. 90Theorem 19.4119.41 1879  19.41v 1901  19.41vv 1902  19.41vvv 1903  19.41vvvv 1904  r19.41 2763  r19.41v 2764
[Margaris] p. 90Theorem 19.4219.42 1880  19.42v 1905  19.42vv 1907  19.42vvv 1908  r19.42v 2765
[Margaris] p. 90Theorem 19.4319.43 1605  r19.43 2766
[Margaris] p. 90Theorem 19.4419.44 1877  r19.44av 2767
[Margaris] p. 90Theorem 19.4519.45 1878  r19.45av 2768  r19.45zv 3647
[Margaris] p. 110Exercise 2(b)eu1 2225
[Megill] p. 444Axiom C5ax-17 1616  ax17o 2157
[Megill] p. 445Lemma L12aecom-o 2151  aecom 1946  ax-10 2140
[Megill] p. 446Lemma L17equtrr 1683
[Megill] p. 446Lemma L18ax9from9o 2148
[Megill] p. 446Lemma L19hbnae-o 2179  hbnae 1955
[Megill] p. 447Remark 9.1df-sb 1649  sbid 1922
[Megill] p. 448Remark 9.6ax15 2021
[Megill] p. 448Scheme C4'ax-5o 2136
[Megill] p. 448Scheme C5'ax-4 2135  sp 1747
[Megill] p. 448Scheme C6'ax-7 1734
[Megill] p. 448Scheme C7'ax-6o 2137
[Megill] p. 448Scheme C8'ax-8 1675
[Megill] p. 448Scheme C9'ax-12o 2142
[Megill] p. 448Scheme C10'ax-9 1654  ax-9o 2138
[Megill] p. 448Scheme C11'ax-10o 2139
[Megill] p. 448Scheme C12'ax-13 1712
[Megill] p. 448Scheme C13'ax-14 1714
[Megill] p. 448Scheme C14'ax-15 2143
[Megill] p. 448Scheme C15'ax-11o 2141
[Megill] p. 448Scheme C16'ax-16 2144
[Megill] p. 448Theorem 9.4dral1-o 2154  dral1 1965  dral2-o 2181  dral2 1966  drex1 1967  drex2 1968  drsb1 2022  drsb2 2061
[Megill] p. 449Theorem 9.7sbcom2 2114  sbequ 2060  sbid2v 2123
[Megill] p. 450Example in Appendixhba1-o 2149  hba1 1786
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 3124  rspsbca 3125  stdpc4 2024
[Mendelson] p. 69Axiom 5ax-5o 2136  ra5 3130  stdpc5 1798
[Mendelson] p. 81Rule Cexlimiv 1634
[Mendelson] p. 95Axiom 6stdpc6 1687
[Mendelson] p. 95Axiom 7stdpc7 1917
[Mendelson] p. 225Axiom system NBGru 3045
[Mendelson] p. 231Exercise 4.10(k)inv1 3577
[Mendelson] p. 231Exercise 4.10(l)unv 3578
[Mendelson] p. 231Exercise 4.10(n)dfin3 3494
[Mendelson] p. 231Exercise 4.10(o)df-nul 3551
[Mendelson] p. 231Exercise 4.10(q)dfin4 3495
[Mendelson] p. 231Exercise 4.10(s)ddif 3398
[Mendelson] p. 231Definition of uniondfun3 3493
[Mendelson] p. 235Exercise 4.12(d)pwv 3886
[Mendelson] p. 235Exercise 4.12(n)uniin 3911
[Mendelson] p. 235Exercise 4.12(p)reli 4873
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5130
[Mendelson] p. 254Proposition 4.22(b)xpen 6093
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6087  xpsneng 6088
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6090  xpcomeng 6091
[Mendelson] p. 254Proposition 4.22(e)xpassen 6094
[Mendelson] p. 255Exercise 4.39endisj 6089
[Mendelson] p. 255Exercise 4.41mapprc 6041
[Mendelson] p. 287Axiom system MKru 3045
[Monk1] p. 26Theorem 2.8(vii)ssin 3477
[Monk1] p. 33Theorem 3.2(i)ssrel 4840
[Monk1] p. 33Theorem 3.2(ii)eqrel 4841
[Monk1] p. 34Definition 3.3df-opab 4616
[Monk1] p. 36Theorem 3.7(i)coi1 5124  coi2 5125
[Monk1] p. 36Theorem 3.8(v)dm0 4931  rn0 4984
[Monk1] p. 36Theorem 3.7(ii)cnvi 5050
[Monk1] p. 37Theorem 3.13(i)relxp 4856
[Monk1] p. 37Theorem 3.13(x)dmxp 4936  rnxp 5069
[Monk1] p. 37Theorem 3.13(ii)xp0 5062  xp0r 4834
[Monk1] p. 38Theorem 3.16(ii)ima0 5029
[Monk1] p. 38Theorem 3.16(viii)imai 5026
[Monk1] p. 39Theorem 3.16(xi)imassrn 5025
[Monk1] p. 41Theorem 4.3(i)fnopfv 5453  funfvop 5441
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5402
[Monk1] p. 42Theorem 4.4(iii)fvelima 5410
[Monk1] p. 43Theorem 4.6funun 5181
[Monk1] p. 43Theorem 4.8(iv)dff13 5512  dff13f 5513
[Monk1] p. 50Definition 5.4fniunfv 5507
[Monk1] p. 52Theorem 5.11(viii)ssint 3942
[Monk2] p. 105Axiom C4ax-5 1557
[Monk2] p. 105Axiom C7ax-8 1675
[Monk2] p. 105Axiom C8ax-11 1746  ax-11o 2141
[Monk2] p. 105Axiom (C8)ax11v 2096
[Monk2] p. 108Lemma 5ax-5o 2136
[Monk2] p. 109Lemma 12ax-7 1734
[Monk2] p. 109Lemma 15equvin 2001  equvini 1987  eqvinop 4605
[Monk2] p. 113Axiom C5-1ax-17 1616  ax17o 2157
[Monk2] p. 113Axiom C5-2ax-6 1729
[Monk2] p. 113Axiom C5-3ax-7 1734
[Monk2] p. 114Lemma 21sp 1747
[Monk2] p. 114Lemma 22ax5o 1749  hba1-o 2149  hba1 1786
[Monk2] p. 114Lemma 23nfia1 1856
[Monk2] p. 114Lemma 24nfa2 1855  nfra2 2668
[Pfenning] p. 17Definition NNCnotnotrd 105
[Quine] p. 16Definition 2.1df-clab 2340  rabid 2787
[Quine] p. 17Definition 2.1''dfsb7 2119
[Quine] p. 18Definition 2.7df-cleq 2346
[Quine] p. 19Definition 2.9df-v 2861
[Quine] p. 34Theorem 5.1abeq2 2458
[Quine] p. 35Theorem 5.2abid2 2470  abid2f 2514
[Quine] p. 40Theorem 6.1sb5 2100
[Quine] p. 40Theorem 6.2sb56 2098  sb6 2099
[Quine] p. 41Theorem 6.3df-clel 2349
[Quine] p. 41Theorem 6.4eqid 2353
[Quine] p. 41Theorem 6.5eqcom 2355
[Quine] p. 42Theorem 6.6df-sbc 3047
[Quine] p. 42Theorem 6.7dfsbcq 3048  dfsbcq2 3049
[Quine] p. 43Theorem 6.8vex 2862
[Quine] p. 43Theorem 6.9isset 2863
[Quine] p. 44Theorem 7.3spcgf 2934  spcgv 2939  spcimgf 2932
[Quine] p. 44Theorem 6.11spsbc 3058  spsbcd 3059
[Quine] p. 44Theorem 6.12elex 2867
[Quine] p. 44Theorem 6.13elab 2985  elabg 2986  elabgf 2983
[Quine] p. 44Theorem 6.14noel 3554
[Quine] p. 48Theorem 7.2snprc 3788
[Quine] p. 48Definition 7.1df-pr 3742  df-sn 3741
[Quine] p. 49Theorem 7.4snss 3838  snssg 3844
[Quine] p. 49Theorem 7.5prss 3861  prssg 3862
[Quine] p. 49Theorem 7.6prid1 3827  prid1g 3825  prid2 3828  prid2g 3826  snid 3760  snidg 3758
[Quine] p. 53Theorem 8.2unisn 3907  unisng 3908
[Quine] p. 53Theorem 8.3uniun 3910
[Quine] p. 54Theorem 8.6elssuni 3919
[Quine] p. 54Theorem 8.7uni0 3918
[Quine] p. 56Theorem 8.17uniabio 4349
[Quine] p. 56Definition 8.18dfiota2 4340
[Quine] p. 57Theorem 8.19iotaval 4350
[Quine] p. 57Theorem 8.22iotanul 4354
[Quine] p. 58Theorem 8.23iotaex 4356
[Quine] p. 61Theorem 9.5opabid 4688  opelopab 4701  opelopaba 4696  opelopabaf 4703  opelopabf 4704  opelopabg 4698  opelopabga 4693  oprabid 5590
[Quine] p. 64Definition 9.11df-xp 4778
[Quine] p. 64Definition 9.12df-cnv 4780
[Quine] p. 64Definition 9.15df-id 4760
[Quine] p. 65Theorem 10.3fun0 5188
[Quine] p. 65Theorem 10.4funi 5172
[Quine] p. 65Theorem 10.5funsn 5182  funsng 5183
[Quine] p. 65Definition 10.1df-fun 4784
[Quine] p. 68Definition 10.11fv2 5365
[Quine] p. 331Axiom system NFru 3045
[Rosser] p. 236Theorem IX.4.21dfpss4 3888
[Rosser] p. 238Definition IX.9.10, df-symdif 3216
[Rosser] p. 245Definitiondf-clos1 5910
[Rosser] p. 246Theorem IX.5.13clos1base 5915
[Rosser] p. 246Theorem IX.5.14clos1conn 5916
[Rosser] p. 247Theorem IX.5.15clos1induct 5917
[Rosser] p. 248Theorem IX.5.16clos1basesuc 5919  clos1basesucg 5921
[Rosser] p. 252Definitiondf-pw1 4137
[Rosser] p. 255Theorem IX.6.14sspw1 4335
[Rosser] p. 275Definitiondf-addc 4378  df-nnc 4379
[Rosser] p. 275Theorem X.1.1eladdc 4398
[Rosser] p. 275Theorem X.1.20cnsuc 4401
[Rosser] p. 276Theorem X.1.3dfnnc3 5922
[Rosser] p. 276Theorem X.1.4peano1 4402
[Rosser] p. 276Theorem X.1.5peano2 4403
[Rosser] p. 276Theorem X.1.6peano5 4409
[Rosser] p. 276Theorem X.1.7nnc0suc 4412
[Rosser] p. 276Theorem X.1.8addcid1 4405  addcid2 4407
[Rosser] p. 276Theorem X.1.9addccom 4406
[Rosser] p. 277Corollary 1addcass 4415
[Rosser] p. 277Theorem X.1.121cnnc 4408
[Rosser] p. 277Theorem X.1.13finds 4411  findsd 4410
[Rosser] p. 278Theorem X.1.14nncaddccl 4419
[Rosser] p. 279Theorem X.1.16elsuc 4413
[Rosser] p. 279Definition from Ex. X.1.4df-lefin 4440
[Rosser] p. 281Definitiondf-op 4567  df-proj1 4568  df-proj2 4569
[Rosser] p. 282Theorem X.2.2phi11 4595
[Rosser] p. 282Theorem X.2.30cnelphi 4596
[Rosser] p. 282Theorem X.2.4phi011 4598
[Rosser] p. 282Theorem X.2.7proj1op 4599
[Rosser] p. 283Theorem X.2.8proj2op 4600
[Rosser] p. 301Theorem X.4.29.Idmsi 5562
[Rosser] p. 302Theorem X.4.29.IIrnsi 5564
[Rosser] p. 303Theorem X.4.37clos1baseima 5920
[Rosser] p. 347Theorem XI.1.6nenpw1pw 6123
[Rosser] p. 348Theorem XI.1.10ensn 6095
[Rosser] p. 348Theorem XI.1.13enadj 6097
[Rosser] p. 350Theorem XI.1.14sbthlem1 6241  sbthlem2 6242
[Rosser] p. 353Theorem XI.1.15sbthlem3 6243
[Rosser] p. 357Theorem XI.1.22enmap2 6105
[Rosser] p. 357Theorem XI.1.23enmap1 6111
[Rosser] p. 360Theorem XI.1.28enprmap 6119  enprmapc 6120
[Rosser] p. 368Theorem XI.1.33enpw1 6099
[Rosser] p. 368Theorem XI.1.35enpw1pw 6112
[Rosser] p. 369Theorem XI.1.36enpw 6124
[Rosser] p. 371Definitiondf-nc 6138
[Rosser] p. 372Definitiondf-ncs 6135
[Rosser] p. 372Theorem XI.2.4ncpw1pwneg 6239
[Rosser] p. 372Theorem XI.2.7df0c2 6175
[Rosser] p. 373Theorem XI.2.70cnc 6176
[Rosser] p. 373Theorem XI.2.81cnc 6177  df1c3 6178  df1c3g 6179
[Rosser] p. 374Theorem XI.2.10ncaddccl 6182
[Rosser] p. 374Theorem XI.2.11nnssnc 6185
[Rosser] p. 375Definitiondf-lec 6136  df-ltc 6137
[Rosser] p. 375Theorem XI.2.12peano4nc 6188
[Rosser] p. 375Theorem XI.2.14lecidg 6234
[Rosser] p. 376Theorem XI.2.14nclecid 6235
[Rosser] p. 376Theorem XI.2.15le0nc 6238  lec0cg 6236
[Rosser] p. 376Theorem XI.2.16lecncvg 6237
[Rosser] p. 376Theorem XI.2.17ltcpw1pwg 6240
[Rosser] p. 376Theorem XI.2.19addlec 6246  addlecncs 6247
[Rosser] p. 376Theorem XI.2.20sbth 6244
[Rosser] p. 377Theorem XI.2.21ltlenlec 6245
[Rosser] p. 377Theorem XI.2.22dflec2 6248
[Rosser] p. 377Theorem XI.2.23leaddc1 6252  leaddc2 6253
[Rosser] p. 377Theorem XI.2.24nc0le1 6254  nc0suc 6255
[Rosser] p. 378Definitiondf-muc 6139
[Rosser] p. 378Theorem XI.2.27mucnc 6169
[Rosser] p. 378Theorem XI.2.28muccom 6172
[Rosser] p. 378Theorem XI.2.29mucass 6173
[Rosser] p. 379Theorem XI.2.30addcdir 6288
[Rosser] p. 379Theorem XI.2.31addcdi 6287
[Rosser] p. 379Theorem XI.2.32muc0 6180
[Rosser] p. 380Theorem XI.2.34muc0or 6289
[Rosser] p. 380Theorem XI.2.35lemuc1 6290
[Rosser] p. 381Definitiondf-ce 6143
[Rosser] p. 381Theorem XI.2.36ncslemuc 6292
[Rosser] p. 381Theorem XI.2.37ncvsq 6293  vvsqenvv 6294
[Rosser] p. 382Theorem XI.2.38elce 6213
[Rosser] p. 382Theorem XI.2.39cenc 6219
[Rosser] p. 382Theorem XI.2.42ce0nnul 6215
[Rosser] p. 383Theorem XI.2.43ce0addcnnul 6217
[Rosser] p. 383Theorem XI.2.44ce0nn 6218
[Rosser] p. 384Theorem XI.2.38ce0nulnc 6222
[Rosser] p. 384Theorem XI.2.47ce0nnulb 6220
[Rosser] p. 384Theorem XI.2.48ce0ncpw1 6223  cecl 6224  ceclb 6221
[Rosser] p. 385Theorem XI.2.49ce0 6228
[Rosser] p. 389Theorem XI.2.70ce2 6230
[Rosser] p. 390Theorem XI.2.71ce2lt 6258
[Rosser] p. 391Theorem XI.3.2addccan2nc 6302  lecadd2 6303
[Rosser] p. 391Theorem XI.3.3nclenn 6286
[Rosser] p. 412Theorem XI.3.24df-frec 6346
[Rosser] p. 525Theorem X.1.17nnsucelr 4428
[Rosser] p. 526Corollary 1addcnul1 4452
[Rosser] p. 526Theorem X.1.18nndisjeq 4429
[Rosser] p. 526Theorem X.1.19prepeano4 4451
[Rosser] p. 526Theorem X.1.20addcnnul 4453
[Rosser] p. 527Definitiondf-ltfin 4441  df-ncfin 4442
[Rosser] p. 527Theorem X.1.21ssfin 4471
[Rosser] p. 527Theorem X.1.22vfinnc 4472
[Rosser] p. 527Theorem X.1.23ncfinprop 4475
[Rosser] p. 527Theorem X.1.24ncfineleq 4478
[Rosser] p. 527Theorem X.1.25ncfinraise 4482
[Rosser] p. 527Theorem X.1.26ncfinlower 4484
[Rosser] p. 528Definitiondf-tfin 4443
[Rosser] p. 528Theorem X.1.27nnpw1ex 4485
[Rosser] p. 528Theorem X.1.28tfinnnul 4491  tfinprop 4490
[Rosser] p. 528Theorem X.1.29tfinnul 4492
[Rosser] p. 528Theorem X.1.30tfin11 4494
[Rosser] p. 528Theorem X.1.31tfinpw1 4495
[Rosser] p. 528Definition adapteddf-tc 6140
[Rosser] p. 529Definitiondf-evenfin 4444  df-oddfin 4445
[Rosser] p. 529Theorem X.1.31ncfintfin 4496
[Rosser] p. 529Theorem X.1.32tfindi 4497
[Rosser] p. 529Theorem X.1.33tfinlefin 4503  tfinltfin 4502
[Rosser] p. 529Theorem X.1.35evenoddnnnul 4515
[Rosser] p. 529Theorem X.1.36evenodddisj 4517
[Rosser] p. 529Theorem X.1.34(a)tfin1c 4500
[Rosser] p. 530Definitiondf-sfin 4446
[Rosser] p. 530Theorem X.1.37eventfin 4518
[Rosser] p. 530Theorem X.1.38oddtfin 4519
[Rosser] p. 530Theorem X.1.39nnadjoin 4521
[Rosser] p. 530Theorem X.1.40nnadjoinpw 4522
[Rosser] p. 530Theorem X.1.41nnpweq 4524
[Rosser] p. 530Theorem X.1.42sfin01 4529
[Rosser] p. 530Theorem X.1.43sfin112 4530
[Rosser] p. 531Theorem X.1.44sfindbl 4531
[Rosser] p. 532Theorem X.1.45sfintfin 4533
[Rosser] p. 532Theorem X.1.46tfinnn 4535
[Rosser] p. 532Theorem X.1.47sfinltfin 4536
[Rosser] p. 533Definitiondf-spfin 4447
[Rosser] p. 533Theorem X.1.48sfin111 4537
[Rosser] p. 534Theorem X.1.49ncvspfin 4539
[Rosser] p. 534Theorem X.1.50spfinsfincl 4540
[Rosser] p. 534Theorem X.1.51spfininduct 4541
[Rosser] p. 534Theorem X.1.53vfinspnn 4542
[Rosser] p. 534Theorem X.1.541cspfin 4544  1cvsfin 4543
[Rosser] p. 534Theorem X.1.55tncveqnc1fin 4545
[Rosser] p. 534Theorem X.1.56t1csfin1c 4546  vfintle 4547
[Rosser] p. 534Theorem X.1.57vfin1cltv 4548
[Rosser] p. 534Theorem X.1.58vfinncvntnn 4549  vfinncvntsp 4550
[Rosser] p. 534Theorem X.1.59vfinspss 4552
[Rosser] p. 536Theorem X.1.60vfinspclt 4553
[Rosser] p. 536Theorem X.1.61vfinspeqtncv 4554
[Rosser] p. 536Theorem X.1.62vfinncsp 4555
[Rosser] p. 536Theorem X.1.63vinf 4556
[Rosser] p. 536Theorem X.1.65nulnnn 4557
[Rosser] p. 537Theorem X.1.66peano4 4558
[Rosser], p. 417Definitiondf-fin 4380
[Sanford] p. 39Rule 3mtp-xor 1536
[Sanford] p. 39Rule 4mpto2 1534
[Sanford] p. 39Rule is sometimes called "detachment," since it detaches the minor premiseax-mp 8
[Sanford] p. 39Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms" mto 167
[Sanford] p. 40Rule 1mpto1 1533
[Schechter] p. 51Definition of antisymmetryintasym 5046
[Schechter] p. 51Definition of irreflexivityintirr 5047
[Schechter] p. 51Definition of symmetrycnvsym 5045
[Schechter] p. 51Definition of transitivitycotr 5044
[Specker] p. 972Theorem 2.4tc11 6265
[Specker] p. 973Theorem 3.4nnc3n3p1 6314  nnc3n3p2 6315  nnc3p1n3p2 6316  nncdiv3 6313
[Specker] p. 973Theorem 4.3ce2nc1 6231
[Specker] p. 973Theorem 4.4ce2ncpw11c 6232
[Specker] p. 973Theorem 4.5nchoicelem8 6332
[Specker] p. 973Theorem 4.8ce2le 6270
[Specker] p. 973Theorem 5.2tcnc1c 6264  tcncv 6263
[Specker] p. 973Theorem 5.5tlecg 6267
[Specker] p. 973Theorem 5.6letc 6268
[Specker] p. 973Theorem 5.8ce2t 6272
[Specker] p. 973Theorem 6.2nchoicelem3 6327
[Specker] p. 973Theorem 6.4nchoicelem4 6328
[Specker] p. 973Theorem 6.5nchoicelem5 6329
[Specker] p. 973Theorem 6.6nchoicelem6 6330
[Specker] p. 973Definition 6.1df-spac 6310
[Specker] p. 974Theorem 6.7nchoicelem7 6331
[Specker] p. 974Theorem 6.8nchoicelem9 6333
[Specker] p. 974Theorem 7.1nchoicelem12 6336
[Specker] p. 974Theorem 7.2nchoicelem17 6341
[Specker] p. 974Theorem 7.3nchoicelem19 6343
[Specker] p. 974Theorem 7.5nchoice 6344
[Stoll] p. 13Definition of symmetric differencesymdif1 3519
[Stoll] p. 16Exercise 4.40dif 3621  dif0 3620
[Stoll] p. 16Exercise 4.8difdifdir 3637
[Stoll] p. 17Theorem 5.1(5)undifv 3624
[Stoll] p. 19Theorem 5.2(13)undm 3512
[Stoll] p. 19Theorem 5.2(13')indm 3513
[Stoll] p. 20Remarkinvdif 3496
[Stoll] p. 43Definitionuniiun 4019
[Stoll] p. 44Definitionintiin 4020
[Stoll] p. 45Definitiondf-iin 3972
[Stoll] p. 45Definition indexed uniondf-iun 3971
[Stoll] p. 176Theorem 3.4(27)iman 413
[Stoll] p. 262Example 4.1symdif1 3519
[Suppes] p. 22Theorem 2eq0 3564
[Suppes] p. 22Theorem 4eqss 3287  eqssd 3289  eqssi 3288
[Suppes] p. 23Theorem 5ss0 3581  ss0b 3580
[Suppes] p. 23Theorem 6sstr 3280
[Suppes] p. 23Theorem 7pssirr 3369
[Suppes] p. 23Theorem 8pssn2lp 3370
[Suppes] p. 23Theorem 9psstr 3373
[Suppes] p. 23Theorem 10pssss 3364
[Suppes] p. 26Theorem 15inidm 3464
[Suppes] p. 26Theorem 16in0 3576
[Suppes] p. 27Theorem 23unidm 3407
[Suppes] p. 27Theorem 24un0 3575
[Suppes] p. 27Theorem 25ssun1 3426
[Suppes] p. 27Theorem 26ssequn1 3433
[Suppes] p. 27Theorem 27unss 3437
[Suppes] p. 27Theorem 28indir 3503
[Suppes] p. 27Theorem 29undir 3504
[Suppes] p. 28Theorem 32difid 3618  difidALT 3619
[Suppes] p. 29Theorem 33difin 3492
[Suppes] p. 29Theorem 34indif 3497
[Suppes] p. 29Theorem 35undif1 3625
[Suppes] p. 29Theorem 36difun2 3629
[Suppes] p. 29Theorem 37difin0 3623
[Suppes] p. 29Theorem 38disjdif 3622
[Suppes] p. 29Theorem 39difundi 3507
[Suppes] p. 29Theorem 40difindi 3509
[Suppes] p. 39Theorem 61uniss 3912
[Suppes] p. 41Theorem 70intsn 3962
[Suppes] p. 42Theorem 71intpr 3959  intprg 3960
[Suppes] p. 42Theorem 78intun 3958
[Suppes] p. 44Definition 15(a)dfiun2 4001  dfiun2g 3999
[Suppes] p. 44Definition 15(b)dfiin2 4002
[Suppes] p. 47Theorem 86elpw 3728  elpwg 3729
[Suppes] p. 47Theorem 87pwid 3735
[Suppes] p. 47Theorem 89pw0 4160
[Suppes] p. 48Theorem 90pwpw0 3855
[Suppes] p. 52Theorem 101xpss12 4854
[Suppes] p. 52Theorem 102xpindi 4878  xpindir 4879
[Suppes] p. 52Theorem 103xpundi 4819  xpundir 4820
[Suppes] p. 58Theorem 2relss 4839
[Suppes] p. 59Theorem 4eldm 4911  eldm2 4912
[Suppes] p. 60Theorem 6dmin 4926
[Suppes] p. 60Theorem 8rnun 5054
[Suppes] p. 60Theorem 9rnin 5055
[Suppes] p. 60Definition 4dfrn2 4915
[Suppes] p. 61Theorem 11brcnv 4905
[Suppes] p. 62Equation 5elcnv 4902  elcnv2 4903
[Suppes] p. 62Theorem 12relcnv 5042
[Suppes] p. 62Theorem 15cnvin 5053
[Suppes] p. 62Theorem 16cnvun 5051
[Suppes] p. 63Theorem 20co02 5122
[Suppes] p. 63Theorem 21dmcoss 4986
[Suppes] p. 64Theorem 26cnvco 4907
[Suppes] p. 64Theorem 27coass 5128
[Suppes] p. 65Theorem 31resundi 4996
[Suppes] p. 65Theorem 34elima 4747  elima2 4748  elima3 4749
[Suppes] p. 65Theorem 35imaundi 5057
[Suppes] p. 66Theorem 40dminss 5059
[Suppes] p. 66Theorem 41imainss 5060
[Suppes] p. 67Exercise 11cnvxp 5061
[Suppes] p. 81Definition 34dfec2 5985
[Suppes] p. 82Theorem 72elec 6001
[Suppes] p. 82Theorem 73erth 6005  erth2 6006
[Suppes] p. 83Theorem 74erdisj 6009
[Suppes] p. 89Theorem 96map0b 6061
[Suppes] p. 89Theorem 97map0 6062
[Suppes] p. 89Theorem 98mapsn 6063
[Suppes] p. 89Theorem 99mapss 6064
[Suppes] p. 92Theorem 4unen 6086
[Suppes] p. 98Exercise 4fundmen 6081  fundmeng 6082
[TakeutiZaring] p. 8Axiom 1ax-ext 2334
[TakeutiZaring] p. 13Definition 4.5df-cleq 2346
[TakeutiZaring] p. 13Proposition 4.6df-clel 2349
[TakeutiZaring] p. 13Proposition 4.9cvjust 2348
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2370
[TakeutiZaring] p. 14Definition 4.16df-oprab 5568
[TakeutiZaring] p. 14Proposition 4.14ru 3045
[TakeutiZaring] p. 15Exercise 1elpr 3751  elpr2 3752  elprg 3750
[TakeutiZaring] p. 15Exercise 2elsn 3748  elsnc 3756  elsnc2 3762  elsnc2g 3761  elsncg 3755
[TakeutiZaring] p. 15Exercise 4sneq 3744  sneqr 3872
[TakeutiZaring] p. 15Definition 5.1dfpr2 3749  dfsn2 3747
[TakeutiZaring] p. 16Definition 5.3dftp2 3772
[TakeutiZaring] p. 16Definition 5.5df-uni 3892
[TakeutiZaring] p. 16Proposition 5.7unipr 3905  uniprg 3906
[TakeutiZaring] p. 17Exercise 1eltp 3771
[TakeutiZaring] p. 17Exercise 5sstr2 3279
[TakeutiZaring] p. 17Exercise 6uncom 3408
[TakeutiZaring] p. 17Exercise 7incom 3448
[TakeutiZaring] p. 17Exercise 8unass 3420
[TakeutiZaring] p. 17Exercise 9inass 3465
[TakeutiZaring] p. 17Exercise 10indi 3501
[TakeutiZaring] p. 17Exercise 11undi 3502
[TakeutiZaring] p. 17Definition 5.9df-pss 3261  dfss2 3262
[TakeutiZaring] p. 17Definition 5.10df-pw 3724
[TakeutiZaring] p. 18Exercise 7unss2 3434
[TakeutiZaring] p. 18Exercise 9df-ss 3259  sseqin2 3474
[TakeutiZaring] p. 18Exercise 10ssid 3290
[TakeutiZaring] p. 18Exercise 12inss1 3475  inss2 3476
[TakeutiZaring] p. 18Exercise 13nss 3329
[TakeutiZaring] p. 18Exercise 15unieq 3900
[TakeutiZaring] p. 18Exercise 18sspwb 4118
[TakeutiZaring] p. 20Definitiondf-rab 2623
[TakeutiZaring] p. 20Definition 5.14dfnul2 3552
[TakeutiZaring] p. 20Proposition 5.15difid 3618  difidALT 3619
[TakeutiZaring] p. 20Proposition 5.17(1)n0 3559  n0f 3558  neq0 3560
[TakeutiZaring] p. 21Definition 5.20df-v 2861
[TakeutiZaring] p. 22Exercise 10ss 3579
[TakeutiZaring] p. 22Exercise 7ssdif0 3609
[TakeutiZaring] p. 22Exercise 11difdif 3392
[TakeutiZaring] p. 22Exercise 13undif3 3515
[TakeutiZaring] p. 22Exercise 14difss 3393
[TakeutiZaring] p. 22Exercise 15sscon 3400
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2619
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2620
[TakeutiZaring] p. 23Proposition 6.2xpex 5149  xpexg 5148
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4779
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5193
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5303  fun11 5196
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5155  svrelfun 5194
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4914
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4916
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4783
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5084  dfrel2 5080
[TakeutiZaring] p. 25Exercise 3xpss 4855
[TakeutiZaring] p. 25Exercise 5relun 4862
[TakeutiZaring] p. 25Exercise 6reluni 4868
[TakeutiZaring] p. 25Exercise 9inxp 4877
[TakeutiZaring] p. 25Exercise 12relres 5007
[TakeutiZaring] p. 25Exercise 13opelres 4965
[TakeutiZaring] p. 25Exercise 14dmres 5001
[TakeutiZaring] p. 25Exercise 15resss 5003
[TakeutiZaring] p. 25Exercise 17resabs1 5008
[TakeutiZaring] p. 25Exercise 18funres 5178
[TakeutiZaring] p. 25Exercise 24relco 5043
[TakeutiZaring] p. 25Exercise 29funco 5177
[TakeutiZaring] p. 25Exercise 30f1co 5304
[TakeutiZaring] p. 26Definition 6.10eu2 2229
[TakeutiZaring] p. 26Definition 6.11fv3 5382
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5136  cnvexg 5135
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5140  dmexg 5139
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5141  rnexg 5138
[TakeutiZaring] p. 27Corollary 6.13fvex 5380
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5385  tz6.12 5386  tz6.12c 5388
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5387  tz6.12i 5389
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4785
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4786
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4788  wfo 4773
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4787  wf1 4772
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4789  wf1o 4774
[TakeutiZaring] p. 28Exercise 4eqfnfv 5434  eqfnfv2 5433  eqfnfv2f 5437
[TakeutiZaring] p. 28Exercise 5fvco 5424
[TakeutiZaring] p. 29Definition 6.18df-br 4633
[TakeutiZaring] p. 30Definition 6.21eliniseg 5036  iniseg 5038
[TakeutiZaring] p. 30Definition 6.22df-eprel 4757
[TakeutiZaring] p. 32Definition 6.28df-iso 4791
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5531
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5532
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5536
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5537
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5538
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5540
[TakeutiZaring] p. 40Proposition 7.20elssuni 3919
[TakeutiZaring] p. 44Exercise 2int0 3940
[TakeutiZaring] p. 44Exercise 4intss1 3941
[TakeutiZaring] p. 44Definition 7.35df-int 3927
[TakeutiZaring] p. 53Proposition 7.532eu5 2288
[TakeutiZaring] p. 59Proposition 8.6iunss2 4011  uniss2 3922
[TakeutiZaring] p. 88Exercise 1en0 6080
[TakeutiZaring] p. 95Definition 10.42df-map 6038
[Tarski] p. 67Axiom B5ax-4 2135
[Tarski] p. 67Scheme B5sp 1747
[Tarski] p. 68Lemma 6equid 1676  equid1 2158  equid1ALT 2176
[Tarski] p. 69Lemma 7equcomi 1679
[Tarski] p. 70Lemma 14spim 1975  spime 1976  spimeh 1667
[Tarski] p. 70Lemma 16ax-11 1746  ax-11o 2141  ax11i 1647
[Tarski] p. 70Lemmas 16 and 17sb6 2099
[Tarski] p. 75Axiom B7ax9v 1655
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1616  ax17o 2157
[Tarski], p. 75Scheme B8 of system S2ax-13 1712  ax-14 1714  ax-8 1675
[WhiteheadRussell] p. 86Theorem *110.641p1e2c 6193
[WhiteheadRussell] p. 96Axiom *1.2pm1.2 499
[WhiteheadRussell] p. 96Axiom *1.3olc 373
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 375
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 508
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 814
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 160
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 108
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 76
[WhiteheadRussell] p. 100Theorem *2.05imim2 49
[WhiteheadRussell] p. 100Theorem *2.06imim1 70
[WhiteheadRussell] p. 101Theorem *2.1pm2.1 406
[WhiteheadRussell] p. 101Theorem *2.06barbara 2301  syl 15
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 385
[WhiteheadRussell] p. 101Theorem *2.08id 19  idALT 20
[WhiteheadRussell] p. 101Theorem *2.11exmid 404
[WhiteheadRussell] p. 101Theorem *2.12notnot1 114
[WhiteheadRussell] p. 101Theorem *2.13pm2.13 407
[WhiteheadRussell] p. 102Theorem *2.14notnot2 104
[WhiteheadRussell] p. 102Theorem *2.15con1 120
[WhiteheadRussell] p. 103Theorem *2.16con3 126  con3th 924
[WhiteheadRussell] p. 103Theorem *2.17ax-3 7
[WhiteheadRussell] p. 103Theorem *2.18pm2.18 102
[WhiteheadRussell] p. 104Theorem *2.2orc 374
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 555
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 100
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 101
[WhiteheadRussell] p. 104Theorem *2.25pm2.25 393
[WhiteheadRussell] p. 104Theorem *2.26pm2.26 853
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 35
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 511
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 512
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 816
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 817
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 815
[WhiteheadRussell] p. 105Definition *2.33df-3or 935
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 558
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 556
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 557
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 47
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 386
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 387
[WhiteheadRussell] p. 107Theorem *2.5pm2.5 144
[WhiteheadRussell] p. 107Theorem *2.6pm2.6 162
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 388
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 389
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 390
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 145
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 147
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 362
[WhiteheadRussell] p. 107Theorem *2.54pm2.54 363
[WhiteheadRussell] p. 107Theorem *2.55orel1 371
[WhiteheadRussell] p. 107Theorem *2.56orel2 372
[WhiteheadRussell] p. 107Theorem *2.61pm2.61 163
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 398
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 763
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 764
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 164
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 391  pm2.67 392
[WhiteheadRussell] p. 107Theorem *2.521pm2.521 146
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 397
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 823
[WhiteheadRussell] p. 108Theorem *2.68pm2.68 399
[WhiteheadRussell] p. 108Theorem *2.69looinv 174
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 818
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 819
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 822
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 821
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 824
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 825
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 71
[WhiteheadRussell] p. 108Theorem *2.85pm2.85 826
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 94
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 484
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 434  pm3.2im 137
[WhiteheadRussell] p. 111Theorem *3.11pm3.11 485
[WhiteheadRussell] p. 111Theorem *3.12pm3.12 486
[WhiteheadRussell] p. 111Theorem *3.13pm3.13 487
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 488
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 435
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 436
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 852
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 570
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 431
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 432
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 443  simplim 143
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 447  simprim 142
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 568
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 569
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 562
[WhiteheadRussell] p. 113Fact)pm3.45 807
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 544
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 542
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 543
[WhiteheadRussell] p. 113Theorem *3.44jao 498  pm3.44 497
[WhiteheadRussell] p. 113Theorem *3.47prth 554
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 832
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 806
[WhiteheadRussell] p. 116Theorem *4.1con34b 283
[WhiteheadRussell] p. 117Theorem *4.2biid 227
[WhiteheadRussell] p. 117Theorem *4.11notbi 286
[WhiteheadRussell] p. 117Theorem *4.12con2bi 318
[WhiteheadRussell] p. 117Theorem *4.13notnot 282
[WhiteheadRussell] p. 117Theorem *4.14pm4.14 561
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 564
[WhiteheadRussell] p. 117Theorem *4.21bicom 191
[WhiteheadRussell] p. 117Theorem *4.22biantr 897  bitr 689
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 624
[WhiteheadRussell] p. 117Theorem *4.25oridm 500  pm4.25 501
[WhiteheadRussell] p. 118Theorem *4.3ancom 437
[WhiteheadRussell] p. 118Theorem *4.4andi 837
[WhiteheadRussell] p. 118Theorem *4.31orcom 376
[WhiteheadRussell] p. 118Theorem *4.32anass 630
[WhiteheadRussell] p. 118Theorem *4.33orass 510
[WhiteheadRussell] p. 118Theorem *4.36anbi1 687
[WhiteheadRussell] p. 118Theorem *4.37orbi1 686
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 842
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 841
[WhiteheadRussell] p. 118Definition *4.34df-3an 936
[WhiteheadRussell] p. 119Theorem *4.41ordi 834
[WhiteheadRussell] p. 119Theorem *4.42pm4.42 926
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 893
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 560
[WhiteheadRussell] p. 119Theorem *4.45orabs 828  pm4.45 669  pm4.45im 545
[WhiteheadRussell] p. 120Theorem *4.5anor 475
[WhiteheadRussell] p. 120Theorem *4.6imor 401
[WhiteheadRussell] p. 120Theorem *4.7anclb 530
[WhiteheadRussell] p. 120Theorem *4.51ianor 474
[WhiteheadRussell] p. 120Theorem *4.52pm4.52 477
[WhiteheadRussell] p. 120Theorem *4.53pm4.53 478
[WhiteheadRussell] p. 120Theorem *4.54pm4.54 479
[WhiteheadRussell] p. 120Theorem *4.55pm4.55 480
[WhiteheadRussell] p. 120Theorem *4.56ioran 476  pm4.56 481
[WhiteheadRussell] p. 120Theorem *4.57oran 482  pm4.57 483
[WhiteheadRussell] p. 120Theorem *4.61pm4.61 415
[WhiteheadRussell] p. 120Theorem *4.62pm4.62 408
[WhiteheadRussell] p. 120Theorem *4.63pm4.63 410
[WhiteheadRussell] p. 120Theorem *4.64pm4.64 361
[WhiteheadRussell] p. 120Theorem *4.65pm4.65 416
[WhiteheadRussell] p. 120Theorem *4.66pm4.66 409
[WhiteheadRussell] p. 120Theorem *4.67pm4.67 417
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 611  pm4.71d 615  pm4.71i 613  pm4.71r 612  pm4.71rd 616  pm4.71ri 614
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 846
[WhiteheadRussell] p. 121Theorem *4.73iba 489
[WhiteheadRussell] p. 121Theorem *4.74biorf 394
[WhiteheadRussell] p. 121Theorem *4.76jcab 833  pm4.76 836
[WhiteheadRussell] p. 121Theorem *4.77jaob 758  pm4.77 762
[WhiteheadRussell] p. 121Theorem *4.78pm4.78 565
[WhiteheadRussell] p. 121Theorem *4.79pm4.79 566
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 354
[WhiteheadRussell] p. 122Theorem *4.81pm4.81 355
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 894
[WhiteheadRussell] p. 122Theorem *4.83pm4.83 895
[WhiteheadRussell] p. 122Theorem *4.84imbi1 313
[WhiteheadRussell] p. 122Theorem *4.85imbi2 314
[WhiteheadRussell] p. 122Theorem *4.86bibi1 317
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 350  impexp 433  pm4.87 567
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 830
[WhiteheadRussell] p. 123Theorem *5.11pm5.11 854
[WhiteheadRussell] p. 123Theorem *5.12pm5.12 855
[WhiteheadRussell] p. 123Theorem *5.13pm5.13 857
[WhiteheadRussell] p. 123Theorem *5.14pm5.14 856
[WhiteheadRussell] p. 124Theorem *5.15pm5.15 859
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 860
[WhiteheadRussell] p. 124Theorem *5.17pm5.17 858
[WhiteheadRussell] p. 124Theorem *5.18nbbn 347  pm5.18 345
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 349
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 831
[WhiteheadRussell] p. 124Theorem *5.22xor 861
[WhiteheadRussell] p. 124Theorem *5.23dfbi3 863
[WhiteheadRussell] p. 124Theorem *5.24pm5.24 864
[WhiteheadRussell] p. 124Theorem *5.25dfor2 400
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 692
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 351
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 326
[WhiteheadRussell] p. 125Theorem *5.6pm5.6 878
[WhiteheadRussell] p. 125Theorem *5.7pm5.7 900
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 571
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 617
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 848
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 869
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 849
[WhiteheadRussell] p. 125Theorem *5.41imdi 352  pm5.41 353
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 531
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 877
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 771
[WhiteheadRussell] p. 125Theorem *5.54pm5.54 870
[WhiteheadRussell] p. 125Theorem *5.55pm5.55 867
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 693
[WhiteheadRussell] p. 125Theorem *5.62pm5.62 889
[WhiteheadRussell] p. 125Theorem *5.63pm5.63 890
[WhiteheadRussell] p. 125Theorem *5.71pm5.71 902
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 330
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 235
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 903
[WhiteheadRussell] p. 147Theorem *10.2219.26 1593
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1615
[WhiteheadRussell] p. 159Theorem *11.07pm11.07 2115
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1738
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1610
[WhiteheadRussell] p. 164Theorem *11.52nalexn 1573
[WhiteheadRussell] p. 164Theorem *11.512exnexn 1580
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1893
[WhiteheadRussell] p. 175Definition *14.02df-eu 2208
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2588
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2589
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2979
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3098
[WhiteheadRussell] p. 190Theorem *14.22iota4 4357
[WhiteheadRussell] p. 191Theorem *14.23iota4an 4358
[WhiteheadRussell] p. 192Theorem *14.26eupick 2267  eupickbi 2270

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