Bibliographic Cross-References
|
|
Intuitionistic Logic Explorer Bibliographic Cross-References |
|
| Mirrors > Home > ILE Home > Bibliographic Cross-References | ||
| Bibliographic Reference | Description | Intuitionistic Logic Explorer Page(s) |
|---|---|---|
| [AczelRathjen], p. 71 | Definition 8.1.4 | enumct 7181 fidcenum 7022 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7022 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7181 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 12642 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 6993 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 6979 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 12657 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 12659 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 12648 znnen 12615 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 12660 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 12661 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 10868 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4573 |
| [AhoHopUll] p. 318 | Section 9.1 | df-word 10936 lencl 10939 wrd0 10960 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8206 addcan2d 8211 addcan2i 8209 addcand 8210 addcani 8208 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8217 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8274 negsubd 8343 negsubi 8304 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8276 negnegd 8328 negnegi 8296 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8411 subdid 8440 subdii 8433 subdir 8412 subdird 8441 subdiri 8434 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8415 mul01d 8419 mul01i 8417 mul02 8413 mul02d 8418 mul02i 8416 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8820 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8771 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8424 mul2negd 8439 mul2negi 8432 mulneg1 8421 mulneg1d 8437 mulneg1i 8430 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 13700 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8740 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9752 rpaddcld 9787 rpmulcl 9753 rpmulcld 9788 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9764 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8131 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8565 ltadd1dd 8583 ltadd1i 8529 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8619 ltmul1a 8618 ltmul1i 8947 ltmul1ii 8955 ltmul2 8883 ltmul2d 9814 ltmul2dd 9828 ltmul2i 8950 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8153 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8495 lt0neg1d 8542 ltneg 8489 ltnegd 8550 ltnegi 8520 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8472 lt2addd 8594 lt2addi 8537 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9729 |
| [Apostol] p. 21 | Exercise 4 | recgt0 8877 recgt0d 8961 recgt0i 8933 recgt0ii 8934 |
| [Apostol] p. 22 | Definition of integers | df-z 9327 |
| [Apostol] p. 22 | Definition of rationals | df-q 9694 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7060 |
| [Apostol] p. 26 | Theorem I.29 | arch 9246 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9445 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9247 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10346 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12036 zneo 9427 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11196 sqrtthi 11284 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 8993 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12203 |
| [Apostol] p. 363 | Remark | absgt0api 11311 |
| [Apostol] p. 363 | Example | abssubd 11358 abssubi 11315 |
| [ApostolNT] p. 14 | Definition | df-dvds 11953 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 11969 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 11993 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 11989 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 11983 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 11985 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 11970 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 11971 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 11976 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12010 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12012 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12014 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12181 |
| [ApostolNT] p. 16 | Definition | isprm2 12285 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12260 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 12672 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12140 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12182 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12184 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12154 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12147 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12312 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12314 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12537 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12089 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12227 |
| [ApostolNT] p. 25 | Definition | df-phi 12379 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12409 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12390 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12394 |
| [ApostolNT] p. 38 | Remark | df-sgm 15218 |
| [ApostolNT] p. 38 | Definition | df-sgm 15218 |
| [ApostolNT] p. 104 | Definition | congr 12268 |
| [ApostolNT] p. 106 | Remark | dvdsval3 11956 |
| [ApostolNT] p. 106 | Definition | moddvds 11964 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12043 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12044 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10433 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10470 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10758 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 11988 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12271 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12590 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12273 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12401 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12420 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12402 |
| [ApostolNT] p. 179 | Definition | df-lgs 15239 lgsprme0 15283 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15284 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15260 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15275 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15326 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15345 2lgsoddprm 15354 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15310 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15321 |
| [ApostolNT] p. 188 | Definition | df-lgs 15239 lgs1 15285 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15276 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15278 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15286 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15287 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 617 pm2.65 660 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5921 onsucelsucexmidlem 4565 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 15642 |
| [Bauer], p. 483 | Definition | n0rf 3463 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15212 2irrexpqap 15214 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6937 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 14889 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 14879 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8672 |
| [BauerSwan], p. 14 | Remark | 0ct 7173 ctm 7175 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 15645 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7181 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7568 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7481 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7570 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7604 addlocpr 7603 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7630 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7633 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7638 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2048 |
| [BellMachover] p. 460 | Notation | df-mo 2049 |
| [BellMachover] p. 460 | Definition | mo3 2099 mo3h 2098 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2181 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4154 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4210 |
| [BellMachover] p. 466 | Axiom Union | axun2 4470 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4578 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4419 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4581 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4532 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4404 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4625 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4650 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1442 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1440 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1443 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1438 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 12999 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13045 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13058 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13554 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13489 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5830 fcofo 5831 |
| [BourbakiTop1] p. | Remark | xnegmnf 9904 xnegpnf 9903 |
| [BourbakiTop1] p. | Remark | rexneg 9905 |
| [BourbakiTop1] p. | Proposition | ishmeo 14540 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14393 |
| [BourbakiTop1] p. | Property V_ii | innei 14399 |
| [BourbakiTop1] p. | Property V_iv | neissex 14401 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14390 neiss 14386 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14458 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 14535 |
| [BourbakiTop1] p. | Property V_iii | elnei 14388 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14234 |
| [Bruck] p. 1 | Section I.1 | df-mgm 12999 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13045 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13231 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4096 |
| [Cohen] p. 301 | Remark | relogoprlem 15104 |
| [Cohen] p. 301 | Property 2 | relogmul 15105 relogmuld 15120 |
| [Cohen] p. 301 | Property 3 | relogdiv 15106 relogdivd 15121 |
| [Cohen] p. 301 | Property 4 | relogexp 15108 |
| [Cohen] p. 301 | Property 1a | log1 15102 |
| [Cohen] p. 301 | Property 1b | loge 15103 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15201 |
| [Cohen4] p. 352 | Definition | rpelogb 15185 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15191 |
| [Cohen4] p. 361 | Property 3 | logbrec 15196 rprelogbdiv 15193 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15189 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15194 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15183 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15184 |
| [Cohen4] p. 367 | Property | rplogbchbase 15186 |
| [Cohen4] p. 377 | Property 2 | logblt 15198 |
| [Crosilla] p. | Axiom 1 | ax-ext 2178 |
| [Crosilla] p. | Axiom 2 | ax-pr 4242 |
| [Crosilla] p. | Axiom 3 | ax-un 4468 |
| [Crosilla] p. | Axiom 4 | ax-nul 4159 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4624 |
| [Crosilla] p. | Axiom 6 | ru 2988 |
| [Crosilla] p. | Axiom 8 | ax-pow 4207 |
| [Crosilla] p. | Axiom 9 | ax-setind 4573 |
| [Crosilla], p. | Axiom 6 | ax-sep 4151 |
| [Crosilla], p. | Axiom 7 | ax-coll 4148 |
| [Crosilla], p. | Axiom 7' | repizf 4149 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4557 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5921 |
| [Crosilla], p. | Definition of ordinal | df-iord 4401 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4571 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3159 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4627 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6709 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4158 |
| [Enderton] p. 19 | Definition | df-tp 3630 |
| [Enderton] p. 26 | Exercise 5 | unissb 3869 |
| [Enderton] p. 26 | Exercise 10 | pwel 4251 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4321 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3986 iinin2m 3985 iunin1 3981 iunin2 3980 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3984 iundif2ss 3982 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 3999 |
| [Enderton] p. 33 | Exercise 25 | iununir 4000 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4007 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4515 iunpwss 4008 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4250 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4225 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4485 rnex 4933 rnexg 4931 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4876 rnuni 5081 |
| [Enderton] p. 42 | Definition of a function | dffun7 5285 dffun8 5286 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5625 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5319 |
| [Enderton] p. 44 | Definition (d) | dfima2 5011 dfima3 5012 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5630 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7273 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5808 |
| [Enderton] p. 52 | Definition | df-map 6709 |
| [Enderton] p. 53 | Exercise 21 | coass 5188 |
| [Enderton] p. 53 | Exercise 27 | dmco 5178 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5329 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5045 |
| [Enderton] p. 54 | Remark | ixpf 6779 ixpssmap 6791 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6758 |
| [Enderton] p. 56 | Theorem 3M | erref 6612 |
| [Enderton] p. 57 | Lemma 3N | erthi 6640 |
| [Enderton] p. 57 | Definition | df-ec 6594 |
| [Enderton] p. 58 | Definition | df-qs 6598 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6699 th3qcor 6698 th3qlem1 6696 th3qlem2 6697 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6594 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4873 |
| [Enderton] p. 68 | Definition of successor | df-suc 4406 |
| [Enderton] p. 71 | Definition | df-tr 4132 dftr4 4136 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4448 unisucg 4449 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4448 unisucg 4449 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4145 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4146 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6532 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6534 onasuc 6524 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5925 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6533 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6535 onmsuc 6531 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6543 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6536 nnacom 6542 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6544 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6545 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6547 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6537 nnmsucr 6546 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6586 |
| [Enderton] p. 129 | Definition | df-en 6800 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5875 |
| [Enderton] p. 133 | Exercise 1 | xpomen 12612 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6926 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6918 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 6907 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7285 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7281 dju1en 7280 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3526 |
| [Enderton] p. 145 | Figure 38 | ffoss 5536 |
| [Enderton] p. 145 | Definition | df-dom 6801 |
| [Enderton] p. 146 | Example 1 | domen 6810 domeng 6811 |
| [Enderton] p. 146 | Example 3 | nndomo 6925 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6894 xpdom1g 6892 xpdom2g 6891 |
| [Enderton] p. 168 | Definition | df-po 4331 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4463 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4424 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4579 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4427 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4552 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4525 |
| [Enderton] p. 194 | Remark | onprc 4588 |
| [Enderton] p. 194 | Exercise 16 | suc11 4594 |
| [Enderton] p. 197 | Definition | df-card 7247 |
| [Enderton] p. 200 | Exercise 25 | tfis 4619 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4590 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4592 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4593 |
| [Geuvers], p. 1 | Remark | expap0 10661 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8642 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8681 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8643 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 7998 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11368 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11376 maxle2 11377 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11378 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11381 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11382 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8609 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7414 enqer 7425 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7418 df-nqqs 7415 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7411 df-plqqs 7416 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7412 df-mqqs 7417 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7419 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7475 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7478 ltbtwnnq 7483 ltbtwnnqq 7482 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7467 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7468 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7604 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7646 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7645 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7664 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7680 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7686 ltaprlem 7685 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7683 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7639 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7659 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7648 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7647 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7655 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7705 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7793 enrer 7802 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7798 df-1r 7799 df-nr 7794 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7796 df-plr 7795 negexsr 7839 recexsrlem 7841 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7797 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 8987 creur 8986 cru 8629 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 7990 axcnre 7948 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11023 crimd 11142 crimi 11102 crre 11022 crred 11141 crrei 11101 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11025 remimd 11107 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11222 absval2d 11350 absval2i 11309 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11049 cjaddd 11130 cjaddi 11097 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11050 cjmuld 11131 cjmuli 11098 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11048 cjcjd 11108 cjcji 11080 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11047 cjreb 11031 cjrebd 11111 cjrebi 11083 cjred 11136 rere 11030 rereb 11028 rerebd 11110 rerebi 11082 rered 11134 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11056 addcjd 11122 addcji 11092 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11166 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11217 abscjd 11355 abscji 11313 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11229 abs00d 11351 abs00i 11310 absne0d 11352 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11261 releabsd 11356 releabsi 11314 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11234 absmuld 11359 absmuli 11316 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11220 sqabsaddi 11317 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11269 abstrid 11361 abstrii 11320 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10631 exp0 10635 expp1 10638 expp1d 10766 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10673 expaddd 10767 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15148 cxpmuld 15173 expmul 10676 expmuld 10768 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10670 mulexpd 10780 rpmulcxp 15145 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10085 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11491 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11493 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11492 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11496 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11489 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11485 climcj 11486 climim 11488 climre 11487 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8066 df-xr 8065 ltxr 9850 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11512 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10390 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14101 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 14600 xmet0 14599 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 14607 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 14609 mstri 14709 xmettri 14608 xmstri 14708 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14515 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 14747 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11475 addcncntop 14798 mulcn2 11477 mulcncntop 14800 subcn2 11476 subcncntop 14799 |
| [Gleason] p. 295 | Remark | bcval3 10843 bcval4 10844 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10858 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10841 df-bc 10840 |
| [Gleason] p. 296 | Remark | bcn0 10847 bcnn 10849 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 11649 |
| [Gleason] p. 308 | Equation 2 | ef0 11837 |
| [Gleason] p. 308 | Equation 3 | efcj 11838 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 11843 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 11847 |
| [Gleason] p. 310 | Equation 14 | sinadd 11901 |
| [Gleason] p. 310 | Equation 15 | cosadd 11902 |
| [Gleason] p. 311 | Equation 17 | sincossq 11913 |
| [Gleason] p. 311 | Equation 18 | cosbnd 11918 sinbnd 11917 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 11818 |
| [Golan] p. 1 | Remark | srgisid 13542 |
| [Golan] p. 1 | Definition | df-srg 13520 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1463 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13143 mndideu 13067 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13170 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13199 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13210 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13232 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 15718 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1434 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1435 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1437 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7292 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6557 |
| [HoTT], p. | Exercise 11.10 | neapmkv 15712 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8684 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7537 df-imp 7536 df-iplp 7535 df-reap 8602 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8698 rerecapb 8870 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6195 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7729 |
| [HoTT], p. | Corollary 11.4.3 | conventions 15367 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 15705 dceqnconst 15704 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 7967 caucvgpr 7749 caucvgprpr 7779 caucvgsr 7869 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7533 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 15710 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4332 ltpopr 7662 ltsopr 7663 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8633 reapcotr 8625 reapirr 8604 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8153 gt0add 8600 leadd1 8457 lelttr 8115 lemul1a 8885 lenlt 8102 ltadd1 8456 ltletr 8116 ltmul1 8619 reaplt 8615 |
| [Jech] p. 4 | Definition of class | cv 1363 cvjust 2191 |
| [Jech] p. 78 | Note | opthprc 4714 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1544 |
| [Kreyszig] p. 3 | Property M1 | metcl 14589 xmetcl 14588 |
| [Kreyszig] p. 4 | Property M2 | meteq0 14596 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8695 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 14678 |
| [Kreyszig] p. 19 | Remark | mopntopon 14679 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 14724 mopnm 14684 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 14722 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 14727 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 14749 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14449 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 13886 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 13877 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 13878 |
| [Kunen] p. 10 | Axiom 0 | a9e 1710 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4150 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6719 mapvalg 6717 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6713 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3926 |
| [Lang] p. 3 | Statement | lidrideqd 13024 mndbn0 13072 |
| [Lang] p. 3 | Definition | df-mnd 13058 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13041 |
| [Lang] p. 5 | Equation | gsumfzreidx 13467 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13258 |
| [Lang] p. 7 | Definition | dfgrp2e 13160 |
| [Levy] p. 338 | Axiom | df-clab 2183 df-clel 2192 df-cleq 2189 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1434 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1435 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1437 |
| [Margaris] p. 40 | Rule C | exlimiv 1612 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 854 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 893 exalim 1516 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 652 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1652 r19.2m 3537 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1568 19.3h 1567 rr19.3v 2903 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1492 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1633 alexim 1659 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1513 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1604 spsbe 1856 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1658 19.9h 1657 19.9v 1885 exlimd 1611 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1678 excomim 1677 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1679 r19.12 2603 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1660 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1482 ralbi 2629 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1569 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1570 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1618 rexbi 2630 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1680 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1471 alimd 1535 alimdh 1481 alimdv 1893 ralimdaa 2563 ralimdv 2565 ralimdva 2564 ralimdvva 2566 sbcimdv 3055 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1681 19.21 1597 19.21bi 1572 19.21h 1571 19.21ht 1595 19.21t 1596 19.21v 1887 alrimd 1624 alrimdd 1623 alrimdh 1493 alrimdv 1890 alrimi 1536 alrimih 1483 alrimiv 1888 alrimivv 1889 r19.21 2573 r19.21be 2588 r19.21bi 2585 r19.21t 2572 r19.21v 2574 ralrimd 2575 ralrimdv 2576 ralrimdva 2577 ralrimdvv 2581 ralrimdvva 2582 ralrimi 2568 ralrimiv 2569 ralrimiva 2570 ralrimivv 2578 ralrimivva 2579 ralrimivvva 2580 ralrimivw 2571 rexlimi 2607 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1895 2eximdv 1896 exim 1613 eximd 1626 eximdh 1625 eximdv 1894 rexim 2591 reximdai 2595 reximddv 2600 reximddv2 2602 reximdv 2598 reximdv2 2596 reximdva 2599 reximdvai 2597 reximi2 2593 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1692 19.23bi 1606 19.23h 1512 19.23ht 1511 19.23t 1691 19.23v 1897 19.23vv 1898 exlimd2 1609 exlimdh 1610 exlimdv 1833 exlimdvv 1912 exlimi 1608 exlimih 1607 exlimiv 1612 exlimivv 1911 r19.23 2605 r19.23v 2606 rexlimd 2611 rexlimdv 2613 rexlimdv3a 2616 rexlimdva 2614 rexlimdva2 2617 rexlimdvaa 2615 rexlimdvv 2621 rexlimdvva 2622 rexlimdvw 2618 rexlimiv 2608 rexlimiva 2609 rexlimivv 2620 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1653 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1640 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1496 19.26-3an 1497 19.26 1495 r19.26-2 2626 r19.26-3 2627 r19.26 2623 r19.26m 2628 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1575 19.27h 1574 19.27v 1914 r19.27av 2632 r19.27m 3546 r19.27mv 3547 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1577 19.28h 1576 19.28v 1915 r19.28av 2633 r19.28m 3540 r19.28mv 3543 rr19.28v 2904 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1634 19.29r 1635 19.29r2 1636 19.29x 1637 r19.29 2634 r19.29d2r 2641 r19.29r 2635 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1641 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1695 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1693 19.32r 1694 r19.32r 2643 r19.32vdc 2646 r19.32vr 2645 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1498 19.33b2 1643 19.33bdc 1644 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1698 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1638 19.35i 1639 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1687 19.36aiv 1916 19.36i 1686 r19.36av 2648 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1688 19.37aiv 1689 r19.37 2649 r19.37av 2650 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1690 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1654 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1646 19.40 1645 r19.40 2651 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1700 19.41h 1699 19.41v 1917 19.41vv 1918 19.41vvv 1919 19.41vvvv 1920 r19.41 2652 r19.41v 2653 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1702 19.42h 1701 19.42v 1921 19.42vv 1926 19.42vvv 1927 19.42vvvv 1928 r19.42v 2654 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1642 r19.43 2655 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1696 r19.44av 2656 r19.44mv 3545 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1697 r19.45av 2657 r19.45mv 3544 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2070 |
| [Megill] p. 444 | Axiom C5 | ax-17 1540 |
| [Megill] p. 445 | Lemma L12 | alequcom 1529 ax-10 1519 |
| [Megill] p. 446 | Lemma L17 | equtrr 1724 |
| [Megill] p. 446 | Lemma L19 | hbnae 1735 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1777 sbid 1788 |
| [Megill] p. 448 | Scheme C5' | ax-4 1524 |
| [Megill] p. 448 | Scheme C6' | ax-7 1462 |
| [Megill] p. 448 | Scheme C8' | ax-8 1518 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1521 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1730 |
| [Megill] p. 448 | Scheme C12' | ax-13 2169 |
| [Megill] p. 448 | Scheme C13' | ax-14 2170 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1837 |
| [Megill] p. 448 | Scheme C16' | ax-16 1828 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1744 dral2 1745 drex1 1812 drex2 1746 drsb1 1813 drsb2 1855 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2006 sbequ 1854 sbid2v 2015 |
| [Megill] p. 450 | Example in Appendix | hba1 1554 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3072 rspsbca 3073 stdpc4 1789 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3078 stdpc5 1598 |
| [Mendelson] p. 81 | Rule C | exlimiv 1612 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1717 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1784 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3487 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3488 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3403 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3451 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3404 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3294 |
| [Mendelson] p. 231 | Definition of union | unssin 3402 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4511 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3838 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4317 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4318 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4319 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3859 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4795 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5190 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4406 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 6906 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6880 xpsneng 6881 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6886 xpcomeng 6887 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6889 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6883 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6711 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6870 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 6911 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6745 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6871 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7284 djucomen 7283 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7282 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6525 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3385 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4751 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4752 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4095 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5185 coi2 5186 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4880 rn0 4922 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5074 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4772 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4886 rnxpm 5099 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4743 xp0 5089 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5028 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5025 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5024 imaexg 5023 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5020 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5692 funfvop 5674 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5604 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5612 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5302 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5815 dff13f 5817 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5785 funrnex 6171 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5809 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5153 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3890 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6213 df-1st 6198 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6214 df-2nd 6199 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1461 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1518 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1520 ax-11o 1837 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1841 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1462 |
| [Monk2] p. 109 | Lemma 15 | equvin 1877 equvini 1772 eqvinop 4276 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1540 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1665 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1462 |
| [Monk2] p. 114 | Lemma 22 | hba1 1554 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1566 nfia1 1594 |
| [Monk2] p. 114 | Lemma 24 | hba2 1565 nfa2 1593 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 832 dftest 15719 |
| [Munkres] p. 77 | Example 2 | distop 14321 |
| [Munkres] p. 78 | Definition of basis | df-bases 14279 isbasis3g 14282 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 12931 tgval2 14287 |
| [Munkres] p. 79 | Remark | tgcl 14300 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14294 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14315 tgss3 14314 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14316 basgen2 14317 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14406 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14348 topcld 14345 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14349 |
| [Munkres] p. 94 | Definition of closure | clsval 14347 |
| [Munkres] p. 94 | Definition of interior | ntrval 14346 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14424 iscn 14433 iscn2 14436 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14466 cncnp2m 14467 cncnpi 14464 df-cnp 14425 iscnp 14435 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 14750 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 6964 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7230 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7218 omniwomnimkv 7233 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3273 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7201 exmidomniim 7207 finomni 7206 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7186 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 15665 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 15667 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 6969 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7268 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7269 exmidfodomrlemrALT 7270 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7215 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 15651 peano4nninf 15650 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 15653 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 15661 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 15663 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 15649 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2183 rabid 2673 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2010 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2189 |
| [Quine] p. 19 | Definition 2.9 | df-v 2765 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2305 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2317 abid2f 2365 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1902 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1900 sb6 1901 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2192 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2196 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2198 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 2990 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 2991 dfsbcq2 2992 |
| [Quine] p. 43 | Theorem 6.8 | vex 2766 |
| [Quine] p. 43 | Theorem 6.9 | isset 2769 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2846 spcgv 2851 spcimgf 2844 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3001 spsbcd 3002 |
| [Quine] p. 44 | Theorem 6.12 | elex 2774 |
| [Quine] p. 44 | Theorem 6.13 | elab 2908 elabg 2910 elabgf 2906 |
| [Quine] p. 44 | Theorem 6.14 | noel 3454 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3687 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3629 df-sn 3628 |
| [Quine] p. 49 | Theorem 7.4 | snss 3757 snssg 3756 |
| [Quine] p. 49 | Theorem 7.5 | prss 3778 prssg 3779 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3728 prid1g 3726 prid2 3729 prid2g 3727 snid 3653 snidg 3651 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4217 snexprc 4219 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4244 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3855 unisng 3856 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3858 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3867 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3866 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5229 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5220 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5230 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5234 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5235 |
| [Quine] p. 58 | Definition 9.1 | df-op 3631 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4290 opabidw 4291 opelopab 4306 opelopaba 4300 opelopabaf 4308 opelopabf 4309 opelopabg 4302 opelopabga 4297 opelopabgf 4304 oprabid 5954 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4669 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4671 |
| [Quine] p. 64 | Definition 9.15 | df-id 4328 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5316 |
| [Quine] p. 65 | Theorem 10.4 | funi 5290 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5306 funsng 5304 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5260 |
| [Quine] p. 65 | Definition 10.2 | args 5038 dffv4g 5555 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5266 fv2 5553 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10816 nn0opth2d 10815 nn0opthd 10814 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5343 funimaexg 5342 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13489 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13554 |
| [Rudin] p. 164 | Equation 27 | efcan 11841 |
| [Rudin] p. 164 | Equation 30 | efzval 11848 |
| [Rudin] p. 167 | Equation 48 | absefi 11934 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1437 |
| [Sanford] p. 39 | Rule 4 | mptxor 1435 |
| [Sanford] p. 40 | Rule 1 | mptnan 1434 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5054 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5056 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5053 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5051 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 13556 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14319 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3428 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3522 dif0 3521 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3535 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3421 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3422 |
| [Stoll] p. 20 | Remark | invdif 3405 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3632 |
| [Stoll] p. 43 | Definition | uniiun 3970 |
| [Stoll] p. 44 | Definition | intiin 3971 |
| [Stoll] p. 45 | Definition | df-iin 3919 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3918 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 890 imanst 889 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3428 |
| [Suppes] p. 22 | Theorem 2 | eq0 3469 |
| [Suppes] p. 22 | Theorem 4 | eqss 3198 eqssd 3200 eqssi 3199 |
| [Suppes] p. 23 | Theorem 5 | ss0 3491 ss0b 3490 |
| [Suppes] p. 23 | Theorem 6 | sstr 3191 |
| [Suppes] p. 25 | Theorem 12 | elin 3346 elun 3304 |
| [Suppes] p. 26 | Theorem 15 | inidm 3372 |
| [Suppes] p. 26 | Theorem 16 | in0 3485 |
| [Suppes] p. 27 | Theorem 23 | unidm 3306 |
| [Suppes] p. 27 | Theorem 24 | un0 3484 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3326 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3333 |
| [Suppes] p. 27 | Theorem 27 | unss 3337 |
| [Suppes] p. 27 | Theorem 28 | indir 3412 |
| [Suppes] p. 27 | Theorem 29 | undir 3413 |
| [Suppes] p. 28 | Theorem 32 | difid 3519 difidALT 3520 |
| [Suppes] p. 29 | Theorem 33 | difin 3400 |
| [Suppes] p. 29 | Theorem 34 | indif 3406 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3525 |
| [Suppes] p. 29 | Theorem 36 | difun2 3530 |
| [Suppes] p. 29 | Theorem 37 | difin0 3524 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3523 |
| [Suppes] p. 29 | Theorem 39 | difundi 3415 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3417 |
| [Suppes] p. 30 | Theorem 41 | nalset 4163 |
| [Suppes] p. 39 | Theorem 61 | uniss 3860 |
| [Suppes] p. 39 | Theorem 65 | uniop 4288 |
| [Suppes] p. 41 | Theorem 70 | intsn 3909 |
| [Suppes] p. 42 | Theorem 71 | intpr 3906 intprg 3907 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4513 op1stbg 4514 |
| [Suppes] p. 42 | Theorem 78 | intun 3905 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3950 dfiun2g 3948 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3951 |
| [Suppes] p. 47 | Theorem 86 | elpw 3611 elpw2 4190 elpw2g 4189 elpwg 3613 |
| [Suppes] p. 47 | Theorem 87 | pwid 3620 |
| [Suppes] p. 47 | Theorem 89 | pw0 3769 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3834 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4770 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4801 xpindir 4802 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4719 xpundir 4720 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4584 |
| [Suppes] p. 58 | Theorem 2 | relss 4750 |
| [Suppes] p. 59 | Theorem 4 | eldm 4863 eldm2 4864 eldm2g 4862 eldmg 4861 |
| [Suppes] p. 59 | Definition 3 | df-dm 4673 |
| [Suppes] p. 60 | Theorem 6 | dmin 4874 |
| [Suppes] p. 60 | Theorem 8 | rnun 5078 |
| [Suppes] p. 60 | Theorem 9 | rnin 5079 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4854 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4849 brcnvg 4847 |
| [Suppes] p. 62 | Equation 5 | elcnv 4843 elcnv2 4844 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5047 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5077 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5075 |
| [Suppes] p. 63 | Theorem 20 | co02 5183 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4935 |
| [Suppes] p. 63 | Definition 7 | df-co 4672 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4851 |
| [Suppes] p. 64 | Theorem 27 | coass 5188 |
| [Suppes] p. 65 | Theorem 31 | resundi 4959 |
| [Suppes] p. 65 | Theorem 34 | elima 5014 elima2 5015 elima3 5016 elimag 5013 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5082 |
| [Suppes] p. 66 | Theorem 40 | dminss 5084 |
| [Suppes] p. 66 | Theorem 41 | imainss 5085 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5088 |
| [Suppes] p. 81 | Definition 34 | dfec2 6595 |
| [Suppes] p. 82 | Theorem 72 | elec 6633 elecg 6632 |
| [Suppes] p. 82 | Theorem 73 | erth 6638 erth2 6639 |
| [Suppes] p. 89 | Theorem 96 | map0b 6746 |
| [Suppes] p. 89 | Theorem 97 | map0 6748 map0g 6747 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6749 |
| [Suppes] p. 89 | Theorem 99 | mapss 6750 |
| [Suppes] p. 92 | Theorem 1 | enref 6824 enrefg 6823 |
| [Suppes] p. 92 | Theorem 2 | ensym 6840 ensymb 6839 ensymi 6841 |
| [Suppes] p. 92 | Theorem 3 | entr 6843 |
| [Suppes] p. 92 | Theorem 4 | unen 6875 |
| [Suppes] p. 94 | Theorem 15 | endom 6822 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6837 |
| [Suppes] p. 94 | Theorem 17 | domtr 6844 |
| [Suppes] p. 95 | Theorem 18 | isbth 7033 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6865 fundmeng 6866 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6893 |
| [Suppes] p. 130 | Definition 3 | df-tr 4132 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4524 |
| [Suppes] p. 134 | Definition 6 | df-suc 4406 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4639 finds 4636 finds1 4638 finds2 4637 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7420 df-ltpq 7413 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4425 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2178 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2189 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2192 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2191 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2214 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5926 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2988 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3643 elpr2 3644 elprg 3642 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3638 elsn2 3656 elsn2g 3655 elsng 3637 velsn 3639 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4264 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3633 sneqr 3790 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3641 dfsn2 3636 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4472 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4270 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4248 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4476 unexg 4478 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3671 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3840 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3163 df-un 3161 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3853 uniprg 3854 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4212 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3670 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4441 elsucg 4439 sstr2 3190 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3307 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3355 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3320 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3373 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3410 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3411 |
| [TakeutiZaring] p. 17 | Definition 5.9 | dfss2 3172 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3607 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3334 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3170 sseqin2 3382 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3203 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3383 inss2 3384 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3243 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3848 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4249 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4256 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2484 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4160 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3159 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3452 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3519 difidALT 3520 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3463 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4575 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2765 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4165 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3489 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4170 ssexg 4172 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4167 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4586 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4577 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3515 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3288 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3424 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3289 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3297 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2480 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2481 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4778 xpexg 4777 xpexgALT 6190 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4670 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5322 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5474 fun11 5325 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5269 svrelfun 5323 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4853 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4855 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4675 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4676 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4672 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5124 dfrel2 5120 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4771 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4780 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4786 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4800 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4974 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4951 opelresg 4953 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4967 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4970 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4975 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5299 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5168 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5298 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5475 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2089 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5266 fv3 5581 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5208 cnvexg 5207 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4932 dmexg 4930 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4933 rnexg 4931 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5575 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5585 tz6.12 5586 tz6.12c 5588 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5549 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5261 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5262 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5264 wfo 5256 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5263 wf1 5255 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5265 wf1o 5257 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5659 eqfnfv2 5660 eqfnfv2f 5663 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5631 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5784 fnexALT 6168 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5783 resfunexgALT 6165 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5343 funimaexg 5342 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4034 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5039 iniseg 5041 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4324 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5267 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5857 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5858 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5863 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5865 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5873 |
| [TakeutiZaring] p. 35 | Notation | wtr 4131 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4389 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4135 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4612 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4416 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4420 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4528 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4403 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4522 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4588 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4618 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4133 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4547 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4523 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3867 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4406 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4450 sucidg 4451 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4537 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4404 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4542 ordelsuc 4541 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4630 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4631 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4632 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4629 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4643 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4635 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4633 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4634 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3888 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4147 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3889 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4553 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3875 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6366 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6423 tfri1d 6393 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6424 tfri2d 6394 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6425 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6360 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6344 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6522 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6518 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6515 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6519 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6567 nnaordi 6566 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3961 uniss2 3870 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6528 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6538 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6529 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6516 omsuc 6530 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6539 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6575 nnmordi 6574 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6517 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7254 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6854 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6918 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6919 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6802 isfi 6820 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6890 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6709 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 6896 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 6909 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1524 |
| [Tarski] p. 68 | Lemma 6 | equid 1715 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1718 |
| [Tarski] p. 70 | Lemma 14 | spim 1752 spime 1755 spimeh 1753 spimh 1751 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1520 ax-11o 1837 ax11i 1728 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1901 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1540 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2169 ax-14 2170 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 712 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 728 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 757 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 766 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 790 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 617 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 644 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 838 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2143 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 738 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 837 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 630 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 886 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 844 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 857 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 643 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 854 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 856 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 713 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 776 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 618 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 622 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 894 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 908 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 769 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 770 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 805 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 806 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 804 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 981 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 779 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 777 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 778 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 739 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 740 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 868 pm2.5gdc 867 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 863 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 741 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 742 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 743 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 656 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 657 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 723 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 892 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 726 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 727 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 866 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 749 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 801 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 802 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 660 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 714 pm2.67 744 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 870 pm2.521gdc 869 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 748 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 811 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 895 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 916 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 807 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 808 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 810 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 809 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 812 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 906 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 755 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 959 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 960 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 961 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 754 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 264 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 265 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 694 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 347 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 261 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 262 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 861 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 860 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 345 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 346 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 690 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 597 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 333 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 331 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 332 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 756 pm3.44 716 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 602 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 786 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 872 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 873 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 891 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 695 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 954 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 758 pm4.25 759 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 819 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 729 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 768 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 793 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 605 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 823 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 982 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 817 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 973 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 951 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 780 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 815 pm4.45 785 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1495 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 958 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 898 imorr 722 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 900 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 751 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 752 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 903 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 940 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 753 pm4.56 781 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 941 oranim 782 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 687 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 899 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 887 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 901 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 688 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 902 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 888 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 828 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 745 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 603 pm4.76 604 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 711 pm4.77 800 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 783 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 904 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 708 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 909 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 952 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 953 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 237 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 240 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 557 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 601 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 910 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 911 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 913 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 912 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1400 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 829 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 905 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1405 pm5.18dc 884 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 707 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 696 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1403 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1408 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1409 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 896 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 475 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 242 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 927 pm5.6r 928 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 956 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 453 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 609 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 918 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 610 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 250 pm5.41 251 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 320 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 926 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 803 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 919 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 914 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 795 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 947 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 948 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 963 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 244 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 179 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 964 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1649 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1499 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1646 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1910 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2048 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2448 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2449 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2902 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3046 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5238 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5239 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2124 eupickbi 2127 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5266 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7257 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |