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 5653 |
[Eisenberg] p.
125 | Definition 8.21 | df-map 6002 |
[Enderton] p.
19 | Definition | df-tp 3744 |
[Enderton] p.
26 | Exercise 5 | unissb 3922 |
[Enderton] p.
30 | Theorem "Distributive laws" | iinin1 4038 iinin2 4037 iinun2 4033 iunin1 4032 iunin2 4031 |
[Enderton] p.
31 | Theorem "De Morgan's laws" | iindif2 4036 iundif2 4034 |
[Enderton] p.
32 | Exercise 20 | unineq 3506 |
[Enderton] p.
33 | Exercise 23 | iinuni 4050 |
[Enderton] p.
33 | Exercise 25 | iununi 4051 |
[Enderton] p.
33 | Exercise 24(a) | iinpw 4055 |
[Enderton] p.
33 | Exercise 24(b) | iunpwss 4056 |
[Enderton] p.
38 | Exercise 6(a) | unipw 4118 |
[Enderton] p. 41 | Lemma
3D | rnex 5108 rnexg 5105 |
[Enderton] p.
41 | Exercise 8 | dmuni 4915 rnuni 5039 |
[Enderton] p.
42 | Definition of a function | dffun7 5134 dffun8 5135 |
[Enderton] p.
43 | Definition of function value | funfv2 5377 |
[Enderton] p.
43 | Definition of single-rooted | funcnv 5157 |
[Enderton] p.
44 | Definition (d) | dfima4 4953 |
[Enderton] p.
47 | Theorem 3H | fvco2 5383 |
[Enderton] p.
50 | Theorem 3K(a) | imauni 5466 |
[Enderton] p.
52 | Definition | df-map 6002 |
[Enderton] p.
53 | Exercise 21 | coass 5098 |
[Enderton] p.
53 | Exercise 27 | dmco 5090 |
[Enderton] p.
53 | Exercise 14(a) | funin 5164 |
[Enderton] p.
53 | Exercise 22(a) | imass2 5025 |
[Enderton] p.
56 | Theorem 3M | erref 5960 |
[Enderton] p. 57 | Lemma
3N | erthi 5971 |
[Enderton] p.
57 | Definition | df-ec 5948 |
[Enderton] p.
58 | Definition | df-qs 5952 |
[Enderton] p.
61 | Exercise 35 | df-ec 5948 |
[Enderton] p.
65 | Exercise 56(a) | dmun 4913 |
[Enderton] p.
79 | Definition of operation value | df-ov 5527 |
[Enderton] p.
129 | Definition | df-en 6030 |
[Enderton] p.
144 | Corollary 6K | undif2 3627 |
[Enderton] p.
145 | Figure 38 | ffoss 5315 |
[Gleason] p.
119 | Proposition 9-2.4 | caovmo 5646 |
[Hailperin] p. 6 | Axiom
P1 | ax-nin 4079 df-nin 3212 |
[Hailperin] p.
10 | Axiom P2 | ax-si 4084 |
[Hailperin] p.
10 | Axiom P3 | ax-ins2 4085 |
[Hailperin] p.
10 | Axiom P4 | ax-ins3 4086 |
[Hailperin] p.
10 | Axiom P5 | ax-xp 4080 |
[Hailperin] p.
10 | Axiom P6 | ax-typlower 4087 |
[Hailperin] p.
10 | Axiom P7 | ax-cnv 4081 |
[Hailperin] p.
10 | Axiom P8 | ax-1c 4082 |
[Hailperin] p.
10 | Axiom P9 | ax-sset 4083 |
[Hamilton] p.
28 | Definition 2.1 | ax-1 6 |
[Hamilton] p.
31 | Example 2.7(a) | idALT 20 |
[Hamilton] p. 73 | Rule
1 | ax-mp 5 |
[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 5737 |
[Holmes] p.
134 | Definition | df-scan 6327 |
[Holmes], p.
134 | Observation | scancan 6332 |
[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 6012 mapvalg 6010 |
[Kunen] p. 31 | Definition
10.24 | mapex 6007 mapexi 6004 |
[KuratowskiMostowski] p.
109 | Section. Eq. 14 | iuniin 3980 |
[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 6 |
[Margaris] p. 49 | Axiom
A2 | ax-2 7 |
[Margaris] p. 49 | Axiom
A3 | ax-3 8 |
[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 3640 |
[Margaris] p.
89 | Theorem 19.3 | 19.3 1785 19.3v 1665 rr19.3v 2981 |
[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 2728 |
[Margaris] p.
90 | Theorem 19.14 | exnal 1574 |
[Margaris] p.
90 | Theorem 19.15 | albi 1564 ralbi 2751 |
[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 2692 ralimdv 2694 ralimdva 2693 sbcimdv 3108 |
[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 2701 r19.21be 2716 r19.21bi 2713 r19.21t 2700 r19.21v 2702 ralrimd 2703 ralrimdv 2704 ralrimdva 2705 ralrimdvv 2709 ralrimdvva 2710 ralrimi 2696 ralrimiv 2697 ralrimiva 2698 ralrimivv 2706 ralrimivva 2707 ralrimivvva 2708 ralrimivw 2699 rexlimi 2732 |
[Margaris] p.
90 | Theorem 19.22 | 2alimdv 1623 2eximdv 1624 exim 1575
eximd 1770 eximdh 1588 eximdv 1622 rexim 2719 reximdai 2723 reximdv 2726 reximdv2 2724 reximdva 2727 reximdvai 2725 reximi2 2721 |
[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 2730 r19.23v 2731 rexlimd 2736 rexlimdv 2738 rexlimdv3a 2741 rexlimdva 2739 rexlimdvaa 2740 rexlimdvv 2745 rexlimdvva 2746 rexlimdvw 2742 rexlimiv 2733 rexlimiva 2734 rexlimivv 2744 |
[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 2748 r19.26-3 2749 r19.26 2747 r19.26m 2750 |
[Margaris] p.
90 | Theorem 19.27 | 19.27 1869 19.27v 1894 r19.27av 2753 r19.27z 3649 r19.27zv 3650 |
[Margaris] p.
90 | Theorem 19.28 | 19.28 1870 19.28v 1895 r19.28av 2754 r19.28z 3643 r19.28zv 3646 rr19.28v 2982 |
[Margaris] p.
90 | Theorem 19.29 | 19.29 1596 19.29r 1597 19.29r2 1598 19.29x 1599 r19.29 2755 r19.29r 2756 |
[Margaris] p.
90 | Theorem 19.30 | 19.30 1604 r19.30 2757 |
[Margaris] p.
90 | Theorem 19.31 | 19.31 1876 |
[Margaris] p.
90 | Theorem 19.32 | 19.32 1875 r19.32v 2758 |
[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 2759 |
[Margaris] p.
90 | Theorem 19.36 | 19.36 1871 19.36aiv 1897 19.36i 1872 19.36v 1896 r19.36av 2760 r19.36zv 3651 |
[Margaris] p.
90 | Theorem 19.37 | 19.37 1873 19.37aiv 1900 19.37v 1899 r19.37 2761 r19.37av 2762 r19.37zv 3647 |
[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 2763 |
[Margaris] p.
90 | Theorem 19.41 | 19.41 1879 19.41v 1901 19.41vv 1902 19.41vvv 1903 19.41vvvv 1904 r19.41 2764 r19.41v 2765 |
[Margaris] p.
90 | Theorem 19.42 | 19.42 1880 19.42v 1905 19.42vv 1907 19.42vvv 1908 r19.42v 2766 |
[Margaris] p.
90 | Theorem 19.43 | 19.43 1605 r19.43 2767 |
[Margaris] p.
90 | Theorem 19.44 | 19.44 1877 r19.44av 2768 |
[Margaris] p.
90 | Theorem 19.45 | 19.45 1878 r19.45av 2769 r19.45zv 3648 |
[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 3125 rspsbca 3126 stdpc4 2024 |
[Mendelson] p.
69 | Axiom 5 | ax-5o 2136 ra5 3131 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 3046 |
[Mendelson] p.
231 | Exercise 4.10(k) | inv1 3578 |
[Mendelson] p.
231 | Exercise 4.10(l) | unv 3579 |
[Mendelson] p.
231 | Exercise 4.10(n) | dfin3 3495 |
[Mendelson] p.
231 | Exercise 4.10(o) | df-nul 3552 |
[Mendelson] p.
231 | Exercise 4.10(q) | dfin4 3496 |
[Mendelson] p.
231 | Exercise 4.10(s) | ddif 3399 |
[Mendelson] p.
231 | Definition of union | dfun3 3494 |
[Mendelson] p.
235 | Exercise 4.12(d) | pwv 3887 |
[Mendelson] p.
235 | Exercise 4.12(n) | uniin 3912 |
[Mendelson] p.
235 | Exercise 4.12(t) | ssdmrn 5100 |
[Mendelson] p.
254 | Proposition 4.22(b) | xpen 6056 |
[Mendelson] p.
254 | Proposition 4.22(c) | xpsnen 6050 xpsneng 6051 |
[Mendelson] p.
254 | Proposition 4.22(d) | xpcomen 6053 xpcomeng 6054 |
[Mendelson] p.
254 | Proposition 4.22(e) | xpassen 6058 |
[Mendelson] p.
255 | Exercise 4.39 | endisj 6052 |
[Mendelson] p.
255 | Exercise 4.41 | mapprc 6005 |
[Mendelson] p.
287 | Axiom system MK | ru 3046 |
[Monk1] p. 26 | Theorem
2.8(vii) | ssin 3478 |
[Monk1] p. 33 | Theorem
3.2(i) | ssrel 4845 |
[Monk1] p. 33 | Theorem
3.2(ii) | eqrel 4846 |
[Monk1] p. 34 | Definition
3.3 | df-opab 4624 |
[Monk1] p. 36 | Theorem
3.7(i) | coi1 5095 coi2 5096 |
[Monk1] p. 36 | Theorem
3.8(v) | dm0 4919 rn0 4970 |
[Monk1] p. 36 | Theorem
3.7(ii) | cnvi 5033 |
[Monk1] p. 37 | Theorem
3.13(x) | dmxp 4924 rnxp 5052 |
[Monk1] p. 37 | Theorem
3.13(ii) | xp0 5045 xp0r 4843 |
[Monk1] p. 38 | Theorem
3.16(ii) | ima0 5014 |
[Monk1] p. 38 | Theorem
3.16(viii) | imai 5011 |
[Monk1] p. 39 | Theorem
3.16(xi) | imassrn 5010 |
[Monk1] p. 41 | Theorem
4.3(i) | fnopfv 5413 funfvop 5401 |
[Monk1] p. 42 | Theorem
4.3(ii) | funopfvb 5362 |
[Monk1] p. 42 | Theorem
4.4(iii) | fvelima 5370 |
[Monk1] p. 43 | Theorem
4.6 | funun 5147 |
[Monk1] p. 43 | Theorem
4.8(iv) | dff13 5472 dff13f 5473 |
[Monk1] p. 50 | Definition
5.4 | fniunfv 5467 |
[Monk1] p. 52 | Theorem
5.11(viii) | ssint 3943 |
[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 4607 |
[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 2669 |
[Pfenning] p.
17 | Definition NNC | notnotrd 105 |
[Quine] p. 16 | Definition
2.1 | df-clab 2340 rabid 2788 |
[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 2862 |
[Quine] p. 34 | Theorem
5.1 | abeq2 2459 |
[Quine] p. 35 | Theorem
5.2 | abid2 2471 abid2f 2515 |
[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 3048 |
[Quine] p. 42 | Theorem
6.7 | dfsbcq 3049 dfsbcq2 3050 |
[Quine] p. 43 | Theorem
6.8 | vex 2863 |
[Quine] p. 43 | Theorem
6.9 | isset 2864 |
[Quine] p. 44 | Theorem
7.3 | spcgf 2935 spcgv 2940 spcimgf 2933 |
[Quine] p. 44 | Theorem
6.11 | spsbc 3059 spsbcd 3060 |
[Quine] p. 44 | Theorem
6.12 | elex 2868 |
[Quine] p. 44 | Theorem
6.13 | elab 2986 elabg 2987 elabgf 2984 |
[Quine] p. 44 | Theorem
6.14 | noel 3555 |
[Quine] p. 48 | Theorem
7.2 | snprc 3789 |
[Quine] p. 48 | Definition
7.1 | df-pr 3743 df-sn 3742 |
[Quine] p. 49 | Theorem
7.4 | snss 3839 snssg 3845 |
[Quine] p. 49 | Theorem
7.5 | prss 3862 prssg 3863 |
[Quine] p. 49 | Theorem
7.6 | prid1 3828 prid1g 3826 prid2 3829 prid2g 3827 snid 3761
snidg 3759 |
[Quine] p. 53 | Theorem
8.2 | unisn 3908 unisng 3909 |
[Quine] p. 53 | Theorem
8.3 | uniun 3911 |
[Quine] p. 54 | Theorem
8.6 | elssuni 3920 |
[Quine] p. 54 | Theorem
8.7 | uni0 3919 |
[Quine] p. 56 | Theorem
8.17 | uniabio 4350 |
[Quine] p. 56 | Definition
8.18 | dfiota2 4341 |
[Quine] p. 57 | Theorem
8.19 | iotaval 4351 |
[Quine] p. 57 | Theorem
8.22 | iotanul 4355 |
[Quine] p. 58 | Theorem
8.23 | iotaex 4357 |
[Quine] p. 61 | Theorem
9.5 | opabid 4696 opelopab 4709 opelopaba 4704 opelopabaf 4711 opelopabf 4712 opelopabg 4706 opelopabga 4701 oprabid 5551 |
[Quine] p. 64 | Definition
9.11 | df-xp 4785 |
[Quine] p. 64 | Definition
9.12 | df-cnv 4786 |
[Quine] p. 64 | Definition
9.15 | df-id 4768 |
[Quine] p. 65 | Theorem
10.3 | fun0 5155 |
[Quine] p. 65 | Theorem
10.4 | funi 5138 |
[Quine] p. 65 | Theorem
10.5 | funsn 5148 |
[Quine] p. 65 | Definition
10.1 | df-fun 4790 |
[Quine] p. 68 | Definition
10.11 | fv2 5325 |
[Quine] p. 331 | Axiom
system NF | ru 3046 |
[Rosser] p. 236 | Theorem
IX.4.21 | dfpss4 3889 |
[Rosser] p.
238 | Definition IX.9.10, | df-symdif 3217 |
[Rosser] p.
245 | Definition | df-clos1 5874 |
[Rosser] p. 246 | Theorem
IX.5.13 | clos1base 5879 |
[Rosser] p. 246 | Theorem
IX.5.14 | clos1conn 5880 |
[Rosser] p. 247 | Theorem
IX.5.15 | clos1induct 5881 |
[Rosser] p. 248 | Theorem
IX.5.16 | clos1basesuc 5883 clos1basesucg 5885 |
[Rosser] p.
252 | Definition | df-pw1 4138 |
[Rosser] p. 255 | Theorem
IX.6.14 | sspw1 4336 |
[Rosser] p.
275 | Definition | df-addc 4379 df-nnc 4380 |
[Rosser] p. 275 | Theorem
X.1.1 | eladdc 4399 |
[Rosser] p. 275 | Theorem
X.1.2 | 0cnsuc 4402 |
[Rosser] p. 276 | Theorem
X.1.3 | dfnnc3 5886 |
[Rosser] p. 276 | Theorem
X.1.4 | peano1 4403 |
[Rosser] p. 276 | Theorem
X.1.5 | peano2 4404 |
[Rosser] p. 276 | Theorem
X.1.6 | peano5 4410 |
[Rosser] p. 276 | Theorem
X.1.7 | nnc0suc 4413 |
[Rosser] p. 276 | Theorem
X.1.8 | addcid1 4406 addcid2 4408 |
[Rosser] p. 276 | Theorem
X.1.9 | addccom 4407 |
[Rosser] p. 277 | Corollary
1 | addcass 4416 |
[Rosser] p. 277 | Theorem
X.1.12 | 1cnnc 4409 |
[Rosser] p. 277 | Theorem
X.1.13 | finds 4412 findsd 4411 |
[Rosser] p. 278 | Theorem
X.1.14 | nncaddccl 4420 |
[Rosser] p. 279 | Theorem
X.1.16 | elsuc 4414 |
[Rosser] p.
279 | Definition from Ex. X.1.4 | df-lefin 4441 |
[Rosser] p.
281 | Definition | df-op 4567 df-proj1 4568 df-proj2 4569 |
[Rosser] p. 282 | Theorem
X.2.2 | phi11 4597 |
[Rosser] p. 282 | Theorem
X.2.3 | 0cnelphi 4598 |
[Rosser] p. 282 | Theorem
X.2.4 | phi011 4600 |
[Rosser] p. 282 | Theorem
X.2.7 | proj1op 4601 |
[Rosser] p. 283 | Theorem
X.2.8 | proj2op 4602 |
[Rosser] p. 301 | Theorem
X.4.29.I | dmsi 5520 |
[Rosser] p. 302 | Theorem
X.4.29.II | rnsi 5522 |
[Rosser] p. 303 | Theorem
X.4.37 | clos1baseima 5884 |
[Rosser] p.
347 | Definition | df-can 6325 df-can 6325 |
[Rosser] p. 347 | Theorem
XI.1.6 | nenpw1pw 6087 |
[Rosser] p. 348 | Theorem
XI.1.8 | vncan 6338 |
[Rosser] p. 348 | Theorem
XI.1.10 | ensn 6059 |
[Rosser] p. 348 | Theorem
XI.1.13 | enadj 6061 |
[Rosser] p. 350 | Theorem
XI.1.14 | sbthlem1 6204 sbthlem2 6205 |
[Rosser] p. 353 | Theorem
XI.1.15 | sbthlem3 6206 |
[Rosser] p. 357 | Theorem
XI.1.22 | enmap2 6069 |
[Rosser] p. 357 | Theorem
XI.1.23 | enmap1 6075 |
[Rosser] p. 360 | Theorem
XI.1.28 | enprmap 6083 enprmapc 6084 |
[Rosser] p. 368 | Theorem
XI.1.33 | enpw1 6063 |
[Rosser] p. 368 | Theorem
XI.1.35 | enpw1pw 6076 |
[Rosser] p. 369 | Theorem
XI.1.36 | enpw 6088 |
[Rosser] p.
371 | Definition | df-nc 6102 |
[Rosser] p.
372 | Definition | df-ncs 6099 |
[Rosser] p. 372 | Theorem
XI.2.4 | ncpw1pwneg 6202 |
[Rosser] p. 372 | Theorem
XI.2.7 | df0c2 6138 |
[Rosser] p. 373 | Theorem
XI.2.7 | 0cnc 6139 |
[Rosser] p. 373 | Theorem
XI.2.8 | 1cnc 6140 df1c3 6141 df1c3g 6142 |
[Rosser] p. 374 | Theorem
XI.2.10 | ncaddccl 6145 |
[Rosser] p. 374 | Theorem
XI.2.11 | nnssnc 6148 |
[Rosser] p.
375 | Definition | df-lec 6100 df-ltc 6101 |
[Rosser] p. 375 | Theorem
XI.2.12 | peano4nc 6151 |
[Rosser] p. 375 | Theorem
XI.2.14 | lecidg 6197 |
[Rosser] p. 376 | Theorem
XI.2.14 | nclecid 6198 |
[Rosser] p. 376 | Theorem
XI.2.15 | le0nc 6201 lec0cg 6199 |
[Rosser] p. 376 | Theorem
XI.2.16 | lecncvg 6200 |
[Rosser] p. 376 | Theorem
XI.2.17 | ltcpw1pwg 6203 |
[Rosser] p. 376 | Theorem
XI.2.19 | addlec 6209 addlecncs 6210 |
[Rosser] p. 376 | Theorem
XI.2.20 | sbth 6207 |
[Rosser] p. 377 | Theorem
XI.2.21 | ltlenlec 6208 |
[Rosser] p. 377 | Theorem
XI.2.22 | dflec2 6211 |
[Rosser] p. 377 | Theorem
XI.2.23 | leaddc1 6215 leaddc2 6216 |
[Rosser] p. 377 | Theorem
XI.2.24 | nc0le1 6217 nc0suc 6218 |
[Rosser] p.
378 | Definition | df-muc 6103 |
[Rosser] p. 378 | Theorem
XI.2.27 | mucnc 6132 |
[Rosser] p. 378 | Theorem
XI.2.28 | muccom 6135 |
[Rosser] p. 378 | Theorem
XI.2.29 | mucass 6136 |
[Rosser] p. 379 | Theorem
XI.2.30 | addcdir 6252 |
[Rosser] p. 379 | Theorem
XI.2.31 | addcdi 6251 |
[Rosser] p. 379 | Theorem
XI.2.32 | muc0 6143 |
[Rosser] p. 380 | Theorem
XI.2.34 | muc0or 6253 |
[Rosser] p. 380 | Theorem
XI.2.35 | lemuc1 6254 |
[Rosser] p.
381 | Definition | df-ce 6107 |
[Rosser] p. 381 | Theorem
XI.2.36 | ncslemuc 6256 |
[Rosser] p. 381 | Theorem
XI.2.37 | ncvsq 6257 vvsqenvv 6258 |
[Rosser] p. 382 | Theorem
XI.2.38 | elce 6176 |
[Rosser] p. 382 | Theorem
XI.2.39 | cenc 6182 |
[Rosser] p. 382 | Theorem
XI.2.42 | ce0nnul 6178 |
[Rosser] p. 383 | Theorem
XI.2.43 | ce0addcnnul 6180 |
[Rosser] p. 383 | Theorem
XI.2.44 | ce0nn 6181 |
[Rosser] p. 384 | Theorem
XI.2.38 | ce0nulnc 6185 |
[Rosser] p. 384 | Theorem
XI.2.47 | ce0nnulb 6183 |
[Rosser] p. 384 | Theorem
XI.2.48 | ce0ncpw1 6186 cecl 6187
ceclb 6184 |
[Rosser] p. 385 | Theorem
XI.2.49 | ce0 6191 |
[Rosser] p. 389 | Theorem
XI.2.70 | ce2 6193 |
[Rosser] p. 390 | Theorem
XI.2.71 | ce2lt 6221 |
[Rosser] p. 391 | Theorem
XI.3.2 | addccan2nc 6266 lecadd2 6267 |
[Rosser] p. 391 | Theorem
XI.3.3 | nclenn 6250 |
[Rosser] p. 412 | Theorem
XI.3.24 | df-frec 6311 |
[Rosser] p. 525 | Theorem
X.1.17 | nnsucelr 4429 |
[Rosser] p. 526 | Corollary
1 | addcnul1 4453 |
[Rosser] p. 526 | Theorem
X.1.18 | nndisjeq 4430 |
[Rosser] p. 526 | Theorem
X.1.19 | prepeano4 4452 |
[Rosser] p. 526 | Theorem
X.1.20 | addcnnul 4454 |
[Rosser] p.
527 | Definition | df-ltfin 4442 df-ncfin 4443 |
[Rosser] p. 527 | Theorem
X.1.21 | ssfin 4471 |
[Rosser] p. 527 | Theorem
X.1.22 | vfinnc 4472 |
[Rosser] p. 527 | Theorem
X.1.23 | ncfinprop 4475 |
[Rosser] p. 527 | Theorem
X.1.24 | ncfineleq 4478 |
[Rosser] p. 527 | Theorem
X.1.25 | ncfinraise 4482 |
[Rosser] p. 527 | Theorem
X.1.26 | ncfinlower 4484 |
[Rosser] p.
528 | Definition | df-tfin 4444 |
[Rosser] p. 528 | Theorem
X.1.27 | nnpw1ex 4485 |
[Rosser] p. 528 | Theorem
X.1.28 | tfinnnul 4491 tfinprop 4490 |
[Rosser] p. 528 | Theorem
X.1.29 | tfinnul 4492 |
[Rosser] p. 528 | Theorem
X.1.30 | tfin11 4494 |
[Rosser] p. 528 | Theorem
X.1.31 | tfinpw1 4495 |
[Rosser] p.
528 | Definition adapted | df-tc 6104 |
[Rosser] p.
529 | Definition | df-evenfin 4445 df-oddfin 4446 |
[Rosser] p. 529 | Theorem
X.1.31 | ncfintfin 4496 |
[Rosser] p. 529 | Theorem
X.1.32 | tfindi 4497 |
[Rosser] p. 529 | Theorem
X.1.33 | tfinlefin 4503 tfinltfin 4502 |
[Rosser] p. 529 | Theorem
X.1.35 | evenoddnnnul 4515 |
[Rosser] p. 529 | Theorem
X.1.36 | evenodddisj 4517 |
[Rosser] p. 529 | Theorem
X.1.34(a) | tfin1c 4500 |
[Rosser] p.
530 | Definition | df-sfin 4447 |
[Rosser] p. 530 | Theorem
X.1.37 | eventfin 4518 |
[Rosser] p. 530 | Theorem
X.1.38 | oddtfin 4519 |
[Rosser] p. 530 | Theorem
X.1.39 | nnadjoin 4521 |
[Rosser] p. 530 | Theorem
X.1.40 | nnadjoinpw 4522 |
[Rosser] p. 530 | Theorem
X.1.41 | nnpweq 4524 |
[Rosser] p. 530 | Theorem
X.1.42 | sfin01 4529 |
[Rosser] p. 530 | Theorem
X.1.43 | sfin112 4530 |
[Rosser] p. 531 | Theorem
X.1.44 | sfindbl 4531 |
[Rosser] p. 532 | Theorem
X.1.45 | sfintfin 4533 |
[Rosser] p. 532 | Theorem
X.1.46 | tfinnn 4535 |
[Rosser] p. 532 | Theorem
X.1.47 | sfinltfin 4536 |
[Rosser] p.
533 | Definition | df-spfin 4448 |
[Rosser] p. 533 | Theorem
X.1.48 | sfin111 4537 |
[Rosser] p. 534 | Theorem
X.1.49 | ncvspfin 4539 |
[Rosser] p. 534 | Theorem
X.1.50 | spfinsfincl 4540 |
[Rosser] p. 534 | Theorem
X.1.51 | spfininduct 4541 |
[Rosser] p. 534 | Theorem
X.1.53 | vfinspnn 4542 |
[Rosser] p. 534 | Theorem
X.1.54 | 1cspfin 4544 1cvsfin 4543 |
[Rosser] p. 534 | Theorem
X.1.55 | tncveqnc1fin 4545 |
[Rosser] p. 534 | Theorem
X.1.56 | t1csfin1c 4546 vfintle 4547 |
[Rosser] p. 534 | Theorem
X.1.57 | vfin1cltv 4548 |
[Rosser] p. 534 | Theorem
X.1.58 | vfinncvntnn 4549 vfinncvntsp 4550 |
[Rosser] p. 534 | Theorem
X.1.59 | vfinspss 4552 |
[Rosser] p. 536 | Theorem
X.1.60 | vfinspclt 4553 |
[Rosser] p. 536 | Theorem
X.1.61 | vfinspeqtncv 4554 |
[Rosser] p. 536 | Theorem
X.1.62 | vfinncsp 4555 |
[Rosser] p. 536 | Theorem
X.1.63 | vinf 4556 |
[Rosser] p. 536 | Theorem
X.1.65 | nulnnn 4557 |
[Rosser] p. 537 | Theorem
X.1.66 | peano4 4558 |
[Rosser], p.
417 | Definition | df-fin 4381 |
[Sanford] p.
39 | Remark | ax-mp 5 |
[Sanford] p. 39 | Rule
3 | mtp-xor 1536 |
[Sanford] p. 39 | Rule
4 | mpto2 1534 |
[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 5029 |
[Schechter] p.
51 | Definition of irreflexivity | intirr 5030 |
[Schechter] p.
51 | Definition of symmetry | cnvsym 5028 |
[Schechter] p.
51 | Definition of transitivity | cotr 5027 |
[Specker] p. 972 | Theorem
2.4 | tc11 6229 |
[Specker] p. 973 | Theorem
3.4 | nnc3n3p1 6279 nnc3n3p2 6280 nnc3p1n3p2 6281 nncdiv3 6278 |
[Specker] p. 973 | Theorem
4.3 | ce2nc1 6194 |
[Specker] p. 973 | Theorem
4.4 | ce2ncpw11c 6195 |
[Specker] p. 973 | Theorem
4.5 | nchoicelem8 6297 |
[Specker] p. 973 | Theorem
4.8 | ce2le 6234 |
[Specker] p. 973 | Theorem
5.2 | tcnc1c 6228 tcncv 6227 |
[Specker] p. 973 | Theorem
5.5 | tlecg 6231 |
[Specker] p. 973 | Theorem
5.6 | letc 6232 |
[Specker] p. 973 | Theorem
5.8 | ce2t 6236 |
[Specker] p. 973 | Theorem
6.2 | nchoicelem3 6292 |
[Specker] p. 973 | Theorem
6.4 | nchoicelem4 6293 |
[Specker] p. 973 | Theorem
6.5 | nchoicelem5 6294 |
[Specker] p. 973 | Theorem
6.6 | nchoicelem6 6295 |
[Specker] p.
973 | Definition 6.1 | df-spac 6275 |
[Specker] p. 974 | Theorem
6.7 | nchoicelem7 6296 |
[Specker] p. 974 | Theorem
6.8 | nchoicelem9 6298 |
[Specker] p. 974 | Theorem
7.1 | nchoicelem12 6301 |
[Specker] p. 974 | Theorem
7.2 | nchoicelem17 6306 |
[Specker] p. 974 | Theorem
7.3 | nchoicelem19 6308 |
[Specker] p. 974 | Theorem
7.5 | nchoice 6309 |
[Stoll] p. 13 | Definition
of symmetric difference | symdif1 3520 |
[Stoll] p. 16 | Exercise
4.4 | 0dif 3622 dif0 3621 |
[Stoll] p. 16 | Exercise
4.8 | difdifdir 3638 |
[Stoll] p. 17 | Theorem
5.1(5) | undifv 3625 |
[Stoll] p. 19 | Theorem
5.2(13) | undm 3513 |
[Stoll] p. 19 | Theorem
5.2(13') | indm 3514 |
[Stoll] p.
20 | Remark | invdif 3497 |
[Stoll] p.
43 | Definition | uniiun 4020 |
[Stoll] p.
44 | Definition | intiin 4021 |
[Stoll] p.
45 | Definition | df-iin 3973 |
[Stoll] p. 45 | Definition
indexed union | df-iun 3972 |
[Stoll] p. 176 | Theorem
3.4(27) | iman 413 |
[Stoll] p. 262 | Example
4.1 | symdif1 3520 |
[Suppes] p. 22 | Theorem
2 | eq0 3565 |
[Suppes] p. 22 | Theorem
4 | eqss 3288 eqssd 3290 eqssi 3289 |
[Suppes] p. 23 | Theorem
5 | ss0 3582 ss0b 3581 |
[Suppes] p. 23 | Theorem
6 | sstr 3281 |
[Suppes] p. 23 | Theorem
7 | pssirr 3370 |
[Suppes] p. 23 | Theorem
8 | pssn2lp 3371 |
[Suppes] p. 23 | Theorem
9 | psstr 3374 |
[Suppes] p. 23 | Theorem
10 | pssss 3365 |
[Suppes] p. 26 | Theorem
15 | inidm 3465 |
[Suppes] p. 26 | Theorem
16 | in0 3577 |
[Suppes] p. 27 | Theorem
23 | unidm 3408 |
[Suppes] p. 27 | Theorem
24 | un0 3576 |
[Suppes] p. 27 | Theorem
25 | ssun1 3427 |
[Suppes] p. 27 | Theorem
26 | ssequn1 3434 |
[Suppes] p. 27 | Theorem
27 | unss 3438 |
[Suppes] p. 27 | Theorem
28 | indir 3504 |
[Suppes] p. 27 | Theorem
29 | undir 3505 |
[Suppes] p. 28 | Theorem
32 | difid 3619 difidALT 3620 |
[Suppes] p. 29 | Theorem
33 | difin 3493 |
[Suppes] p. 29 | Theorem
34 | indif 3498 |
[Suppes] p. 29 | Theorem
35 | undif1 3626 |
[Suppes] p. 29 | Theorem
36 | difun2 3630 |
[Suppes] p. 29 | Theorem
37 | difin0 3624 |
[Suppes] p. 29 | Theorem
38 | disjdif 3623 |
[Suppes] p. 29 | Theorem
39 | difundi 3508 |
[Suppes] p. 29 | Theorem
40 | difindi 3510 |
[Suppes] p. 39 | Theorem
61 | uniss 3913 |
[Suppes] p. 41 | Theorem
70 | intsn 3963 |
[Suppes] p. 42 | Theorem
71 | intpr 3960 intprg 3961 |
[Suppes] p. 42 | Theorem
78 | intun 3959 |
[Suppes] p. 44 | Definition
15(a) | dfiun2 4002 dfiun2g 4000 |
[Suppes] p. 44 | Definition
15(b) | dfiin2 4003 |
[Suppes] p. 47 | Theorem
86 | elpw 3729 elpwg 3730 |
[Suppes] p. 47 | Theorem
87 | pwid 3736 |
[Suppes] p. 47 | Theorem
89 | pw0 4161 |
[Suppes] p. 48 | Theorem
90 | pwpw0 3856 |
[Suppes] p. 52 | Theorem
101 | xpss12 4856 |
[Suppes] p. 52 | Theorem
102 | xpindi 4865 xpindir 4866 |
[Suppes] p. 52 | Theorem
103 | xpundi 4833 xpundir 4834 |
[Suppes] p. 59 | Theorem
4 | eldm 4899 eldm2 4900 |
[Suppes] p. 60 | Theorem
6 | dmin 4914 |
[Suppes] p. 60 | Theorem
8 | rnun 5037 |
[Suppes] p. 60 | Theorem
9 | rnin 5038 |
[Suppes] p. 60 | Definition
4 | dfrn2 4903 |
[Suppes] p. 61 | Theorem
11 | brcnv 4893 |
[Suppes] p. 62 | Equation
5 | elcnv 4890 elcnv2 4891 |
[Suppes] p. 62 | Theorem
15 | cnvin 5036 |
[Suppes] p. 62 | Theorem
16 | cnvun 5034 |
[Suppes] p. 63 | Theorem
20 | co02 5093 |
[Suppes] p. 63 | Theorem
21 | dmcoss 4972 |
[Suppes] p. 64 | Theorem
26 | cnvco 4895 |
[Suppes] p. 64 | Theorem
27 | coass 5098 |
[Suppes] p. 65 | Theorem
31 | resundi 4982 |
[Suppes] p. 65 | Theorem
34 | elima 4755 elima2 4756 elima3 4757 |
[Suppes] p. 65 | Theorem
35 | imaundi 5040 |
[Suppes] p. 66 | Theorem
40 | dminss 5042 |
[Suppes] p. 66 | Theorem
41 | imainss 5043 |
[Suppes] p. 67 | Exercise
11 | cnvxp 5044 |
[Suppes] p. 81 | Definition
34 | dfec2 5949 |
[Suppes] p. 82 | Theorem
72 | elec 5965 |
[Suppes] p. 82 | Theorem
73 | erth 5969 erth2 5970 |
[Suppes] p. 83 | Theorem
74 | erdisj 5973 |
[Suppes] p. 89 | Theorem
96 | map0b 6025 |
[Suppes] p. 89 | Theorem
97 | map0 6026 |
[Suppes] p. 89 | Theorem
98 | mapsn 6027 |
[Suppes] p. 89 | Theorem
99 | mapss 6028 |
[Suppes] p. 92 | Theorem
4 | unen 6049 |
[Suppes] p. 98 | Exercise
4 | fundmen 6044 fundmeng 6045 |
[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 5529 |
[TakeutiZaring] p.
14 | Proposition 4.14 | ru 3046 |
[TakeutiZaring] p.
15 | Exercise 1 | elpr 3752 elpr2 3753 elprg 3751 |
[TakeutiZaring] p.
15 | Exercise 2 | elsn 3749 elsnc 3757 elsnc2 3763 elsnc2g 3762 elsncg 3756 |
[TakeutiZaring] p.
15 | Exercise 4 | sneq 3745 sneqr 3873 |
[TakeutiZaring] p.
15 | Definition 5.1 | dfpr2 3750 dfsn2 3748 |
[TakeutiZaring] p.
16 | Definition 5.3 | dftp2 3773 |
[TakeutiZaring] p.
16 | Definition 5.5 | df-uni 3893 |
[TakeutiZaring] p.
16 | Proposition 5.7 | unipr 3906 uniprg 3907 |
[TakeutiZaring] p.
17 | Exercise 1 | eltp 3772 |
[TakeutiZaring] p.
17 | Exercise 5 | sstr2 3280 |
[TakeutiZaring] p.
17 | Exercise 6 | uncom 3409 |
[TakeutiZaring] p.
17 | Exercise 7 | incom 3449 |
[TakeutiZaring] p.
17 | Exercise 8 | unass 3421 |
[TakeutiZaring] p.
17 | Exercise 9 | inass 3466 |
[TakeutiZaring] p.
17 | Exercise 10 | indi 3502 |
[TakeutiZaring] p.
17 | Exercise 11 | undi 3503 |
[TakeutiZaring] p.
17 | Definition 5.9 | df-pss 3262 dfss2 3263 |
[TakeutiZaring] p.
17 | Definition 5.10 | df-pw 3725 |
[TakeutiZaring] p.
18 | Exercise 7 | unss2 3435 |
[TakeutiZaring] p.
18 | Exercise 9 | df-ss 3260 sseqin2 3475 |
[TakeutiZaring] p.
18 | Exercise 10 | ssid 3291 |
[TakeutiZaring] p.
18 | Exercise 12 | inss1 3476 inss2 3477 |
[TakeutiZaring] p.
18 | Exercise 13 | nss 3330 |
[TakeutiZaring] p.
18 | Exercise 15 | unieq 3901 |
[TakeutiZaring] p.
18 | Exercise 18 | sspwb 4119 |
[TakeutiZaring] p.
20 | Definition | df-rab 2624 |
[TakeutiZaring] p.
20 | Definition 5.14 | dfnul2 3553 |
[TakeutiZaring] p.
20 | Proposition 5.15 | difid 3619 difidALT 3620 |
[TakeutiZaring] p.
20 | Proposition 5.17(1) | n0 3560 n0f 3559
neq0 3561 |
[TakeutiZaring] p.
21 | Definition 5.20 | df-v 2862 |
[TakeutiZaring] p.
22 | Exercise 1 | 0ss 3580 |
[TakeutiZaring] p.
22 | Exercise 7 | ssdif0 3610 |
[TakeutiZaring] p.
22 | Exercise 11 | difdif 3393 |
[TakeutiZaring] p.
22 | Exercise 13 | undif3 3516 |
[TakeutiZaring] p.
22 | Exercise 14 | difss 3394 |
[TakeutiZaring] p.
22 | Exercise 15 | sscon 3401 |
[TakeutiZaring] p.
22 | Definition 4.15(3) | df-ral 2620 |
[TakeutiZaring] p.
22 | Definition 4.15(4) | df-rex 2621 |
[TakeutiZaring] p.
23 | Proposition 6.2 | xpex 5116 xpexg 5115 |
[TakeutiZaring] p.
24 | Definition 6.4(3) | f1funfun 5264 fun11 5160 |
[TakeutiZaring] p.
24 | Definition 6.4(4) | dffun4 5122 |
[TakeutiZaring] p.
24 | Definition 6.5(1) | dfdm3 4902 |
[TakeutiZaring] p.
24 | Definition 6.5(2) | dfrn3 4904 |
[TakeutiZaring] p.
24 | Definition 6.6(1) | df-res 4789 |
[TakeutiZaring] p.
25 | Exercise 9 | inxp 4864 |
[TakeutiZaring] p.
25 | Exercise 13 | opelres 4951 |
[TakeutiZaring] p.
25 | Exercise 14 | dmres 4987 |
[TakeutiZaring] p.
25 | Exercise 15 | resss 4989 |
[TakeutiZaring] p.
25 | Exercise 17 | resabs1 4993 |
[TakeutiZaring] p.
25 | Exercise 18 | funres 5144 |
[TakeutiZaring] p.
25 | Exercise 29 | funco 5143 |
[TakeutiZaring] p.
25 | Exercise 30 | f1co 5265 |
[TakeutiZaring] p.
26 | Definition 6.10 | eu2 2229 |
[TakeutiZaring] p.
26 | Definition 6.11 | fv3 5342 |
[TakeutiZaring] p.
26 | Corollary 6.8(1) | cnvex 5103 cnvexg 5102 |
[TakeutiZaring] p.
26 | Corollary 6.8(2) | dmex 5107 dmexg 5106 |
[TakeutiZaring] p.
26 | Corollary 6.8(3) | rnex 5108 rnexg 5105 |
[TakeutiZaring] p.
27 | Corollary 6.13 | fvex 5340 |
[TakeutiZaring] p.
27 | Theorem 6.12(1) | tz6.12-1 5345 tz6.12 5346 tz6.12c 5348 |
[TakeutiZaring] p.
27 | Theorem 6.12(2) | tz6.12-2 5347 tz6.12i 5349 |
[TakeutiZaring] p.
27 | Definition 6.15(1) | df-fn 4791 |
[TakeutiZaring] p.
27 | Definition 6.15(3) | df-f 4792 |
[TakeutiZaring] p.
27 | Definition 6.15(4) | df-fo 4794 wfo 4780 |
[TakeutiZaring] p.
27 | Definition 6.15(5) | df-f1 4793 wf1 4779 |
[TakeutiZaring] p.
27 | Definition 6.15(6) | df-f1o 4795 wf1o 4781 |
[TakeutiZaring] p.
28 | Exercise 4 | eqfnfv 5393 eqfnfv2 5394 eqfnfv2f 5397 |
[TakeutiZaring] p.
28 | Exercise 5 | fvco 5384 |
[TakeutiZaring] p.
29 | Definition 6.18 | df-br 4641 |
[TakeutiZaring] p.
30 | Definition 6.21 | eliniseg 5021 iniseg 5023 |
[TakeutiZaring] p.
30 | Definition 6.22 | df-eprel 4765 |
[TakeutiZaring] p.
32 | Definition 6.28 | df-iso 4797 |
[TakeutiZaring] p.
33 | Proposition 6.30(1) | isoid 5491 |
[TakeutiZaring] p.
33 | Proposition 6.30(2) | isocnv 5492 |
[TakeutiZaring] p.
33 | Proposition 6.30(3) | isotr 5496 |
[TakeutiZaring] p.
33 | Proposition 6.31(1) | isomin 5497 |
[TakeutiZaring] p.
33 | Proposition 6.31(2) | isoini 5498 |
[TakeutiZaring] p.
34 | Proposition 6.33 | f1oiso 5500 |
[TakeutiZaring] p.
40 | Proposition 7.20 | elssuni 3920 |
[TakeutiZaring] p.
44 | Exercise 2 | int0 3941 |
[TakeutiZaring] p.
44 | Exercise 4 | intss1 3942 |
[TakeutiZaring] p.
44 | Definition 7.35 | df-int 3928 |
[TakeutiZaring] p.
53 | Proposition 7.53 | 2eu5 2288 |
[TakeutiZaring] p.
59 | Proposition 8.6 | iunss2 4012 uniss2 3923 |
[TakeutiZaring] p.
88 | Exercise 1 | en0 6043 |
[TakeutiZaring] p.
95 | Definition 10.42 | df-map 6002 |
[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 6156 |
[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 6 |
[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 8 |
[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 7 |
[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 2589 |
[WhiteheadRussell] p.
178 | Theorem *13.181 | pm13.181 2590 |
[WhiteheadRussell] p.
178 | Theorem *13.183 | pm13.183 2980 |
[WhiteheadRussell] p.
185 | Theorem *14.121 | sbeqalb 3099 |
[WhiteheadRussell] p.
190 | Theorem *14.22 | iota4 4358 |
[WhiteheadRussell] p.
191 | Theorem *14.23 | iota4an 4359 |
[WhiteheadRussell] p.
192 | Theorem *14.26 | eupick 2267 eupickbi 2270 |