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 5652
[Eisenberg] p. 125Definition 8.21df-map 6001
[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 5107  rnexg 5104
[Enderton] p. 41Exercise 8dmuni 4914  rnuni 5038
[Enderton] p. 42Definition of a functiondffun7 5133  dffun8 5134
[Enderton] p. 43Definition of function valuefunfv2 5376
[Enderton] p. 43Definition of single-rootedfuncnv 5156
[Enderton] p. 44Definition (d)dfima4 4952
[Enderton] p. 47Theorem 3Hfvco2 5382
[Enderton] p. 50Theorem 3K(a)imauni 5465
[Enderton] p. 52Definitiondf-map 6001
[Enderton] p. 53Exercise 21coass 5097
[Enderton] p. 53Exercise 27dmco 5089
[Enderton] p. 53Exercise 14(a)funin 5163
[Enderton] p. 53Exercise 22(a)imass2 5024
[Enderton] p. 56Theorem 3Merref 5959
[Enderton] p. 57Lemma 3Nerthi 5970
[Enderton] p. 57Definitiondf-ec 5947
[Enderton] p. 58Definitiondf-qs 5951
[Enderton] p. 61Exercise 35df-ec 5947
[Enderton] p. 65Exercise 56(a)dmun 4912
[Enderton] p. 79Definition of operation valuedf-ov 5526
[Enderton] p. 129Definitiondf-en 6029
[Enderton] p. 144Corollary 6Kundif2 3626
[Enderton] p. 145Figure 38ffoss 5314
[Gleason] p. 119Proposition 9-2.4caovmo 5645
[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 6
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 5
[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 5736
[Holmes] p. 134Definitiondf-scan 6326
[Holmes], p. 134Observationscancan 6331
[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 6011  mapvalg 6009
[Kunen] p. 31Definition 10.24mapex 6006  mapexi 6003
[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 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3ax-3 8
[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(t)ssdmrn 5099
[Mendelson] p. 254Proposition 4.22(b)xpen 6055
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6049  xpsneng 6050
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6052  xpcomeng 6053
[Mendelson] p. 254Proposition 4.22(e)xpassen 6057
[Mendelson] p. 255Exercise 4.39endisj 6051
[Mendelson] p. 255Exercise 4.41mapprc 6004
[Mendelson] p. 287Axiom system MKru 3045
[Monk1] p. 26Theorem 2.8(vii)ssin 3477
[Monk1] p. 33Theorem 3.2(i)ssrel 4844
[Monk1] p. 33Theorem 3.2(ii)eqrel 4845
[Monk1] p. 34Definition 3.3df-opab 4623
[Monk1] p. 36Theorem 3.7(i)coi1 5094  coi2 5095
[Monk1] p. 36Theorem 3.8(v)dm0 4918  rn0 4969
[Monk1] p. 36Theorem 3.7(ii)cnvi 5032
[Monk1] p. 37Theorem 3.13(x)dmxp 4923  rnxp 5051
[Monk1] p. 37Theorem 3.13(ii)xp0 5044  xp0r 4842
[Monk1] p. 38Theorem 3.16(ii)ima0 5013
[Monk1] p. 38Theorem 3.16(viii)imai 5010
[Monk1] p. 39Theorem 3.16(xi)imassrn 5009
[Monk1] p. 41Theorem 4.3(i)fnopfv 5412  funfvop 5400
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5361
[Monk1] p. 42Theorem 4.4(iii)fvelima 5369
[Monk1] p. 43Theorem 4.6funun 5146
[Monk1] p. 43Theorem 4.8(iv)dff13 5471  dff13f 5472
[Monk1] p. 50Definition 5.4fniunfv 5466
[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 4606
[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 4695  opelopab 4708  opelopaba 4703  opelopabaf 4710  opelopabf 4711  opelopabg 4705  opelopabga 4700  oprabid 5550
[Quine] p. 64Definition 9.11df-xp 4784
[Quine] p. 64Definition 9.12df-cnv 4785
[Quine] p. 64Definition 9.15df-id 4767
[Quine] p. 65Theorem 10.3fun0 5154
[Quine] p. 65Theorem 10.4funi 5137
[Quine] p. 65Theorem 10.5funsn 5147
[Quine] p. 65Definition 10.1df-fun 4789
[Quine] p. 68Definition 10.11fv2 5324
[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 5873
[Rosser] p. 246Theorem IX.5.13clos1base 5878
[Rosser] p. 246Theorem IX.5.14clos1conn 5879
[Rosser] p. 247Theorem IX.5.15clos1induct 5880
[Rosser] p. 248Theorem IX.5.16clos1basesuc 5882  clos1basesucg 5884
[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 5885
[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 4566  df-proj1 4567  df-proj2 4568
[Rosser] p. 282Theorem X.2.2phi11 4596
[Rosser] p. 282Theorem X.2.30cnelphi 4597
[Rosser] p. 282Theorem X.2.4phi011 4599
[Rosser] p. 282Theorem X.2.7proj1op 4600
[Rosser] p. 283Theorem X.2.8proj2op 4601
[Rosser] p. 301Theorem X.4.29.Idmsi 5519
[Rosser] p. 302Theorem X.4.29.IIrnsi 5521
[Rosser] p. 303Theorem X.4.37clos1baseima 5883
[Rosser] p. 347Definitiondf-can 6324  df-can 6324
[Rosser] p. 347Theorem XI.1.6nenpw1pw 6086
[Rosser] p. 348Theorem XI.1.8vncan 6337
[Rosser] p. 348Theorem XI.1.10ensn 6058
[Rosser] p. 348Theorem XI.1.13enadj 6060
[Rosser] p. 350Theorem XI.1.14sbthlem1 6203  sbthlem2 6204
[Rosser] p. 353Theorem XI.1.15sbthlem3 6205
[Rosser] p. 357Theorem XI.1.22enmap2 6068
[Rosser] p. 357Theorem XI.1.23enmap1 6074
[Rosser] p. 360Theorem XI.1.28enprmap 6082  enprmapc 6083
[Rosser] p. 368Theorem XI.1.33enpw1 6062
[Rosser] p. 368Theorem XI.1.35enpw1pw 6075
[Rosser] p. 369Theorem XI.1.36enpw 6087
[Rosser] p. 371Definitiondf-nc 6101
[Rosser] p. 372Definitiondf-ncs 6098
[Rosser] p. 372Theorem XI.2.4ncpw1pwneg 6201
[Rosser] p. 372Theorem XI.2.7df0c2 6137
[Rosser] p. 373Theorem XI.2.70cnc 6138
[Rosser] p. 373Theorem XI.2.81cnc 6139  df1c3 6140  df1c3g 6141
[Rosser] p. 374Theorem XI.2.10ncaddccl 6144
[Rosser] p. 374Theorem XI.2.11nnssnc 6147
[Rosser] p. 375Definitiondf-lec 6099  df-ltc 6100
[Rosser] p. 375Theorem XI.2.12peano4nc 6150
[Rosser] p. 375Theorem XI.2.14lecidg 6196
[Rosser] p. 376Theorem XI.2.14nclecid 6197
[Rosser] p. 376Theorem XI.2.15le0nc 6200  lec0cg 6198
[Rosser] p. 376Theorem XI.2.16lecncvg 6199
[Rosser] p. 376Theorem XI.2.17ltcpw1pwg 6202
[Rosser] p. 376Theorem XI.2.19addlec 6208  addlecncs 6209
[Rosser] p. 376Theorem XI.2.20sbth 6206
[Rosser] p. 377Theorem XI.2.21ltlenlec 6207
[Rosser] p. 377Theorem XI.2.22dflec2 6210
[Rosser] p. 377Theorem XI.2.23leaddc1 6214  leaddc2 6215
[Rosser] p. 377Theorem XI.2.24nc0le1 6216  nc0suc 6217
[Rosser] p. 378Definitiondf-muc 6102
[Rosser] p. 378Theorem XI.2.27mucnc 6131
[Rosser] p. 378Theorem XI.2.28muccom 6134
[Rosser] p. 378Theorem XI.2.29mucass 6135
[Rosser] p. 379Theorem XI.2.30addcdir 6251
[Rosser] p. 379Theorem XI.2.31addcdi 6250
[Rosser] p. 379Theorem XI.2.32muc0 6142
[Rosser] p. 380Theorem XI.2.34muc0or 6252
[Rosser] p. 380Theorem XI.2.35lemuc1 6253
[Rosser] p. 381Definitiondf-ce 6106
[Rosser] p. 381Theorem XI.2.36ncslemuc 6255
[Rosser] p. 381Theorem XI.2.37ncvsq 6256  vvsqenvv 6257
[Rosser] p. 382Theorem XI.2.38elce 6175
[Rosser] p. 382Theorem XI.2.39cenc 6181
[Rosser] p. 382Theorem XI.2.42ce0nnul 6177
[Rosser] p. 383Theorem XI.2.43ce0addcnnul 6179
[Rosser] p. 383Theorem XI.2.44ce0nn 6180
[Rosser] p. 384Theorem XI.2.38ce0nulnc 6184
[Rosser] p. 384Theorem XI.2.47ce0nnulb 6182
[Rosser] p. 384Theorem XI.2.48ce0ncpw1 6185  cecl 6186  ceclb 6183
[Rosser] p. 385Theorem XI.2.49ce0 6190
[Rosser] p. 389Theorem XI.2.70ce2 6192
[Rosser] p. 390Theorem XI.2.71ce2lt 6220
[Rosser] p. 391Theorem XI.3.2addccan2nc 6265  lecadd2 6266
[Rosser] p. 391Theorem XI.3.3nclenn 6249
[Rosser] p. 412Theorem XI.3.24df-frec 6310
[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 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 4443
[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. 528Definition adapteddf-tc 6103
[Rosser] p. 529Definitiondf-evenfin 4444  df-oddfin 4445
[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 4446
[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 4447
[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. 39Remarkax-mp 5
[Sanford] p. 39Rule 3mtp-xor 1536
[Sanford] p. 39Rule 4mpto2 1534
[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 5028
[Schechter] p. 51Definition of irreflexivityintirr 5029
[Schechter] p. 51Definition of symmetrycnvsym 5027
[Schechter] p. 51Definition of transitivitycotr 5026
[Specker] p. 972Theorem 2.4tc11 6228
[Specker] p. 973Theorem 3.4nnc3n3p1 6278  nnc3n3p2 6279  nnc3p1n3p2 6280  nncdiv3 6277
[Specker] p. 973Theorem 4.3ce2nc1 6193
[Specker] p. 973Theorem 4.4ce2ncpw11c 6194
[Specker] p. 973Theorem 4.5nchoicelem8 6296
[Specker] p. 973Theorem 4.8ce2le 6233
[Specker] p. 973Theorem 5.2tcnc1c 6227  tcncv 6226
[Specker] p. 973Theorem 5.5tlecg 6230
[Specker] p. 973Theorem 5.6letc 6231
[Specker] p. 973Theorem 5.8ce2t 6235
[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 4855
[Suppes] p. 52Theorem 102xpindi 4864  xpindir 4865
[Suppes] p. 52Theorem 103xpundi 4832  xpundir 4833
[Suppes] p. 59Theorem 4eldm 4898  eldm2 4899
[Suppes] p. 60Theorem 6dmin 4913
[Suppes] p. 60Theorem 8rnun 5036
[Suppes] p. 60Theorem 9rnin 5037
[Suppes] p. 60Definition 4dfrn2 4902
[Suppes] p. 61Theorem 11brcnv 4892
[Suppes] p. 62Equation 5elcnv 4889  elcnv2 4890
[Suppes] p. 62Theorem 15cnvin 5035
[Suppes] p. 62Theorem 16cnvun 5033
[Suppes] p. 63Theorem 20co02 5092
[Suppes] p. 63Theorem 21dmcoss 4971
[Suppes] p. 64Theorem 26cnvco 4894
[Suppes] p. 64Theorem 27coass 5097
[Suppes] p. 65Theorem 31resundi 4981
[Suppes] p. 65Theorem 34elima 4754  elima2 4755  elima3 4756
[Suppes] p. 65Theorem 35imaundi 5039
[Suppes] p. 66Theorem 40dminss 5041
[Suppes] p. 66Theorem 41imainss 5042
[Suppes] p. 67Exercise 11cnvxp 5043
[Suppes] p. 81Definition 34dfec2 5948
[Suppes] p. 82Theorem 72elec 5964
[Suppes] p. 82Theorem 73erth 5968  erth2 5969
[Suppes] p. 83Theorem 74erdisj 5972
[Suppes] p. 89Theorem 96map0b 6024
[Suppes] p. 89Theorem 97map0 6025
[Suppes] p. 89Theorem 98mapsn 6026
[Suppes] p. 89Theorem 99mapss 6027
[Suppes] p. 92Theorem 4unen 6048
[Suppes] p. 98Exercise 4fundmen 6043  fundmeng 6044
[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 5528
[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 5115  xpexg 5114
[TakeutiZaring] p. 24Definition 6.4(3)f1funfun 5263  fun11 5159
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5121
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4901
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4903
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4788
[TakeutiZaring] p. 25Exercise 9inxp 4863
[TakeutiZaring] p. 25Exercise 13opelres 4950
[TakeutiZaring] p. 25Exercise 14dmres 4986
[TakeutiZaring] p. 25Exercise 15resss 4988
[TakeutiZaring] p. 25Exercise 17resabs1 4992
[TakeutiZaring] p. 25Exercise 18funres 5143
[TakeutiZaring] p. 25Exercise 29funco 5142
[TakeutiZaring] p. 25Exercise 30f1co 5264
[TakeutiZaring] p. 26Definition 6.10eu2 2229
[TakeutiZaring] p. 26Definition 6.11fv3 5341
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5102  cnvexg 5101
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 5106  dmexg 5105
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 5107  rnexg 5104
[TakeutiZaring] p. 27Corollary 6.13fvex 5339
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5344  tz6.12 5345  tz6.12c 5347
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5346  tz6.12i 5348
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4790
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4791
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4793  wfo 4779
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4792  wf1 4778
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4794  wf1o 4780
[TakeutiZaring] p. 28Exercise 4eqfnfv 5392  eqfnfv2 5393  eqfnfv2f 5396
[TakeutiZaring] p. 28Exercise 5fvco 5383
[TakeutiZaring] p. 29Definition 6.18df-br 4640
[TakeutiZaring] p. 30Definition 6.21eliniseg 5020  iniseg 5022
[TakeutiZaring] p. 30Definition 6.22df-eprel 4764
[TakeutiZaring] p. 32Definition 6.28df-iso 4796
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5490
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5491
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5495
[TakeutiZaring] p. 33Proposition 6.31(1)isomin 5496
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5497
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5499
[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 6042
[TakeutiZaring] p. 95Definition 10.42df-map 6001
[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 6155
[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 6
[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 8
[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 7
[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]