Bibliographic Cross-References
|
|
Intuitionistic Logic Explorer Bibliographic Cross-References |
|
| Mirrors > Home > ILE Home > Bibliographic Cross-References | ||
| Bibliographic Reference | Description | Intuitionistic Logic Explorer Page(s) |
|---|---|---|
| [ than ] equality." ([Geuvers], p. 1 | Partness is more basic | expap0 9285 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4262 |
| [Apostol] p. 18 | Theorem I.1 | addcan 7191 addcan2d 7196 addcan2i 7194 addcand 7195 addcani 7193 |
| [Apostol] p. 18 | Theorem I.2 | negeu 7202 |
| [Apostol] p. 18 | Theorem I.3 | negsub 7259 negsubd 7328 negsubi 7289 |
| [Apostol] p. 18 | Theorem I.4 | negneg 7261 negnegd 7313 negnegi 7281 |
| [Apostol] p. 18 | Theorem I.5 | subdi 7382 subdid 7411 subdii 7404 subdir 7383 subdird 7412 subdiri 7405 |
| [Apostol] p. 18 | Theorem I.6 | mul01 7386 mul01d 7390 mul01i 7388 mul02 7384 mul02d 7389 mul02i 7387 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 7768 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 7720 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 7395 mul2negd 7410 mul2negi 7403 mulneg1 7392 mulneg1d 7408 mulneg1i 7401 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 7689 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 8606 rpaddcld 8638 rpmulcl 8607 rpmulcld 8639 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 8616 |
| [Apostol] p. 20 | Theorem I.17 | lttri 7122 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 7529 ltadd1dd 7547 ltadd1i 7494 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 7583 ltmul1a 7582 ltmul1i 7886 ltmul1ii 7894 ltmul2 7822 ltmul2d 8665 ltmul2dd 8679 ltmul2i 7889 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 7141 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 7463 lt0neg1d 7507 ltneg 7457 ltnegd 7514 ltnegi 7485 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 7440 lt2addd 7558 lt2addi 7502 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 8584 |
| [Apostol] p. 21 | Exercise 4 | recgt0 7816 recgt0d 7900 recgt0i 7872 recgt0ii 7873 |
| [Apostol] p. 22 | Definition of integers | df-z 8246 |
| [Apostol] p. 22 | Definition of rationals | df-q 8555 |
| [Apostol] p. 26 | Theorem I.29 | arch 8178 |
| [Apostol] p. 28 | Exercise 2 | btwnz 8357 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 8179 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 9111 |
| [Apostol] p. 28 | Exercise 10(a) | zneo 8339 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 9629 sqrtthi 9715 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 7917 |
| [Apostol] p. 363 | Remark | absgt0api 9742 |
| [Apostol] p. 363 | Example | abssubd 9789 abssubi 9746 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 9183 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 546 pm2.65 585 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5511 onsucelsucexmidlem 4254 |
| [Bauer], p. 483 | Definition | n0rf 3233 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6336 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 6599 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 6512 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 6601 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 6635 addlocpr 6634 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 6661 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 6664 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 6669 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 1903 |
| [BellMachover] p. 460 | Notation | df-mo 1904 |
| [BellMachover] p. 460 | Definition | mo3 1954 mo3h 1953 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2025 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 3878 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 3930 |
| [BellMachover] p. 466 | Axiom Union | axun2 4172 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4267 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4121 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4269 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4222 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4106 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4312 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4336 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1320 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1318 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1321 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5423 fcofo 5424 |
| [BourbakiTop1] p. | Remark | xnegmnf 8742 xnegpnf 8741 |
| [BourbakiTop1] p. | Remark | rexneg 8743 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 3820 |
| [Crosilla] p. | Axiom 1 | ax-ext 2022 |
| [Crosilla] p. | Axiom 2 | ax-pr 3944 |
| [Crosilla] p. | Axiom 3 | ax-un 4170 |
| [Crosilla] p. | Axiom 4 | ax-nul 3883 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4311 |
| [Crosilla] p. | Axiom 6 | ru 2763 |
| [Crosilla] p. | Axiom 8 | ax-pow 3927 |
| [Crosilla] p. | Axiom 9 | ax-setind 4262 |
| [Crosilla], p. | Axiom 6 | ax-sep 3875 |
| [Crosilla], p. | Axiom 7 | ax-coll 3872 |
| [Crosilla], p. | Axiom 7' | repizf 3873 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4247 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5511 |
| [Crosilla], p. | Definition of ordinal | df-iord 4103 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4260 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 2920 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4314 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 3882 |
| [Enderton] p. 19 | Definition | df-tp 3383 |
| [Enderton] p. 26 | Exercise 5 | unissb 3610 |
| [Enderton] p. 26 | Exercise 10 | pwel 3954 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4023 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3726 iinin2m 3725 iunin1 3721 iunin2 3720 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3724 iundif2ss 3722 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 3737 |
| [Enderton] p. 33 | Exercise 25 | iununir 3738 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 3742 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4211 iunpwss 3743 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 3953 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 3943 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4182 rnex 4599 rnexg 4597 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4545 rnuni 4735 |
| [Enderton] p. 42 | Definition of a function | dffun7 4928 dffun8 4929 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5237 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 4960 |
| [Enderton] p. 44 | Definition (d) | dfima2 4670 dfima3 4671 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5242 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5400 |
| [Enderton] p. 53 | Exercise 21 | coass 4839 |
| [Enderton] p. 53 | Exercise 27 | dmco 4829 |
| [Enderton] p. 53 | Exercise 14(a) | funin 4970 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 4701 |
| [Enderton] p. 56 | Theorem 3M | erref 6126 |
| [Enderton] p. 57 | Lemma 3N | erthi 6152 |
| [Enderton] p. 57 | Definition | df-ec 6108 |
| [Enderton] p. 58 | Definition | df-qs 6112 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6211 th3qcor 6210 th3qlem1 6208 th3qlem2 6209 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6108 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4542 |
| [Enderton] p. 68 | Definition of successor | df-suc 4108 |
| [Enderton] p. 71 | Definition | df-tr 3855 dftr4 3859 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4150 unisucg 4151 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4150 unisucg 4151 |
| [Enderton] p. 73 | Exercise 5(a) | truni 3868 |
| [Enderton] p. 73 | Exercise 5(b) | trint 3869 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6053 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6055 onasuc 6046 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5515 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6054 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6056 onmsuc 6052 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6064 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6057 nnacom 6063 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6065 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6066 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6068 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6058 nnmsucr 6067 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6100 |
| [Enderton] p. 129 | Definition | df-en 6222 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6327 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6320 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3299 |
| [Enderton] p. 145 | Figure 38 | ffoss 5158 |
| [Enderton] p. 145 | Definition | df-dom 6223 |
| [Enderton] p. 146 | Example 1 | domen 6232 domeng 6233 |
| [Enderton] p. 146 | Example 3 | nndomo 6326 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6309 xpdom1g 6307 xpdom2g 6306 |
| [Enderton] p. 168 | Definition | df-po 4033 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4165 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4126 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4129 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4242 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4215 |
| [Enderton] p. 194 | Remark | onprc 4276 |
| [Enderton] p. 194 | Exercise 16 | suc11 4282 |
| [Enderton] p. 197 | Definition | df-card 6360 |
| [Enderton] p. 200 | Exercise 25 | tfis 4306 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4278 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4280 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4281 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 7606 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 7635 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 7607 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 7003 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 7573 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 6445 enqer 6456 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 6449 df-nqqs 6446 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 6442 df-plqqs 6447 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 6443 df-mqqs 6448 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 6450 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 6506 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 6509 ltbtwnnq 6514 ltbtwnnqq 6513 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 6498 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 6499 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 6635 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 6677 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 6676 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 6695 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 6711 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 6717 ltaprlem 6716 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 6714 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 6670 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 6690 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 6679 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 6678 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 6686 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 6736 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 6811 enrer 6820 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 6816 df-1r 6817 df-nr 6812 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 6814 df-plr 6813 negexsr 6857 recexsrlem 6859 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 6815 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 7912 creur 7911 cru 7593 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 6995 axcnre 6955 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 9458 crimd 9577 crimi 9537 crre 9457 crred 9576 crrei 9536 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 9460 remimd 9542 |
| [Gleason] p. 133 | Definition 10.36 | absval2 9655 absval2d 9781 absval2i 9740 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 9484 cjaddd 9565 cjaddi 9532 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 9485 cjmuld 9566 cjmuli 9533 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 9483 cjcjd 9543 cjcji 9515 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 9482 cjreb 9466 cjrebd 9546 cjrebi 9518 cjred 9571 rere 9465 rereb 9463 rerebd 9545 rerebi 9517 rered 9569 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 9491 addcjd 9557 addcji 9527 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 9599 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 9650 abscjd 9786 abscji 9744 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 9662 abs00d 9782 abs00i 9741 absne0d 9783 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 9692 releabsd 9787 releabsi 9745 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 9667 absmuld 9790 absmuli 9747 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 9653 sqabsaddi 9748 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 9700 abstrid 9792 abstrii 9751 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 9260 df-iexp 9255 exp0 9259 expp1 9262 expp1d 9382 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 9297 expaddd 9383 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | expmul 9300 expmuld 9384 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 9294 mulexpd 9396 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 8876 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 9846 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 9848 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 9847 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 9851 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 9844 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 9840 climcj 9841 climim 9843 climre 9842 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 7065 df-xr 7064 ltxr 8695 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 9866 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 9142 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 9831 mulcn2 9833 subcn2 9832 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 7 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1338 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 9898 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1314 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1315 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1317 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6077 |
| [HoTT], p. | Section 11.2.1 | df-iltp 6568 df-imp 6567 df-iplp 6566 df-reap 7566 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 6760 |
| [HoTT], p. | Corollary 11.4.3 | conventions 9892 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 6974 caucvgpr 6780 caucvgprpr 6810 caucvgsr 6886 |
| [HoTT], p. | Definition 11.2.1 | df-inp 6564 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4034 ltpopr 6693 ltsopr 6694 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 7597 reapcotr 7589 reapirr 7568 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 7141 gt0add 7564 leadd1 7425 lelttr 7106 lemul1a 7824 lenlt 7094 ltadd1 7424 ltletr 7107 ltmul1 7583 reaplt 7579 |
| [Jech] p. 4 | Definition of class | cv 1242 cvjust 2035 |
| [Jech] p. 78 | Note | opthprc 4391 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1423 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 7649 |
| [Kunen] p. 10 | Axiom 0 | a9e 1586 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 3874 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3667 |
| [Levy] p. 338 | Axiom | df-clab 2027 df-clel 2036 df-cleq 2033 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1314 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1315 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1317 |
| [Margaris] p. 40 | Rule C | exlimiv 1489 |
| [Margaris] p. 49 | Axiom A1 | ax-1 5 |
| [Margaris] p. 49 | Axiom A2 | ax-2 6 |
| [Margaris] p. 49 | Axiom A3 | condc 749 |
| [Margaris] p. 49 | Definition | dfbi2 368 dfordc 791 exalim 1391 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 40 |
| [Margaris] p. 60 | Theorem 8 | mth8 579 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1529 r19.2m 3309 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1446 19.3h 1445 rr19.3v 2682 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1367 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1510 alexim 1536 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1388 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1482 spsbe 1723 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1535 19.9h 1534 19.9v 1751 exlimd 1488 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1554 excomim 1553 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1555 r19.12 2422 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1537 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1357 ralbi 2445 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1447 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1448 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1495 rexbi 2446 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1556 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1346 alimd 1414 alimdh 1356 alimdv 1759 ralimdaa 2386 ralimdv 2388 ralimdva 2387 sbcimdv 2823 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1557 19.21 1475 19.21bi 1450 19.21h 1449 19.21ht 1473 19.21t 1474 19.21v 1753 alrimd 1501 alrimdd 1500 alrimdh 1368 alrimdv 1756 alrimi 1415 alrimih 1358 alrimiv 1754 alrimivv 1755 r19.21 2395 r19.21be 2410 r19.21bi 2407 r19.21t 2394 r19.21v 2396 ralrimd 2397 ralrimdv 2398 ralrimdva 2399 ralrimdvv 2403 ralrimdvva 2404 ralrimi 2390 ralrimiv 2391 ralrimiva 2392 ralrimivv 2400 ralrimivva 2401 ralrimivvva 2402 ralrimivw 2393 rexlimi 2426 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1761 2eximdv 1762 exim 1490 eximd 1503 eximdh 1502 eximdv 1760 rexim 2413 reximdai 2417 reximdv 2420 reximdv2 2418 reximdva 2421 reximdvai 2419 reximi2 2415 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1568 19.23bi 1483 19.23h 1387 19.23ht 1386 19.23t 1567 19.23v 1763 19.23vv 1764 exlimd2 1486 exlimdh 1487 exlimdv 1700 exlimdvv 1777 exlimi 1485 exlimih 1484 exlimiv 1489 exlimivv 1776 r19.23 2424 r19.23v 2425 rexlimd 2430 rexlimdv 2432 rexlimdv3a 2435 rexlimdva 2433 rexlimdvaa 2434 rexlimdvv 2439 rexlimdvva 2440 rexlimdvw 2436 rexlimiv 2427 rexlimiva 2428 rexlimivv 2438 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1530 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1517 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1371 19.26-3an 1372 19.26 1370 r19.26-2 2442 r19.26-3 2443 r19.26 2441 r19.26m 2444 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1453 19.27h 1452 19.27v 1779 r19.27av 2448 r19.27m 3316 r19.27mv 3317 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1455 19.28h 1454 19.28v 1780 r19.28av 2449 r19.28m 3311 r19.28mv 3314 rr19.28v 2683 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1511 19.29r 1512 19.29r2 1513 19.29x 1514 r19.29 2450 r19.29d2r 2455 r19.29r 2451 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1518 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1571 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1569 19.32r 1570 r19.32r 2457 r19.32vdc 2459 r19.32vr 2458 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1373 19.33b2 1520 19.33bdc 1521 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1574 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1515 19.35i 1516 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1563 19.36aiv 1781 19.36i 1562 r19.36av 2461 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1564 19.37aiv 1565 r19.37 2462 r19.37av 2463 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1566 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1531 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1523 19.40 1522 r19.40 2464 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1576 19.41h 1575 19.41v 1782 19.41vv 1783 19.41vvv 1784 19.41vvvv 1785 r19.41 2465 r19.41v 2466 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1578 19.42h 1577 19.42v 1786 19.42vv 1788 19.42vvv 1789 19.42vvvv 1790 r19.42v 2467 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1519 r19.43 2468 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1572 r19.44av 2469 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1573 r19.45av 2470 r19.45mv 3315 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 1925 |
| [Megill] p. 444 | Axiom C5 | ax-17 1419 |
| [Megill] p. 445 | Lemma L12 | alequcom 1408 ax-10 1396 |
| [Megill] p. 446 | Lemma L17 | equtrr 1596 |
| [Megill] p. 446 | Lemma L19 | hbnae 1609 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1646 sbid 1657 |
| [Megill] p. 448 | Scheme C5' | ax-4 1400 |
| [Megill] p. 448 | Scheme C6' | ax-7 1337 |
| [Megill] p. 448 | Scheme C8' | ax-8 1395 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1398 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1604 |
| [Megill] p. 448 | Scheme C12' | ax-13 1404 |
| [Megill] p. 448 | Scheme C13' | ax-14 1405 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1704 |
| [Megill] p. 448 | Scheme C16' | ax-16 1695 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1618 dral2 1619 drex1 1679 drex2 1620 drsb1 1680 drsb2 1722 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 1863 sbequ 1721 sbid2v 1872 |
| [Megill] p. 450 | Example in Appendix | hba1 1433 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 2840 rspsbca 2841 stdpc4 1658 |
| [Mendelson] p. 69 | Axiom 5 | ra5 2846 stdpc5 1476 |
| [Mendelson] p. 81 | Rule C | exlimiv 1489 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1591 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1653 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3253 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3254 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3177 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3225 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3178 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3075 |
| [Mendelson] p. 231 | Definition of union | unssin 3176 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4207 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3579 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4019 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4020 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4021 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3600 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4465 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 4841 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4108 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6295 xpsneng 6296 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6301 xpcomeng 6302 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6304 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6298 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6047 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3159 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4428 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4429 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 3819 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 4836 coi2 4837 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4549 rn0 4588 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 4728 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4447 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4555 rnxpm 4752 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4420 xp0 4743 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 4684 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 4681 |
| [Monk1] p. 39 | Theorem 3.17 | imaexg 4680 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 4679 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5297 funfvop 5279 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5217 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5225 |
| [Monk1] p. 43 | Theorem 4.6 | funun 4944 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5407 dff13f 5409 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5384 funrnex 5741 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5401 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 4804 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3631 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 5782 df-1st 5767 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 5783 df-2nd 5768 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1336 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1395 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1397 ax-11o 1704 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1708 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1337 |
| [Monk2] p. 109 | Lemma 15 | equvin 1743 equvini 1641 eqvinop 3980 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1419 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1541 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1337 |
| [Monk2] p. 114 | Lemma 22 | hba1 1433 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1444 nfia1 1472 |
| [Monk2] p. 114 | Lemma 24 | hba2 1443 nfa2 1471 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 740 dftest 822 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2027 rabid 2485 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 1867 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2033 |
| [Quine] p. 19 | Definition 2.9 | df-v 2559 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2146 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2158 abid2f 2202 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1767 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1765 sb6 1766 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2036 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2040 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2042 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 2765 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 2766 dfsbcq2 2767 |
| [Quine] p. 43 | Theorem 6.8 | vex 2560 |
| [Quine] p. 43 | Theorem 6.9 | isset 2561 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2635 spcgv 2640 spcimgf 2633 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 2775 spsbcd 2776 |
| [Quine] p. 44 | Theorem 6.12 | elex 2566 |
| [Quine] p. 44 | Theorem 6.13 | elab 2687 elabg 2688 elabgf 2685 |
| [Quine] p. 44 | Theorem 6.14 | noel 3228 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3435 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3382 df-sn 3381 |
| [Quine] p. 49 | Theorem 7.4 | snss 3494 snssg 3500 |
| [Quine] p. 49 | Theorem 7.5 | prss 3520 prssg 3521 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3476 prid1g 3474 prid2 3477 prid2g 3475 snid 3402 snidg 3400 |
| [Quine] p. 51 | Theorem 7.12 | snexg 3936 snexprc 3938 |
| [Quine] p. 51 | Theorem 7.13 | prexg 3947 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3596 unisng 3597 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3599 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3608 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3607 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 4877 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 4868 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 4878 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 4882 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 4883 |
| [Quine] p. 58 | Definition 9.1 | df-op 3384 |
| [Quine] p. 61 | Theorem 9.5 | opabid 3994 opelopab 4008 opelopaba 4003 opelopabaf 4010 opelopabf 4011 opelopabg 4005 opelopabga 4000 oprabid 5537 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4351 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4353 |
| [Quine] p. 64 | Definition 9.15 | df-id 4030 |
| [Quine] p. 65 | Theorem 10.3 | fun0 4957 |
| [Quine] p. 65 | Theorem 10.4 | funi 4932 |
| [Quine] p. 65 | Theorem 10.5 | funsn 4948 funsng 4946 |
| [Quine] p. 65 | Definition 10.1 | df-fun 4904 |
| [Quine] p. 65 | Definition 10.2 | args 4694 dffv4g 5175 |
| [Quine] p. 68 | Definition 10.11 | df-fv 4910 fv2 5173 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 4984 funimaexg 4983 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1317 |
| [Sanford] p. 39 | Rule 4 | mptxor 1315 |
| [Sanford] p. 40 | Rule 1 | mptnan 1314 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 4709 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 4711 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 4708 |
| [Schechter] p. 51 | Definition of transitivity | cotr 4706 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3202 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3295 dif0 3294 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3307 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3195 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3196 |
| [Stoll] p. 20 | Remark | invdif 3179 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3385 |
| [Stoll] p. 43 | Definition | uniiun 3710 |
| [Stoll] p. 44 | Definition | intiin 3711 |
| [Stoll] p. 45 | Definition | df-iin 3660 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3659 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 786 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3202 |
| [Suppes] p. 22 | Theorem 2 | eq0 3239 |
| [Suppes] p. 22 | Theorem 4 | eqss 2960 eqssd 2962 eqssi 2961 |
| [Suppes] p. 23 | Theorem 5 | ss0 3257 ss0b 3256 |
| [Suppes] p. 23 | Theorem 6 | sstr 2953 |
| [Suppes] p. 23 | Theorem 7 | pssirr 3044 |
| [Suppes] p. 23 | Theorem 8 | pssn2lp 3045 |
| [Suppes] p. 23 | Theorem 9 | psstr 3049 |
| [Suppes] p. 23 | Theorem 10 | pssss 3039 |
| [Suppes] p. 25 | Theorem 12 | elin 3126 elun 3084 |
| [Suppes] p. 26 | Theorem 15 | inidm 3146 |
| [Suppes] p. 26 | Theorem 16 | in0 3252 |
| [Suppes] p. 27 | Theorem 23 | unidm 3086 |
| [Suppes] p. 27 | Theorem 24 | un0 3251 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3106 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3113 |
| [Suppes] p. 27 | Theorem 27 | unss 3117 |
| [Suppes] p. 27 | Theorem 28 | indir 3186 |
| [Suppes] p. 27 | Theorem 29 | undir 3187 |
| [Suppes] p. 28 | Theorem 32 | difid 3292 difidALT 3293 |
| [Suppes] p. 29 | Theorem 33 | difin 3174 |
| [Suppes] p. 29 | Theorem 34 | indif 3180 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3298 |
| [Suppes] p. 29 | Theorem 36 | difun2 3302 |
| [Suppes] p. 29 | Theorem 37 | difin0 3297 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3296 |
| [Suppes] p. 29 | Theorem 39 | difundi 3189 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3191 |
| [Suppes] p. 30 | Theorem 41 | nalset 3887 |
| [Suppes] p. 39 | Theorem 61 | uniss 3601 |
| [Suppes] p. 39 | Theorem 65 | uniop 3992 |
| [Suppes] p. 41 | Theorem 70 | intsn 3650 |
| [Suppes] p. 42 | Theorem 71 | intpr 3647 intprg 3648 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4209 op1stbg 4210 |
| [Suppes] p. 42 | Theorem 78 | intun 3646 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3691 dfiun2g 3689 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3692 |
| [Suppes] p. 47 | Theorem 86 | elpw 3365 elpw2 3911 elpw2g 3910 elpwg 3367 |
| [Suppes] p. 47 | Theorem 87 | pwid 3373 |
| [Suppes] p. 47 | Theorem 89 | pw0 3511 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3575 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4445 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4471 xpindir 4472 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4396 xpundir 4397 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4272 |
| [Suppes] p. 58 | Theorem 2 | relss 4427 |
| [Suppes] p. 59 | Theorem 4 | eldm 4532 eldm2 4533 eldm2g 4531 eldmg 4530 |
| [Suppes] p. 59 | Definition 3 | df-dm 4355 |
| [Suppes] p. 60 | Theorem 6 | dmin 4543 |
| [Suppes] p. 60 | Theorem 8 | rnun 4732 |
| [Suppes] p. 60 | Theorem 9 | rnin 4733 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4523 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4518 brcnvg 4516 |
| [Suppes] p. 62 | Equation 5 | elcnv 4512 elcnv2 4513 |
| [Suppes] p. 62 | Theorem 12 | relcnv 4703 |
| [Suppes] p. 62 | Theorem 15 | cnvin 4731 |
| [Suppes] p. 62 | Theorem 16 | cnvun 4729 |
| [Suppes] p. 63 | Theorem 20 | co02 4834 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4601 |
| [Suppes] p. 63 | Definition 7 | df-co 4354 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4520 |
| [Suppes] p. 64 | Theorem 27 | coass 4839 |
| [Suppes] p. 65 | Theorem 31 | resundi 4625 |
| [Suppes] p. 65 | Theorem 34 | elima 4673 elima2 4674 elima3 4675 elimag 4672 |
| [Suppes] p. 65 | Theorem 35 | imaundi 4736 |
| [Suppes] p. 66 | Theorem 40 | dminss 4738 |
| [Suppes] p. 66 | Theorem 41 | imainss 4739 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 4742 |
| [Suppes] p. 81 | Definition 34 | dfec2 6109 |
| [Suppes] p. 82 | Theorem 72 | elec 6145 elecg 6144 |
| [Suppes] p. 82 | Theorem 73 | erth 6150 erth2 6151 |
| [Suppes] p. 92 | Theorem 1 | enref 6245 enrefg 6244 |
| [Suppes] p. 92 | Theorem 2 | ensym 6261 ensymb 6260 ensymi 6262 |
| [Suppes] p. 92 | Theorem 3 | entr 6264 |
| [Suppes] p. 92 | Theorem 4 | unen 6293 |
| [Suppes] p. 94 | Theorem 15 | endom 6243 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6258 |
| [Suppes] p. 94 | Theorem 17 | domtr 6265 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6286 fundmeng 6287 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6308 |
| [Suppes] p. 130 | Definition 3 | df-tr 3855 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4214 |
| [Suppes] p. 134 | Definition 6 | df-suc 4108 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4326 finds 4323 finds1 4325 finds2 4324 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 6451 df-ltpq 6444 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4127 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2022 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2033 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2036 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2035 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2057 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5516 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2763 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3396 elpr2 3397 elprg 3395 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3391 elsn2 3405 elsn2g 3404 elsng 3390 velsn 3392 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 3968 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3386 sneqr 3531 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3394 dfsn2 3389 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4174 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 3974 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 3951 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4176 unexg 4178 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3419 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3581 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 2924 df-un 2922 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3594 uniprg 3595 |
| [TakeutiZaring] p. 17 | Axiom 4 | pwex 3932 pwexg 3933 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3418 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4143 elsucg 4141 sstr2 2952 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3087 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3129 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3100 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3147 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3184 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3185 |
| [TakeutiZaring] p. 17 | Definition 5.9 | df-pss 2933 dfss2 2934 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3361 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3114 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 2931 sseqin2 3156 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 2964 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3157 inss2 3158 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3003 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3589 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 3952 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 3959 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2315 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 3884 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 2920 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3226 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3292 difidALT 3293 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3233 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4264 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2559 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 3888 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3255 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 3894 ssexg 3896 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 3891 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4274 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4266 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3286 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3069 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3198 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3070 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3077 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2311 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2312 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4453 xpexg 4452 xpexgALT 5760 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4352 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 4963 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5100 fun11 4966 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 4913 svrelfun 4964 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4522 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4524 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4357 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4358 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4354 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 4775 dfrel2 4771 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4446 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4454 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4460 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4470 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4639 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4617 opelresg 4619 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4632 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4635 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4640 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 4941 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 4819 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 4940 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5101 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 1944 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 4910 fv3 5197 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 4856 cnvexg 4855 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4598 dmexg 4596 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4599 rnexg 4597 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5192 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5200 tz6.12 5201 tz6.12c 5203 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5169 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 4905 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 4906 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 4908 wfo 4900 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 4907 wf1 4899 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 4909 wf1o 4901 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5265 eqfnfv2 5266 eqfnfv2f 5269 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5243 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5383 fnexALT 5740 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5382 resfunexgALT 5737 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 4984 funimaexg 4983 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 3765 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 4695 iniseg 4697 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4026 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 4911 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5450 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5451 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5456 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5457 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5465 |
| [TakeutiZaring] p. 35 | Notation | wtr 3854 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4091 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 3858 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4300 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4118 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4122 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4218 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4105 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4212 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4276 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4305 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 3856 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4237 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4213 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3608 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4108 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4152 sucidg 4153 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 4227 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4106 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4232 ordelsuc 4231 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4317 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4318 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4319 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4316 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4329 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4322 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4320 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4321 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3629 trint0m 3871 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3630 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4243 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3616 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 5923 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 5951 tfri1d 5949 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 5952 tfri2d 5950 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 5953 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 5917 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 5901 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6044 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6040 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6037 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6041 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6082 nnaordi 6081 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3702 uniss2 3611 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6059 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6050 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6038 omsuc 6051 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6060 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6090 nnmordi 6089 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6039 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 6367 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6275 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6320 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6321 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6224 isfi 6241 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6305 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1400 |
| [Tarski] p. 68 | Lemma 6 | equid 1589 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1592 |
| [Tarski] p. 70 | Lemma 14 | spim 1626 spime 1629 spimeh 1627 spimh 1625 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1397 ax-11o 1704 ax11i 1602 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1766 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1419 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 1404 ax-14 1405 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 632 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 646 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 673 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 682 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 703 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 546 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 5 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 572 |
| [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.1dc 745 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 1998 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 656 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 744 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 559 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 779 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 751 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 753 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 571 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 749 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 750 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 633 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 692 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 547 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 551 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 792 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 813 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 35 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 685 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 686 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 717 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 718 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 716 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 886 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 695 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 693 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 694 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 47 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 657 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 658 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 763 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 759 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 659 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 660 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 661 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 581 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 582 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 641 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 790 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 644 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 645 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 762 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 667 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 713 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 714 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 585 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 634 pm2.67 662 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 764 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 666 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 723 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 793 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 821 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 719 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 720 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 722 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 721 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 6 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 724 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 725 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 71 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 811 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 94 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 671 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 126 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 864 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 865 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 866 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 670 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 251 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 252 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 627 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 329 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 248 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 249 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 102 simplimdc 757 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 103 simprimdc 756 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 327 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 328 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37dc 788 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 529 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 316 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 314 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 315 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 672 pm3.44 635 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | prth 326 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 534 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 699 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 765 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 160 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 766 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 787 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 789 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 128 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 859 bitr 441 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 375 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 674 pm4.25 675 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 253 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 731 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 647 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 381 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 684 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 439 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 706 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 537 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 735 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 887 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 729 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 878 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 856 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 696 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 727 pm4.45 698 pm4.45im 317 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1370 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 863 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 796 imorr 797 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 302 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 799 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 803 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 804 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 805 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 846 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 669 pm4.56 806 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | oranim 807 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 782 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 798 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 780 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 801 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 783 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 802 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 781 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 369 pm4.71d 373 pm4.71i 371 pm4.71r 370 pm4.71rd 374 pm4.71ri 372 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 736 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 284 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 663 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 535 pm4.76 536 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 631 pm4.77 712 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 808 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 809 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 623 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 814 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 857 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 858 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 225 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 226 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 229 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 237 impexp 250 pm4.87 493 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 533 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 815 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 816 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 818 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 817 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1280 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 737 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 810 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1285 pm5.18dc 777 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 622 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 611 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1283 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1288 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1289 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 794 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 444 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 238 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 231 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 835 pm5.6r 836 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 861 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 330 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 426 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 541 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 826 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 542 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 239 pm5.41 240 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 303 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 834 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 715 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 827 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 819 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 708 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 852 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 853 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 868 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 233 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 168 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 869 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1526 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1374 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1523 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1775 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 1903 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2286 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2287 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2681 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 2815 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 4885 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 4886 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 1979 eupickbi 1982 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 4910 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |