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 9506 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4280 |
| [Apostol] p. 18 | Theorem I.1 | addcan 7288 addcan2d 7293 addcan2i 7291 addcand 7292 addcani 7290 |
| [Apostol] p. 18 | Theorem I.2 | negeu 7299 |
| [Apostol] p. 18 | Theorem I.3 | negsub 7356 negsubd 7425 negsubi 7386 |
| [Apostol] p. 18 | Theorem I.4 | negneg 7358 negnegd 7410 negnegi 7378 |
| [Apostol] p. 18 | Theorem I.5 | subdi 7489 subdid 7518 subdii 7511 subdir 7490 subdird 7519 subdiri 7512 |
| [Apostol] p. 18 | Theorem I.6 | mul01 7493 mul01d 7497 mul01i 7495 mul02 7491 mul02d 7496 mul02i 7494 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 7880 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 7832 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 7502 mul2negd 7517 mul2negi 7510 mulneg1 7499 mulneg1d 7515 mulneg1i 7508 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 7801 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 8757 rpaddcld 8789 rpmulcl 8758 rpmulcld 8790 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 8767 |
| [Apostol] p. 20 | Theorem I.17 | lttri 7215 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 7638 ltadd1dd 7656 ltadd1i 7603 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 7692 ltmul1a 7691 ltmul1i 7998 ltmul1ii 8006 ltmul2 7934 ltmul2d 8816 ltmul2dd 8830 ltmul2i 8001 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 7236 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 7572 lt0neg1d 7616 ltneg 7566 ltnegd 7623 ltnegi 7594 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 7549 lt2addd 7667 lt2addi 7611 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 8735 |
| [Apostol] p. 21 | Exercise 4 | recgt0 7928 recgt0d 8012 recgt0i 7984 recgt0ii 7985 |
| [Apostol] p. 22 | Definition of integers | df-z 8352 |
| [Apostol] p. 22 | Definition of rationals | df-q 8705 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 6407 |
| [Apostol] p. 26 | Theorem I.29 | arch 8285 |
| [Apostol] p. 28 | Exercise 2 | btwnz 8466 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 8286 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 9265 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 10270 zneo 8448 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 9917 sqrtthi 10005 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 8042 |
| [Apostol] p. 363 | Remark | absgt0api 10032 |
| [Apostol] p. 363 | Example | abssubd 10079 abssubi 10036 |
| [ApostolNT] p. 14 | Definition | df-dvds 10196 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 10208 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 10232 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 10228 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 10222 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 10224 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 10209 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 10210 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 10215 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 10245 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 10247 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 10249 |
| [ApostolNT] p. 15 | Definition | dfgcd2 10403 |
| [ApostolNT] p. 16 | Definition | isprm2 10499 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 10474 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 10365 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 10404 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 10406 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 10378 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 10371 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 10523 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 10525 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 10324 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucialg 10441 |
| [ApostolNT] p. 104 | Definition | congr 10482 |
| [ApostolNT] p. 106 | Remark | dvdsval3 10199 |
| [ApostolNT] p. 106 | Definition | moddvds 10204 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 10277 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 10279 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 9343 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 9380 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 10227 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 10485 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 10487 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 578 pm2.65 617 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5531 onsucelsucexmidlem 4272 |
| [Bauer], p. 483 | Definition | n0rf 3260 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6361 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 6691 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 6604 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 6693 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 6727 addlocpr 6726 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 6753 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 6756 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 6761 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 1944 |
| [BellMachover] p. 460 | Notation | df-mo 1945 |
| [BellMachover] p. 460 | Definition | mo3 1995 mo3h 1994 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2066 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 3899 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 3951 |
| [BellMachover] p. 466 | Axiom Union | axun2 4190 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4285 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4139 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4288 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4240 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4124 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4330 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4354 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1360 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1358 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1361 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5443 fcofo 5444 |
| [BourbakiTop1] p. | Remark | xnegmnf 8896 xnegpnf 8895 |
| [BourbakiTop1] p. | Remark | rexneg 8897 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 3841 |
| [Crosilla] p. | Axiom 1 | ax-ext 2063 |
| [Crosilla] p. | Axiom 2 | ax-pr 3964 |
| [Crosilla] p. | Axiom 3 | ax-un 4188 |
| [Crosilla] p. | Axiom 4 | ax-nul 3904 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4329 |
| [Crosilla] p. | Axiom 6 | ru 2814 |
| [Crosilla] p. | Axiom 8 | ax-pow 3948 |
| [Crosilla] p. | Axiom 9 | ax-setind 4280 |
| [Crosilla], p. | Axiom 6 | ax-sep 3896 |
| [Crosilla], p. | Axiom 7 | ax-coll 3893 |
| [Crosilla], p. | Axiom 7' | repizf 3894 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4265 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5531 |
| [Crosilla], p. | Definition of ordinal | df-iord 4121 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4278 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 2975 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4332 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 3903 |
| [Enderton] p. 19 | Definition | df-tp 3406 |
| [Enderton] p. 26 | Exercise 5 | unissb 3631 |
| [Enderton] p. 26 | Exercise 10 | pwel 3973 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4041 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3747 iinin2m 3746 iunin1 3742 iunin2 3741 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3745 iundif2ss 3743 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 3758 |
| [Enderton] p. 33 | Exercise 25 | iununir 3759 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 3763 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4229 iunpwss 3764 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 3972 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 3963 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4200 rnex 4617 rnexg 4615 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4563 rnuni 4755 |
| [Enderton] p. 42 | Definition of a function | dffun7 4948 dffun8 4949 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5258 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 4980 |
| [Enderton] p. 44 | Definition (d) | dfima2 4690 dfima3 4691 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5263 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5421 |
| [Enderton] p. 53 | Exercise 21 | coass 4859 |
| [Enderton] p. 53 | Exercise 27 | dmco 4849 |
| [Enderton] p. 53 | Exercise 14(a) | funin 4990 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 4721 |
| [Enderton] p. 56 | Theorem 3M | erref 6149 |
| [Enderton] p. 57 | Lemma 3N | erthi 6175 |
| [Enderton] p. 57 | Definition | df-ec 6131 |
| [Enderton] p. 58 | Definition | df-qs 6135 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6234 th3qcor 6233 th3qlem1 6231 th3qlem2 6232 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6131 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4560 |
| [Enderton] p. 68 | Definition of successor | df-suc 4126 |
| [Enderton] p. 71 | Definition | df-tr 3876 dftr4 3880 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4168 unisucg 4169 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4168 unisucg 4169 |
| [Enderton] p. 73 | Exercise 5(a) | truni 3889 |
| [Enderton] p. 73 | Exercise 5(b) | trint 3890 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6076 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6078 onasuc 6069 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5535 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6077 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6079 onmsuc 6075 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6087 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6080 nnacom 6086 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6088 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6089 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6091 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6081 nnmsucr 6090 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6123 |
| [Enderton] p. 129 | Definition | df-en 6245 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6351 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6343 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3319 |
| [Enderton] p. 145 | Figure 38 | ffoss 5178 |
| [Enderton] p. 145 | Definition | df-dom 6246 |
| [Enderton] p. 146 | Example 1 | domen 6255 domeng 6256 |
| [Enderton] p. 146 | Example 3 | nndomo 6350 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6332 xpdom1g 6330 xpdom2g 6329 |
| [Enderton] p. 168 | Definition | df-po 4051 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4183 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4144 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4286 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4147 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4260 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4233 |
| [Enderton] p. 194 | Remark | onprc 4295 |
| [Enderton] p. 194 | Exercise 16 | suc11 4301 |
| [Enderton] p. 197 | Definition | df-card 6449 |
| [Enderton] p. 200 | Exercise 25 | tfis 4324 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4297 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4299 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4300 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 7715 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 7744 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 7716 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 7095 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 10089 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 10097 maxle2 10098 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 10099 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 10102 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 10103 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 7682 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 6537 enqer 6548 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 6541 df-nqqs 6538 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 6534 df-plqqs 6539 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 6535 df-mqqs 6540 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 6542 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 6598 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 6601 ltbtwnnq 6606 ltbtwnnqq 6605 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 6590 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 6591 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 6727 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 6769 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 6768 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 6787 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 6803 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 6809 ltaprlem 6808 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 6806 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 6762 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 6782 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 6771 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 6770 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 6778 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 6828 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 6903 enrer 6912 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 6908 df-1r 6909 df-nr 6904 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 6906 df-plr 6905 negexsr 6949 recexsrlem 6951 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 6907 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 8037 creur 8036 cru 7702 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 7087 axcnre 7047 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 9745 crimd 9864 crimi 9824 crre 9744 crred 9863 crrei 9823 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 9747 remimd 9829 |
| [Gleason] p. 133 | Definition 10.36 | absval2 9943 absval2d 10071 absval2i 10030 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 9771 cjaddd 9852 cjaddi 9819 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 9772 cjmuld 9853 cjmuli 9820 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 9770 cjcjd 9830 cjcji 9802 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 9769 cjreb 9753 cjrebd 9833 cjrebi 9805 cjred 9858 rere 9752 rereb 9750 rerebd 9832 rerebi 9804 rered 9856 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 9778 addcjd 9844 addcji 9814 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 9887 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 9938 abscjd 10076 abscji 10034 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 9950 abs00d 10072 abs00i 10031 absne0d 10073 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 9982 releabsd 10077 releabsi 10035 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 9955 absmuld 10080 absmuli 10037 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 9941 sqabsaddi 10038 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 9990 abstrid 10082 abstrii 10041 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 9481 df-iexp 9476 exp0 9480 expp1 9483 expp1d 9606 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 9518 expaddd 9607 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | expmul 9521 expmuld 9608 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 9515 mulexpd 9620 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 9031 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 10164 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 10166 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 10165 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 10169 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 10162 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 10158 climcj 10159 climim 10161 climre 10160 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 7158 df-xr 7157 ltxr 8849 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 10184 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 9302 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 10149 mulcn2 10151 subcn2 10150 |
| [Gleason] p. 295 | Remark | bcval3 9678 bcval4 9679 |
| [Gleason] p. 295 | Equation 2 | bcpasc 9693 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 9676 df-bc 9675 |
| [Gleason] p. 296 | Remark | bcn0 9682 bcnn 9684 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 7 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1378 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 10786 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1354 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1355 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1357 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6100 |
| [HoTT], p. | Section 11.2.1 | df-iltp 6660 df-imp 6659 df-iplp 6658 df-reap 7675 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 6852 |
| [HoTT], p. | Corollary 11.4.3 | conventions 10559 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 7066 caucvgpr 6872 caucvgprpr 6902 caucvgsr 6978 |
| [HoTT], p. | Definition 11.2.1 | df-inp 6656 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4052 ltpopr 6785 ltsopr 6786 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 7706 reapcotr 7698 reapirr 7677 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 7236 gt0add 7673 leadd1 7534 lelttr 7199 lemul1a 7936 lenlt 7187 ltadd1 7533 ltletr 7200 ltmul1 7692 reaplt 7688 |
| [Jech] p. 4 | Definition of class | cv 1283 cvjust 2076 |
| [Jech] p. 78 | Note | opthprc 4409 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1463 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 7758 |
| [Kunen] p. 10 | Axiom 0 | a9e 1626 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 3895 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3688 |
| [Levy] p. 338 | Axiom | df-clab 2068 df-clel 2077 df-cleq 2074 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1354 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1355 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1357 |
| [Margaris] p. 40 | Rule C | exlimiv 1529 |
| [Margaris] p. 49 | Axiom A1 | ax-1 5 |
| [Margaris] p. 49 | Axiom A2 | ax-2 6 |
| [Margaris] p. 49 | Axiom A3 | condc 782 |
| [Margaris] p. 49 | Definition | dfbi2 380 dfordc 824 exalim 1431 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 44 |
| [Margaris] p. 60 | Theorem 8 | mth8 611 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1569 r19.2m 3329 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1486 19.3h 1485 rr19.3v 2733 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1407 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1550 alexim 1576 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1428 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1522 spsbe 1763 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1575 19.9h 1574 19.9v 1792 exlimd 1528 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1594 excomim 1593 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1595 r19.12 2466 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1577 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1397 ralbi 2489 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1487 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1488 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1535 rexbi 2490 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1596 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1386 alimd 1454 alimdh 1396 alimdv 1800 ralimdaa 2428 ralimdv 2430 ralimdva 2429 sbcimdv 2879 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1597 19.21 1515 19.21bi 1490 19.21h 1489 19.21ht 1513 19.21t 1514 19.21v 1794 alrimd 1541 alrimdd 1540 alrimdh 1408 alrimdv 1797 alrimi 1455 alrimih 1398 alrimiv 1795 alrimivv 1796 r19.21 2437 r19.21be 2452 r19.21bi 2449 r19.21t 2436 r19.21v 2438 ralrimd 2439 ralrimdv 2440 ralrimdva 2441 ralrimdvv 2445 ralrimdvva 2446 ralrimi 2432 ralrimiv 2433 ralrimiva 2434 ralrimivv 2442 ralrimivva 2443 ralrimivvva 2444 ralrimivw 2435 rexlimi 2470 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1802 2eximdv 1803 exim 1530 eximd 1543 eximdh 1542 eximdv 1801 rexim 2455 reximdai 2459 reximddv 2464 reximddv2 2465 reximdv 2462 reximdv2 2460 reximdva 2463 reximdvai 2461 reximi2 2457 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1608 19.23bi 1523 19.23h 1427 19.23ht 1426 19.23t 1607 19.23v 1804 19.23vv 1805 exlimd2 1526 exlimdh 1527 exlimdv 1740 exlimdvv 1818 exlimi 1525 exlimih 1524 exlimiv 1529 exlimivv 1817 r19.23 2468 r19.23v 2469 rexlimd 2474 rexlimdv 2476 rexlimdv3a 2479 rexlimdva 2477 rexlimdvaa 2478 rexlimdvv 2483 rexlimdvva 2484 rexlimdvw 2480 rexlimiv 2471 rexlimiva 2472 rexlimivv 2482 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1570 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1557 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1411 19.26-3an 1412 19.26 1410 r19.26-2 2486 r19.26-3 2487 r19.26 2485 r19.26m 2488 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1493 19.27h 1492 19.27v 1820 r19.27av 2492 r19.27m 3336 r19.27mv 3337 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1495 19.28h 1494 19.28v 1821 r19.28av 2493 r19.28m 3331 r19.28mv 3334 rr19.28v 2734 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1551 19.29r 1552 19.29r2 1553 19.29x 1554 r19.29 2494 r19.29d2r 2499 r19.29r 2495 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1558 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1611 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1609 19.32r 1610 r19.32r 2501 r19.32vdc 2503 r19.32vr 2502 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1413 19.33b2 1560 19.33bdc 1561 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1614 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1555 19.35i 1556 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1603 19.36aiv 1822 19.36i 1602 r19.36av 2505 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1604 19.37aiv 1605 r19.37 2506 r19.37av 2507 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1606 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1571 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1563 19.40 1562 r19.40 2508 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1616 19.41h 1615 19.41v 1823 19.41vv 1824 19.41vvv 1825 19.41vvvv 1826 r19.41 2509 r19.41v 2510 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1618 19.42h 1617 19.42v 1827 19.42vv 1829 19.42vvv 1830 19.42vvvv 1831 r19.42v 2511 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1559 r19.43 2512 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1612 r19.44av 2513 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1613 r19.45av 2514 r19.45mv 3335 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 1966 |
| [Megill] p. 444 | Axiom C5 | ax-17 1459 |
| [Megill] p. 445 | Lemma L12 | alequcom 1448 ax-10 1436 |
| [Megill] p. 446 | Lemma L17 | equtrr 1636 |
| [Megill] p. 446 | Lemma L19 | hbnae 1649 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1686 sbid 1697 |
| [Megill] p. 448 | Scheme C5' | ax-4 1440 |
| [Megill] p. 448 | Scheme C6' | ax-7 1377 |
| [Megill] p. 448 | Scheme C8' | ax-8 1435 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1438 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1644 |
| [Megill] p. 448 | Scheme C12' | ax-13 1444 |
| [Megill] p. 448 | Scheme C13' | ax-14 1445 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1744 |
| [Megill] p. 448 | Scheme C16' | ax-16 1735 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1658 dral2 1659 drex1 1719 drex2 1660 drsb1 1720 drsb2 1762 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 1904 sbequ 1761 sbid2v 1913 |
| [Megill] p. 450 | Example in Appendix | hba1 1473 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 2896 rspsbca 2897 stdpc4 1698 |
| [Mendelson] p. 69 | Axiom 5 | ra5 2902 stdpc5 1516 |
| [Mendelson] p. 81 | Rule C | exlimiv 1529 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1631 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1693 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3280 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3281 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3204 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3252 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3205 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3103 |
| [Mendelson] p. 231 | Definition of union | unssin 3203 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4225 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3600 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4037 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4038 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4039 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3621 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4483 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 4861 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4126 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6318 xpsneng 6319 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6324 xpcomeng 6325 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6327 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6321 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6070 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3188 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4446 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4447 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 3840 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 4856 coi2 4857 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4567 rn0 4606 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 4748 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4465 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4573 rnxpm 4772 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4438 xp0 4763 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 4704 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 4701 |
| [Monk1] p. 39 | Theorem 3.17 | imaexg 4700 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 4699 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5318 funfvop 5300 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5238 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5246 |
| [Monk1] p. 43 | Theorem 4.6 | funun 4964 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5428 dff13f 5430 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5405 funrnex 5761 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5422 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 4824 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3652 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 5802 df-1st 5787 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 5803 df-2nd 5788 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1376 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1435 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1437 ax-11o 1744 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1748 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1377 |
| [Monk2] p. 109 | Lemma 15 | equvin 1784 equvini 1681 eqvinop 3998 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1459 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1581 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1377 |
| [Monk2] p. 114 | Lemma 22 | hba1 1473 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1484 nfia1 1512 |
| [Monk2] p. 114 | Lemma 24 | hba2 1483 nfa2 1511 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 773 dftest 855 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2068 rabid 2529 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 1908 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2074 |
| [Quine] p. 19 | Definition 2.9 | df-v 2603 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2187 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2199 abid2f 2243 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1808 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1806 sb6 1807 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2077 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2081 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2083 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 2816 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 2817 dfsbcq2 2818 |
| [Quine] p. 43 | Theorem 6.8 | vex 2604 |
| [Quine] p. 43 | Theorem 6.9 | isset 2605 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2680 spcgv 2685 spcimgf 2678 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 2826 spsbcd 2827 |
| [Quine] p. 44 | Theorem 6.12 | elex 2610 |
| [Quine] p. 44 | Theorem 6.13 | elab 2738 elabg 2739 elabgf 2736 |
| [Quine] p. 44 | Theorem 6.14 | noel 3255 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3457 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3405 df-sn 3404 |
| [Quine] p. 49 | Theorem 7.4 | snss 3516 snssg 3522 |
| [Quine] p. 49 | Theorem 7.5 | prss 3541 prssg 3542 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3498 prid1g 3496 prid2 3499 prid2g 3497 snid 3425 snidg 3423 |
| [Quine] p. 51 | Theorem 7.12 | snexg 3956 snexprc 3958 |
| [Quine] p. 51 | Theorem 7.13 | prexg 3966 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3617 unisng 3618 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3620 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3629 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3628 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 4897 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 4888 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 4898 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 4902 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 4903 |
| [Quine] p. 58 | Definition 9.1 | df-op 3407 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4012 opelopab 4026 opelopaba 4021 opelopabaf 4028 opelopabf 4029 opelopabg 4023 opelopabga 4018 oprabid 5557 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4369 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4371 |
| [Quine] p. 64 | Definition 9.15 | df-id 4048 |
| [Quine] p. 65 | Theorem 10.3 | fun0 4977 |
| [Quine] p. 65 | Theorem 10.4 | funi 4952 |
| [Quine] p. 65 | Theorem 10.5 | funsn 4968 funsng 4966 |
| [Quine] p. 65 | Definition 10.1 | df-fun 4924 |
| [Quine] p. 65 | Definition 10.2 | args 4714 dffv4g 5195 |
| [Quine] p. 68 | Definition 10.11 | df-fv 4930 fv2 5193 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 9651 nn0opth2d 9650 nn0opthd 9649 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5004 funimaexg 5003 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1357 |
| [Sanford] p. 39 | Rule 4 | mptxor 1355 |
| [Sanford] p. 40 | Rule 1 | mptnan 1354 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 4729 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 4731 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 4728 |
| [Schechter] p. 51 | Definition of transitivity | cotr 4726 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3229 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3315 dif0 3314 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3327 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3222 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3223 |
| [Stoll] p. 20 | Remark | invdif 3206 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3408 |
| [Stoll] p. 43 | Definition | uniiun 3731 |
| [Stoll] p. 44 | Definition | intiin 3732 |
| [Stoll] p. 45 | Definition | df-iin 3681 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3680 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 819 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3229 |
| [Suppes] p. 22 | Theorem 2 | eq0 3266 |
| [Suppes] p. 22 | Theorem 4 | eqss 3014 eqssd 3016 eqssi 3015 |
| [Suppes] p. 23 | Theorem 5 | ss0 3284 ss0b 3283 |
| [Suppes] p. 23 | Theorem 6 | sstr 3007 |
| [Suppes] p. 25 | Theorem 12 | elin 3155 elun 3113 |
| [Suppes] p. 26 | Theorem 15 | inidm 3175 |
| [Suppes] p. 26 | Theorem 16 | in0 3279 |
| [Suppes] p. 27 | Theorem 23 | unidm 3115 |
| [Suppes] p. 27 | Theorem 24 | un0 3278 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3135 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3142 |
| [Suppes] p. 27 | Theorem 27 | unss 3146 |
| [Suppes] p. 27 | Theorem 28 | indir 3213 |
| [Suppes] p. 27 | Theorem 29 | undir 3214 |
| [Suppes] p. 28 | Theorem 32 | difid 3312 difidALT 3313 |
| [Suppes] p. 29 | Theorem 33 | difin 3201 |
| [Suppes] p. 29 | Theorem 34 | indif 3207 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3318 |
| [Suppes] p. 29 | Theorem 36 | difun2 3322 |
| [Suppes] p. 29 | Theorem 37 | difin0 3317 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3316 |
| [Suppes] p. 29 | Theorem 39 | difundi 3216 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3218 |
| [Suppes] p. 30 | Theorem 41 | nalset 3908 |
| [Suppes] p. 39 | Theorem 61 | uniss 3622 |
| [Suppes] p. 39 | Theorem 65 | uniop 4010 |
| [Suppes] p. 41 | Theorem 70 | intsn 3671 |
| [Suppes] p. 42 | Theorem 71 | intpr 3668 intprg 3669 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4227 op1stbg 4228 |
| [Suppes] p. 42 | Theorem 78 | intun 3667 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3712 dfiun2g 3710 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3713 |
| [Suppes] p. 47 | Theorem 86 | elpw 3388 elpw2 3932 elpw2g 3931 elpwg 3390 |
| [Suppes] p. 47 | Theorem 87 | pwid 3396 |
| [Suppes] p. 47 | Theorem 89 | pw0 3532 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3596 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4463 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4489 xpindir 4490 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4414 xpundir 4415 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4291 |
| [Suppes] p. 58 | Theorem 2 | relss 4445 |
| [Suppes] p. 59 | Theorem 4 | eldm 4550 eldm2 4551 eldm2g 4549 eldmg 4548 |
| [Suppes] p. 59 | Definition 3 | df-dm 4373 |
| [Suppes] p. 60 | Theorem 6 | dmin 4561 |
| [Suppes] p. 60 | Theorem 8 | rnun 4752 |
| [Suppes] p. 60 | Theorem 9 | rnin 4753 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4541 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4536 brcnvg 4534 |
| [Suppes] p. 62 | Equation 5 | elcnv 4530 elcnv2 4531 |
| [Suppes] p. 62 | Theorem 12 | relcnv 4723 |
| [Suppes] p. 62 | Theorem 15 | cnvin 4751 |
| [Suppes] p. 62 | Theorem 16 | cnvun 4749 |
| [Suppes] p. 63 | Theorem 20 | co02 4854 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4619 |
| [Suppes] p. 63 | Definition 7 | df-co 4372 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4538 |
| [Suppes] p. 64 | Theorem 27 | coass 4859 |
| [Suppes] p. 65 | Theorem 31 | resundi 4643 |
| [Suppes] p. 65 | Theorem 34 | elima 4693 elima2 4694 elima3 4695 elimag 4692 |
| [Suppes] p. 65 | Theorem 35 | imaundi 4756 |
| [Suppes] p. 66 | Theorem 40 | dminss 4758 |
| [Suppes] p. 66 | Theorem 41 | imainss 4759 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 4762 |
| [Suppes] p. 81 | Definition 34 | dfec2 6132 |
| [Suppes] p. 82 | Theorem 72 | elec 6168 elecg 6167 |
| [Suppes] p. 82 | Theorem 73 | erth 6173 erth2 6174 |
| [Suppes] p. 92 | Theorem 1 | enref 6268 enrefg 6267 |
| [Suppes] p. 92 | Theorem 2 | ensym 6284 ensymb 6283 ensymi 6285 |
| [Suppes] p. 92 | Theorem 3 | entr 6287 |
| [Suppes] p. 92 | Theorem 4 | unen 6316 |
| [Suppes] p. 94 | Theorem 15 | endom 6266 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6281 |
| [Suppes] p. 94 | Theorem 17 | domtr 6288 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6309 fundmeng 6310 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6331 |
| [Suppes] p. 130 | Definition 3 | df-tr 3876 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4232 |
| [Suppes] p. 134 | Definition 6 | df-suc 4126 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4344 finds 4341 finds1 4343 finds2 4342 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 6543 df-ltpq 6536 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4145 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2063 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2074 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2077 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2076 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2098 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5536 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2814 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3419 elpr2 3420 elprg 3418 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3414 elsn2 3428 elsn2g 3427 elsng 3413 velsn 3415 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 3986 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3409 sneqr 3552 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3417 dfsn2 3412 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4192 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 3992 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 3970 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4194 unexg 4196 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3441 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3602 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 2979 df-un 2977 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3615 uniprg 3616 |
| [TakeutiZaring] p. 17 | Axiom 4 | pwex 3953 pwexg 3954 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3440 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4161 elsucg 4159 sstr2 3006 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3116 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3158 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3129 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3176 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3211 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3212 |
| [TakeutiZaring] p. 17 | Definition 5.9 | dfss2 2988 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3384 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3143 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 2986 sseqin2 3185 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3018 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3186 inss2 3187 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3057 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3610 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 3971 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 3978 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2357 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 3905 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 2975 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3253 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3312 difidALT 3313 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3260 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4282 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2603 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 3909 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3282 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 3915 ssexg 3917 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 3912 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4293 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4284 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3308 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3097 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3225 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3098 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3106 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2353 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2354 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4471 xpexg 4470 xpexgALT 5780 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4370 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 4983 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5120 fun11 4986 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 4933 svrelfun 4984 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4540 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4542 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4375 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4376 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4372 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 4795 dfrel2 4791 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4464 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4472 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4478 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4488 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4657 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4635 opelresg 4637 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4650 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4653 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4658 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 4961 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 4839 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 4960 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5121 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 1985 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 4930 fv3 5218 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 4876 cnvexg 4875 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4616 dmexg 4614 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4617 rnexg 4615 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5212 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5221 tz6.12 5222 tz6.12c 5224 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5189 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 4925 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 4926 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 4928 wfo 4920 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 4927 wf1 4919 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 4929 wf1o 4921 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5286 eqfnfv2 5287 eqfnfv2f 5290 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5264 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5404 fnexALT 5760 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5403 resfunexgALT 5757 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5004 funimaexg 5003 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 3786 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 4715 iniseg 4717 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4044 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 4931 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5470 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5471 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5476 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5477 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5485 |
| [TakeutiZaring] p. 35 | Notation | wtr 3875 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4109 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 3879 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4318 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4136 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4140 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4236 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4123 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4230 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4295 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4323 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 3877 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4255 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4231 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3629 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4126 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4170 sucidg 4171 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 4245 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4124 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4250 ordelsuc 4249 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4335 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4336 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4337 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4334 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4347 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4340 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4338 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4339 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3650 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 3891 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3651 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4261 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3637 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 5946 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 5974 tfri1d 5972 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 5975 tfri2d 5973 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 5976 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 5940 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 5924 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6067 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6063 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6060 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6064 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6105 nnaordi 6104 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3723 uniss2 3632 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6082 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6073 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6061 omsuc 6074 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6083 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6113 nnmordi 6112 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6062 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 6456 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6298 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6343 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6344 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6247 isfi 6264 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6328 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1440 |
| [Tarski] p. 68 | Lemma 6 | equid 1629 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1632 |
| [Tarski] p. 70 | Lemma 14 | spim 1666 spime 1669 spimeh 1667 spimh 1665 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1437 ax-11o 1744 ax11i 1642 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1807 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1459 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 1444 ax-14 1445 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 664 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 678 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 705 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 714 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 735 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 578 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 5 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 604 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 81 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 54 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 75 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 778 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2039 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 688 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 777 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 591 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 812 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 784 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 786 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 603 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 782 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 783 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 665 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 724 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 579 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 583 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 825 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 846 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 39 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 717 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 718 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 750 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 751 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 749 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 920 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 727 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 725 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 726 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 52 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 689 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 690 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 796 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 792 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 691 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 692 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 693 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 613 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 614 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 673 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 823 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 676 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 677 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 795 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 699 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 617 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 666 pm2.67 694 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 797 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 698 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 756 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 826 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 854 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 752 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 753 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 755 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 754 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 6 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 757 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 758 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 76 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 844 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 99 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 703 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 137 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 898 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 899 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 900 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 702 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 260 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 261 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 659 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 339 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 257 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 258 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 107 simplimdc 790 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 108 simprimdc 789 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 337 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 338 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 821 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 561 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 326 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 324 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 325 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 704 pm3.44 667 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | prth 336 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 566 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 731 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 798 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 169 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 799 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 820 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 822 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 138 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 893 bitr 455 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 387 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 706 pm4.25 707 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 262 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 764 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 679 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 393 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 716 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 453 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 738 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 569 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 768 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 921 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 762 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 912 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 890 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 728 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 760 pm4.45 730 pm4.45im 327 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1410 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 897 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 829 imorr 830 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 312 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 832 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 836 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 837 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 838 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 879 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 701 pm4.56 839 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 880 oranim 840 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 815 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 831 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 813 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 834 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 816 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 835 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 814 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 381 pm4.71d 385 pm4.71i 383 pm4.71r 382 pm4.71rd 386 pm4.71ri 384 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 769 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 294 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 695 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 567 pm4.76 568 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 663 pm4.77 745 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 841 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 842 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 655 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 847 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 891 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 892 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 234 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 235 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 238 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 246 impexp 259 pm4.87 523 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 565 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 848 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 849 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 851 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 850 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1320 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 770 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 843 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1325 pm5.18dc 810 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 654 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 643 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1323 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1328 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1329 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 827 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 458 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 247 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 240 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 868 pm5.6r 869 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 895 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 340 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 440 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 573 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 859 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 574 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 248 pm5.41 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 313 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 867 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 748 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 860 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 852 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 740 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 886 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 887 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 902 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 242 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 177 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 903 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1566 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1414 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1563 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1816 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 1944 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2326 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2327 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2732 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 2870 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 4905 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 4906 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2020 eupickbi 2023 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 4930 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 6459 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |