![]() |
New Foundations Explorer Bibliographic Cross-References |
|
Mirrors > Home > NFE Home > Bibliographic Cross-References |
Bibliographic Reference | Description | Higher-Order Logic Explorer Page(s) |
---|---|---|
[BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
[BellMachover] p. 97 | Definition 10.1 | df-eu 2208 |
[BellMachover] p. 460 | Notation | df-mo 2209 |
[BellMachover] p. 460 | Definition | mo3 2235 |
[BellMachover] p. 461 | Axiom Ext | ax-ext 2334 |
[BellMachover] p. 462 | Theorem 1.1 | bm1.1 2338 |
[ChoquetDD] p. 2 | Definition of mapping | df-mpt 5652 |
[Eisenberg] p. 125 | Definition 8.21 | df-map 6001 |
[Enderton] p. 19 | Definition | df-tp 3743 |
[Enderton] p. 26 | Exercise 5 | unissb 3921 |
[Enderton] p. 30 | Theorem "Distributive laws" | iinin1 4037 iinin2 4036 iinun2 4032 iunin1 4031 iunin2 4030 |
[Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2 4035 iundif2 4033 |
[Enderton] p. 32 | Exercise 20 | unineq 3505 |
[Enderton] p. 33 | Exercise 23 | iinuni 4049 |
[Enderton] p. 33 | Exercise 25 | iununi 4050 |
[Enderton] p. 33 | Exercise 24(a) | iinpw 4054 |
[Enderton] p. 33 | Exercise 24(b) | iunpwss 4055 |
[Enderton] p. 38 | Exercise 6(a) | unipw 4117 |
[Enderton] p. 41 | Lemma 3D | rnex 5107 rnexg 5104 |
[Enderton] p. 41 | Exercise 8 | dmuni 4914 rnuni 5038 |
[Enderton] p. 42 | Definition of a function | dffun7 5133 dffun8 5134 |
[Enderton] p. 43 | Definition of function value | funfv2 5376 |
[Enderton] p. 43 | Definition of single-rooted | funcnv 5156 |
[Enderton] p. 44 | Definition (d) | dfima4 4952 |
[Enderton] p. 47 | Theorem 3H | fvco2 5382 |
[Enderton] p. 50 | Theorem 3K(a) | imauni 5465 |
[Enderton] p. 52 | Definition | df-map 6001 |
[Enderton] p. 53 | Exercise 21 | coass 5097 |
[Enderton] p. 53 | Exercise 27 | dmco 5089 |
[Enderton] p. 53 | Exercise 14(a) | funin 5163 |
[Enderton] p. 53 | Exercise 22(a) | imass2 5024 |
[Enderton] p. 56 | Theorem 3M | erref 5959 |
[Enderton] p. 57 | Lemma 3N | erthi 5970 |
[Enderton] p. 57 | Definition | df-ec 5947 |
[Enderton] p. 58 | Definition | df-qs 5951 |
[Enderton] p. 61 | Exercise 35 | df-ec 5947 |
[Enderton] p. 65 | Exercise 56(a) | dmun 4912 |
[Enderton] p. 79 | Definition of operation value | df-ov 5526 |
[Enderton] p. 129 | Definition | df-en 6029 |
[Enderton] p. 144 | Corollary 6K | undif2 3626 |
[Enderton] p. 145 | Figure 38 | ffoss 5314 |
[Gleason] p. 119 | Proposition 9-2.4 | caovmo 5645 |
[Hailperin] p. 6 | Axiom P1 | ax-nin 4078 df-nin 3211 |
[Hailperin] p. 10 | Axiom P2 | ax-si 4083 |
[Hailperin] p. 10 | Axiom P3 | ax-ins2 4084 |
[Hailperin] p. 10 | Axiom P4 | ax-ins3 4085 |
[Hailperin] p. 10 | Axiom P5 | ax-xp 4079 |
[Hailperin] p. 10 | Axiom P6 | ax-typlower 4086 |
[Hailperin] p. 10 | Axiom P7 | ax-cnv 4080 |
[Hailperin] p. 10 | Axiom P8 | ax-1c 4081 |
[Hailperin] p. 10 | Axiom P9 | ax-sset 4082 |
[Hamilton] p. 28 | Definition 2.1 | ax-1 5 |
[Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
[Hamilton] p. 73 | Rule 1 | ax-mp 8 |
[Hamilton] p. 74 | Rule 2 | ax-gen 1546 |
[Hitchcock] p. 5 | Rule A3 | mpto1 1533 |
[Hitchcock] p. 5 | Rule A4 | mpto2 1534 |
[Hitchcock] p. 5 | Rule A5 | mtp-xor 1536 |
[Holmes] p. 40 | Definition | df-txp 5736 |
[Holmes] p. 134 | Definition | df-scan 6326 |
[Holmes], p. 134 | Observation | scancan 6331 |
[Jech] p. 4 | Definition of class | cv 1641 cvjust 2348 |
[KalishMontague] p. 81 | Note 1 | ax-9 1654 |
[KalishMontague] p. 85 | Lemma 2 | equid 1676 |
[KalishMontague] p. 85 | Lemma 3 | equcomi 1679 |
[KalishMontague] p. 86 | Lemma 7 | cbvalivw 1674 cbvaliw 1673 |
[KalishMontague] p. 87 | Lemma 8 | spimvw 1669 spimw 1668 |
[KalishMontague] p. 87 | Lemma 9 | spfw 1691 spw 1694 |
[Kunen] p. 10 | Axiom 0 | a9e 1951 |
[Kunen] p. 24 | Definition 10.24 | mapval 6011 mapvalg 6009 |
[Kunen] p. 31 | Definition 10.24 | mapex 6006 mapexi 6003 |
[KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3979 |
[Levy] p. 338 | Axiom | df-clab 2340 df-clel 2349 df-cleq 2346 |
[Lopez-Astorga] p. 12 | Rule 1 | mpto1 1533 |
[Lopez-Astorga] p. 12 | Rule 2 | mpto2 1534 |
[Lopez-Astorga] p. 12 | Rule 3 | mtp-xor 1536 |
[Margaris] p. 40 | Rule C | exlimiv 1634 |
[Margaris] p. 49 | Axiom A1 | ax-1 5 |
[Margaris] p. 49 | Axiom A2 | ax-2 6 |
[Margaris] p. 49 | Axiom A3 | ax-3 7 |
[Margaris] p. 49 | Definition | df-an 360 df-ex 1542 df-or 359 dfbi2 609 |
[Margaris] p. 51 | Theorem 1 | idALT 20 |
[Margaris] p. 56 | Theorem 3 | syld 40 |
[Margaris] p. 60 | Theorem 8 | mth8 138 |
[Margaris] p. 89 | Theorem 19.2 | 19.2 1659 19.2g 1757 r19.2z 3639 |
[Margaris] p. 89 | Theorem 19.3 | 19.3 1785 19.3v 1665 rr19.3v 2980 |
[Margaris] p. 89 | Theorem 19.5 | alcom 1737 |
[Margaris] p. 89 | Theorem 19.6 | alex 1572 |
[Margaris] p. 89 | Theorem 19.7 | alnex 1543 |
[Margaris] p. 89 | Theorem 19.8 | 19.8a 1756 |
[Margaris] p. 89 | Theorem 19.9 | 19.9 1783 19.9h 1780 19.9v 1664 |
[Margaris] p. 89 | Theorem 19.11 | excom 1741 excomim 1742 |
[Margaris] p. 89 | Theorem 19.12 | 19.12 1847 r19.12 2727 |
[Margaris] p. 90 | Theorem 19.14 | exnal 1574 |
[Margaris] p. 90 | Theorem 19.15 | albi 1564 ralbi 2750 |
[Margaris] p. 90 | Theorem 19.16 | 19.16 1860 |
[Margaris] p. 90 | Theorem 19.17 | 19.17 1861 |
[Margaris] p. 90 | Theorem 19.18 | exbi 1581 |
[Margaris] p. 90 | Theorem 19.19 | 19.19 1862 |
[Margaris] p. 90 | Theorem 19.20 | alim 1558 alimd 1764 alimdh 1563 alimdv 1621 ralimdaa 2691 ralimdv 2693 ralimdva 2692 sbcimdv 3107 |
[Margaris] p. 90 | Theorem 19.21 | 19.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. 90 | Theorem 19.22 | 2alimdv 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. 90 | Theorem 19.23 | 19.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. 90 | Theorem 19.24 | 19.24 1662 |
[Margaris] p. 90 | Theorem 19.25 | 19.25 1603 |
[Margaris] p. 90 | Theorem 19.26 | 19.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. 90 | Theorem 19.27 | 19.27 1869 19.27v 1894 r19.27av 2752 r19.27z 3648 r19.27zv 3649 |
[Margaris] p. 90 | Theorem 19.28 | 19.28 1870 19.28v 1895 r19.28av 2753 r19.28z 3642 r19.28zv 3645 rr19.28v 2981 |
[Margaris] p. 90 | Theorem 19.29 | 19.29 1596 19.29r 1597 19.29r2 1598 19.29x 1599 r19.29 2754 r19.29r 2755 |
[Margaris] p. 90 | Theorem 19.30 | 19.30 1604 r19.30 2756 |
[Margaris] p. 90 | Theorem 19.31 | 19.31 1876 |
[Margaris] p. 90 | Theorem 19.32 | 19.32 1875 r19.32v 2757 |
[Margaris] p. 90 | Theorem 19.33 | 19.33 1607 19.33b 1608 |
[Margaris] p. 90 | Theorem 19.34 | 19.34 1663 |
[Margaris] p. 90 | Theorem 19.35 | 19.35 1600 19.35i 1601 19.35ri 1602 r19.35 2758 |
[Margaris] p. 90 | Theorem 19.36 | 19.36 1871 19.36aiv 1897 19.36i 1872 19.36v 1896 r19.36av 2759 r19.36zv 3650 |
[Margaris] p. 90 | Theorem 19.37 | 19.37 1873 19.37aiv 1900 19.37v 1899 r19.37 2760 r19.37av 2761 r19.37zv 3646 |
[Margaris] p. 90 | Theorem 19.38 | 19.38 1794 |
[Margaris] p. 90 | Theorem 19.39 | 19.39 1661 |
[Margaris] p. 90 | Theorem 19.40 | 19.40-2 1610 19.40 1609 r19.40 2762 |
[Margaris] p. 90 | Theorem 19.41 | 19.41 1879 19.41v 1901 19.41vv 1902 19.41vvv 1903 19.41vvvv 1904 r19.41 2763 r19.41v 2764 |
[Margaris] p. 90 | Theorem 19.42 | 19.42 1880 19.42v 1905 19.42vv 1907 19.42vvv 1908 r19.42v 2765 |
[Margaris] p. 90 | Theorem 19.43 | 19.43 1605 r19.43 2766 |
[Margaris] p. 90 | Theorem 19.44 | 19.44 1877 r19.44av 2767 |
[Margaris] p. 90 | Theorem 19.45 | 19.45 1878 r19.45av 2768 r19.45zv 3647 |
[Margaris] p. 110 | Exercise 2(b) | eu1 2225 |
[Megill] p. 444 | Axiom C5 | ax-17 1616 ax17o 2157 |
[Megill] p. 445 | Lemma L12 | aecom-o 2151 aecom 1946 ax-10 2140 |
[Megill] p. 446 | Lemma L17 | equtrr 1683 |
[Megill] p. 446 | Lemma L18 | ax9from9o 2148 |
[Megill] p. 446 | Lemma L19 | hbnae-o 2179 hbnae 1955 |
[Megill] p. 447 | Remark 9.1 | df-sb 1649 sbid 1922 |
[Megill] p. 448 | Remark 9.6 | ax15 2021 |
[Megill] p. 448 | Scheme C4' | ax-5o 2136 |
[Megill] p. 448 | Scheme C5' | ax-4 2135 sp 1747 |
[Megill] p. 448 | Scheme C6' | ax-7 1734 |
[Megill] p. 448 | Scheme C7' | ax-6o 2137 |
[Megill] p. 448 | Scheme C8' | ax-8 1675 |
[Megill] p. 448 | Scheme C9' | ax-12o 2142 |
[Megill] p. 448 | Scheme C10' | ax-9 1654 ax-9o 2138 |
[Megill] p. 448 | Scheme C11' | ax-10o 2139 |
[Megill] p. 448 | Scheme C12' | ax-13 1712 |
[Megill] p. 448 | Scheme C13' | ax-14 1714 |
[Megill] p. 448 | Scheme C14' | ax-15 2143 |
[Megill] p. 448 | Scheme C15' | ax-11o 2141 |
[Megill] p. 448 | Scheme C16' | ax-16 2144 |
[Megill] p. 448 | Theorem 9.4 | dral1-o 2154 dral1 1965 dral2-o 2181 dral2 1966 drex1 1967 drex2 1968 drsb1 2022 drsb2 2061 |
[Megill] p. 449 | Theorem 9.7 | sbcom2 2114 sbequ 2060 sbid2v 2123 |
[Megill] p. 450 | Example in Appendix | hba1-o 2149 hba1 1786 |
[Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
[Mendelson] p. 69 | Axiom 4 | rspsbc 3124 rspsbca 3125 stdpc4 2024 |
[Mendelson] p. 69 | Axiom 5 | ax-5o 2136 ra5 3130 stdpc5 1798 |
[Mendelson] p. 81 | Rule C | exlimiv 1634 |
[Mendelson] p. 95 | Axiom 6 | stdpc6 1687 |
[Mendelson] p. 95 | Axiom 7 | stdpc7 1917 |
[Mendelson] p. 225 | Axiom system NBG | ru 3045 |
[Mendelson] p. 231 | Exercise 4.10(k) | inv1 3577 |
[Mendelson] p. 231 | Exercise 4.10(l) | unv 3578 |
[Mendelson] p. 231 | Exercise 4.10(n) | dfin3 3494 |
[Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3551 |
[Mendelson] p. 231 | Exercise 4.10(q) | dfin4 3495 |
[Mendelson] p. 231 | Exercise 4.10(s) | ddif 3398 |
[Mendelson] p. 231 | Definition of union | dfun3 3493 |
[Mendelson] p. 235 | Exercise 4.12(d) | pwv 3886 |
[Mendelson] p. 235 | Exercise 4.12(n) | uniin 3911 |
[Mendelson] p. 235 | Exercise 4.12(t) | ssdmrn 5099 |
[Mendelson] p. 254 | Proposition 4.22(b) | xpen 6055 |
[Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6049 xpsneng 6050 |
[Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6052 xpcomeng 6053 |
[Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6057 |
[Mendelson] p. 255 | Exercise 4.39 | endisj 6051 |
[Mendelson] p. 255 | Exercise 4.41 | mapprc 6004 |
[Mendelson] p. 287 | Axiom system MK | ru 3045 |
[Monk1] p. 26 | Theorem 2.8(vii) | ssin 3477 |
[Monk1] p. 33 | Theorem 3.2(i) | ssrel 4844 |
[Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4845 |
[Monk1] p. 34 | Definition 3.3 | df-opab 4623 |
[Monk1] p. 36 | Theorem 3.7(i) | coi1 5094 coi2 5095 |
[Monk1] p. 36 | Theorem 3.8(v) | dm0 4918 rn0 4969 |
[Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5032 |
[Monk1] p. 37 | Theorem 3.13(x) | dmxp 4923 rnxp 5051 |
[Monk1] p. 37 | Theorem 3.13(ii) | xp0 5044 xp0r 4842 |
[Monk1] p. 38 | Theorem 3.16(ii) | ima0 5013 |
[Monk1] p. 38 | Theorem 3.16(viii) | imai 5010 |
[Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5009 |
[Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5412 funfvop 5400 |
[Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5361 |
[Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5369 |
[Monk1] p. 43 | Theorem 4.6 | funun 5146 |
[Monk1] p. 43 | Theorem 4.8(iv) | dff13 5471 dff13f 5472 |
[Monk1] p. 50 | Definition 5.4 | fniunfv 5466 |
[Monk1] p. 52 | Theorem 5.11(viii) | ssint 3942 |
[Monk2] p. 105 | Axiom C4 | ax-5 1557 |
[Monk2] p. 105 | Axiom C7 | ax-8 1675 |
[Monk2] p. 105 | Axiom C8 | ax-11 1746 ax-11o 2141 |
[Monk2] p. 105 | Axiom (C8) | ax11v 2096 |
[Monk2] p. 108 | Lemma 5 | ax-5o 2136 |
[Monk2] p. 109 | Lemma 12 | ax-7 1734 |
[Monk2] p. 109 | Lemma 15 | equvin 2001 equvini 1987 eqvinop 4606 |
[Monk2] p. 113 | Axiom C5-1 | ax-17 1616 ax17o 2157 |
[Monk2] p. 113 | Axiom C5-2 | ax-6 1729 |
[Monk2] p. 113 | Axiom C5-3 | ax-7 1734 |
[Monk2] p. 114 | Lemma 21 | sp 1747 |
[Monk2] p. 114 | Lemma 22 | ax5o 1749 hba1-o 2149 hba1 1786 |
[Monk2] p. 114 | Lemma 23 | nfia1 1856 |
[Monk2] p. 114 | Lemma 24 | nfa2 1855 nfra2 2668 |
[Pfenning] p. 17 | Definition NNC | notnotrd 105 |
[Quine] p. 16 | Definition 2.1 | df-clab 2340 rabid 2787 |
[Quine] p. 17 | Definition 2.1'' | dfsb7 2119 |
[Quine] p. 18 | Definition 2.7 | df-cleq 2346 |
[Quine] p. 19 | Definition 2.9 | df-v 2861 |
[Quine] p. 34 | Theorem 5.1 | abeq2 2458 |
[Quine] p. 35 | Theorem 5.2 | abid2 2470 abid2f 2514 |
[Quine] p. 40 | Theorem 6.1 | sb5 2100 |
[Quine] p. 40 | Theorem 6.2 | sb56 2098 sb6 2099 |
[Quine] p. 41 | Theorem 6.3 | df-clel 2349 |
[Quine] p. 41 | Theorem 6.4 | eqid 2353 |
[Quine] p. 41 | Theorem 6.5 | eqcom 2355 |
[Quine] p. 42 | Theorem 6.6 | df-sbc 3047 |
[Quine] p. 42 | Theorem 6.7 | dfsbcq 3048 dfsbcq2 3049 |
[Quine] p. 43 | Theorem 6.8 | vex 2862 |
[Quine] p. 43 | Theorem 6.9 | isset 2863 |
[Quine] p. 44 | Theorem 7.3 | spcgf 2934 spcgv 2939 spcimgf 2932 |
[Quine] p. 44 | Theorem 6.11 | spsbc 3058 spsbcd 3059 |
[Quine] p. 44 | Theorem 6.12 | elex 2867 |
[Quine] p. 44 | Theorem 6.13 | elab 2985 elabg 2986 elabgf 2983 |
[Quine] p. 44 | Theorem 6.14 | noel 3554 |
[Quine] p. 48 | Theorem 7.2 | snprc 3788 |
[Quine] p. 48 | Definition 7.1 | df-pr 3742 df-sn 3741 |
[Quine] p. 49 | Theorem 7.4 | snss 3838 snssg 3844 |
[Quine] p. 49 | Theorem 7.5 | prss 3861 prssg 3862 |
[Quine] p. 49 | Theorem 7.6 | prid1 3827 prid1g 3825 prid2 3828 prid2g 3826 snid 3760 snidg 3758 |
[Quine] p. 53 | Theorem 8.2 | unisn 3907 unisng 3908 |
[Quine] p. 53 | Theorem 8.3 | uniun 3910 |
[Quine] p. 54 | Theorem 8.6 | elssuni 3919 |
[Quine] p. 54 | Theorem 8.7 | uni0 3918 |
[Quine] p. 56 | Theorem 8.17 | uniabio 4349 |
[Quine] p. 56 | Definition 8.18 | dfiota2 4340 |
[Quine] p. 57 | Theorem 8.19 | iotaval 4350 |
[Quine] p. 57 | Theorem 8.22 | iotanul 4354 |
[Quine] p. 58 | Theorem 8.23 | iotaex 4356 |
[Quine] p. 61 | Theorem 9.5 | opabid 4695 opelopab 4708 opelopaba 4703 opelopabaf 4710 opelopabf 4711 opelopabg 4705 opelopabga 4700 oprabid 5550 |
[Quine] p. 64 | Definition 9.11 | df-xp 4784 |
[Quine] p. 64 | Definition 9.12 | df-cnv 4785 |
[Quine] p. 64 | Definition 9.15 | df-id 4767 |
[Quine] p. 65 | Theorem 10.3 | fun0 5154 |
[Quine] p. 65 | Theorem 10.4 | funi 5137 |
[Quine] p. 65 | Theorem 10.5 | funsn 5147 |
[Quine] p. 65 | Definition 10.1 | df-fun 4789 |
[Quine] p. 68 | Definition 10.11 | fv2 5324 |
[Quine] p. 331 | Axiom system NF | ru 3045 |
[Rosser] p. 236 | Theorem IX.4.21 | dfpss4 3888 |
[Rosser] p. 238 | Definition IX.9.10, | df-symdif 3216 |
[Rosser] p. 245 | Definition | df-clos1 5873 |
[Rosser] p. 246 | Theorem IX.5.13 | clos1base 5878 |
[Rosser] p. 246 | Theorem IX.5.14 | clos1conn 5879 |
[Rosser] p. 247 | Theorem IX.5.15 | clos1induct 5880 |
[Rosser] p. 248 | Theorem IX.5.16 | clos1basesuc 5882 clos1basesucg 5884 |
[Rosser] p. 252 | Definition | df-pw1 4137 |
[Rosser] p. 255 | Theorem IX.6.14 | sspw1 4335 |
[Rosser] p. 275 | Definition | df-addc 4378 df-nnc 4379 |
[Rosser] p. 275 | Theorem X.1.1 | eladdc 4398 |
[Rosser] p. 275 | Theorem X.1.2 | 0cnsuc 4401 |
[Rosser] p. 276 | Theorem X.1.3 | dfnnc3 5885 |
[Rosser] p. 276 | Theorem X.1.4 | peano1 4402 |
[Rosser] p. 276 | Theorem X.1.5 | peano2 4403 |
[Rosser] p. 276 | Theorem X.1.6 | peano5 4409 |
[Rosser] p. 276 | Theorem X.1.7 | nnc0suc 4412 |
[Rosser] p. 276 | Theorem X.1.8 | addcid1 4405 addcid2 4407 |
[Rosser] p. 276 | Theorem X.1.9 | addccom 4406 |
[Rosser] p. 277 | Corollary 1 | addcass 4415 |
[Rosser] p. 277 | Theorem X.1.12 | 1cnnc 4408 |
[Rosser] p. 277 | Theorem X.1.13 | finds 4411 findsd 4410 |
[Rosser] p. 278 | Theorem X.1.14 | nncaddccl 4419 |
[Rosser] p. 279 | Theorem X.1.16 | elsuc 4413 |
[Rosser] p. 279 | Definition from Ex. X.1.4 | df-lefin 4440 |
[Rosser] p. 281 | Definition | df-op 4566 df-proj1 4567 df-proj2 4568 |
[Rosser] p. 282 | Theorem X.2.2 | phi11 4596 |
[Rosser] p. 282 | Theorem X.2.3 | 0cnelphi 4597 |
[Rosser] p. 282 | Theorem X.2.4 | phi011 4599 |
[Rosser] p. 282 | Theorem X.2.7 | proj1op 4600 |
[Rosser] p. 283 | Theorem X.2.8 | proj2op 4601 |
[Rosser] p. 301 | Theorem X.4.29.I | dmsi 5519 |
[Rosser] p. 302 | Theorem X.4.29.II | rnsi 5521 |
[Rosser] p. 303 | Theorem X.4.37 | clos1baseima 5883 |
[Rosser] p. 347 | Definition | df-can 6324 df-can 6324 |
[Rosser] p. 347 | Theorem XI.1.6 | nenpw1pw 6086 |
[Rosser] p. 348 | Theorem XI.1.8 | vncan 6337 |
[Rosser] p. 348 | Theorem XI.1.10 | ensn 6058 |
[Rosser] p. 348 | Theorem XI.1.13 | enadj 6060 |
[Rosser] p. 350 | Theorem XI.1.14 | sbthlem1 6203 sbthlem2 6204 |
[Rosser] p. 353 | Theorem XI.1.15 | sbthlem3 6205 |
[Rosser] p. 357 | Theorem XI.1.22 | enmap2 6068 |
[Rosser] p. 357 | Theorem XI.1.23 | enmap1 6074 |
[Rosser] p. 360 | Theorem XI.1.28 | enprmap 6082 enprmapc 6083 |
[Rosser] p. 368 | Theorem XI.1.33 | enpw1 6062 |
[Rosser] p. 368 | Theorem XI.1.35 | enpw1pw 6075 |
[Rosser] p. 369 | Theorem XI.1.36 | enpw 6087 |
[Rosser] p. 371 | Definition | df-nc 6101 |
[Rosser] p. 372 | Definition | df-ncs 6098 |
[Rosser] p. 372 | Theorem XI.2.4 | ncpw1pwneg 6201 |
[Rosser] p. 372 | Theorem XI.2.7 | df0c2 6137 |
[Rosser] p. 373 | Theorem XI.2.7 | 0cnc 6138 |
[Rosser] p. 373 | Theorem XI.2.8 | 1cnc 6139 df1c3 6140 df1c3g 6141 |
[Rosser] p. 374 | Theorem XI.2.10 | ncaddccl 6144 |
[Rosser] p. 374 | Theorem XI.2.11 | nnssnc 6147 |
[Rosser] p. 375 | Definition | df-lec 6099 df-ltc 6100 |
[Rosser] p. 375 | Theorem XI.2.12 | peano4nc 6150 |
[Rosser] p. 375 | Theorem XI.2.14 | lecidg 6196 |
[Rosser] p. 376 | Theorem XI.2.14 | nclecid 6197 |
[Rosser] p. 376 | Theorem XI.2.15 | le0nc 6200 lec0cg 6198 |
[Rosser] p. 376 | Theorem XI.2.16 | lecncvg 6199 |
[Rosser] p. 376 | Theorem XI.2.17 | ltcpw1pwg 6202 |
[Rosser] p. 376 | Theorem XI.2.19 | addlec 6208 addlecncs 6209 |
[Rosser] p. 376 | Theorem XI.2.20 | sbth 6206 |
[Rosser] p. 377 | Theorem XI.2.21 | ltlenlec 6207 |
[Rosser] p. 377 | Theorem XI.2.22 | dflec2 6210 |
[Rosser] p. 377 | Theorem XI.2.23 | leaddc1 6214 leaddc2 6215 |
[Rosser] p. 377 | Theorem XI.2.24 | nc0le1 6216 nc0suc 6217 |
[Rosser] p. 378 | Definition | df-muc 6102 |
[Rosser] p. 378 | Theorem XI.2.27 | mucnc 6131 |
[Rosser] p. 378 | Theorem XI.2.28 | muccom 6134 |
[Rosser] p. 378 | Theorem XI.2.29 | mucass 6135 |
[Rosser] p. 379 | Theorem XI.2.30 | addcdir 6251 |
[Rosser] p. 379 | Theorem XI.2.31 | addcdi 6250 |
[Rosser] p. 379 | Theorem XI.2.32 | muc0 6142 |
[Rosser] p. 380 | Theorem XI.2.34 | muc0or 6252 |
[Rosser] p. 380 | Theorem XI.2.35 | lemuc1 6253 |
[Rosser] p. 381 | Definition | df-ce 6106 |
[Rosser] p. 381 | Theorem XI.2.36 | ncslemuc 6255 |
[Rosser] p. 381 | Theorem XI.2.37 | ncvsq 6256 vvsqenvv 6257 |
[Rosser] p. 382 | Theorem XI.2.38 | elce 6175 |
[Rosser] p. 382 | Theorem XI.2.39 | cenc 6181 |
[Rosser] p. 382 | Theorem XI.2.42 | ce0nnul 6177 |
[Rosser] p. 383 | Theorem XI.2.43 | ce0addcnnul 6179 |
[Rosser] p. 383 | Theorem XI.2.44 | ce0nn 6180 |
[Rosser] p. 384 | Theorem XI.2.38 | ce0nulnc 6184 |
[Rosser] p. 384 | Theorem XI.2.47 | ce0nnulb 6182 |
[Rosser] p. 384 | Theorem XI.2.48 | ce0ncpw1 6185 cecl 6186 ceclb 6183 |
[Rosser] p. 385 | Theorem XI.2.49 | ce0 6190 |
[Rosser] p. 389 | Theorem XI.2.70 | ce2 6192 |
[Rosser] p. 390 | Theorem XI.2.71 | ce2lt 6220 |
[Rosser] p. 391 | Theorem XI.3.2 | addccan2nc 6265 lecadd2 6266 |
[Rosser] p. 391 | Theorem XI.3.3 | nclenn 6249 |
[Rosser] p. 412 | Theorem XI.3.24 | df-frec 6310 |
[Rosser] p. 525 | Theorem X.1.17 | nnsucelr 4428 |
[Rosser] p. 526 | Corollary 1 | addcnul1 4452 |
[Rosser] p. 526 | Theorem X.1.18 | nndisjeq 4429 |
[Rosser] p. 526 | Theorem X.1.19 | prepeano4 4451 |
[Rosser] p. 526 | Theorem X.1.20 | addcnnul 4453 |
[Rosser] p. 527 | Definition | df-ltfin 4441 df-ncfin 4442 |
[Rosser] p. 527 | Theorem X.1.21 | ssfin 4470 |
[Rosser] p. 527 | Theorem X.1.22 | vfinnc 4471 |
[Rosser] p. 527 | Theorem X.1.23 | ncfinprop 4474 |
[Rosser] p. 527 | Theorem X.1.24 | ncfineleq 4477 |
[Rosser] p. 527 | Theorem X.1.25 | ncfinraise 4481 |
[Rosser] p. 527 | Theorem X.1.26 | ncfinlower 4483 |
[Rosser] p. 528 | Definition | df-tfin 4443 |
[Rosser] p. 528 | Theorem X.1.27 | nnpw1ex 4484 |
[Rosser] p. 528 | Theorem X.1.28 | tfinnnul 4490 tfinprop 4489 |
[Rosser] p. 528 | Theorem X.1.29 | tfinnul 4491 |
[Rosser] p. 528 | Theorem X.1.30 | tfin11 4493 |
[Rosser] p. 528 | Theorem X.1.31 | tfinpw1 4494 |
[Rosser] p. 528 | Definition adapted | df-tc 6103 |
[Rosser] p. 529 | Definition | df-evenfin 4444 df-oddfin 4445 |
[Rosser] p. 529 | Theorem X.1.31 | ncfintfin 4495 |
[Rosser] p. 529 | Theorem X.1.32 | tfindi 4496 |
[Rosser] p. 529 | Theorem X.1.33 | tfinlefin 4502 tfinltfin 4501 |
[Rosser] p. 529 | Theorem X.1.35 | evenoddnnnul 4514 |
[Rosser] p. 529 | Theorem X.1.36 | evenodddisj 4516 |
[Rosser] p. 529 | Theorem X.1.34(a) | tfin1c 4499 |
[Rosser] p. 530 | Definition | df-sfin 4446 |
[Rosser] p. 530 | Theorem X.1.37 | eventfin 4517 |
[Rosser] p. 530 | Theorem X.1.38 | oddtfin 4518 |
[Rosser] p. 530 | Theorem X.1.39 | nnadjoin 4520 |
[Rosser] p. 530 | Theorem X.1.40 | nnadjoinpw 4521 |
[Rosser] p. 530 | Theorem X.1.41 | nnpweq 4523 |
[Rosser] p. 530 | Theorem X.1.42 | sfin01 4528 |
[Rosser] p. 530 | Theorem X.1.43 | sfin112 4529 |
[Rosser] p. 531 | Theorem X.1.44 | sfindbl 4530 |
[Rosser] p. 532 | Theorem X.1.45 | sfintfin 4532 |
[Rosser] p. 532 | Theorem X.1.46 | tfinnn 4534 |
[Rosser] p. 532 | Theorem X.1.47 | sfinltfin 4535 |
[Rosser] p. 533 | Definition | df-spfin 4447 |
[Rosser] p. 533 | Theorem X.1.48 | sfin111 4536 |
[Rosser] p. 534 | Theorem X.1.49 | ncvspfin 4538 |
[Rosser] p. 534 | Theorem X.1.50 | spfinsfincl 4539 |
[Rosser] p. 534 | Theorem X.1.51 | spfininduct 4540 |
[Rosser] p. 534 | Theorem X.1.53 | vfinspnn 4541 |
[Rosser] p. 534 | Theorem X.1.54 | 1cspfin 4543 1cvsfin 4542 |
[Rosser] p. 534 | Theorem X.1.55 | tncveqnc1fin 4544 |
[Rosser] p. 534 | Theorem X.1.56 | t1csfin1c 4545 vfintle 4546 |
[Rosser] p. 534 | Theorem X.1.57 | vfin1cltv 4547 |
[Rosser] p. 534 | Theorem X.1.58 | vfinncvntnn 4548 vfinncvntsp 4549 |
[Rosser] p. 534 | Theorem X.1.59 | vfinspss 4551 |
[Rosser] p. 536 | Theorem X.1.60 | vfinspclt 4552 |
[Rosser] p. 536 | Theorem X.1.61 | vfinspeqtncv 4553 |
[Rosser] p. 536 | Theorem X.1.62 | vfinncsp 4554 |
[Rosser] p. 536 | Theorem X.1.63 | vinf 4555 |
[Rosser] p. 536 | Theorem X.1.65 | nulnnn 4556 |
[Rosser] p. 537 | Theorem X.1.66 | peano4 4557 |
[Rosser], p. 417 | Definition | df-fin 4380 |
[Sanford] p. 39 | Rule 3 | mtp-xor 1536 |
[Sanford] p. 39 | Rule 4 | mpto2 1534 |
[Sanford] p. 39 | Rule is sometimes called "detachment," since it detaches the minor premise | ax-mp 8 |
[Sanford] p. 39 | Rule 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. 40 | Rule 1 | mpto1 1533 |
[Schechter] p. 51 | Definition of antisymmetry | intasym 5028 |
[Schechter] p. 51 | Definition of irreflexivity | intirr 5029 |
[Schechter] p. 51 | Definition of symmetry | cnvsym 5027 |
[Schechter] p. 51 | Definition of transitivity | cotr 5026 |
[Specker] p. 972 | Theorem 2.4 | tc11 6228 |
[Specker] p. 973 | Theorem 3.4 | nnc3n3p1 6278 nnc3n3p2 6279 nnc3p1n3p2 6280 nncdiv3 6277 |
[Specker] p. 973 | Theorem 4.3 | ce2nc1 6193 |
[Specker] p. 973 | Theorem 4.4 | ce2ncpw11c 6194 |
[Specker] p. 973 | Theorem 4.5 | nchoicelem8 6296 |
[Specker] p. 973 | Theorem 4.8 | ce2le 6233 |
[Specker] p. 973 | Theorem 5.2 | tcnc1c 6227 tcncv 6226 |
[Specker] p. 973 | Theorem 5.5 | tlecg 6230 |
[Specker] p. 973 | Theorem 5.6 | letc 6231 |
[Specker] p. 973 | Theorem 5.8 | ce2t 6235 |
[Specker] p. 973 | Theorem 6.2 | nchoicelem3 6291 |
[Specker] p. 973 | Theorem 6.4 | nchoicelem4 6292 |
[Specker] p. 973 | Theorem 6.5 | nchoicelem5 6293 |
[Specker] p. 973 | Theorem 6.6 | nchoicelem6 6294 |
[Specker] p. 973 | Definition 6.1 | df-spac 6274 |
[Specker] p. 974 | Theorem 6.7 | nchoicelem7 6295 |
[Specker] p. 974 | Theorem 6.8 | nchoicelem9 6297 |
[Specker] p. 974 | Theorem 7.1 | nchoicelem12 6300 |
[Specker] p. 974 | Theorem 7.2 | nchoicelem17 6305 |
[Specker] p. 974 | Theorem 7.3 | nchoicelem19 6307 |
[Specker] p. 974 | Theorem 7.5 | nchoice 6308 |
[Stoll] p. 13 | Definition of symmetric difference | symdif1 3519 |
[Stoll] p. 16 | Exercise 4.4 | 0dif 3621 dif0 3620 |
[Stoll] p. 16 | Exercise 4.8 | difdifdir 3637 |
[Stoll] p. 17 | Theorem 5.1(5) | undifv 3624 |
[Stoll] p. 19 | Theorem 5.2(13) | undm 3512 |
[Stoll] p. 19 | Theorem 5.2(13') | indm 3513 |
[Stoll] p. 20 | Remark | invdif 3496 |
[Stoll] p. 43 | Definition | uniiun 4019 |
[Stoll] p. 44 | Definition | intiin 4020 |
[Stoll] p. 45 | Definition | df-iin 3972 |
[Stoll] p. 45 | Definition indexed union | df-iun 3971 |
[Stoll] p. 176 | Theorem 3.4(27) | iman 413 |
[Stoll] p. 262 | Example 4.1 | symdif1 3519 |
[Suppes] p. 22 | Theorem 2 | eq0 3564 |
[Suppes] p. 22 | Theorem 4 | eqss 3287 eqssd 3289 eqssi 3288 |
[Suppes] p. 23 | Theorem 5 | ss0 3581 ss0b 3580 |
[Suppes] p. 23 | Theorem 6 | sstr 3280 |
[Suppes] p. 23 | Theorem 7 | pssirr 3369 |
[Suppes] p. 23 | Theorem 8 | pssn2lp 3370 |
[Suppes] p. 23 | Theorem 9 | psstr 3373 |
[Suppes] p. 23 | Theorem 10 | pssss 3364 |
[Suppes] p. 26 | Theorem 15 | inidm 3464 |
[Suppes] p. 26 | Theorem 16 | in0 3576 |
[Suppes] p. 27 | Theorem 23 | unidm 3407 |
[Suppes] p. 27 | Theorem 24 | un0 3575 |
[Suppes] p. 27 | Theorem 25 | ssun1 3426 |
[Suppes] p. 27 | Theorem 26 | ssequn1 3433 |
[Suppes] p. 27 | Theorem 27 | unss 3437 |
[Suppes] p. 27 | Theorem 28 | indir 3503 |
[Suppes] p. 27 | Theorem 29 | undir 3504 |
[Suppes] p. 28 | Theorem 32 | difid 3618 difidALT 3619 |
[Suppes] p. 29 | Theorem 33 | difin 3492 |
[Suppes] p. 29 | Theorem 34 | indif 3497 |
[Suppes] p. 29 | Theorem 35 | undif1 3625 |
[Suppes] p. 29 | Theorem 36 | difun2 3629 |
[Suppes] p. 29 | Theorem 37 | difin0 3623 |
[Suppes] p. 29 | Theorem 38 | disjdif 3622 |
[Suppes] p. 29 | Theorem 39 | difundi 3507 |
[Suppes] p. 29 | Theorem 40 | difindi 3509 |
[Suppes] p. 39 | Theorem 61 | uniss 3912 |
[Suppes] p. 41 | Theorem 70 | intsn 3962 |
[Suppes] p. 42 | Theorem 71 | intpr 3959 intprg 3960 |
[Suppes] p. 42 | Theorem 78 | intun 3958 |
[Suppes] p. 44 | Definition 15(a) | dfiun2 4001 dfiun2g 3999 |
[Suppes] p. 44 | Definition 15(b) | dfiin2 4002 |
[Suppes] p. 47 | Theorem 86 | elpw 3728 elpwg 3729 |
[Suppes] p. 47 | Theorem 87 | pwid 3735 |
[Suppes] p. 47 | Theorem 89 | pw0 4160 |
[Suppes] p. 48 | Theorem 90 | pwpw0 3855 |
[Suppes] p. 52 | Theorem 101 | xpss12 4855 |
[Suppes] p. 52 | Theorem 102 | xpindi 4864 xpindir 4865 |
[Suppes] p. 52 | Theorem 103 | xpundi 4832 xpundir 4833 |
[Suppes] p. 59 | Theorem 4 | eldm 4898 eldm2 4899 |
[Suppes] p. 60 | Theorem 6 | dmin 4913 |
[Suppes] p. 60 | Theorem 8 | rnun 5036 |
[Suppes] p. 60 | Theorem 9 | rnin 5037 |
[Suppes] p. 60 | Definition 4 | dfrn2 4902 |
[Suppes] p. 61 | Theorem 11 | brcnv 4892 |
[Suppes] p. 62 | Equation 5 | elcnv 4889 elcnv2 4890 |
[Suppes] p. 62 | Theorem 15 | cnvin 5035 |
[Suppes] p. 62 | Theorem 16 | cnvun 5033 |
[Suppes] p. 63 | Theorem 20 | co02 5092 |
[Suppes] p. 63 | Theorem 21 | dmcoss 4971 |
[Suppes] p. 64 | Theorem 26 | cnvco 4894 |
[Suppes] p. 64 | Theorem 27 | coass 5097 |
[Suppes] p. 65 | Theorem 31 | resundi 4981 |
[Suppes] p. 65 | Theorem 34 | elima 4754 elima2 4755 elima3 4756 |
[Suppes] p. 65 | Theorem 35 | imaundi 5039 |
[Suppes] p. 66 | Theorem 40 | dminss 5041 |
[Suppes] p. 66 | Theorem 41 | imainss 5042 |
[Suppes] p. 67 | Exercise 11 | cnvxp 5043 |
[Suppes] p. 81 | Definition 34 | dfec2 5948 |
[Suppes] p. 82 | Theorem 72 | elec 5964 |
[Suppes] p. 82 | Theorem 73 | erth 5968 erth2 5969 |
[Suppes] p. 83 | Theorem 74 | erdisj 5972 |
[Suppes] p. 89 | Theorem 96 | map0b 6024 |
[Suppes] p. 89 | Theorem 97 | map0 6025 |
[Suppes] p. 89 | Theorem 98 | mapsn 6026 |
[Suppes] p. 89 | Theorem 99 | mapss 6027 |
[Suppes] p. 92 | Theorem 4 | unen 6048 |
[Suppes] p. 98 | Exercise 4 | fundmen 6043 fundmeng 6044 |
[TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2334 |
[TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2346 |
[TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2349 |
[TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2348 |
[TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2370 |
[TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5528 |
[TakeutiZaring] p. 14 | Proposition 4.14 | ru 3045 |
[TakeutiZaring] p. 15 | Exercise 1 | elpr 3751 elpr2 3752 elprg 3750 |
[TakeutiZaring] p. 15 | Exercise 2 | elsn 3748 elsnc 3756 elsnc2 3762 elsnc2g 3761 elsncg 3755 |
[TakeutiZaring] p. 15 | Exercise 4 | sneq 3744 sneqr 3872 |
[TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3749 dfsn2 3747 |
[TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3772 |
[TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3892 |
[TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3905 uniprg 3906 |
[TakeutiZaring] p. 17 | Exercise 1 | eltp 3771 |
[TakeutiZaring] p. 17 | Exercise 5 | sstr2 3279 |
[TakeutiZaring] p. 17 | Exercise 6 | uncom 3408 |
[TakeutiZaring] p. 17 | Exercise 7 | incom 3448 |
[TakeutiZaring] p. 17 | Exercise 8 | unass 3420 |
[TakeutiZaring] p. 17 | Exercise 9 | inass 3465 |
[TakeutiZaring] p. 17 | Exercise 10 | indi 3501 |
[TakeutiZaring] p. 17 | Exercise 11 | undi 3502 |
[TakeutiZaring] p. 17 | Definition 5.9 | df-pss 3261 dfss2 3262 |
[TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3724 |
[TakeutiZaring] p. 18 | Exercise 7 | unss2 3434 |
[TakeutiZaring] p. 18 | Exercise 9 | df-ss 3259 sseqin2 3474 |
[TakeutiZaring] p. 18 | Exercise 10 | ssid 3290 |
[TakeutiZaring] p. 18 | Exercise 12 | inss1 3475 inss2 3476 |
[TakeutiZaring] p. 18 | Exercise 13 | nss 3329 |
[TakeutiZaring] p. 18 | Exercise 15 | unieq 3900 |
[TakeutiZaring] p. 18 | Exercise 18 | sspwb 4118 |
[TakeutiZaring] p. 20 | Definition | df-rab 2623 |
[TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3552 |
[TakeutiZaring] p. 20 | Proposition 5.15 | difid 3618 difidALT 3619 |
[TakeutiZaring] p. 20 | Proposition 5.17(1) | n0 3559 n0f 3558 neq0 3560 |
[TakeutiZaring] p. 21 | Definition 5.20 | df-v 2861 |
[TakeutiZaring] p. 22 | Exercise 1 | 0ss 3579 |
[TakeutiZaring] p. 22 | Exercise 7 | ssdif0 3609 |
[TakeutiZaring] p. 22 | Exercise 11 | difdif 3392 |
[TakeutiZaring] p. 22 | Exercise 13 | undif3 3515 |
[TakeutiZaring] p. 22 | Exercise 14 | difss 3393 |
[TakeutiZaring] p. 22 | Exercise 15 | sscon 3400 |
[TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2619 |
[TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2620 |
[TakeutiZaring] p. 23 | Proposition 6.2 | xpex 5115 xpexg 5114 |
[TakeutiZaring] p. 24 | Definition 6.4(3) | f1funfun 5263 fun11 5159 |
[TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5121 |
[TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4901 |
[TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4903 |
[TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4788 |
[TakeutiZaring] p. 25 | Exercise 9 | inxp 4863 |
[TakeutiZaring] p. 25 | Exercise 13 | opelres 4950 |
[TakeutiZaring] p. 25 | Exercise 14 | dmres 4986 |
[TakeutiZaring] p. 25 | Exercise 15 | resss 4988 |
[TakeutiZaring] p. 25 | Exercise 17 | resabs1 4992 |
[TakeutiZaring] p. 25 | Exercise 18 | funres 5143 |
[TakeutiZaring] p. 25 | Exercise 29 | funco 5142 |
[TakeutiZaring] p. 25 | Exercise 30 | f1co 5264 |
[TakeutiZaring] p. 26 | Definition 6.10 | eu2 2229 |
[TakeutiZaring] p. 26 | Definition 6.11 | fv3 5341 |
[TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5102 cnvexg 5101 |
[TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5106 dmexg 5105 |
[TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5107 rnexg 5104 |
[TakeutiZaring] p. 27 | Corollary 6.13 | fvex 5339 |
[TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5344 tz6.12 5345 tz6.12c 5347 |
[TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5346 tz6.12i 5348 |
[TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 4790 |
[TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 4791 |
[TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 4793 wfo 4779 |
[TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 4792 wf1 4778 |
[TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 4794 wf1o 4780 |
[TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5392 eqfnfv2 5393 eqfnfv2f 5396 |
[TakeutiZaring] p. 28 | Exercise 5 | fvco 5383 |
[TakeutiZaring] p. 29 | Definition 6.18 | df-br 4640 |
[TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5020 iniseg 5022 |
[TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4764 |
[TakeutiZaring] p. 32 | Definition 6.28 | df-iso 4796 |
[TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5490 |
[TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5491 |
[TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5495 |
[TakeutiZaring] p. 33 | Proposition 6.31(1) | isomin 5496 |
[TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5497 |
[TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5499 |
[TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3919 |
[TakeutiZaring] p. 44 | Exercise 2 | int0 3940 |
[TakeutiZaring] p. 44 | Exercise 4 | intss1 3941 |
[TakeutiZaring] p. 44 | Definition 7.35 | df-int 3927 |
[TakeutiZaring] p. 53 | Proposition 7.53 | 2eu5 2288 |
[TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4011 uniss2 3922 |
[TakeutiZaring] p. 88 | Exercise 1 | en0 6042 |
[TakeutiZaring] p. 95 | Definition 10.42 | df-map 6001 |
[Tarski] p. 67 | Axiom B5 | ax-4 2135 |
[Tarski] p. 67 | Scheme B5 | sp 1747 |
[Tarski] p. 68 | Lemma 6 | equid 1676 equid1 2158 equid1ALT 2176 |
[Tarski] p. 69 | Lemma 7 | equcomi 1679 |
[Tarski] p. 70 | Lemma 14 | spim 1975 spime 1976 spimeh 1667 |
[Tarski] p. 70 | Lemma 16 | ax-11 1746 ax-11o 2141 ax11i 1647 |
[Tarski] p. 70 | Lemmas 16 and 17 | sb6 2099 |
[Tarski] p. 75 | Axiom B7 | ax9v 1655 |
[Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1616 ax17o 2157 |
[Tarski], p. 75 | Scheme B8 of system S2 | ax-13 1712 ax-14 1714 ax-8 1675 |
[WhiteheadRussell] p. 86 | Theorem *110.64 | 1p1e2c 6155 |
[WhiteheadRussell] p. 96 | Axiom *1.2 | pm1.2 499 |
[WhiteheadRussell] p. 96 | Axiom *1.3 | olc 373 |
[WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 375 |
[WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 508 |
[WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 814 |
[WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 160 |
[WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 5 |
[WhiteheadRussell] p. 100 | Theorem *2.03 | con2 108 |
[WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 76 |
[WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 49 |
[WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 70 |
[WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1 406 |
[WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2301 syl 15 |
[WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 385 |
[WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
[WhiteheadRussell] p. 101 | Theorem *2.11 | exmid 404 |
[WhiteheadRussell] p. 101 | Theorem *2.12 | notnot1 114 |
[WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13 407 |
[WhiteheadRussell] p. 102 | Theorem *2.14 | notnot2 104 |
[WhiteheadRussell] p. 102 | Theorem *2.15 | con1 120 |
[WhiteheadRussell] p. 103 | Theorem *2.16 | con3 126 con3th 924 |
[WhiteheadRussell] p. 103 | Theorem *2.17 | ax-3 7 |
[WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18 102 |
[WhiteheadRussell] p. 104 | Theorem *2.2 | orc 374 |
[WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 555 |
[WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 100 |
[WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 101 |
[WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25 393 |
[WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26 853 |
[WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 35 |
[WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 511 |
[WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 512 |
[WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 816 |
[WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 817 |
[WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 815 |
[WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 935 |
[WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 558 |
[WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 556 |
[WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 557 |
[WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 47 |
[WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 386 |
[WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 387 |
[WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5 144 |
[WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6 162 |
[WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 388 |
[WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 389 |
[WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 390 |
[WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 145 |
[WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 147 |
[WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 362 |
[WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54 363 |
[WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 371 |
[WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 372 |
[WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61 163 |
[WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 398 |
[WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 763 |
[WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 764 |
[WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 164 |
[WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 391 pm2.67 392 |
[WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521 146 |
[WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 397 |
[WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 823 |
[WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68 399 |
[WhiteheadRussell] p. 108 | Theorem *2.69 | looinv 174 |
[WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 818 |
[WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 819 |
[WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 822 |
[WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 821 |
[WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 6 |
[WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 824 |
[WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 825 |
[WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 71 |
[WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85 826 |
[WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 94 |
[WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 484 |
[WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 434 pm3.2im 137 |
[WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11 485 |
[WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12 486 |
[WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13 487 |
[WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 488 |
[WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 435 |
[WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 436 |
[WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 852 |
[WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 570 |
[WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 431 |
[WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 432 |
[WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 443 simplim 143 |
[WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 447 simprim 142 |
[WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 568 |
[WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 569 |
[WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 562 |
[WhiteheadRussell] p. 113 | Fact) | pm3.45 807 |
[WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 544 |
[WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 542 |
[WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 543 |
[WhiteheadRussell] p. 113 | Theorem *3.44 | jao 498 pm3.44 497 |
[WhiteheadRussell] p. 113 | Theorem *3.47 | prth 554 |
[WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 832 |
[WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 806 |
[WhiteheadRussell] p. 116 | Theorem *4.1 | con34b 283 |
[WhiteheadRussell] p. 117 | Theorem *4.2 | biid 227 |
[WhiteheadRussell] p. 117 | Theorem *4.11 | notbi 286 |
[WhiteheadRussell] p. 117 | Theorem *4.12 | con2bi 318 |
[WhiteheadRussell] p. 117 | Theorem *4.13 | notnot 282 |
[WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14 561 |
[WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 564 |
[WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 191 |
[WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 897 bitr 689 |
[WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 624 |
[WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 500 pm4.25 501 |
[WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 437 |
[WhiteheadRussell] p. 118 | Theorem *4.4 | andi 837 |
[WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 376 |
[WhiteheadRussell] p. 118 | Theorem *4.32 | anass 630 |
[WhiteheadRussell] p. 118 | Theorem *4.33 | orass 510 |
[WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 687 |
[WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 686 |
[WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 842 |
[WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 841 |
[WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 936 |
[WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 834 |
[WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42 926 |
[WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 893 |
[WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 560 |
[WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 828 pm4.45 669 pm4.45im 545 |
[WhiteheadRussell] p. 120 | Theorem *4.5 | anor 475 |
[WhiteheadRussell] p. 120 | Theorem *4.6 | imor 401 |
[WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 530 |
[WhiteheadRussell] p. 120 | Theorem *4.51 | ianor 474 |
[WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52 477 |
[WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53 478 |
[WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54 479 |
[WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55 480 |
[WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 476 pm4.56 481 |
[WhiteheadRussell] p. 120 | Theorem *4.57 | oran 482 pm4.57 483 |
[WhiteheadRussell] p. 120 | Theorem *4.61 | pm4.61 415 |
[WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62 408 |
[WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63 410 |
[WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64 361 |
[WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65 416 |
[WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66 409 |
[WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67 417 |
[WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 611 pm4.71d 615 pm4.71i 613 pm4.71r 612 pm4.71rd 616 pm4.71ri 614 |
[WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 846 |
[WhiteheadRussell] p. 121 | Theorem *4.73 | iba 489 |
[WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 394 |
[WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 833 pm4.76 836 |
[WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 758 pm4.77 762 |
[WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78 565 |
[WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79 566 |
[WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 354 |
[WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81 355 |
[WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 894 |
[WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83 895 |
[WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 313 |
[WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 314 |
[WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 317 |
[WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 350 impexp 433 pm4.87 567 |
[WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 830 |
[WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11 854 |
[WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12 855 |
[WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13 857 |
[WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14 856 |
[WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15 859 |
[WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 860 |
[WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17 858 |
[WhiteheadRussell] p. 124 | Theorem *5.18 | nbbn 347 pm5.18 345 |
[WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 349 |
[WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 831 |
[WhiteheadRussell] p. 124 | Theorem *5.22 | xor 861 |
[WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3 863 |
[WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24 864 |
[WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2 400 |
[WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 692 |
[WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 351 |
[WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 326 |
[WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6 878 |
[WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7 900 |
[WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 571 |
[WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 617 |
[WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 848 |
[WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 869 |
[WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 849 |
[WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 352 pm5.41 353 |
[WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 531 |
[WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 877 |
[WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 771 |
[WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54 870 |
[WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55 867 |
[WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 693 |
[WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62 889 |
[WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63 890 |
[WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71 902 |
[WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 330 |
[WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 235 |
[WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 903 |
[WhiteheadRussell] p. 147 | Theorem *10.22 | 19.26 1593 |
[WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1615 |
[WhiteheadRussell] p. 159 | Theorem *11.07 | pm11.07 2115 |
[WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1738 |
[WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1610 |
[WhiteheadRussell] p. 164 | Theorem *11.5 | 2nalexn 1573 |
[WhiteheadRussell] p. 164 | Theorem *11.51 | 2exnexn 1580 |
[WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1893 |
[WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2208 |
[WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2588 |
[WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2589 |
[WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2979 |
[WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3098 |
[WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 4357 |
[WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 4358 |
[WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2267 eupickbi 2270 |
This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |