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 7290 fidcenum 7131 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7131 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7290 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13004 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7102 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7088 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13019 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13021 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13010 znnen 12977 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13022 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13023 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11006 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4629 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11134 df-pfx 11213 df-substr 11186 df-word 11080 lencl 11083 wrd0 11104 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8334 addcan2d 8339 addcan2i 8337 addcand 8338 addcani 8336 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8345 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8402 negsubd 8471 negsubi 8432 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8404 negnegd 8456 negnegi 8424 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8539 subdid 8568 subdii 8561 subdir 8540 subdird 8569 subdiri 8562 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8543 mul01d 8547 mul01i 8545 mul02 8541 mul02d 8546 mul02i 8544 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8948 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8899 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8552 mul2negd 8567 mul2negi 8560 mulneg1 8549 mulneg1d 8565 mulneg1i 8558 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14116 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8868 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9881 rpaddcld 9916 rpmulcl 9882 rpmulcld 9917 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9893 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8259 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8693 ltadd1dd 8711 ltadd1i 8657 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8747 ltmul1a 8746 ltmul1i 9075 ltmul1ii 9083 ltmul2 9011 ltmul2d 9943 ltmul2dd 9957 ltmul2i 9078 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8281 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8623 lt0neg1d 8670 ltneg 8617 ltnegd 8678 ltnegi 8648 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8600 lt2addd 8722 lt2addi 8665 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9858 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9005 recgt0d 9089 recgt0i 9061 recgt0ii 9062 |
| [Apostol] p. 22 | Definition of integers | df-z 9455 |
| [Apostol] p. 22 | Definition of rationals | df-q 9823 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7169 |
| [Apostol] p. 26 | Theorem I.29 | arch 9374 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9574 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9375 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10484 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12390 zneo 9556 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11550 sqrtthi 11638 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9121 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12565 |
| [Apostol] p. 363 | Remark | absgt0api 11665 |
| [Apostol] p. 363 | Example | abssubd 11712 abssubi 11669 |
| [ApostolNT] p. 14 | Definition | df-dvds 12307 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12323 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12347 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12343 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12337 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12339 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12324 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12325 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12330 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12364 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12366 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12368 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12543 |
| [ApostolNT] p. 16 | Definition | isprm2 12647 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12622 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13034 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12502 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12544 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12546 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12516 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12509 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12674 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12676 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12899 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12443 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12589 |
| [ApostolNT] p. 25 | Definition | df-phi 12741 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12771 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12752 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12756 |
| [ApostolNT] p. 38 | Remark | df-sgm 15664 |
| [ApostolNT] p. 38 | Definition | df-sgm 15664 |
| [ApostolNT] p. 104 | Definition | congr 12630 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12310 |
| [ApostolNT] p. 106 | Definition | moddvds 12318 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12397 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12398 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10571 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10608 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10896 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12342 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12633 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12952 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12635 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12763 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12782 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12764 |
| [ApostolNT] p. 179 | Definition | df-lgs 15685 lgsprme0 15729 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15730 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15706 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15721 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15772 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15791 2lgsoddprm 15800 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15756 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15767 |
| [ApostolNT] p. 188 | Definition | df-lgs 15685 lgs1 15731 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15722 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15724 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15732 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15733 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 619 pm2.65 663 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6006 onsucelsucexmidlem 4621 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16392 |
| [Bauer], p. 483 | Definition | n0rf 3504 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15658 2irrexpqap 15660 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 7046 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15335 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15325 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8800 |
| [BauerSwan], p. 14 | Remark | 0ct 7282 ctm 7284 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16395 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7290 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7696 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7609 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7698 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7732 addlocpr 7731 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7758 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7761 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7766 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2080 |
| [BellMachover] p. 460 | Notation | df-mo 2081 |
| [BellMachover] p. 460 | Definition | mo3 2132 mo3h 2131 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2214 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4205 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4261 |
| [BellMachover] p. 466 | Axiom Union | axun2 4526 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4634 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4475 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4637 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4588 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4460 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4681 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4706 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1473 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1471 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1474 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1469 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15867 isuhgropm 15889 isusgropen 15971 isuspgropen 15970 |
| [Bollobas] p. 4 | Definition | df-wlks 16039 |
| [Bollobas] p. 5 | Definition | df-trls 16100 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15878 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13397 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13443 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13458 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13969 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13904 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5913 fcofo 5914 |
| [BourbakiTop1] p. | Remark | xnegmnf 10033 xnegpnf 10032 |
| [BourbakiTop1] p. | Remark | rexneg 10034 |
| [BourbakiTop1] p. | Proposition | ishmeo 14986 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14839 |
| [BourbakiTop1] p. | Property V_ii | innei 14845 |
| [BourbakiTop1] p. | Property V_iv | neissex 14847 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14836 neiss 14832 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14904 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 14981 |
| [BourbakiTop1] p. | Property V_iii | elnei 14834 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14680 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13397 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13443 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13640 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4147 |
| [Church] p. 129 | Section II.24 | df-ifp 984 dfifp2dc 987 |
| [Cohen] p. 301 | Remark | relogoprlem 15550 |
| [Cohen] p. 301 | Property 2 | relogmul 15551 relogmuld 15566 |
| [Cohen] p. 301 | Property 3 | relogdiv 15552 relogdivd 15567 |
| [Cohen] p. 301 | Property 4 | relogexp 15554 |
| [Cohen] p. 301 | Property 1a | log1 15548 |
| [Cohen] p. 301 | Property 1b | loge 15549 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15647 |
| [Cohen4] p. 352 | Definition | rpelogb 15631 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15637 |
| [Cohen4] p. 361 | Property 3 | logbrec 15642 rprelogbdiv 15639 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15635 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15640 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15629 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15630 |
| [Cohen4] p. 367 | Property | rplogbchbase 15632 |
| [Cohen4] p. 377 | Property 2 | logblt 15644 |
| [Crosilla] p. | Axiom 1 | ax-ext 2211 |
| [Crosilla] p. | Axiom 2 | ax-pr 4293 |
| [Crosilla] p. | Axiom 3 | ax-un 4524 |
| [Crosilla] p. | Axiom 4 | ax-nul 4210 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4680 |
| [Crosilla] p. | Axiom 6 | ru 3027 |
| [Crosilla] p. | Axiom 8 | ax-pow 4258 |
| [Crosilla] p. | Axiom 9 | ax-setind 4629 |
| [Crosilla], p. | Axiom 6 | ax-sep 4202 |
| [Crosilla], p. | Axiom 7 | ax-coll 4199 |
| [Crosilla], p. | Axiom 7' | repizf 4200 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4613 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6006 |
| [Crosilla], p. | Definition of ordinal | df-iord 4457 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4627 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15878 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3199 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4683 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6805 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4209 |
| [Enderton] p. 19 | Definition | df-tp 3674 |
| [Enderton] p. 26 | Exercise 5 | unissb 3918 |
| [Enderton] p. 26 | Exercise 10 | pwel 4304 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4377 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4035 iinin2m 4034 iunin1 4030 iunin2 4029 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4033 iundif2ss 4031 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4048 |
| [Enderton] p. 33 | Exercise 25 | iununir 4049 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4056 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4571 iunpwss 4057 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4303 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4276 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4541 rnex 4992 rnexg 4989 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4933 rnuni 5140 |
| [Enderton] p. 42 | Definition of a function | dffun7 5345 dffun8 5346 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5700 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5382 |
| [Enderton] p. 44 | Definition (d) | dfima2 5070 dfima3 5071 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5705 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7396 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5891 |
| [Enderton] p. 52 | Definition | df-map 6805 |
| [Enderton] p. 53 | Exercise 21 | coass 5247 |
| [Enderton] p. 53 | Exercise 27 | dmco 5237 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5392 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5104 |
| [Enderton] p. 54 | Remark | ixpf 6875 ixpssmap 6887 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6854 |
| [Enderton] p. 56 | Theorem 3M | erref 6708 |
| [Enderton] p. 57 | Lemma 3N | erthi 6736 |
| [Enderton] p. 57 | Definition | df-ec 6690 |
| [Enderton] p. 58 | Definition | df-qs 6694 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6795 th3qcor 6794 th3qlem1 6792 th3qlem2 6793 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6690 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4930 |
| [Enderton] p. 68 | Definition of successor | df-suc 4462 |
| [Enderton] p. 71 | Definition | df-tr 4183 dftr4 4187 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4504 unisucg 4505 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4504 unisucg 4505 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4196 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4197 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6628 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6630 onasuc 6620 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6010 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6629 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6631 onmsuc 6627 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6639 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6632 nnacom 6638 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6640 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6641 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6643 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6633 nnmsucr 6642 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6682 |
| [Enderton] p. 129 | Definition | df-en 6896 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5958 |
| [Enderton] p. 133 | Exercise 1 | xpomen 12974 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7035 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7026 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7015 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7408 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7404 dju1en 7403 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3567 |
| [Enderton] p. 145 | Figure 38 | ffoss 5606 |
| [Enderton] p. 145 | Definition | df-dom 6897 |
| [Enderton] p. 146 | Example 1 | domen 6908 domeng 6909 |
| [Enderton] p. 146 | Example 3 | nndomo 7033 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7002 xpdom1g 7000 xpdom2g 6999 |
| [Enderton] p. 168 | Definition | df-po 4387 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4519 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4480 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4635 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4483 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4608 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4581 |
| [Enderton] p. 194 | Remark | onprc 4644 |
| [Enderton] p. 194 | Exercise 16 | suc11 4650 |
| [Enderton] p. 197 | Definition | df-card 7359 |
| [Enderton] p. 200 | Exercise 25 | tfis 4675 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4646 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4648 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4649 |
| [Geuvers], p. 1 | Remark | expap0 10799 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8770 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8809 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8771 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8126 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11722 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11730 maxle2 11731 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11732 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11735 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11736 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8737 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7542 enqer 7553 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7546 df-nqqs 7543 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7539 df-plqqs 7544 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7540 df-mqqs 7545 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7547 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7603 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7606 ltbtwnnq 7611 ltbtwnnqq 7610 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7595 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7596 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7732 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7774 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7773 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7792 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7808 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7814 ltaprlem 7813 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7811 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7767 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7787 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7776 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7775 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7783 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7833 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7921 enrer 7930 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7926 df-1r 7927 df-nr 7922 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7924 df-plr 7923 negexsr 7967 recexsrlem 7969 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7925 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9115 creur 9114 cru 8757 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8118 axcnre 8076 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11377 crimd 11496 crimi 11456 crre 11376 crred 11495 crrei 11455 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11379 remimd 11461 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11576 absval2d 11704 absval2i 11663 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11403 cjaddd 11484 cjaddi 11451 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11404 cjmuld 11485 cjmuli 11452 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11402 cjcjd 11462 cjcji 11434 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11401 cjreb 11385 cjrebd 11465 cjrebi 11437 cjred 11490 rere 11384 rereb 11382 rerebd 11464 rerebi 11436 rered 11488 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11410 addcjd 11476 addcji 11446 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11520 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11571 abscjd 11709 abscji 11667 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11583 abs00d 11705 abs00i 11664 absne0d 11706 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11615 releabsd 11710 releabsi 11668 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11588 absmuld 11713 absmuli 11670 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11574 sqabsaddi 11671 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11623 abstrid 11715 abstrii 11674 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10769 exp0 10773 expp1 10776 expp1d 10904 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10811 expaddd 10905 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15594 cxpmuld 15619 expmul 10814 expmuld 10906 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10808 mulexpd 10918 rpmulcxp 15591 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10214 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11845 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11847 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11846 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11850 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11843 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11839 climcj 11840 climim 11842 climre 11841 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8194 df-xr 8193 ltxr 9979 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11866 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10528 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14517 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15046 xmet0 15045 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15053 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15055 mstri 15155 xmettri 15054 xmstri 15154 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14961 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15193 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11829 addcncntop 15244 mulcn2 11831 mulcncntop 15246 subcn2 11830 subcncntop 15245 |
| [Gleason] p. 295 | Remark | bcval3 10981 bcval4 10982 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10996 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10979 df-bc 10978 |
| [Gleason] p. 296 | Remark | bcn0 10985 bcnn 10987 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12003 |
| [Gleason] p. 308 | Equation 2 | ef0 12191 |
| [Gleason] p. 308 | Equation 3 | efcj 12192 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12197 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12201 |
| [Gleason] p. 310 | Equation 14 | sinadd 12255 |
| [Gleason] p. 310 | Equation 15 | cosadd 12256 |
| [Gleason] p. 311 | Equation 17 | sincossq 12267 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12272 sinbnd 12271 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12172 |
| [Golan] p. 1 | Remark | srgisid 13957 |
| [Golan] p. 1 | Definition | df-srg 13935 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1495 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13552 mndideu 13467 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13579 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13608 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13619 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13641 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16472 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1465 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1466 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1468 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7415 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6653 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16466 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8812 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7665 df-imp 7664 df-iplp 7663 df-reap 8730 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8826 rerecapb 8998 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6289 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7857 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16109 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16459 dceqnconst 16458 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8095 caucvgpr 7877 caucvgprpr 7907 caucvgsr 7997 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7661 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16464 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4388 ltpopr 7790 ltsopr 7791 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8761 reapcotr 8753 reapirr 8732 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8281 gt0add 8728 leadd1 8585 lelttr 8243 lemul1a 9013 lenlt 8230 ltadd1 8584 ltletr 8244 ltmul1 8747 reaplt 8743 |
| [Jech] p. 4 | Definition of class | cv 1394 cvjust 2224 |
| [Jech] p. 78 | Note | opthprc 4770 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1576 |
| [Kreyszig] p. 3 | Property M1 | metcl 15035 xmetcl 15034 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15042 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8823 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15124 |
| [Kreyszig] p. 19 | Remark | mopntopon 15125 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15170 mopnm 15130 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15168 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15173 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15195 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14895 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14302 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14293 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14294 |
| [Kunen] p. 10 | Axiom 0 | a9e 1742 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4201 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6815 mapvalg 6813 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6809 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3975 |
| [Lang] p. 3 | Statement | lidrideqd 13422 mndbn0 13472 |
| [Lang] p. 3 | Definition | df-mnd 13458 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13439 |
| [Lang] p. 5 | Equation | gsumfzreidx 13882 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13673 |
| [Lang] p. 7 | Definition | dfgrp2e 13569 |
| [Levy] p. 338 | Axiom | df-clab 2216 df-clel 2225 df-cleq 2222 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1465 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1466 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1468 |
| [Margaris] p. 40 | Rule C | exlimiv 1644 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 858 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 897 exalim 1548 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 655 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1684 r19.2m 3578 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1600 19.3h 1599 rr19.3v 2942 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1524 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1665 alexim 1691 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1545 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1636 spsbe 1888 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1690 19.9h 1689 19.9v 1917 exlimd 1643 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1710 excomim 1709 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1711 r19.12 2637 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1692 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1514 ralbi 2663 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1601 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1602 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1650 rexbi 2664 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1712 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1503 alimd 1567 alimdh 1513 alimdv 1925 ralimdaa 2596 ralimdv 2598 ralimdva 2597 ralimdvva 2599 sbcimdv 3094 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1713 19.21 1629 19.21bi 1604 19.21h 1603 19.21ht 1627 19.21t 1628 19.21v 1919 alrimd 1656 alrimdd 1655 alrimdh 1525 alrimdv 1922 alrimi 1568 alrimih 1515 alrimiv 1920 alrimivv 1921 r19.21 2606 r19.21be 2621 r19.21bi 2618 r19.21t 2605 r19.21v 2607 ralrimd 2608 ralrimdv 2609 ralrimdva 2610 ralrimdvv 2614 ralrimdvva 2615 ralrimi 2601 ralrimiv 2602 ralrimiva 2603 ralrimivv 2611 ralrimivva 2612 ralrimivvva 2613 ralrimivw 2604 rexlimi 2641 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1927 2eximdv 1928 exim 1645 eximd 1658 eximdh 1657 eximdv 1926 rexim 2624 reximdai 2628 reximddv 2633 reximddv2 2635 reximdv 2631 reximdv2 2629 reximdva 2632 reximdvai 2630 reximi2 2626 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1724 19.23bi 1638 19.23h 1544 19.23ht 1543 19.23t 1723 19.23v 1929 19.23vv 1930 exlimd2 1641 exlimdh 1642 exlimdv 1865 exlimdvv 1944 exlimi 1640 exlimih 1639 exlimiv 1644 exlimivv 1943 r19.23 2639 r19.23v 2640 rexlimd 2645 rexlimdv 2647 rexlimdv3a 2650 rexlimdva 2648 rexlimdva2 2651 rexlimdvaa 2649 rexlimdvv 2655 rexlimdvva 2656 rexlimdvw 2652 rexlimiv 2642 rexlimiva 2643 rexlimivv 2654 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1685 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1672 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1528 19.26-3an 1529 19.26 1527 r19.26-2 2660 r19.26-3 2661 r19.26 2657 r19.26m 2662 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1607 19.27h 1606 19.27v 1946 r19.27av 2666 r19.27m 3587 r19.27mv 3588 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1609 19.28h 1608 19.28v 1947 r19.28av 2667 r19.28m 3581 r19.28mv 3584 rr19.28v 2943 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1666 19.29r 1667 19.29r2 1668 19.29x 1669 r19.29 2668 r19.29d2r 2675 r19.29r 2669 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1673 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1727 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1725 19.32r 1726 r19.32r 2677 r19.32vdc 2680 r19.32vr 2679 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1530 19.33b2 1675 19.33bdc 1676 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1730 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1670 19.35i 1671 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1719 19.36aiv 1948 19.36i 1718 r19.36av 2682 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1720 19.37aiv 1721 r19.37 2683 r19.37av 2684 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1722 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1686 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1678 19.40 1677 r19.40 2685 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1732 19.41h 1731 19.41v 1949 19.41vv 1950 19.41vvv 1951 19.41vvvv 1952 r19.41 2686 r19.41v 2687 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1734 19.42h 1733 19.42v 1953 19.42vv 1958 19.42vvv 1959 19.42vvvv 1960 r19.42v 2688 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1674 r19.43 2689 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1728 r19.44av 2690 r19.44mv 3586 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1729 r19.45av 2691 r19.45mv 3585 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2102 |
| [Megill] p. 444 | Axiom C5 | ax-17 1572 |
| [Megill] p. 445 | Lemma L12 | alequcom 1561 ax-10 1551 |
| [Megill] p. 446 | Lemma L17 | equtrr 1756 |
| [Megill] p. 446 | Lemma L19 | hbnae 1767 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1809 sbid 1820 |
| [Megill] p. 448 | Scheme C5' | ax-4 1556 |
| [Megill] p. 448 | Scheme C6' | ax-7 1494 |
| [Megill] p. 448 | Scheme C8' | ax-8 1550 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1553 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1762 |
| [Megill] p. 448 | Scheme C12' | ax-13 2202 |
| [Megill] p. 448 | Scheme C13' | ax-14 2203 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1869 |
| [Megill] p. 448 | Scheme C16' | ax-16 1860 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1776 dral2 1777 drex1 1844 drex2 1778 drsb1 1845 drsb2 1887 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2038 sbequ 1886 sbid2v 2047 |
| [Megill] p. 450 | Example in Appendix | hba1 1586 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3112 rspsbca 3113 stdpc4 1821 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3118 stdpc5 1630 |
| [Mendelson] p. 81 | Rule C | exlimiv 1644 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1749 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1816 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3528 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3529 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3444 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3492 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3445 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3335 |
| [Mendelson] p. 231 | Definition of union | unssin 3443 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4567 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3887 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4373 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4374 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4375 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3908 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4851 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5249 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4462 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7014 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6988 xpsneng 6989 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6994 xpcomeng 6995 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6997 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6991 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6807 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6972 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7019 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6841 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6973 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7407 djucomen 7406 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7405 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6621 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3426 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4807 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4808 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4146 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5244 coi2 5245 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4937 rn0 4980 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5133 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4828 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4944 rnxpm 5158 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4799 xp0 5148 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5087 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5084 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5083 imaexg 5082 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5079 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5767 funfvop 5749 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5677 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5687 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5362 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5898 dff13f 5900 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5866 funrnex 6265 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5892 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5212 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3939 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6307 df-1st 6292 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6308 df-2nd 6293 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1493 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1550 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1552 ax-11o 1869 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1873 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1494 |
| [Monk2] p. 109 | Lemma 15 | equvin 1909 equvini 1804 eqvinop 4329 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1572 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1697 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1494 |
| [Monk2] p. 114 | Lemma 22 | hba1 1586 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1598 nfia1 1626 |
| [Monk2] p. 114 | Lemma 24 | hba2 1597 nfa2 1625 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 836 dftest 16473 |
| [Munkres] p. 77 | Example 2 | distop 14767 |
| [Munkres] p. 78 | Definition of basis | df-bases 14725 isbasis3g 14728 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13301 tgval2 14733 |
| [Munkres] p. 79 | Remark | tgcl 14746 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14740 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14761 tgss3 14760 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14762 basgen2 14763 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14852 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14794 topcld 14791 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14795 |
| [Munkres] p. 94 | Definition of closure | clsval 14793 |
| [Munkres] p. 94 | Definition of interior | ntrval 14792 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14870 iscn 14879 iscn2 14882 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14912 cncnp2m 14913 cncnpi 14910 df-cnp 14871 iscnp 14881 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15196 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7073 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7339 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7327 omniwomnimkv 7342 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3314 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7310 exmidomniim 7316 finomni 7315 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7295 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16417 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16421 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7078 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7387 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7388 exmidfodomrlemrALT 7389 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7324 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16403 peano4nninf 16402 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16405 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16413 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16415 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16401 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2216 rabid 2707 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2042 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2222 |
| [Quine] p. 19 | Definition 2.9 | df-v 2801 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2338 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2350 abid2f 2398 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1934 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1932 sb6 1933 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2225 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2229 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2231 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3029 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3030 dfsbcq2 3031 |
| [Quine] p. 43 | Theorem 6.8 | vex 2802 |
| [Quine] p. 43 | Theorem 6.9 | isset 2806 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2885 spcgv 2890 spcimgf 2883 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3040 spsbcd 3041 |
| [Quine] p. 44 | Theorem 6.12 | elex 2811 |
| [Quine] p. 44 | Theorem 6.13 | elab 2947 elabg 2949 elabgf 2945 |
| [Quine] p. 44 | Theorem 6.14 | noel 3495 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3731 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3673 df-sn 3672 |
| [Quine] p. 49 | Theorem 7.4 | snss 3803 snssg 3802 |
| [Quine] p. 49 | Theorem 7.5 | prss 3824 prssg 3825 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3772 prid1g 3770 prid2 3773 prid2g 3771 snid 3697 snidg 3695 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4268 snexprc 4270 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4295 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3904 unisng 3905 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3907 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3916 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3915 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5289 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5279 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5290 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5294 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5295 |
| [Quine] p. 58 | Definition 9.1 | df-op 3675 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4344 opabidw 4345 opelopab 4360 opelopaba 4354 opelopabaf 4362 opelopabf 4363 opelopabg 4356 opelopabga 4351 opelopabgf 4358 oprabid 6039 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4725 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4727 |
| [Quine] p. 64 | Definition 9.15 | df-id 4384 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5379 |
| [Quine] p. 65 | Theorem 10.4 | funi 5350 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5369 funsng 5367 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5320 |
| [Quine] p. 65 | Definition 10.2 | args 5097 dffv4g 5626 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5326 fv2 5624 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10954 nn0opth2d 10953 nn0opthd 10952 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5406 funimaexg 5405 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13904 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13969 |
| [Rudin] p. 164 | Equation 27 | efcan 12195 |
| [Rudin] p. 164 | Equation 30 | efzval 12202 |
| [Rudin] p. 167 | Equation 48 | absefi 12288 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1468 |
| [Sanford] p. 39 | Rule 4 | mptxor 1466 |
| [Sanford] p. 40 | Rule 1 | mptnan 1465 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5113 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5115 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5112 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5110 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 13971 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14765 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3469 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3563 dif0 3562 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3576 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3462 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3463 |
| [Stoll] p. 20 | Remark | invdif 3446 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3676 |
| [Stoll] p. 43 | Definition | uniiun 4019 |
| [Stoll] p. 44 | Definition | intiin 4020 |
| [Stoll] p. 45 | Definition | df-iin 3968 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3967 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 894 imanst 893 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3469 |
| [Suppes] p. 22 | Theorem 2 | eq0 3510 |
| [Suppes] p. 22 | Theorem 4 | eqss 3239 eqssd 3241 eqssi 3240 |
| [Suppes] p. 23 | Theorem 5 | ss0 3532 ss0b 3531 |
| [Suppes] p. 23 | Theorem 6 | sstr 3232 |
| [Suppes] p. 25 | Theorem 12 | elin 3387 elun 3345 |
| [Suppes] p. 26 | Theorem 15 | inidm 3413 |
| [Suppes] p. 26 | Theorem 16 | in0 3526 |
| [Suppes] p. 27 | Theorem 23 | unidm 3347 |
| [Suppes] p. 27 | Theorem 24 | un0 3525 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3367 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3374 |
| [Suppes] p. 27 | Theorem 27 | unss 3378 |
| [Suppes] p. 27 | Theorem 28 | indir 3453 |
| [Suppes] p. 27 | Theorem 29 | undir 3454 |
| [Suppes] p. 28 | Theorem 32 | difid 3560 difidALT 3561 |
| [Suppes] p. 29 | Theorem 33 | difin 3441 |
| [Suppes] p. 29 | Theorem 34 | indif 3447 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3566 |
| [Suppes] p. 29 | Theorem 36 | difun2 3571 |
| [Suppes] p. 29 | Theorem 37 | difin0 3565 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3564 |
| [Suppes] p. 29 | Theorem 39 | difundi 3456 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3458 |
| [Suppes] p. 30 | Theorem 41 | nalset 4214 |
| [Suppes] p. 39 | Theorem 61 | uniss 3909 |
| [Suppes] p. 39 | Theorem 65 | uniop 4342 |
| [Suppes] p. 41 | Theorem 70 | intsn 3958 |
| [Suppes] p. 42 | Theorem 71 | intpr 3955 intprg 3956 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4569 op1stbg 4570 |
| [Suppes] p. 42 | Theorem 78 | intun 3954 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3999 dfiun2g 3997 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4000 |
| [Suppes] p. 47 | Theorem 86 | elpw 3655 elpw2 4241 elpw2g 4240 elpwg 3657 |
| [Suppes] p. 47 | Theorem 87 | pwid 3664 |
| [Suppes] p. 47 | Theorem 89 | pw0 3815 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3883 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4826 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4857 xpindir 4858 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4775 xpundir 4776 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4640 |
| [Suppes] p. 58 | Theorem 2 | relss 4806 |
| [Suppes] p. 59 | Theorem 4 | eldm 4920 eldm2 4921 eldm2g 4919 eldmg 4918 |
| [Suppes] p. 59 | Definition 3 | df-dm 4729 |
| [Suppes] p. 60 | Theorem 6 | dmin 4931 |
| [Suppes] p. 60 | Theorem 8 | rnun 5137 |
| [Suppes] p. 60 | Theorem 9 | rnin 5138 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4910 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4905 brcnvg 4903 |
| [Suppes] p. 62 | Equation 5 | elcnv 4899 elcnv2 4900 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5106 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5136 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5134 |
| [Suppes] p. 63 | Theorem 20 | co02 5242 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4994 |
| [Suppes] p. 63 | Definition 7 | df-co 4728 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4907 |
| [Suppes] p. 64 | Theorem 27 | coass 5247 |
| [Suppes] p. 65 | Theorem 31 | resundi 5018 |
| [Suppes] p. 65 | Theorem 34 | elima 5073 elima2 5074 elima3 5075 elimag 5072 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5141 |
| [Suppes] p. 66 | Theorem 40 | dminss 5143 |
| [Suppes] p. 66 | Theorem 41 | imainss 5144 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5147 |
| [Suppes] p. 81 | Definition 34 | dfec2 6691 |
| [Suppes] p. 82 | Theorem 72 | elec 6729 elecg 6728 |
| [Suppes] p. 82 | Theorem 73 | erth 6734 erth2 6735 |
| [Suppes] p. 89 | Theorem 96 | map0b 6842 |
| [Suppes] p. 89 | Theorem 97 | map0 6844 map0g 6843 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6845 |
| [Suppes] p. 89 | Theorem 99 | mapss 6846 |
| [Suppes] p. 92 | Theorem 1 | enref 6924 enrefg 6923 |
| [Suppes] p. 92 | Theorem 2 | ensym 6941 ensymb 6940 ensymi 6942 |
| [Suppes] p. 92 | Theorem 3 | entr 6944 |
| [Suppes] p. 92 | Theorem 4 | unen 6977 |
| [Suppes] p. 94 | Theorem 15 | endom 6922 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6938 |
| [Suppes] p. 94 | Theorem 17 | domtr 6945 |
| [Suppes] p. 95 | Theorem 18 | isbth 7142 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6967 fundmeng 6968 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7001 |
| [Suppes] p. 130 | Definition 3 | df-tr 4183 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4580 |
| [Suppes] p. 134 | Definition 6 | df-suc 4462 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4695 finds 4692 finds1 4694 finds2 4693 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7548 df-ltpq 7541 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4481 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2211 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2222 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2225 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2247 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6011 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3027 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3687 elpr2 3688 elprg 3686 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3682 elsn2 3700 elsn2g 3699 elsng 3681 velsn 3683 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4317 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3677 sneqr 3838 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3685 dfsn2 3680 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4528 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4323 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4301 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4532 unexg 4534 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3715 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3889 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3203 df-un 3201 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3902 uniprg 3903 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4263 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3714 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4497 elsucg 4495 sstr2 3231 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3348 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3396 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3361 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3414 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3451 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3452 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3212 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3651 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3375 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3210 dfss2 3214 sseqin2 3423 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3244 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3424 inss2 3425 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3284 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3897 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4302 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4309 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2517 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4211 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3199 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3493 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3560 difidALT 3561 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3504 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4631 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2801 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4216 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3530 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4221 ssexg 4223 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4218 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4642 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4633 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3556 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3329 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3465 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3330 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3338 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2513 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2514 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4834 xpexg 4833 xpexgALT 6284 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4726 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5385 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5544 fun11 5388 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5329 svrelfun 5386 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4909 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4911 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4731 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4732 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4728 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5183 dfrel2 5179 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4827 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4836 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4842 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4856 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5033 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5010 opelresg 5012 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5026 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5029 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5034 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5359 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5227 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5358 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5545 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2122 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5326 fv3 5652 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5267 cnvexg 5266 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4991 dmexg 4988 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4992 rnexg 4989 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5646 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5656 tz6.12 5657 tz6.12c 5659 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5620 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5321 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5322 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5324 wfo 5316 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5323 wf1 5315 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5325 wf1o 5317 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5734 eqfnfv2 5735 eqfnfv2f 5738 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5706 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5865 fnexALT 6262 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5864 resfunexgALT 6259 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5406 funimaexg 5405 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4084 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5098 iniseg 5100 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4380 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5327 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5940 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5941 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5946 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5948 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5956 |
| [TakeutiZaring] p. 35 | Notation | wtr 4182 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4445 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4186 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4668 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4472 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4476 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4584 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4459 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4578 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4644 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4674 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4184 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4603 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4579 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3916 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4462 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4506 sucidg 4507 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4593 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4460 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4598 ordelsuc 4597 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4686 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4687 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4688 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4685 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4699 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4691 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4689 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4690 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3937 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4198 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3938 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4609 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3924 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6460 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6517 tfri1d 6487 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6518 tfri2d 6488 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6519 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6454 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6438 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6618 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6614 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6611 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6615 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6663 nnaordi 6662 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4010 uniss2 3919 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6624 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6634 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6625 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6612 omsuc 6626 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6635 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6671 nnmordi 6670 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6613 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7367 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6955 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7026 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7027 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6898 isfi 6920 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6998 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6805 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7004 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7017 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1556 |
| [Tarski] p. 68 | Lemma 6 | equid 1747 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1750 |
| [Tarski] p. 70 | Lemma 14 | spim 1784 spime 1787 spimeh 1785 spimh 1783 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1552 ax-11o 1869 ax11i 1760 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1933 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1572 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2202 ax-14 2203 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 716 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 732 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 761 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 770 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 794 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 619 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 646 |
| [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 842 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2176 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 742 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 841 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 632 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 890 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 848 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 861 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 645 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 858 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 860 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 717 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 780 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 620 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 624 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 898 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 912 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 773 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 774 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 809 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 810 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 808 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1003 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 783 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 781 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 782 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 743 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 744 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 872 pm2.5gdc 871 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 867 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 745 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 659 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 660 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 727 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 896 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 730 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 731 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 870 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 753 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 805 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 806 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 663 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 718 pm2.67 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 874 pm2.521gdc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 752 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 899 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 920 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 811 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 812 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 910 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 759 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 963 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 964 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 965 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 758 |
| [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 698 |
| [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 865 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 864 |
| [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 693 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 599 |
| [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 760 pm3.44 720 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 604 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 790 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 876 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 877 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 895 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 699 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 958 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 762 pm4.25 763 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 823 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 733 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 772 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 797 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 607 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 827 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1004 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 821 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 977 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 955 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 784 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 819 pm4.45 789 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1527 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 962 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 902 imorr 726 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 904 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 755 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 756 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 944 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 757 pm4.56 785 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 945 oranim 786 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 690 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 903 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 891 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 691 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 892 |
| [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 832 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 749 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 605 pm4.76 606 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 715 pm4.77 804 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 787 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 908 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 712 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 913 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 956 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 957 |
| [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 603 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 914 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 915 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 916 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1431 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 833 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 909 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1436 pm5.18dc 888 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 711 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 700 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1434 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1439 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1440 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 900 |
| [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 931 pm5.6r 932 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 960 |
| [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 611 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 922 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 612 |
| [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 930 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 807 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 923 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 918 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 799 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 951 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 952 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 967 |
| [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 968 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1681 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1531 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1678 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1942 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2080 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2481 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2482 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2941 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3085 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5298 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5299 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2157 eupickbi 2160 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5326 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7371 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |