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 7176 fidcenum 7017 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7017 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7176 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 12585 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 6988 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 6976 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 12600 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 12602 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 12591 znnen 12558 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 12603 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 12604 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 10850 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4570 |
| [AhoHopUll] p. 318 | Section 9.1 | df-word 10918 lencl 10921 wrd0 10942 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8201 addcan2d 8206 addcan2i 8204 addcand 8205 addcani 8203 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8212 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8269 negsubd 8338 negsubi 8299 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8271 negnegd 8323 negnegi 8291 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8406 subdid 8435 subdii 8428 subdir 8407 subdird 8436 subdiri 8429 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8410 mul01d 8414 mul01i 8412 mul02 8408 mul02d 8413 mul02i 8411 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8814 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8765 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8419 mul2negd 8434 mul2negi 8427 mulneg1 8416 mulneg1d 8432 mulneg1i 8425 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 13643 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8734 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9746 rpaddcld 9781 rpmulcl 9747 rpmulcld 9782 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9758 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8126 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8559 ltadd1dd 8577 ltadd1i 8523 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8613 ltmul1a 8612 ltmul1i 8941 ltmul1ii 8949 ltmul2 8877 ltmul2d 9808 ltmul2dd 9822 ltmul2i 8944 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8148 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8489 lt0neg1d 8536 ltneg 8483 ltnegd 8544 ltnegi 8514 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8466 lt2addd 8588 lt2addi 8531 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9723 |
| [Apostol] p. 21 | Exercise 4 | recgt0 8871 recgt0d 8955 recgt0i 8927 recgt0ii 8928 |
| [Apostol] p. 22 | Definition of integers | df-z 9321 |
| [Apostol] p. 22 | Definition of rationals | df-q 9688 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7055 |
| [Apostol] p. 26 | Theorem I.29 | arch 9240 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9439 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9241 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10328 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12015 zneo 9421 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11178 sqrtthi 11266 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 8987 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12176 |
| [Apostol] p. 363 | Remark | absgt0api 11293 |
| [Apostol] p. 363 | Example | abssubd 11340 abssubi 11297 |
| [ApostolNT] p. 14 | Definition | df-dvds 11934 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 11950 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 11974 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 11970 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 11964 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 11966 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 11951 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 11952 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 11957 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 11990 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 11992 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 11994 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12154 |
| [ApostolNT] p. 16 | Definition | isprm2 12258 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12233 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 12615 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12113 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12155 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12157 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12127 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12120 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12285 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12287 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12509 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12068 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12200 |
| [ApostolNT] p. 25 | Definition | df-phi 12352 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12381 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12363 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12367 |
| [ApostolNT] p. 104 | Definition | congr 12241 |
| [ApostolNT] p. 106 | Remark | dvdsval3 11937 |
| [ApostolNT] p. 106 | Definition | moddvds 11945 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12022 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12023 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10415 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10452 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10740 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 11969 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12244 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12246 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12374 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12392 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12375 |
| [ApostolNT] p. 179 | Definition | df-lgs 15155 lgsprme0 15199 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15200 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15176 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15191 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15242 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15261 2lgsoddprm 15270 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15226 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15237 |
| [ApostolNT] p. 188 | Definition | df-lgs 15155 lgs1 15201 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15192 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15194 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15202 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15203 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 617 pm2.65 660 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5918 onsucelsucexmidlem 4562 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 15558 |
| [Bauer], p. 483 | Definition | n0rf 3460 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15149 2irrexpqap 15151 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6934 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 14832 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 14822 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8666 |
| [BauerSwan], p. 14 | Remark | 0ct 7168 ctm 7170 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 15561 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7176 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7563 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7476 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7565 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7599 addlocpr 7598 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7625 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7628 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7633 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2045 |
| [BellMachover] p. 460 | Notation | df-mo 2046 |
| [BellMachover] p. 460 | Definition | mo3 2096 mo3h 2095 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2178 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4151 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4207 |
| [BellMachover] p. 466 | Axiom Union | axun2 4467 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4575 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4416 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4578 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4529 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4401 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4622 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4647 |
| [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 12942 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 12988 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13001 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13497 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13432 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5827 fcofo 5828 |
| [BourbakiTop1] p. | Remark | xnegmnf 9898 xnegpnf 9897 |
| [BourbakiTop1] p. | Remark | rexneg 9899 |
| [BourbakiTop1] p. | Proposition | ishmeo 14483 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14336 |
| [BourbakiTop1] p. | Property V_ii | innei 14342 |
| [BourbakiTop1] p. | Property V_iv | neissex 14344 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14333 neiss 14329 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14401 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 14478 |
| [BourbakiTop1] p. | Property V_iii | elnei 14331 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14177 |
| [Bruck] p. 1 | Section I.1 | df-mgm 12942 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 12988 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13174 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4093 |
| [Cohen] p. 301 | Remark | relogoprlem 15044 |
| [Cohen] p. 301 | Property 2 | relogmul 15045 relogmuld 15060 |
| [Cohen] p. 301 | Property 3 | relogdiv 15046 relogdivd 15061 |
| [Cohen] p. 301 | Property 4 | relogexp 15048 |
| [Cohen] p. 301 | Property 1a | log1 15042 |
| [Cohen] p. 301 | Property 1b | loge 15043 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15138 |
| [Cohen4] p. 352 | Definition | rpelogb 15122 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15128 |
| [Cohen4] p. 361 | Property 3 | logbrec 15133 rprelogbdiv 15130 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15126 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15131 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15120 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15121 |
| [Cohen4] p. 367 | Property | rplogbchbase 15123 |
| [Cohen4] p. 377 | Property 2 | logblt 15135 |
| [Crosilla] p. | Axiom 1 | ax-ext 2175 |
| [Crosilla] p. | Axiom 2 | ax-pr 4239 |
| [Crosilla] p. | Axiom 3 | ax-un 4465 |
| [Crosilla] p. | Axiom 4 | ax-nul 4156 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4621 |
| [Crosilla] p. | Axiom 6 | ru 2985 |
| [Crosilla] p. | Axiom 8 | ax-pow 4204 |
| [Crosilla] p. | Axiom 9 | ax-setind 4570 |
| [Crosilla], p. | Axiom 6 | ax-sep 4148 |
| [Crosilla], p. | Axiom 7 | ax-coll 4145 |
| [Crosilla], p. | Axiom 7' | repizf 4146 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4554 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5918 |
| [Crosilla], p. | Definition of ordinal | df-iord 4398 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4568 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3156 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4624 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6706 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4155 |
| [Enderton] p. 19 | Definition | df-tp 3627 |
| [Enderton] p. 26 | Exercise 5 | unissb 3866 |
| [Enderton] p. 26 | Exercise 10 | pwel 4248 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4318 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3983 iinin2m 3982 iunin1 3978 iunin2 3977 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3981 iundif2ss 3979 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 3996 |
| [Enderton] p. 33 | Exercise 25 | iununir 3997 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4004 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4512 iunpwss 4005 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4247 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4222 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4482 rnex 4930 rnexg 4928 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4873 rnuni 5078 |
| [Enderton] p. 42 | Definition of a function | dffun7 5282 dffun8 5283 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5622 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5316 |
| [Enderton] p. 44 | Definition (d) | dfima2 5008 dfima3 5009 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5627 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7268 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5805 |
| [Enderton] p. 52 | Definition | df-map 6706 |
| [Enderton] p. 53 | Exercise 21 | coass 5185 |
| [Enderton] p. 53 | Exercise 27 | dmco 5175 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5326 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5042 |
| [Enderton] p. 54 | Remark | ixpf 6776 ixpssmap 6788 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6755 |
| [Enderton] p. 56 | Theorem 3M | erref 6609 |
| [Enderton] p. 57 | Lemma 3N | erthi 6637 |
| [Enderton] p. 57 | Definition | df-ec 6591 |
| [Enderton] p. 58 | Definition | df-qs 6595 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6696 th3qcor 6695 th3qlem1 6693 th3qlem2 6694 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6591 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4870 |
| [Enderton] p. 68 | Definition of successor | df-suc 4403 |
| [Enderton] p. 71 | Definition | df-tr 4129 dftr4 4133 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4445 unisucg 4446 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4445 unisucg 4446 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4142 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4143 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6529 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6531 onasuc 6521 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5922 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6530 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6532 onmsuc 6528 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6540 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6533 nnacom 6539 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6541 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6542 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6544 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6534 nnmsucr 6543 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6583 |
| [Enderton] p. 129 | Definition | df-en 6797 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5872 |
| [Enderton] p. 133 | Exercise 1 | xpomen 12555 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6923 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6915 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 6904 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7280 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7276 dju1en 7275 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3523 |
| [Enderton] p. 145 | Figure 38 | ffoss 5533 |
| [Enderton] p. 145 | Definition | df-dom 6798 |
| [Enderton] p. 146 | Example 1 | domen 6807 domeng 6808 |
| [Enderton] p. 146 | Example 3 | nndomo 6922 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6891 xpdom1g 6889 xpdom2g 6888 |
| [Enderton] p. 168 | Definition | df-po 4328 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4460 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4421 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4576 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4424 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4549 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4522 |
| [Enderton] p. 194 | Remark | onprc 4585 |
| [Enderton] p. 194 | Exercise 16 | suc11 4591 |
| [Enderton] p. 197 | Definition | df-card 7242 |
| [Enderton] p. 200 | Exercise 25 | tfis 4616 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4587 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4589 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4590 |
| [Geuvers], p. 1 | Remark | expap0 10643 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8636 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8675 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8637 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 7993 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11350 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11358 maxle2 11359 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11360 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11363 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11364 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8603 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7409 enqer 7420 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7413 df-nqqs 7410 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7406 df-plqqs 7411 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7407 df-mqqs 7412 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7414 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7470 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7473 ltbtwnnq 7478 ltbtwnnqq 7477 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7462 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7463 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7599 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7641 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7640 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7659 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7675 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7681 ltaprlem 7680 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7678 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7634 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7654 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7643 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7642 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7650 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7700 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7788 enrer 7797 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7793 df-1r 7794 df-nr 7789 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7791 df-plr 7790 negexsr 7834 recexsrlem 7836 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7792 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 8981 creur 8980 cru 8623 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 7985 axcnre 7943 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11005 crimd 11124 crimi 11084 crre 11004 crred 11123 crrei 11083 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11007 remimd 11089 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11204 absval2d 11332 absval2i 11291 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11031 cjaddd 11112 cjaddi 11079 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11032 cjmuld 11113 cjmuli 11080 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11030 cjcjd 11090 cjcji 11062 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11029 cjreb 11013 cjrebd 11093 cjrebi 11065 cjred 11118 rere 11012 rereb 11010 rerebd 11092 rerebi 11064 rered 11116 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11038 addcjd 11104 addcji 11074 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11148 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11199 abscjd 11337 abscji 11295 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11211 abs00d 11333 abs00i 11292 absne0d 11334 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11243 releabsd 11338 releabsi 11296 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11216 absmuld 11341 absmuli 11298 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11202 sqabsaddi 11299 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11251 abstrid 11343 abstrii 11302 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10613 exp0 10617 expp1 10620 expp1d 10748 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10655 expaddd 10749 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15088 cxpmuld 15111 expmul 10658 expmuld 10750 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10652 mulexpd 10762 rpmulcxp 15085 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10079 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11472 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11474 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11473 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11477 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11470 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11466 climcj 11467 climim 11469 climre 11468 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8061 df-xr 8060 ltxr 9844 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11493 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10372 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14044 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 14543 xmet0 14542 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 14550 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 14552 mstri 14652 xmettri 14551 xmstri 14651 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14458 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 14690 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11456 addcncntop 14741 mulcn2 11458 mulcncntop 14743 subcn2 11457 subcncntop 14742 |
| [Gleason] p. 295 | Remark | bcval3 10825 bcval4 10826 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10840 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10823 df-bc 10822 |
| [Gleason] p. 296 | Remark | bcn0 10829 bcnn 10831 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 11630 |
| [Gleason] p. 308 | Equation 2 | ef0 11818 |
| [Gleason] p. 308 | Equation 3 | efcj 11819 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 11824 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 11828 |
| [Gleason] p. 310 | Equation 14 | sinadd 11882 |
| [Gleason] p. 310 | Equation 15 | cosadd 11883 |
| [Gleason] p. 311 | Equation 17 | sincossq 11894 |
| [Gleason] p. 311 | Equation 18 | cosbnd 11899 sinbnd 11898 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 11799 |
| [Golan] p. 1 | Remark | srgisid 13485 |
| [Golan] p. 1 | Definition | df-srg 13463 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1460 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13086 mndideu 13010 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13113 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13142 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13153 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13175 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 15634 |
| [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 7287 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6554 |
| [HoTT], p. | Exercise 11.10 | neapmkv 15628 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8678 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7532 df-imp 7531 df-iplp 7530 df-reap 8596 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8692 rerecapb 8864 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6192 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7724 |
| [HoTT], p. | Corollary 11.4.3 | conventions 15283 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 15621 dceqnconst 15620 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 7962 caucvgpr 7744 caucvgprpr 7774 caucvgsr 7864 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7528 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 15626 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4329 ltpopr 7657 ltsopr 7658 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8627 reapcotr 8619 reapirr 8598 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8148 gt0add 8594 leadd1 8451 lelttr 8110 lemul1a 8879 lenlt 8097 ltadd1 8450 ltletr 8111 ltmul1 8613 reaplt 8609 |
| [Jech] p. 4 | Definition of class | cv 1363 cvjust 2188 |
| [Jech] p. 78 | Note | opthprc 4711 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1541 |
| [Kreyszig] p. 3 | Property M1 | metcl 14532 xmetcl 14531 |
| [Kreyszig] p. 4 | Property M2 | meteq0 14539 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8689 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 14621 |
| [Kreyszig] p. 19 | Remark | mopntopon 14622 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 14667 mopnm 14627 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 14665 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 14670 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 14692 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14392 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 13829 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 13820 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 13821 |
| [Kunen] p. 10 | Axiom 0 | a9e 1707 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4147 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6716 mapvalg 6714 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6710 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3923 |
| [Lang] p. 3 | Statement | lidrideqd 12967 mndbn0 13015 |
| [Lang] p. 3 | Definition | df-mnd 13001 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 12984 |
| [Lang] p. 5 | Equation | gsumfzreidx 13410 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13201 |
| [Lang] p. 7 | Definition | dfgrp2e 13103 |
| [Levy] p. 338 | Axiom | df-clab 2180 df-clel 2189 df-cleq 2186 |
| [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 1609 |
| [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 1513 |
| [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 1649 r19.2m 3534 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1565 19.3h 1564 rr19.3v 2900 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1489 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1630 alexim 1656 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1510 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1601 spsbe 1853 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1655 19.9h 1654 19.9v 1882 exlimd 1608 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1675 excomim 1674 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1676 r19.12 2600 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1657 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1479 ralbi 2626 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1566 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1567 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1615 rexbi 2627 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1677 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1468 alimd 1532 alimdh 1478 alimdv 1890 ralimdaa 2560 ralimdv 2562 ralimdva 2561 ralimdvva 2563 sbcimdv 3052 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1678 19.21 1594 19.21bi 1569 19.21h 1568 19.21ht 1592 19.21t 1593 19.21v 1884 alrimd 1621 alrimdd 1620 alrimdh 1490 alrimdv 1887 alrimi 1533 alrimih 1480 alrimiv 1885 alrimivv 1886 r19.21 2570 r19.21be 2585 r19.21bi 2582 r19.21t 2569 r19.21v 2571 ralrimd 2572 ralrimdv 2573 ralrimdva 2574 ralrimdvv 2578 ralrimdvva 2579 ralrimi 2565 ralrimiv 2566 ralrimiva 2567 ralrimivv 2575 ralrimivva 2576 ralrimivvva 2577 ralrimivw 2568 rexlimi 2604 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1892 2eximdv 1893 exim 1610 eximd 1623 eximdh 1622 eximdv 1891 rexim 2588 reximdai 2592 reximddv 2597 reximddv2 2599 reximdv 2595 reximdv2 2593 reximdva 2596 reximdvai 2594 reximi2 2590 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1689 19.23bi 1603 19.23h 1509 19.23ht 1508 19.23t 1688 19.23v 1894 19.23vv 1895 exlimd2 1606 exlimdh 1607 exlimdv 1830 exlimdvv 1909 exlimi 1605 exlimih 1604 exlimiv 1609 exlimivv 1908 r19.23 2602 r19.23v 2603 rexlimd 2608 rexlimdv 2610 rexlimdv3a 2613 rexlimdva 2611 rexlimdva2 2614 rexlimdvaa 2612 rexlimdvv 2618 rexlimdvva 2619 rexlimdvw 2615 rexlimiv 2605 rexlimiva 2606 rexlimivv 2617 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1650 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1637 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1493 19.26-3an 1494 19.26 1492 r19.26-2 2623 r19.26-3 2624 r19.26 2620 r19.26m 2625 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1572 19.27h 1571 19.27v 1911 r19.27av 2629 r19.27m 3543 r19.27mv 3544 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1574 19.28h 1573 19.28v 1912 r19.28av 2630 r19.28m 3537 r19.28mv 3540 rr19.28v 2901 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1631 19.29r 1632 19.29r2 1633 19.29x 1634 r19.29 2631 r19.29d2r 2638 r19.29r 2632 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1638 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1692 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1690 19.32r 1691 r19.32r 2640 r19.32vdc 2643 r19.32vr 2642 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1495 19.33b2 1640 19.33bdc 1641 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1695 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1635 19.35i 1636 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1684 19.36aiv 1913 19.36i 1683 r19.36av 2645 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1685 19.37aiv 1686 r19.37 2646 r19.37av 2647 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1687 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1651 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1643 19.40 1642 r19.40 2648 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1697 19.41h 1696 19.41v 1914 19.41vv 1915 19.41vvv 1916 19.41vvvv 1917 r19.41 2649 r19.41v 2650 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1699 19.42h 1698 19.42v 1918 19.42vv 1923 19.42vvv 1924 19.42vvvv 1925 r19.42v 2651 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1639 r19.43 2652 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1693 r19.44av 2653 r19.44mv 3542 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1694 r19.45av 2654 r19.45mv 3541 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2067 |
| [Megill] p. 444 | Axiom C5 | ax-17 1537 |
| [Megill] p. 445 | Lemma L12 | alequcom 1526 ax-10 1516 |
| [Megill] p. 446 | Lemma L17 | equtrr 1721 |
| [Megill] p. 446 | Lemma L19 | hbnae 1732 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1774 sbid 1785 |
| [Megill] p. 448 | Scheme C5' | ax-4 1521 |
| [Megill] p. 448 | Scheme C6' | ax-7 1459 |
| [Megill] p. 448 | Scheme C8' | ax-8 1515 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1518 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1727 |
| [Megill] p. 448 | Scheme C12' | ax-13 2166 |
| [Megill] p. 448 | Scheme C13' | ax-14 2167 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1834 |
| [Megill] p. 448 | Scheme C16' | ax-16 1825 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1741 dral2 1742 drex1 1809 drex2 1743 drsb1 1810 drsb2 1852 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2003 sbequ 1851 sbid2v 2012 |
| [Megill] p. 450 | Example in Appendix | hba1 1551 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3069 rspsbca 3070 stdpc4 1786 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3075 stdpc5 1595 |
| [Mendelson] p. 81 | Rule C | exlimiv 1609 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1714 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1781 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3484 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3485 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3400 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3448 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3401 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3291 |
| [Mendelson] p. 231 | Definition of union | unssin 3399 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4508 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3835 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4314 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4315 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4316 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3856 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4792 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5187 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4403 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 6903 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6877 xpsneng 6878 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6883 xpcomeng 6884 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6886 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6880 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6708 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6867 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 6908 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6742 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6868 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7279 djucomen 7278 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7277 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6522 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3382 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4748 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4749 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4092 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5182 coi2 5183 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4877 rn0 4919 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5071 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4769 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4883 rnxpm 5096 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4740 xp0 5086 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5025 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5022 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5021 imaexg 5020 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5017 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5689 funfvop 5671 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5601 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5609 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5299 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5812 dff13f 5814 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5782 funrnex 6168 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5806 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5150 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3887 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6210 df-1st 6195 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6211 df-2nd 6196 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1458 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1515 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1517 ax-11o 1834 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1838 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1459 |
| [Monk2] p. 109 | Lemma 15 | equvin 1874 equvini 1769 eqvinop 4273 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1537 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1662 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1459 |
| [Monk2] p. 114 | Lemma 22 | hba1 1551 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1563 nfia1 1591 |
| [Monk2] p. 114 | Lemma 24 | hba2 1562 nfa2 1590 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 832 dftest 15635 |
| [Munkres] p. 77 | Example 2 | distop 14264 |
| [Munkres] p. 78 | Definition of basis | df-bases 14222 isbasis3g 14225 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 12874 tgval2 14230 |
| [Munkres] p. 79 | Remark | tgcl 14243 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14237 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14258 tgss3 14257 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14259 basgen2 14260 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14349 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14291 topcld 14288 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14292 |
| [Munkres] p. 94 | Definition of closure | clsval 14290 |
| [Munkres] p. 94 | Definition of interior | ntrval 14289 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14367 iscn 14376 iscn2 14379 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14409 cncnp2m 14410 cncnpi 14407 df-cnp 14368 iscnp 14378 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 14693 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 6961 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7225 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7213 omniwomnimkv 7228 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3270 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7196 exmidomniim 7202 finomni 7201 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7181 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 15581 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 15583 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 6966 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7263 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7264 exmidfodomrlemrALT 7265 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7210 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 15567 peano4nninf 15566 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 15569 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 15577 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 15579 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 15565 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2180 rabid 2670 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2007 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2186 |
| [Quine] p. 19 | Definition 2.9 | df-v 2762 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2302 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2314 abid2f 2362 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1899 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1897 sb6 1898 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2189 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2193 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2195 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 2987 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 2988 dfsbcq2 2989 |
| [Quine] p. 43 | Theorem 6.8 | vex 2763 |
| [Quine] p. 43 | Theorem 6.9 | isset 2766 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2843 spcgv 2848 spcimgf 2841 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 2998 spsbcd 2999 |
| [Quine] p. 44 | Theorem 6.12 | elex 2771 |
| [Quine] p. 44 | Theorem 6.13 | elab 2905 elabg 2907 elabgf 2903 |
| [Quine] p. 44 | Theorem 6.14 | noel 3451 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3684 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3626 df-sn 3625 |
| [Quine] p. 49 | Theorem 7.4 | snss 3754 snssg 3753 |
| [Quine] p. 49 | Theorem 7.5 | prss 3775 prssg 3776 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3725 prid1g 3723 prid2 3726 prid2g 3724 snid 3650 snidg 3648 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4214 snexprc 4216 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4241 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3852 unisng 3853 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3855 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3864 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3863 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5226 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5217 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5227 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5231 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5232 |
| [Quine] p. 58 | Definition 9.1 | df-op 3628 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4287 opabidw 4288 opelopab 4303 opelopaba 4297 opelopabaf 4305 opelopabf 4306 opelopabg 4299 opelopabga 4294 opelopabgf 4301 oprabid 5951 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4666 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4668 |
| [Quine] p. 64 | Definition 9.15 | df-id 4325 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5313 |
| [Quine] p. 65 | Theorem 10.4 | funi 5287 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5303 funsng 5301 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5257 |
| [Quine] p. 65 | Definition 10.2 | args 5035 dffv4g 5552 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5263 fv2 5550 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10798 nn0opth2d 10797 nn0opthd 10796 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5340 funimaexg 5339 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13432 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13497 |
| [Rudin] p. 164 | Equation 27 | efcan 11822 |
| [Rudin] p. 164 | Equation 30 | efzval 11829 |
| [Rudin] p. 167 | Equation 48 | absefi 11915 |
| [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 5051 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5053 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5050 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5048 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 13499 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14262 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3425 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3519 dif0 3518 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3532 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3418 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3419 |
| [Stoll] p. 20 | Remark | invdif 3402 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3629 |
| [Stoll] p. 43 | Definition | uniiun 3967 |
| [Stoll] p. 44 | Definition | intiin 3968 |
| [Stoll] p. 45 | Definition | df-iin 3916 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3915 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 890 imanst 889 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3425 |
| [Suppes] p. 22 | Theorem 2 | eq0 3466 |
| [Suppes] p. 22 | Theorem 4 | eqss 3195 eqssd 3197 eqssi 3196 |
| [Suppes] p. 23 | Theorem 5 | ss0 3488 ss0b 3487 |
| [Suppes] p. 23 | Theorem 6 | sstr 3188 |
| [Suppes] p. 25 | Theorem 12 | elin 3343 elun 3301 |
| [Suppes] p. 26 | Theorem 15 | inidm 3369 |
| [Suppes] p. 26 | Theorem 16 | in0 3482 |
| [Suppes] p. 27 | Theorem 23 | unidm 3303 |
| [Suppes] p. 27 | Theorem 24 | un0 3481 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3323 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3330 |
| [Suppes] p. 27 | Theorem 27 | unss 3334 |
| [Suppes] p. 27 | Theorem 28 | indir 3409 |
| [Suppes] p. 27 | Theorem 29 | undir 3410 |
| [Suppes] p. 28 | Theorem 32 | difid 3516 difidALT 3517 |
| [Suppes] p. 29 | Theorem 33 | difin 3397 |
| [Suppes] p. 29 | Theorem 34 | indif 3403 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3522 |
| [Suppes] p. 29 | Theorem 36 | difun2 3527 |
| [Suppes] p. 29 | Theorem 37 | difin0 3521 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3520 |
| [Suppes] p. 29 | Theorem 39 | difundi 3412 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3414 |
| [Suppes] p. 30 | Theorem 41 | nalset 4160 |
| [Suppes] p. 39 | Theorem 61 | uniss 3857 |
| [Suppes] p. 39 | Theorem 65 | uniop 4285 |
| [Suppes] p. 41 | Theorem 70 | intsn 3906 |
| [Suppes] p. 42 | Theorem 71 | intpr 3903 intprg 3904 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4510 op1stbg 4511 |
| [Suppes] p. 42 | Theorem 78 | intun 3902 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3947 dfiun2g 3945 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3948 |
| [Suppes] p. 47 | Theorem 86 | elpw 3608 elpw2 4187 elpw2g 4186 elpwg 3610 |
| [Suppes] p. 47 | Theorem 87 | pwid 3617 |
| [Suppes] p. 47 | Theorem 89 | pw0 3766 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3831 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4767 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4798 xpindir 4799 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4716 xpundir 4717 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4581 |
| [Suppes] p. 58 | Theorem 2 | relss 4747 |
| [Suppes] p. 59 | Theorem 4 | eldm 4860 eldm2 4861 eldm2g 4859 eldmg 4858 |
| [Suppes] p. 59 | Definition 3 | df-dm 4670 |
| [Suppes] p. 60 | Theorem 6 | dmin 4871 |
| [Suppes] p. 60 | Theorem 8 | rnun 5075 |
| [Suppes] p. 60 | Theorem 9 | rnin 5076 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4851 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4846 brcnvg 4844 |
| [Suppes] p. 62 | Equation 5 | elcnv 4840 elcnv2 4841 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5044 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5074 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5072 |
| [Suppes] p. 63 | Theorem 20 | co02 5180 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4932 |
| [Suppes] p. 63 | Definition 7 | df-co 4669 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4848 |
| [Suppes] p. 64 | Theorem 27 | coass 5185 |
| [Suppes] p. 65 | Theorem 31 | resundi 4956 |
| [Suppes] p. 65 | Theorem 34 | elima 5011 elima2 5012 elima3 5013 elimag 5010 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5079 |
| [Suppes] p. 66 | Theorem 40 | dminss 5081 |
| [Suppes] p. 66 | Theorem 41 | imainss 5082 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5085 |
| [Suppes] p. 81 | Definition 34 | dfec2 6592 |
| [Suppes] p. 82 | Theorem 72 | elec 6630 elecg 6629 |
| [Suppes] p. 82 | Theorem 73 | erth 6635 erth2 6636 |
| [Suppes] p. 89 | Theorem 96 | map0b 6743 |
| [Suppes] p. 89 | Theorem 97 | map0 6745 map0g 6744 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6746 |
| [Suppes] p. 89 | Theorem 99 | mapss 6747 |
| [Suppes] p. 92 | Theorem 1 | enref 6821 enrefg 6820 |
| [Suppes] p. 92 | Theorem 2 | ensym 6837 ensymb 6836 ensymi 6838 |
| [Suppes] p. 92 | Theorem 3 | entr 6840 |
| [Suppes] p. 92 | Theorem 4 | unen 6872 |
| [Suppes] p. 94 | Theorem 15 | endom 6819 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6834 |
| [Suppes] p. 94 | Theorem 17 | domtr 6841 |
| [Suppes] p. 95 | Theorem 18 | isbth 7028 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6862 fundmeng 6863 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6890 |
| [Suppes] p. 130 | Definition 3 | df-tr 4129 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4521 |
| [Suppes] p. 134 | Definition 6 | df-suc 4403 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4636 finds 4633 finds1 4635 finds2 4634 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7415 df-ltpq 7408 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4422 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2175 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2186 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2189 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2188 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2211 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5923 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2985 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3640 elpr2 3641 elprg 3639 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3635 elsn2 3653 elsn2g 3652 elsng 3634 velsn 3636 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4261 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3630 sneqr 3787 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3638 dfsn2 3633 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4469 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4267 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4245 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4473 unexg 4475 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3668 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3837 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3160 df-un 3158 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3850 uniprg 3851 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4209 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3667 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4438 elsucg 4436 sstr2 3187 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3304 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3352 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3317 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3370 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3407 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3408 |
| [TakeutiZaring] p. 17 | Definition 5.9 | dfss2 3169 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3604 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3331 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3167 sseqin2 3379 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3200 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3380 inss2 3381 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3240 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3845 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4246 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4253 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2481 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4157 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3156 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3449 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3516 difidALT 3517 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3460 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4572 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2762 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4162 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3486 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4167 ssexg 4169 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4164 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4583 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4574 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3512 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3285 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3421 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3286 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3294 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2477 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2478 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4775 xpexg 4774 xpexgALT 6187 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4667 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5319 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5471 fun11 5322 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5266 svrelfun 5320 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4850 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4852 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4672 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4673 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4669 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5121 dfrel2 5117 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4768 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4777 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4783 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4797 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4971 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4948 opelresg 4950 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4964 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4967 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4972 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5296 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5165 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5295 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5472 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2086 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5263 fv3 5578 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5205 cnvexg 5204 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4929 dmexg 4927 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4930 rnexg 4928 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5572 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5582 tz6.12 5583 tz6.12c 5585 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5546 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5258 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5259 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5261 wfo 5253 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5260 wf1 5252 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5262 wf1o 5254 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5656 eqfnfv2 5657 eqfnfv2f 5660 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5628 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5781 fnexALT 6165 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5780 resfunexgALT 6162 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5340 funimaexg 5339 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4031 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5036 iniseg 5038 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4321 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5264 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5854 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5855 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5860 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5862 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5870 |
| [TakeutiZaring] p. 35 | Notation | wtr 4128 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4386 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4132 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4609 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4413 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4417 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4525 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4400 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4519 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4585 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4615 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4130 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4544 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4520 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3864 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4403 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4447 sucidg 4448 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4534 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4401 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4539 ordelsuc 4538 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4627 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4628 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4629 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4626 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4640 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4632 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4630 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4631 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3885 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4144 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3886 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4550 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3872 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6363 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6420 tfri1d 6390 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6421 tfri2d 6391 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6422 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6357 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6341 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6519 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6515 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6512 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6516 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6564 nnaordi 6563 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3958 uniss2 3867 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6525 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6535 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6526 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6513 omsuc 6527 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6536 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6572 nnmordi 6571 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6514 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7249 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6851 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6915 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6916 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6799 isfi 6817 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6887 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6706 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 6893 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 6906 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1521 |
| [Tarski] p. 68 | Lemma 6 | equid 1712 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1715 |
| [Tarski] p. 70 | Lemma 14 | spim 1749 spime 1752 spimeh 1750 spimh 1748 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1517 ax-11o 1834 ax11i 1725 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1898 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1537 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2166 ax-14 2167 |
| [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 2140 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 1492 |
| [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 1646 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1496 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1643 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1907 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2045 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2445 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2446 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2899 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3043 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5235 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5236 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2121 eupickbi 2124 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5263 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7252 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |