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 7190 fidcenum 7031 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7031 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7190 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 12667 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7002 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 6988 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 12682 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 12684 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 12673 znnen 12640 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 12685 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 12686 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 10885 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4574 |
| [AhoHopUll] p. 318 | Section 9.1 | df-word 10953 lencl 10956 wrd0 10977 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8223 addcan2d 8228 addcan2i 8226 addcand 8227 addcani 8225 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8234 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8291 negsubd 8360 negsubi 8321 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8293 negnegd 8345 negnegi 8313 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8428 subdid 8457 subdii 8450 subdir 8429 subdird 8458 subdiri 8451 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8432 mul01d 8436 mul01i 8434 mul02 8430 mul02d 8435 mul02i 8433 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8837 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8788 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8441 mul2negd 8456 mul2negi 8449 mulneg1 8438 mulneg1d 8454 mulneg1i 8447 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 13776 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8757 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9769 rpaddcld 9804 rpmulcl 9770 rpmulcld 9805 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9781 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8148 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8582 ltadd1dd 8600 ltadd1i 8546 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8636 ltmul1a 8635 ltmul1i 8964 ltmul1ii 8972 ltmul2 8900 ltmul2d 9831 ltmul2dd 9845 ltmul2i 8967 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8170 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8512 lt0neg1d 8559 ltneg 8506 ltnegd 8567 ltnegi 8537 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8489 lt2addd 8611 lt2addi 8554 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9746 |
| [Apostol] p. 21 | Exercise 4 | recgt0 8894 recgt0d 8978 recgt0i 8950 recgt0ii 8951 |
| [Apostol] p. 22 | Definition of integers | df-z 9344 |
| [Apostol] p. 22 | Definition of rationals | df-q 9711 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7069 |
| [Apostol] p. 26 | Theorem I.29 | arch 9263 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9462 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9264 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10363 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12053 zneo 9444 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11213 sqrtthi 11301 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9010 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12228 |
| [Apostol] p. 363 | Remark | absgt0api 11328 |
| [Apostol] p. 363 | Example | abssubd 11375 abssubi 11332 |
| [ApostolNT] p. 14 | Definition | df-dvds 11970 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 11986 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12010 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12006 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12000 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12002 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 11987 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 11988 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 11993 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12027 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12029 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12031 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12206 |
| [ApostolNT] p. 16 | Definition | isprm2 12310 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12285 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 12697 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12165 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12207 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12209 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12179 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12172 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12337 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12339 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12562 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12106 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12252 |
| [ApostolNT] p. 25 | Definition | df-phi 12404 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12434 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12415 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12419 |
| [ApostolNT] p. 38 | Remark | df-sgm 15302 |
| [ApostolNT] p. 38 | Definition | df-sgm 15302 |
| [ApostolNT] p. 104 | Definition | congr 12293 |
| [ApostolNT] p. 106 | Remark | dvdsval3 11973 |
| [ApostolNT] p. 106 | Definition | moddvds 11981 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12060 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12061 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10450 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10487 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10775 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12005 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12296 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12615 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12298 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12426 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12445 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12427 |
| [ApostolNT] p. 179 | Definition | df-lgs 15323 lgsprme0 15367 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15368 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15344 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15359 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15410 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15429 2lgsoddprm 15438 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15394 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15405 |
| [ApostolNT] p. 188 | Definition | df-lgs 15323 lgs1 15369 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15360 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15362 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15370 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15371 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 617 pm2.65 660 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5924 onsucelsucexmidlem 4566 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 15728 |
| [Bauer], p. 483 | Definition | n0rf 3464 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15296 2irrexpqap 15298 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6946 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 14973 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 14963 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8689 |
| [BauerSwan], p. 14 | Remark | 0ct 7182 ctm 7184 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 15731 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7190 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7585 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7498 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7587 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7621 addlocpr 7620 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7647 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7650 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7655 |
| [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 4155 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4211 |
| [BellMachover] p. 466 | Axiom Union | axun2 4471 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4579 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4420 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4582 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4533 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4405 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4626 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4651 |
| [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 13058 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13104 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13119 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13630 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13565 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5833 fcofo 5834 |
| [BourbakiTop1] p. | Remark | xnegmnf 9921 xnegpnf 9920 |
| [BourbakiTop1] p. | Remark | rexneg 9922 |
| [BourbakiTop1] p. | Proposition | ishmeo 14624 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14477 |
| [BourbakiTop1] p. | Property V_ii | innei 14483 |
| [BourbakiTop1] p. | Property V_iv | neissex 14485 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14474 neiss 14470 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14542 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 14619 |
| [BourbakiTop1] p. | Property V_iii | elnei 14472 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14318 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13058 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13104 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13301 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4097 |
| [Cohen] p. 301 | Remark | relogoprlem 15188 |
| [Cohen] p. 301 | Property 2 | relogmul 15189 relogmuld 15204 |
| [Cohen] p. 301 | Property 3 | relogdiv 15190 relogdivd 15205 |
| [Cohen] p. 301 | Property 4 | relogexp 15192 |
| [Cohen] p. 301 | Property 1a | log1 15186 |
| [Cohen] p. 301 | Property 1b | loge 15187 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15285 |
| [Cohen4] p. 352 | Definition | rpelogb 15269 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15275 |
| [Cohen4] p. 361 | Property 3 | logbrec 15280 rprelogbdiv 15277 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15273 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15278 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15267 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15268 |
| [Cohen4] p. 367 | Property | rplogbchbase 15270 |
| [Cohen4] p. 377 | Property 2 | logblt 15282 |
| [Crosilla] p. | Axiom 1 | ax-ext 2178 |
| [Crosilla] p. | Axiom 2 | ax-pr 4243 |
| [Crosilla] p. | Axiom 3 | ax-un 4469 |
| [Crosilla] p. | Axiom 4 | ax-nul 4160 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4625 |
| [Crosilla] p. | Axiom 6 | ru 2988 |
| [Crosilla] p. | Axiom 8 | ax-pow 4208 |
| [Crosilla] p. | Axiom 9 | ax-setind 4574 |
| [Crosilla], p. | Axiom 6 | ax-sep 4152 |
| [Crosilla], p. | Axiom 7 | ax-coll 4149 |
| [Crosilla], p. | Axiom 7' | repizf 4150 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4558 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5924 |
| [Crosilla], p. | Definition of ordinal | df-iord 4402 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4572 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3159 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4628 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6718 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4159 |
| [Enderton] p. 19 | Definition | df-tp 3631 |
| [Enderton] p. 26 | Exercise 5 | unissb 3870 |
| [Enderton] p. 26 | Exercise 10 | pwel 4252 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4322 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3987 iinin2m 3986 iunin1 3982 iunin2 3981 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3985 iundif2ss 3983 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4000 |
| [Enderton] p. 33 | Exercise 25 | iununir 4001 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4008 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4516 iunpwss 4009 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4251 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4226 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4486 rnex 4934 rnexg 4932 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4877 rnuni 5082 |
| [Enderton] p. 42 | Definition of a function | dffun7 5286 dffun8 5287 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5628 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5320 |
| [Enderton] p. 44 | Definition (d) | dfima2 5012 dfima3 5013 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5633 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7289 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5811 |
| [Enderton] p. 52 | Definition | df-map 6718 |
| [Enderton] p. 53 | Exercise 21 | coass 5189 |
| [Enderton] p. 53 | Exercise 27 | dmco 5179 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5330 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5046 |
| [Enderton] p. 54 | Remark | ixpf 6788 ixpssmap 6800 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6767 |
| [Enderton] p. 56 | Theorem 3M | erref 6621 |
| [Enderton] p. 57 | Lemma 3N | erthi 6649 |
| [Enderton] p. 57 | Definition | df-ec 6603 |
| [Enderton] p. 58 | Definition | df-qs 6607 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6708 th3qcor 6707 th3qlem1 6705 th3qlem2 6706 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6603 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4874 |
| [Enderton] p. 68 | Definition of successor | df-suc 4407 |
| [Enderton] p. 71 | Definition | df-tr 4133 dftr4 4137 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4449 unisucg 4450 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4449 unisucg 4450 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4146 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4147 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6541 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6543 onasuc 6533 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5928 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6542 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6544 onmsuc 6540 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6552 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6545 nnacom 6551 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6553 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6554 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6556 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6546 nnmsucr 6555 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6595 |
| [Enderton] p. 129 | Definition | df-en 6809 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5878 |
| [Enderton] p. 133 | Exercise 1 | xpomen 12637 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6935 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6927 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 6916 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7301 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7297 dju1en 7296 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3527 |
| [Enderton] p. 145 | Figure 38 | ffoss 5539 |
| [Enderton] p. 145 | Definition | df-dom 6810 |
| [Enderton] p. 146 | Example 1 | domen 6819 domeng 6820 |
| [Enderton] p. 146 | Example 3 | nndomo 6934 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6903 xpdom1g 6901 xpdom2g 6900 |
| [Enderton] p. 168 | Definition | df-po 4332 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4464 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4425 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4580 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4428 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4553 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4526 |
| [Enderton] p. 194 | Remark | onprc 4589 |
| [Enderton] p. 194 | Exercise 16 | suc11 4595 |
| [Enderton] p. 197 | Definition | df-card 7257 |
| [Enderton] p. 200 | Exercise 25 | tfis 4620 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4591 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4593 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4594 |
| [Geuvers], p. 1 | Remark | expap0 10678 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8659 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8698 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8660 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8015 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11385 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11393 maxle2 11394 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11395 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11398 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11399 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8626 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7431 enqer 7442 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7435 df-nqqs 7432 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7428 df-plqqs 7433 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7429 df-mqqs 7434 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7436 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7492 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7495 ltbtwnnq 7500 ltbtwnnqq 7499 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7484 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7485 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7621 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7663 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7662 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7681 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7697 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7703 ltaprlem 7702 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7700 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7656 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7676 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7665 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7664 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7672 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7722 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7810 enrer 7819 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7815 df-1r 7816 df-nr 7811 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7813 df-plr 7812 negexsr 7856 recexsrlem 7858 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7814 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9004 creur 9003 cru 8646 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8007 axcnre 7965 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11040 crimd 11159 crimi 11119 crre 11039 crred 11158 crrei 11118 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11042 remimd 11124 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11239 absval2d 11367 absval2i 11326 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11066 cjaddd 11147 cjaddi 11114 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11067 cjmuld 11148 cjmuli 11115 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11065 cjcjd 11125 cjcji 11097 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11064 cjreb 11048 cjrebd 11128 cjrebi 11100 cjred 11153 rere 11047 rereb 11045 rerebd 11127 rerebi 11099 rered 11151 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11073 addcjd 11139 addcji 11109 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11183 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11234 abscjd 11372 abscji 11330 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11246 abs00d 11368 abs00i 11327 absne0d 11369 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11278 releabsd 11373 releabsi 11331 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11251 absmuld 11376 absmuli 11333 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11237 sqabsaddi 11334 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11286 abstrid 11378 abstrii 11337 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10648 exp0 10652 expp1 10655 expp1d 10783 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10690 expaddd 10784 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15232 cxpmuld 15257 expmul 10693 expmuld 10785 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10687 mulexpd 10797 rpmulcxp 15229 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10102 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11508 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11510 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11509 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11513 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11506 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11502 climcj 11503 climim 11505 climre 11504 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8083 df-xr 8082 ltxr 9867 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11529 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10407 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14177 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 14684 xmet0 14683 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 14691 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 14693 mstri 14793 xmettri 14692 xmstri 14792 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14599 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 14831 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11492 addcncntop 14882 mulcn2 11494 mulcncntop 14884 subcn2 11493 subcncntop 14883 |
| [Gleason] p. 295 | Remark | bcval3 10860 bcval4 10861 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10875 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10858 df-bc 10857 |
| [Gleason] p. 296 | Remark | bcn0 10864 bcnn 10866 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 11666 |
| [Gleason] p. 308 | Equation 2 | ef0 11854 |
| [Gleason] p. 308 | Equation 3 | efcj 11855 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 11860 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 11864 |
| [Gleason] p. 310 | Equation 14 | sinadd 11918 |
| [Gleason] p. 310 | Equation 15 | cosadd 11919 |
| [Gleason] p. 311 | Equation 17 | sincossq 11930 |
| [Gleason] p. 311 | Equation 18 | cosbnd 11935 sinbnd 11934 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 11835 |
| [Golan] p. 1 | Remark | srgisid 13618 |
| [Golan] p. 1 | Definition | df-srg 13596 |
| [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 13213 mndideu 13128 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13240 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13269 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13280 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13302 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 15805 |
| [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 7308 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6566 |
| [HoTT], p. | Exercise 11.10 | neapmkv 15799 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8701 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7554 df-imp 7553 df-iplp 7552 df-reap 8619 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8715 rerecapb 8887 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6204 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7746 |
| [HoTT], p. | Corollary 11.4.3 | conventions 15451 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 15792 dceqnconst 15791 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 7984 caucvgpr 7766 caucvgprpr 7796 caucvgsr 7886 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7550 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 15797 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4333 ltpopr 7679 ltsopr 7680 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8650 reapcotr 8642 reapirr 8621 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8170 gt0add 8617 leadd1 8474 lelttr 8132 lemul1a 8902 lenlt 8119 ltadd1 8473 ltletr 8133 ltmul1 8636 reaplt 8632 |
| [Jech] p. 4 | Definition of class | cv 1363 cvjust 2191 |
| [Jech] p. 78 | Note | opthprc 4715 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1544 |
| [Kreyszig] p. 3 | Property M1 | metcl 14673 xmetcl 14672 |
| [Kreyszig] p. 4 | Property M2 | meteq0 14680 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8712 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 14762 |
| [Kreyszig] p. 19 | Remark | mopntopon 14763 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 14808 mopnm 14768 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 14806 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 14811 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 14833 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14533 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 13962 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 13953 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 13954 |
| [Kunen] p. 10 | Axiom 0 | a9e 1710 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4151 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6728 mapvalg 6726 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6722 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3927 |
| [Lang] p. 3 | Statement | lidrideqd 13083 mndbn0 13133 |
| [Lang] p. 3 | Definition | df-mnd 13119 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13100 |
| [Lang] p. 5 | Equation | gsumfzreidx 13543 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13334 |
| [Lang] p. 7 | Definition | dfgrp2e 13230 |
| [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 3538 |
| [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 3547 r19.27mv 3548 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1577 19.28h 1576 19.28v 1915 r19.28av 2633 r19.28m 3541 r19.28mv 3544 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 3546 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1697 r19.45av 2657 r19.45mv 3545 |
| [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 3488 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3489 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3404 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3452 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3405 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3295 |
| [Mendelson] p. 231 | Definition of union | unssin 3403 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4512 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3839 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4318 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4319 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4320 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3860 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4796 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5191 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4407 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 6915 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6889 xpsneng 6890 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6895 xpcomeng 6896 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6898 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6892 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6720 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6879 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 6920 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6754 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6880 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7300 djucomen 7299 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7298 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6534 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3386 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4752 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4753 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4096 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5186 coi2 5187 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4881 rn0 4923 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5075 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4773 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4887 rnxpm 5100 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4744 xp0 5090 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5029 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5026 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5025 imaexg 5024 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5021 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5695 funfvop 5677 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5607 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5615 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5303 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5818 dff13f 5820 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5788 funrnex 6180 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5812 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5154 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3891 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6222 df-1st 6207 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6223 df-2nd 6208 |
| [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 4277 |
| [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 15806 |
| [Munkres] p. 77 | Example 2 | distop 14405 |
| [Munkres] p. 78 | Definition of basis | df-bases 14363 isbasis3g 14366 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 12962 tgval2 14371 |
| [Munkres] p. 79 | Remark | tgcl 14384 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14378 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14399 tgss3 14398 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14400 basgen2 14401 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14490 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14432 topcld 14429 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14433 |
| [Munkres] p. 94 | Definition of closure | clsval 14431 |
| [Munkres] p. 94 | Definition of interior | ntrval 14430 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14508 iscn 14517 iscn2 14520 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14550 cncnp2m 14551 cncnpi 14548 df-cnp 14509 iscnp 14519 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 14834 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 6973 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7239 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7227 omniwomnimkv 7242 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3274 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7210 exmidomniim 7216 finomni 7215 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7195 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 15752 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 15754 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 6978 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7280 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7281 exmidfodomrlemrALT 7282 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7224 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 15738 peano4nninf 15737 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 15740 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 15748 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 15750 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 15736 |
| [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 3455 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3688 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3630 df-sn 3629 |
| [Quine] p. 49 | Theorem 7.4 | snss 3758 snssg 3757 |
| [Quine] p. 49 | Theorem 7.5 | prss 3779 prssg 3780 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3729 prid1g 3727 prid2 3730 prid2g 3728 snid 3654 snidg 3652 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4218 snexprc 4220 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4245 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3856 unisng 3857 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3859 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3868 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3867 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5230 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5221 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5231 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5235 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5236 |
| [Quine] p. 58 | Definition 9.1 | df-op 3632 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4291 opabidw 4292 opelopab 4307 opelopaba 4301 opelopabaf 4309 opelopabf 4310 opelopabg 4303 opelopabga 4298 opelopabgf 4305 oprabid 5957 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4670 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4672 |
| [Quine] p. 64 | Definition 9.15 | df-id 4329 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5317 |
| [Quine] p. 65 | Theorem 10.4 | funi 5291 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5307 funsng 5305 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5261 |
| [Quine] p. 65 | Definition 10.2 | args 5039 dffv4g 5558 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5267 fv2 5556 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10833 nn0opth2d 10832 nn0opthd 10831 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5344 funimaexg 5343 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13565 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13630 |
| [Rudin] p. 164 | Equation 27 | efcan 11858 |
| [Rudin] p. 164 | Equation 30 | efzval 11865 |
| [Rudin] p. 167 | Equation 48 | absefi 11951 |
| [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 5055 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5057 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5054 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5052 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 13632 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14403 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3429 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3523 dif0 3522 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3536 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3422 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3423 |
| [Stoll] p. 20 | Remark | invdif 3406 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3633 |
| [Stoll] p. 43 | Definition | uniiun 3971 |
| [Stoll] p. 44 | Definition | intiin 3972 |
| [Stoll] p. 45 | Definition | df-iin 3920 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3919 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 890 imanst 889 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3429 |
| [Suppes] p. 22 | Theorem 2 | eq0 3470 |
| [Suppes] p. 22 | Theorem 4 | eqss 3199 eqssd 3201 eqssi 3200 |
| [Suppes] p. 23 | Theorem 5 | ss0 3492 ss0b 3491 |
| [Suppes] p. 23 | Theorem 6 | sstr 3192 |
| [Suppes] p. 25 | Theorem 12 | elin 3347 elun 3305 |
| [Suppes] p. 26 | Theorem 15 | inidm 3373 |
| [Suppes] p. 26 | Theorem 16 | in0 3486 |
| [Suppes] p. 27 | Theorem 23 | unidm 3307 |
| [Suppes] p. 27 | Theorem 24 | un0 3485 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3327 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3334 |
| [Suppes] p. 27 | Theorem 27 | unss 3338 |
| [Suppes] p. 27 | Theorem 28 | indir 3413 |
| [Suppes] p. 27 | Theorem 29 | undir 3414 |
| [Suppes] p. 28 | Theorem 32 | difid 3520 difidALT 3521 |
| [Suppes] p. 29 | Theorem 33 | difin 3401 |
| [Suppes] p. 29 | Theorem 34 | indif 3407 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3526 |
| [Suppes] p. 29 | Theorem 36 | difun2 3531 |
| [Suppes] p. 29 | Theorem 37 | difin0 3525 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3524 |
| [Suppes] p. 29 | Theorem 39 | difundi 3416 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3418 |
| [Suppes] p. 30 | Theorem 41 | nalset 4164 |
| [Suppes] p. 39 | Theorem 61 | uniss 3861 |
| [Suppes] p. 39 | Theorem 65 | uniop 4289 |
| [Suppes] p. 41 | Theorem 70 | intsn 3910 |
| [Suppes] p. 42 | Theorem 71 | intpr 3907 intprg 3908 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4514 op1stbg 4515 |
| [Suppes] p. 42 | Theorem 78 | intun 3906 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3951 dfiun2g 3949 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3952 |
| [Suppes] p. 47 | Theorem 86 | elpw 3612 elpw2 4191 elpw2g 4190 elpwg 3614 |
| [Suppes] p. 47 | Theorem 87 | pwid 3621 |
| [Suppes] p. 47 | Theorem 89 | pw0 3770 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3835 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4771 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4802 xpindir 4803 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4720 xpundir 4721 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4585 |
| [Suppes] p. 58 | Theorem 2 | relss 4751 |
| [Suppes] p. 59 | Theorem 4 | eldm 4864 eldm2 4865 eldm2g 4863 eldmg 4862 |
| [Suppes] p. 59 | Definition 3 | df-dm 4674 |
| [Suppes] p. 60 | Theorem 6 | dmin 4875 |
| [Suppes] p. 60 | Theorem 8 | rnun 5079 |
| [Suppes] p. 60 | Theorem 9 | rnin 5080 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4855 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4850 brcnvg 4848 |
| [Suppes] p. 62 | Equation 5 | elcnv 4844 elcnv2 4845 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5048 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5078 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5076 |
| [Suppes] p. 63 | Theorem 20 | co02 5184 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4936 |
| [Suppes] p. 63 | Definition 7 | df-co 4673 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4852 |
| [Suppes] p. 64 | Theorem 27 | coass 5189 |
| [Suppes] p. 65 | Theorem 31 | resundi 4960 |
| [Suppes] p. 65 | Theorem 34 | elima 5015 elima2 5016 elima3 5017 elimag 5014 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5083 |
| [Suppes] p. 66 | Theorem 40 | dminss 5085 |
| [Suppes] p. 66 | Theorem 41 | imainss 5086 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5089 |
| [Suppes] p. 81 | Definition 34 | dfec2 6604 |
| [Suppes] p. 82 | Theorem 72 | elec 6642 elecg 6641 |
| [Suppes] p. 82 | Theorem 73 | erth 6647 erth2 6648 |
| [Suppes] p. 89 | Theorem 96 | map0b 6755 |
| [Suppes] p. 89 | Theorem 97 | map0 6757 map0g 6756 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6758 |
| [Suppes] p. 89 | Theorem 99 | mapss 6759 |
| [Suppes] p. 92 | Theorem 1 | enref 6833 enrefg 6832 |
| [Suppes] p. 92 | Theorem 2 | ensym 6849 ensymb 6848 ensymi 6850 |
| [Suppes] p. 92 | Theorem 3 | entr 6852 |
| [Suppes] p. 92 | Theorem 4 | unen 6884 |
| [Suppes] p. 94 | Theorem 15 | endom 6831 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6846 |
| [Suppes] p. 94 | Theorem 17 | domtr 6853 |
| [Suppes] p. 95 | Theorem 18 | isbth 7042 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6874 fundmeng 6875 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6902 |
| [Suppes] p. 130 | Definition 3 | df-tr 4133 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4525 |
| [Suppes] p. 134 | Definition 6 | df-suc 4407 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4640 finds 4637 finds1 4639 finds2 4638 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7437 df-ltpq 7430 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4426 |
| [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 5929 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2988 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3644 elpr2 3645 elprg 3643 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3639 elsn2 3657 elsn2g 3656 elsng 3638 velsn 3640 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4265 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3634 sneqr 3791 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3642 dfsn2 3637 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4473 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4271 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4249 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4477 unexg 4479 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3672 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3841 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3163 df-un 3161 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3854 uniprg 3855 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4213 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3671 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4442 elsucg 4440 sstr2 3191 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3308 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3356 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3321 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3374 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3411 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3412 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3172 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3608 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3335 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3170 dfss2 3174 sseqin2 3383 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3204 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3384 inss2 3385 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3244 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3849 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4250 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4257 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2484 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4161 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3159 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3453 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3520 difidALT 3521 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3464 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4576 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2765 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4166 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3490 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4171 ssexg 4173 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4168 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4587 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4578 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3516 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3289 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3425 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3290 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3298 |
| [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 4779 xpexg 4778 xpexgALT 6199 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4671 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5323 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5477 fun11 5326 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5270 svrelfun 5324 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4854 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4856 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4676 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4677 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4673 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5125 dfrel2 5121 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4772 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4781 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4787 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4801 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4975 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4952 opelresg 4954 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4968 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4971 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4976 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5300 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5169 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5299 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5478 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2089 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5267 fv3 5584 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5209 cnvexg 5208 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4933 dmexg 4931 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4934 rnexg 4932 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5578 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5588 tz6.12 5589 tz6.12c 5591 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5552 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5262 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5263 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5265 wfo 5257 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5264 wf1 5256 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5266 wf1o 5258 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5662 eqfnfv2 5663 eqfnfv2f 5666 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5634 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5787 fnexALT 6177 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5786 resfunexgALT 6174 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5344 funimaexg 5343 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4035 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5040 iniseg 5042 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4325 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5268 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5860 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5861 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5866 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5868 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5876 |
| [TakeutiZaring] p. 35 | Notation | wtr 4132 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4390 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4136 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4613 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4417 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4421 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4529 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4404 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4523 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4589 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4619 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4134 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4548 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4524 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3868 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4407 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4451 sucidg 4452 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4538 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4405 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4543 ordelsuc 4542 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4631 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4632 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4633 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4630 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4644 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4636 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4634 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4635 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3889 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4148 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3890 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4554 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3876 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6375 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6432 tfri1d 6402 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6433 tfri2d 6403 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6434 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6369 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6353 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6531 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6527 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6524 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6528 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6576 nnaordi 6575 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3962 uniss2 3871 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6537 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6547 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6538 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6525 omsuc 6539 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6548 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6584 nnmordi 6583 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6526 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7265 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6863 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6927 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6928 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6811 isfi 6829 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6899 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6718 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 6905 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 6918 |
| [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 5239 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5240 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2124 eupickbi 2127 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5267 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7269 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |