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 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 6021
[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 5140  rnexg 5137
[Enderton] p. 41Exercise 8dmuni 4926  rnuni 5055
[Enderton] p. 42Definition of a functiondffun7 5167  dffun8 5168
[Enderton] p. 43Definition of function valuefunfv2 5416
[Enderton] p. 43Definition of single-rootedfuncnv 5190
[Enderton] p. 44Definition (d)dfima4 4966
[Enderton] p. 47Theorem 3Hfvco2 5422
[Enderton] p. 50Theorem 3K(a)imauni 5505
[Enderton] p. 52Definitiondf-map 6021
[Enderton] p. 53Exercise 21coass 5127
[Enderton] p. 53Exercise 27dmco 5116
[Enderton] p. 53Exercise 14(a)funin 5199
[Enderton] p. 53Exercise 22(a)imass2 5039
[Enderton] p. 56Theorem 3Merref 5979
[Enderton] p. 57Lemma 3Nerthi 5990
[Enderton] p. 57Definitiondf-ec 5967
[Enderton] p. 58Definitiondf-qs 5971
[Enderton] p. 61Exercise 35df-ec 5967
[Enderton] p. 65Exercise 56(a)dmun 4924
[Enderton] p. 79Definition of operation valuedf-ov 5566
[Enderton] p. 129Definitiondf-en 6049
[Enderton] p. 144Corollary 6Kundif2 3626
[Enderton] p. 145Figure 38ffoss 5354
[Gleason] p. 119Proposition 9-2.4caovmo 5687
[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)id1 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 5787
[Jech] p. 4Definition of classcv 1641  cvjust 2348
[KalishMontague] p. 81Axiom B7' in footnote 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 6031  mapvalg 6029
[Kunen] p. 31Definition 10.24mapex 6026  mapexi 6023
[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 1id1 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.8id1 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 4872
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5129
[Mendelson] p. 254Proposition 4.22(b)xpen 6076
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6070  xpsneng 6071
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6073  xpcomeng 6074
[Mendelson] p. 254Proposition 4.22(e)xpassen 6077
[Mendelson] p. 255Exercise 4.39endisj 6072
[Mendelson] p. 255Exercise 4.41mapprc 6024
[Mendelson] p. 287Axiom system MKru 3045
[Monk1] p. 26Theorem 2.8(vii)ssin 3477
[Monk1] p. 33Theorem 3.2(i)ssrel 4839
[Monk1] p. 33Theorem 3.2(ii)eqrel 4840
[Monk1] p. 34Definition 3.3df-opab 4615
[Monk1] p. 36Theorem 3.7(i)coi1 5123  coi2 5124
[Monk1] p. 36Theorem 3.8(v)dm0 4930  rn0 4983
[Monk1] p. 36Theorem 3.7(ii)cnvi 5049
[Monk1] p. 37Theorem 3.13(i)relxp 4855
[Monk1] p. 37Theorem 3.13(x)dmxp 4935  rnxp 5068
[Monk1] p. 37Theorem 3.13(ii)xp0 5061  xp0r 4833
[Monk1] p. 38Theorem 3.16(ii)ima0 5028
[Monk1] p. 38Theorem 3.16(viii)imai 5025
[Monk1] p. 39Theorem 3.16(xi)imassrn 5024
[Monk1] p. 41Theorem 4.3(i)fnopfv 5452  funfvop 5440
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5401
[Monk1] p. 42Theorem 4.4(iii)fvelima 5409
[Monk1] p. 43Theorem 4.6funun 5180
[Monk1] p. 43Theorem 4.8(iv)dff13 5511  dff13f 5512
[Monk1] p. 50Definition 5.4fniunfv 5506
[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 4604
[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 4687  opelopab 4700  opelopaba 4695  opelopabaf 4702  opelopabf 4703  opelopabg 4697  opelopabga 4692  oprabid 5589
[Quine] p. 64Definition 9.11df-xp 4777
[Quine] p. 64Definition 9.12df-cnv 4779
[Quine] p. 64Definition 9.15df-id 4759
[Quine] p. 65Theorem 10.3fun0 5187
[Quine] p. 65Theorem 10.4funi 5171
[Quine] p. 65Theorem 10.5funsn 5181  funsng 5182
[Quine] p. 65Definition 10.1df-fun 4783
[Quine] p. 68Definition 10.11fv2 5364
[Quine] p. 331Axiom system NFru 3045
[Rosser] p. Definitiondf-tc 6123
[Rosser] p. 236Theorem IX.4.21dfpss4 3888
[Rosser] p. 238Definition IX.9.10, df-symdif 3216
[Rosser] p. 245Definitiondf-clos1 5895
[Rosser] p. 246Theorem IX.5.13clos1base 5900
[Rosser] p. 246Theorem IX.5.14clos1conn 5901
[Rosser] p. 247Theorem IX.5.15clos1induct 5902
[Rosser] p. 248Theorem IX.5.16clos1basesuc 5904
[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 5906
[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 4411
[Rosser] p. 276Theorem X.1.8addcid1 4405  addcid2 4407
[Rosser] p. 276Theorem X.1.9addccom 4406
[Rosser] p. 277Corollary 1addcass 4414
[Rosser] p. 277Theorem X.1.121cnnc 4408
[Rosser] p. 277Theorem X.1.13finds 4410
[Rosser] p. 278Theorem X.1.14nncaddccl 4418
[Rosser] p. 279Theorem X.1.16elsuc 4412
[Rosser] p. 279Definition from Ex. X.1.4df-lefin 4439
[Rosser] p. 281Definitiondf-op 4566  df-proj1 4567  df-proj2 4568
[Rosser] p. 282Theorem X.2.2phi11 4594
[Rosser] p. 282Theorem X.2.30cnelphi 4595
[Rosser] p. 282Theorem X.2.4phi011 4597
[Rosser] p. 282Theorem X.2.7proj1op 4598
[Rosser] p. 283Theorem X.2.8proj2op 4599
[Rosser] p. 301Theorem X.4.29.Idmsi 5561
[Rosser] p. 302Theorem X.4.29.IIrnsi 5563
[Rosser] p. 303Theorem X.4.37clos1baseima 5905
[Rosser] p. 347Theorem XI.1.6nenpw1pw 6106
[Rosser] p. 350Theorem XI.1.14sbthlem1 6224  sbthlem2 6225
[Rosser] p. 353Theorem XI.1.15sbthlem3 6226
[Rosser] p. 357Theorem XI.1.22enmap2 6088
[Rosser] p. 357Theorem XI.1.23enmap1 6094
[Rosser] p. 368Theorem XI.1.33enpw1 6082
[Rosser] p. 368Theorem XI.1.35enpw1pw 6095
[Rosser] p. 369Theorem XI.1.36enpw 6107
[Rosser] p. 371Definitiondf-nc 6121
[Rosser] p. 372Definitiondf-ncs 6118
[Rosser] p. 372Theorem XI.2.4ncpw1pwneg 6222
[Rosser] p. 375Definitiondf-lec 6119  df-ltc 6120
[Rosser] p. 375Theorem XI.2.12peano4nc 6171
[Rosser] p. 375Theorem XI.2.14lecidg 6217
[Rosser] p. 376Theorem XI.2.14nclecid 6218
[Rosser] p. 376Theorem XI.2.15le0nc 6221  lec0cg 6219
[Rosser] p. 376Theorem XI.2.16lecncvg 6220
[Rosser] p. 376Theorem XI.2.17ltcpw1pwg 6223
[Rosser] p. 376Theorem XI.2.19addlec 6229  addlecncs 6230
[Rosser] p. 376Theorem XI.2.20sbth 6227
[Rosser] p. 377Theorem XI.2.21ltlenlec 6228
[Rosser] p. 377Theorem XI.2.22dflec2 6231
[Rosser] p. 377Theorem XI.2.23leaddc1 6235  leaddc2 6236
[Rosser] p. 377Theorem XI.2.24nc0le1 6237  nc0suc 6238
[Rosser] p. 378Definitiondf-muc 6122
[Rosser] p. 378Theorem XI.2.27mucnc 6152
[Rosser] p. 378Theorem XI.2.28muccom 6155
[Rosser] p. 378Theorem XI.2.29mucass 6156
[Rosser] p. 379Theorem XI.2.32muc0 6163
[Rosser] p. 381Definitiondf-ce 6126
[Rosser] p. 382Theorem XI.2.38elce 6196
[Rosser] p. 382Theorem XI.2.39cenc 6202
[Rosser] p. 382Theorem XI.2.42ce0nnul 6198
[Rosser] p. 383Theorem XI.2.43ce0addcnnul 6200
[Rosser] p. 383Theorem XI.2.44ce0nn 6201
[Rosser] p. 384Theorem XI.2.38ce0nulnc 6205
[Rosser] p. 384Theorem XI.2.47ce0nnulb 6203
[Rosser] p. 384Theorem XI.2.48ce0ncpw1 6206  cecl 6207  ceclb 6204
[Rosser] p. 385Theorem XI.2.49ce0 6211
[Rosser] p. 390Theorem XI.2.71ce2lt 6241
[Rosser] p. 391Theorem XI.3.3nclenn 6269
[Rosser] p. 525Theorem X.1.17nnsucelr 4427
[Rosser] p. 526Corollary 1addcnul1 4451
[Rosser] p. 526Theorem X.1.18nndisjeq 4428
[Rosser] p. 526Theorem X.1.19prepeano4 4450
[Rosser] p. 526Theorem X.1.20addcnnul 4452
[Rosser] p. 527Definitiondf-ltfin 4440  df-ncfin 4441
[Rosser] p. 527Theorem X.1.21ssfin 4470
[Rosser] p. 527Theorem X.1.22vfinnc 4471
[Rosser] p. 527Theorem X.1.23ncfinprop 4474
[Rosser] p. 527Theorem X.1.24ncfineleq 4477
[Rosser] p. 527Theorem X.1.25ncfinraise 4481
[Rosser] p. 527Theorem X.1.26ncfinlower 4483
[Rosser] p. 528Definitiondf-tfin 4442
[Rosser] p. 528Theorem X.1.27nnpw1ex 4484
[Rosser] p. 528Theorem X.1.28tfinnnul 4490  tfinprop 4489
[Rosser] p. 528Theorem X.1.29tfinnul 4491
[Rosser] p. 528Theorem X.1.30tfin11 4493
[Rosser] p. 528Theorem X.1.31tfinpw1 4494
[Rosser] p. 529Definitiondf-evenfin 4443  df-oddfin 4444
[Rosser] p. 529Theorem X.1.31ncfintfin 4495
[Rosser] p. 529Theorem X.1.32tfindi 4496
[Rosser] p. 529Theorem X.1.33tfinlefin 4502  tfinltfin 4501
[Rosser] p. 529Theorem X.1.35evenoddnnnul 4514
[Rosser] p. 529Theorem X.1.36evenodddisj 4516
[Rosser] p. 529Theorem X.1.34(a)tfin1c 4499
[Rosser] p. 530Definitiondf-sfin 4445
[Rosser] p. 530Theorem X.1.37eventfin 4517
[Rosser] p. 530Theorem X.1.38oddtfin 4518
[Rosser] p. 530Theorem X.1.39nnadjoin 4520
[Rosser] p. 530Theorem X.1.40nnadjoinpw 4521
[Rosser] p. 530Theorem X.1.41nnpweq 4523
[Rosser] p. 530Theorem X.1.42sfin01 4528
[Rosser] p. 530Theorem X.1.43sfin112 4529
[Rosser] p. 531Theorem X.1.44sfindbl 4530
[Rosser] p. 532Theorem X.1.45sfintfin 4532
[Rosser] p. 532Theorem X.1.46tfinnn 4534
[Rosser] p. 532Theorem X.1.47sfinltfin 4535
[Rosser] p. 533Definitiondf-spfin 4446
[Rosser] p. 533Theorem X.1.48sfin111 4536
[Rosser] p. 534Theorem X.1.49ncvspfin 4538
[Rosser] p. 534Theorem X.1.50spfinsfincl 4539
[Rosser] p. 534Theorem X.1.51spfininduct 4540
[Rosser] p. 534Theorem X.1.53vfinspnn 4541
[Rosser] p. 534Theorem X.1.541cspfin 4543  1cvsfin 4542
[Rosser] p. 534Theorem X.1.55tncveqnc1fin 4544
[Rosser] p. 534Theorem X.1.56t1csfin1c 4545  vfintle 4546
[Rosser] p. 534Theorem X.1.57vfin1cltv 4547
[Rosser] p. 534Theorem X.1.58vfinncvntnn 4548  vfinncvntsp 4549
[Rosser] p. 534Theorem X.1.59vfinspss 4551
[Rosser] p. 536Theorem X.1.60vfinspclt 4552
[Rosser] p. 536Theorem X.1.61vfinspeqtncv 4553
[Rosser] p. 536Theorem X.1.62vfinncsp 4554
[Rosser] p. 536Theorem X.1.63vinf 4555
[Rosser] p. 536Theorem X.1.65nulnnn 4556
[Rosser] p. 537Theorem X.1.66peano4 4557
[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 5045
[Schechter] p. 51Definition of irreflexivityintirr 5046
[Schechter] p. 51Definition of symmetrycnvsym 5044
[Schechter] p. 51Definition of transitivitycotr 5043
[Specker] p. 973Theorem 3.4nnc3n3p1 6278  nnc3n3p2 6279  nnc3p1n3p2 6280  nncdiv3 6277
[Specker] p. 973Theorem 4.5nchoicelem8 6296
[Specker] p. 973Theorem 6.2nchoicelem3 6291
[Specker] p. 973Theorem 6.4nchoicelem4 6292
[Specker] p. 973Theorem 6.5nchoicelem5 6293
[Specker] p. 973Theorem 6.6nchoicelem6 6294
[Specker] p. 973Definition 6.1df-spac 6274
[Specker] p. 974Theorem 6.7nchoicelem7 6295
[Specker] p. 974Theorem 6.8nchoicelem9 6297
[Specker] p. 974Theorem 7.1nchoicelem12 6300
[Specker] p. 974Theorem 7.2nchoicelem17 6305
[Specker] p. 974Theorem 7.3nchoicelem19 6307
[Specker] p. 974Theorem 7.5nchoice 6308
[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 4853
[Suppes] p. 52Theorem 102xpindi 4877  xpindir 4878
[Suppes] p. 52Theorem 103xpundi 4818  xpundir 4819
[Suppes] p. 58Theorem 2relss 4838
[Suppes] p. 59Theorem 4eldm 4910  eldm2 4911
[Suppes] p. 60Theorem 6dmin 4925
[Suppes] p. 60Theorem 8rnun 5053
[Suppes] p. 60Theorem 9rnin 5054
[Suppes] p. 60Definition 4dfrn2 4914
[Suppes] p. 61Theorem 11brcnv 4904
[Suppes] p. 62Equation 5elcnv 4901  elcnv2 4902
[Suppes] p. 62Theorem 12relcnv 5041
[Suppes] p. 62Theorem 15cnvin 5052
[Suppes] p. 62Theorem 16cnvun 5050
[Suppes] p. 63Theorem 20co02 5121
[Suppes] p. 63Theorem 21dmcoss 4985
[Suppes] p. 64Theorem 26cnvco 4906
[Suppes] p. 64Theorem 27coass 5127
[Suppes] p. 65Theorem 31resundi 4995
[Suppes] p. 65Theorem 34elima 4746  elima2 4747  elima3 4748
[Suppes] p. 65Theorem 35imaundi 5056
[Suppes] p. 66Theorem 40dminss 5058
[Suppes] p. 66Theorem 41imainss 5059
[Suppes] p. 67Exercise 11cnvxp 5060
[Suppes] p. 81Definition 34dfec2 5968
[Suppes] p. 82Theorem 72elec 5984
[Suppes] p. 82Theorem 73erth 5988  erth2 5989
[Suppes] p. 83Theorem 74erdisj 5992
[Suppes] p. 89Theorem 96map0b 6044
[Suppes] p. 89Theorem 97map0 6045
[Suppes] p. 89Theorem 98mapsn 6046
[Suppes] p. 89Theorem 99mapss 6047
[Suppes] p. 92Theorem 4unen 6069
[Suppes] p. 98Exercise 4fundmen 6064  fundmeng 6065
[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 5567
[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 5148  xpexg 5147
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4778
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5192
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5302  fun11 5195
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5154  svrelfun 5193
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4913
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4915
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4782
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5083  dfrel2 5079
[TakeutiZaring] p. 25Exercise 3xpss 4854
[TakeutiZaring] p. 25Exercise 5relun 4861
[TakeutiZaring] p. 25Exercise 6reluni 4867
[TakeutiZaring] p. 25Exercise 9inxp 4876
[TakeutiZaring] p. 25Exercise 12relres 5006
[TakeutiZaring] p. 25Exercise 13opelres 4964
[TakeutiZaring] p. 25Exercise 14dmres 5000
[TakeutiZaring] p. 25Exercise 15resss 5002
[TakeutiZaring] p. 25Exercise 17resabs1 5007
[TakeutiZaring] p. 25Exercise 18funres 5177
[TakeutiZaring] p. 25Exercise 24relco 5042
[TakeutiZaring] p. 25Exercise 29funco 5176
[TakeutiZaring] p. 25Exercise 30f1co 5303
[TakeutiZaring] p. 26Definition 6.10eu2 2229
[TakeutiZaring] p. 26Definition 6.11fv3 5381
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5135  cnvexg 5134
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5139  dmexg 5138
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5140  rnexg 5137
[TakeutiZaring] p. 27Corollary 6.13fvex 5379
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5384  tz6.12 5385  tz6.12c 5387
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5386  tz6.12i 5388
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4784
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4785
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4787  wfo 4772
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4786  wf1 4771
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4788  wf1o 4773
[TakeutiZaring] p. 28Exercise 4eqfnfv 5433  eqfnfv2 5432  eqfnfv2f 5436
[TakeutiZaring] p. 28Exercise 5fvco 5423
[TakeutiZaring] p. 29Definition 6.18df-br 4632
[TakeutiZaring] p. 30Definition 6.21eliniseg 5035  iniseg 5037
[TakeutiZaring] p. 30Definition 6.22df-eprel 4756
[TakeutiZaring] p. 32Definition 6.28df-iso 4790
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5530
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5531
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5535
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5536
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5537
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5539
[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 6063
[TakeutiZaring] p. 95Definition 10.42df-map 6021
[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. 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  id1 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. 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. 113Theorem *3.45 (Fact)pm3.45 807
[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]