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 7317 fidcenum 7158 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7158 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7317 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13067 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7127 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7113 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13082 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13084 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13073 znnen 13040 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13085 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13086 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11042 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4635 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11175 df-pfx 11261 df-substr 11234 df-word 11121 lencl 11124 wrd0 11145 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8362 addcan2d 8367 addcan2i 8365 addcand 8366 addcani 8364 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8373 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8430 negsubd 8499 negsubi 8460 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8432 negnegd 8484 negnegi 8452 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8567 subdid 8596 subdii 8589 subdir 8568 subdird 8597 subdiri 8590 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8571 mul01d 8575 mul01i 8573 mul02 8569 mul02d 8574 mul02i 8572 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8976 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8927 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8580 mul2negd 8595 mul2negi 8588 mulneg1 8577 mulneg1d 8593 mulneg1i 8586 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14180 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8896 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9915 rpaddcld 9950 rpmulcl 9916 rpmulcld 9951 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9927 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8287 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8721 ltadd1dd 8739 ltadd1i 8685 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8775 ltmul1a 8774 ltmul1i 9103 ltmul1ii 9111 ltmul2 9039 ltmul2d 9977 ltmul2dd 9991 ltmul2i 9106 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8309 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8651 lt0neg1d 8698 ltneg 8645 ltnegd 8706 ltnegi 8676 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8628 lt2addd 8750 lt2addi 8693 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9892 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9033 recgt0d 9117 recgt0i 9089 recgt0ii 9090 |
| [Apostol] p. 22 | Definition of integers | df-z 9483 |
| [Apostol] p. 22 | Definition of rationals | df-q 9857 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7196 |
| [Apostol] p. 26 | Theorem I.29 | arch 9402 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9602 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9403 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10520 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12453 zneo 9584 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11612 sqrtthi 11700 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9149 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12628 |
| [Apostol] p. 363 | Remark | absgt0api 11727 |
| [Apostol] p. 363 | Example | abssubd 11774 abssubi 11731 |
| [ApostolNT] p. 14 | Definition | df-dvds 12370 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12386 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12410 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12406 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12400 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12402 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12387 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12388 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12393 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12427 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12429 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12431 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12606 |
| [ApostolNT] p. 16 | Definition | isprm2 12710 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12685 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13097 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12565 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12607 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12609 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12579 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12572 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12737 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12739 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12962 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12506 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12652 |
| [ApostolNT] p. 25 | Definition | df-phi 12804 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12834 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12815 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12819 |
| [ApostolNT] p. 38 | Remark | df-sgm 15733 |
| [ApostolNT] p. 38 | Definition | df-sgm 15733 |
| [ApostolNT] p. 104 | Definition | congr 12693 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12373 |
| [ApostolNT] p. 106 | Definition | moddvds 12381 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12460 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12461 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10607 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10644 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10932 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12405 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12696 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13015 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12698 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12826 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12845 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12827 |
| [ApostolNT] p. 179 | Definition | df-lgs 15754 lgsprme0 15798 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15799 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15775 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15790 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15841 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15860 2lgsoddprm 15869 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15825 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15836 |
| [ApostolNT] p. 188 | Definition | df-lgs 15754 lgs1 15800 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15791 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15793 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15801 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15802 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 621 pm2.65 665 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6020 onsucelsucexmidlem 4627 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16657 |
| [Bauer], p. 483 | Definition | n0rf 3507 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15727 2irrexpqap 15729 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7134 ssfiexmid 7066 ssfiexmidt 7068 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15404 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15394 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8828 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7317 |
| [BauerSwan], p. 14 | Remark | 0ct 7309 ctm 7311 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16660 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7724 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7637 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7726 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7760 addlocpr 7759 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7786 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7789 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7794 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2082 |
| [BellMachover] p. 460 | Notation | df-mo 2083 |
| [BellMachover] p. 460 | Definition | mo3 2134 mo3h 2133 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2216 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4210 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4267 |
| [BellMachover] p. 466 | Axiom Union | axun2 4532 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4640 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4481 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4643 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4594 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4466 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4687 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4712 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1475 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1473 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1476 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1471 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15936 isuhgropm 15959 isusgropen 16043 isuspgropen 16042 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16132 uhgrspansubgr 16155 |
| [Bollobas] p. 4 | Definition | df-wlks 16196 |
| [Bollobas] p. 5 | Definition | df-trls 16259 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15948 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13460 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13506 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13521 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14033 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13968 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5927 fcofo 5928 |
| [BourbakiTop1] p. | Remark | xnegmnf 10067 xnegpnf 10066 |
| [BourbakiTop1] p. | Remark | rexneg 10068 |
| [BourbakiTop1] p. | Proposition | ishmeo 15055 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14908 |
| [BourbakiTop1] p. | Property V_ii | innei 14914 |
| [BourbakiTop1] p. | Property V_iv | neissex 14916 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14905 neiss 14901 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14973 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15050 |
| [BourbakiTop1] p. | Property V_iii | elnei 14903 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14749 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13460 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13506 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13703 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4152 |
| [Church] p. 129 | Section II.24 | df-ifp 986 dfifp2dc 989 |
| [Cohen] p. 301 | Remark | relogoprlem 15619 |
| [Cohen] p. 301 | Property 2 | relogmul 15620 relogmuld 15635 |
| [Cohen] p. 301 | Property 3 | relogdiv 15621 relogdivd 15636 |
| [Cohen] p. 301 | Property 4 | relogexp 15623 |
| [Cohen] p. 301 | Property 1a | log1 15617 |
| [Cohen] p. 301 | Property 1b | loge 15618 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15716 |
| [Cohen4] p. 352 | Definition | rpelogb 15700 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15706 |
| [Cohen4] p. 361 | Property 3 | logbrec 15711 rprelogbdiv 15708 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15704 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15709 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15698 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15699 |
| [Cohen4] p. 367 | Property | rplogbchbase 15701 |
| [Cohen4] p. 377 | Property 2 | logblt 15713 |
| [Crosilla] p. | Axiom 1 | ax-ext 2213 |
| [Crosilla] p. | Axiom 2 | ax-pr 4299 |
| [Crosilla] p. | Axiom 3 | ax-un 4530 |
| [Crosilla] p. | Axiom 4 | ax-nul 4215 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4686 |
| [Crosilla] p. | Axiom 6 | ru 3030 |
| [Crosilla] p. | Axiom 8 | ax-pow 4264 |
| [Crosilla] p. | Axiom 9 | ax-setind 4635 |
| [Crosilla], p. | Axiom 6 | ax-sep 4207 |
| [Crosilla], p. | Axiom 7 | ax-coll 4204 |
| [Crosilla], p. | Axiom 7' | repizf 4205 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4619 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6020 |
| [Crosilla], p. | Definition of ordinal | df-iord 4463 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4633 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16132 uhgrspansubgr 16155 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15948 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3202 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4689 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6822 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4214 |
| [Enderton] p. 19 | Definition | df-tp 3677 |
| [Enderton] p. 26 | Exercise 5 | unissb 3923 |
| [Enderton] p. 26 | Exercise 10 | pwel 4310 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4383 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4040 iinin2m 4039 iunin1 4035 iunin2 4034 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4038 iundif2ss 4036 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4053 |
| [Enderton] p. 33 | Exercise 25 | iununir 4054 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4061 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4577 iunpwss 4062 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4309 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4282 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4547 rnex 5000 rnexg 4997 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4941 rnuni 5148 |
| [Enderton] p. 42 | Definition of a function | dffun7 5353 dffun8 5354 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5711 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5391 |
| [Enderton] p. 44 | Definition (d) | dfima2 5078 dfima3 5079 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5716 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7424 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5905 |
| [Enderton] p. 52 | Definition | df-map 6822 |
| [Enderton] p. 53 | Exercise 21 | coass 5255 |
| [Enderton] p. 53 | Exercise 27 | dmco 5245 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5401 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5112 |
| [Enderton] p. 54 | Remark | ixpf 6892 ixpssmap 6904 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6871 |
| [Enderton] p. 56 | Theorem 3M | erref 6725 |
| [Enderton] p. 57 | Lemma 3N | erthi 6753 |
| [Enderton] p. 57 | Definition | df-ec 6707 |
| [Enderton] p. 58 | Definition | df-qs 6711 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6812 th3qcor 6811 th3qlem1 6809 th3qlem2 6810 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6707 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4938 |
| [Enderton] p. 68 | Definition of successor | df-suc 4468 |
| [Enderton] p. 71 | Definition | df-tr 4188 dftr4 4192 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4510 unisucg 4511 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4510 unisucg 4511 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4201 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4202 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6645 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6647 onasuc 6637 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6024 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6646 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6648 onmsuc 6644 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6656 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6649 nnacom 6655 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6657 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6658 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6660 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6650 nnmsucr 6659 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6699 |
| [Enderton] p. 129 | Definition | df-en 6913 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5972 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13037 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7055 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7046 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7035 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7436 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7432 dju1en 7431 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3570 |
| [Enderton] p. 145 | Figure 38 | ffoss 5617 |
| [Enderton] p. 145 | Definition | df-dom 6914 |
| [Enderton] p. 146 | Example 1 | domen 6925 domeng 6926 |
| [Enderton] p. 146 | Example 3 | nndomo 7053 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7022 xpdom1g 7020 xpdom2g 7019 |
| [Enderton] p. 168 | Definition | df-po 4393 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4525 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4486 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4641 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4489 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4614 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4587 |
| [Enderton] p. 194 | Remark | onprc 4650 |
| [Enderton] p. 194 | Exercise 16 | suc11 4656 |
| [Enderton] p. 197 | Definition | df-card 7386 |
| [Enderton] p. 200 | Exercise 25 | tfis 4681 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4652 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4654 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4655 |
| [Geuvers], p. 1 | Remark | expap0 10835 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8798 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8837 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8799 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8154 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11784 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11792 maxle2 11793 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11794 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11797 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11798 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8765 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7570 enqer 7581 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7574 df-nqqs 7571 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7567 df-plqqs 7572 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7568 df-mqqs 7573 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7575 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7631 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7634 ltbtwnnq 7639 ltbtwnnqq 7638 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7623 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7624 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7760 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7802 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7801 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7820 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7836 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7842 ltaprlem 7841 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7839 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7795 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7815 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7804 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7803 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7811 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7861 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7949 enrer 7958 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7954 df-1r 7955 df-nr 7950 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7952 df-plr 7951 negexsr 7995 recexsrlem 7997 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7953 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9143 creur 9142 cru 8785 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8146 axcnre 8104 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11439 crimd 11558 crimi 11518 crre 11438 crred 11557 crrei 11517 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11441 remimd 11523 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11638 absval2d 11766 absval2i 11725 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11465 cjaddd 11546 cjaddi 11513 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11466 cjmuld 11547 cjmuli 11514 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11464 cjcjd 11524 cjcji 11496 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11463 cjreb 11447 cjrebd 11527 cjrebi 11499 cjred 11552 rere 11446 rereb 11444 rerebd 11526 rerebi 11498 rered 11550 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11472 addcjd 11538 addcji 11508 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11582 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11633 abscjd 11771 abscji 11729 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11645 abs00d 11767 abs00i 11726 absne0d 11768 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11677 releabsd 11772 releabsi 11730 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11650 absmuld 11775 absmuli 11732 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11636 sqabsaddi 11733 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11685 abstrid 11777 abstrii 11736 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10805 exp0 10809 expp1 10812 expp1d 10940 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10847 expaddd 10941 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15663 cxpmuld 15688 expmul 10850 expmuld 10942 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10844 mulexpd 10954 rpmulcxp 15660 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10248 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11907 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11909 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11908 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11912 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11905 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11901 climcj 11902 climim 11904 climre 11903 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8222 df-xr 8221 ltxr 10013 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11928 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10564 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14581 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15115 xmet0 15114 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15122 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15124 mstri 15224 xmettri 15123 xmstri 15223 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15030 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15262 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11891 addcncntop 15313 mulcn2 11893 mulcncntop 15315 subcn2 11892 subcncntop 15314 |
| [Gleason] p. 295 | Remark | bcval3 11017 bcval4 11018 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11032 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11015 df-bc 11014 |
| [Gleason] p. 296 | Remark | bcn0 11021 bcnn 11023 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12066 |
| [Gleason] p. 308 | Equation 2 | ef0 12254 |
| [Gleason] p. 308 | Equation 3 | efcj 12255 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12260 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12264 |
| [Gleason] p. 310 | Equation 14 | sinadd 12318 |
| [Gleason] p. 310 | Equation 15 | cosadd 12319 |
| [Gleason] p. 311 | Equation 17 | sincossq 12330 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12335 sinbnd 12334 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12235 |
| [Golan] p. 1 | Remark | srgisid 14021 |
| [Golan] p. 1 | Definition | df-srg 13999 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1497 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13615 mndideu 13530 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13642 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13671 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13682 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13704 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16748 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1467 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1468 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1470 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7443 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6670 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16732 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8840 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7693 df-imp 7692 df-iplp 7691 df-reap 8758 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8854 rerecapb 9026 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6303 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7885 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16372 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16725 dceqnconst 16724 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8123 caucvgpr 7905 caucvgprpr 7935 caucvgsr 8025 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7689 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16730 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4394 ltpopr 7818 ltsopr 7819 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8789 reapcotr 8781 reapirr 8760 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8309 gt0add 8756 leadd1 8613 lelttr 8271 lemul1a 9041 lenlt 8258 ltadd1 8612 ltletr 8272 ltmul1 8775 reaplt 8771 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16305 |
| [Jech] p. 4 | Definition of class | cv 1396 cvjust 2226 |
| [Jech] p. 78 | Note | opthprc 4777 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1578 |
| [Kreyszig] p. 3 | Property M1 | metcl 15104 xmetcl 15103 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15111 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8851 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15193 |
| [Kreyszig] p. 19 | Remark | mopntopon 15194 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15239 mopnm 15199 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15237 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15242 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15264 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14964 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14366 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14357 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14358 |
| [Kunen] p. 10 | Axiom 0 | a9e 1744 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4206 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6832 mapvalg 6830 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6826 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3980 |
| [Lang] p. 3 | Statement | lidrideqd 13485 mndbn0 13535 |
| [Lang] p. 3 | Definition | df-mnd 13521 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13502 |
| [Lang] p. 5 | Equation | gsumfzreidx 13945 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13736 |
| [Lang] p. 7 | Definition | dfgrp2e 13632 |
| [Levy] p. 338 | Axiom | df-clab 2218 df-clel 2227 df-cleq 2224 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1467 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1468 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1470 |
| [Margaris] p. 40 | Rule C | exlimiv 1646 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 860 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 899 exalim 1550 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 657 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1686 r19.2m 3581 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1602 19.3h 1601 rr19.3v 2945 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1526 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1667 alexim 1693 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1547 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1638 spsbe 1890 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1692 19.9h 1691 19.9v 1919 exlimd 1645 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1712 excomim 1711 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1713 r19.12 2639 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1694 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1516 ralbi 2665 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1603 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1604 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1652 rexbi 2666 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1714 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1505 alimd 1569 alimdh 1515 alimdv 1927 ralimdaa 2598 ralimdv 2600 ralimdva 2599 ralimdvva 2601 sbcimdv 3097 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1715 19.21 1631 19.21bi 1606 19.21h 1605 19.21ht 1629 19.21t 1630 19.21v 1921 alrimd 1658 alrimdd 1657 alrimdh 1527 alrimdv 1924 alrimi 1570 alrimih 1517 alrimiv 1922 alrimivv 1923 r19.21 2608 r19.21be 2623 r19.21bi 2620 r19.21t 2607 r19.21v 2609 ralrimd 2610 ralrimdv 2611 ralrimdva 2612 ralrimdvv 2616 ralrimdvva 2617 ralrimi 2603 ralrimiv 2604 ralrimiva 2605 ralrimivv 2613 ralrimivva 2614 ralrimivvva 2615 ralrimivw 2606 rexlimi 2643 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1929 2eximdv 1930 exim 1647 eximd 1660 eximdh 1659 eximdv 1928 rexim 2626 reximdai 2630 reximddv 2635 reximddv2 2637 reximdv 2633 reximdv2 2631 reximdva 2634 reximdvai 2632 reximi2 2628 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1726 19.23bi 1640 19.23h 1546 19.23ht 1545 19.23t 1725 19.23v 1931 19.23vv 1932 exlimd2 1643 exlimdh 1644 exlimdv 1867 exlimdvv 1946 exlimi 1642 exlimih 1641 exlimiv 1646 exlimivv 1945 r19.23 2641 r19.23v 2642 rexlimd 2647 rexlimdv 2649 rexlimdv3a 2652 rexlimdva 2650 rexlimdva2 2653 rexlimdvaa 2651 rexlimdvv 2657 rexlimdvva 2658 rexlimdvw 2654 rexlimiv 2644 rexlimiva 2645 rexlimivv 2656 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1687 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1674 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1530 19.26-3an 1531 19.26 1529 r19.26-2 2662 r19.26-3 2663 r19.26 2659 r19.26m 2664 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1609 19.27h 1608 19.27v 1948 r19.27av 2668 r19.27m 3590 r19.27mv 3591 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1611 19.28h 1610 19.28v 1949 r19.28av 2669 r19.28m 3584 r19.28mv 3587 rr19.28v 2946 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1668 19.29r 1669 19.29r2 1670 19.29x 1671 r19.29 2670 r19.29d2r 2677 r19.29r 2671 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1675 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1729 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1727 19.32r 1728 r19.32r 2679 r19.32vdc 2682 r19.32vr 2681 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1532 19.33b2 1677 19.33bdc 1678 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1732 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1672 19.35i 1673 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1721 19.36aiv 1950 19.36i 1720 r19.36av 2684 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1722 19.37aiv 1723 r19.37 2685 r19.37av 2686 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1724 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1688 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1680 19.40 1679 r19.40 2687 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1734 19.41h 1733 19.41v 1951 19.41vv 1952 19.41vvv 1953 19.41vvvv 1954 r19.41 2688 r19.41v 2689 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1736 19.42h 1735 19.42v 1955 19.42vv 1960 19.42vvv 1961 19.42vvvv 1962 r19.42v 2690 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1676 r19.43 2691 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1730 r19.44av 2692 r19.44mv 3589 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1731 r19.45av 2693 r19.45mv 3588 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2104 |
| [Megill] p. 444 | Axiom C5 | ax-17 1574 |
| [Megill] p. 445 | Lemma L12 | alequcom 1563 ax-10 1553 |
| [Megill] p. 446 | Lemma L17 | equtrr 1758 |
| [Megill] p. 446 | Lemma L19 | hbnae 1769 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1811 sbid 1822 |
| [Megill] p. 448 | Scheme C5' | ax-4 1558 |
| [Megill] p. 448 | Scheme C6' | ax-7 1496 |
| [Megill] p. 448 | Scheme C8' | ax-8 1552 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1555 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1764 |
| [Megill] p. 448 | Scheme C12' | ax-13 2204 |
| [Megill] p. 448 | Scheme C13' | ax-14 2205 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1871 |
| [Megill] p. 448 | Scheme C16' | ax-16 1862 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1778 dral2 1779 drex1 1846 drex2 1780 drsb1 1847 drsb2 1889 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2040 sbequ 1888 sbid2v 2049 |
| [Megill] p. 450 | Example in Appendix | hba1 1588 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3115 rspsbca 3116 stdpc4 1823 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3121 stdpc5 1632 |
| [Mendelson] p. 81 | Rule C | exlimiv 1646 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1751 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1818 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3531 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3532 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3447 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3495 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3448 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3338 |
| [Mendelson] p. 231 | Definition of union | unssin 3446 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4573 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3892 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4379 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4380 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4381 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3913 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4859 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5257 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4468 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7034 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7008 xpsneng 7009 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7014 xpcomeng 7015 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7017 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7011 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6824 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6989 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7039 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6858 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6990 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7435 djucomen 7434 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7433 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6638 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3429 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4814 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4815 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4151 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5252 coi2 5253 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4945 rn0 4988 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5141 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4835 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4952 rnxpm 5166 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4806 xp0 5156 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5095 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5092 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5091 imaexg 5090 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5087 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5778 funfvop 5760 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5688 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5698 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5371 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5912 dff13f 5914 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5880 funrnex 6279 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5906 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5220 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3944 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6321 df-1st 6306 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6322 df-2nd 6307 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1495 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1552 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1554 ax-11o 1871 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1875 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1496 |
| [Monk2] p. 109 | Lemma 15 | equvin 1911 equvini 1806 eqvinop 4335 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1574 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1699 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1496 |
| [Monk2] p. 114 | Lemma 22 | hba1 1588 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1600 nfia1 1628 |
| [Monk2] p. 114 | Lemma 24 | hba2 1599 nfa2 1627 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 838 dftest 16749 |
| [Munkres] p. 77 | Example 2 | distop 14836 |
| [Munkres] p. 78 | Definition of basis | df-bases 14794 isbasis3g 14797 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13364 tgval2 14802 |
| [Munkres] p. 79 | Remark | tgcl 14815 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14809 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14830 tgss3 14829 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14831 basgen2 14832 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14921 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14863 topcld 14860 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14864 |
| [Munkres] p. 94 | Definition of closure | clsval 14862 |
| [Munkres] p. 94 | Definition of interior | ntrval 14861 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14939 iscn 14948 iscn2 14951 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14981 cncnp2m 14982 cncnpi 14979 df-cnp 14940 iscnp 14950 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15265 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7096 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7366 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7354 omniwomnimkv 7369 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3317 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7337 exmidomniim 7343 finomni 7342 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7322 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16682 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16686 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7103 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7415 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7416 exmidfodomrlemrALT 7417 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7351 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16668 peano4nninf 16667 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16670 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16678 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16680 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16666 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2218 rabid 2709 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2044 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2224 |
| [Quine] p. 19 | Definition 2.9 | df-v 2804 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2340 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2352 abid2f 2400 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1936 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1934 sb6 1935 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2227 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2231 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2233 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3032 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3033 dfsbcq2 3034 |
| [Quine] p. 43 | Theorem 6.8 | vex 2805 |
| [Quine] p. 43 | Theorem 6.9 | isset 2809 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2888 spcgv 2893 spcimgf 2886 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3043 spsbcd 3044 |
| [Quine] p. 44 | Theorem 6.12 | elex 2814 |
| [Quine] p. 44 | Theorem 6.13 | elab 2950 elabg 2952 elabgf 2948 |
| [Quine] p. 44 | Theorem 6.14 | noel 3498 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3734 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3676 df-sn 3675 |
| [Quine] p. 49 | Theorem 7.4 | snss 3808 snssg 3807 |
| [Quine] p. 49 | Theorem 7.5 | prss 3829 prssg 3830 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3777 prid1g 3775 prid2 3778 prid2g 3776 snid 3700 snidg 3698 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4274 snexprc 4276 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4301 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3909 unisng 3910 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3912 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3921 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3920 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5297 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5287 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5298 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5302 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5303 |
| [Quine] p. 58 | Definition 9.1 | df-op 3678 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4350 opabidw 4351 opelopab 4366 opelopaba 4360 opelopabaf 4368 opelopabf 4369 opelopabg 4362 opelopabga 4357 opelopabgf 4364 oprabid 6053 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4731 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4733 |
| [Quine] p. 64 | Definition 9.15 | df-id 4390 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5388 |
| [Quine] p. 65 | Theorem 10.4 | funi 5358 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5378 funsng 5376 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5328 |
| [Quine] p. 65 | Definition 10.2 | args 5105 dffv4g 5637 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5334 fv2 5635 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10990 nn0opth2d 10989 nn0opthd 10988 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5415 funimaexg 5414 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13968 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14033 |
| [Rudin] p. 164 | Equation 27 | efcan 12258 |
| [Rudin] p. 164 | Equation 30 | efzval 12265 |
| [Rudin] p. 167 | Equation 48 | absefi 12351 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1470 |
| [Sanford] p. 39 | Rule 4 | mptxor 1468 |
| [Sanford] p. 40 | Rule 1 | mptnan 1467 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5121 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5123 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5120 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5118 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14035 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14834 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3472 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3566 dif0 3565 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3579 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3465 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3466 |
| [Stoll] p. 20 | Remark | invdif 3449 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3679 |
| [Stoll] p. 43 | Definition | uniiun 4024 |
| [Stoll] p. 44 | Definition | intiin 4025 |
| [Stoll] p. 45 | Definition | df-iin 3973 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3972 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 896 imanst 895 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3472 |
| [Suppes] p. 22 | Theorem 2 | eq0 3513 |
| [Suppes] p. 22 | Theorem 4 | eqss 3242 eqssd 3244 eqssi 3243 |
| [Suppes] p. 23 | Theorem 5 | ss0 3535 ss0b 3534 |
| [Suppes] p. 23 | Theorem 6 | sstr 3235 |
| [Suppes] p. 25 | Theorem 12 | elin 3390 elun 3348 |
| [Suppes] p. 26 | Theorem 15 | inidm 3416 |
| [Suppes] p. 26 | Theorem 16 | in0 3529 |
| [Suppes] p. 27 | Theorem 23 | unidm 3350 |
| [Suppes] p. 27 | Theorem 24 | un0 3528 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3370 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3377 |
| [Suppes] p. 27 | Theorem 27 | unss 3381 |
| [Suppes] p. 27 | Theorem 28 | indir 3456 |
| [Suppes] p. 27 | Theorem 29 | undir 3457 |
| [Suppes] p. 28 | Theorem 32 | difid 3563 difidALT 3564 |
| [Suppes] p. 29 | Theorem 33 | difin 3444 |
| [Suppes] p. 29 | Theorem 34 | indif 3450 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3569 |
| [Suppes] p. 29 | Theorem 36 | difun2 3574 |
| [Suppes] p. 29 | Theorem 37 | difin0 3568 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3567 |
| [Suppes] p. 29 | Theorem 39 | difundi 3459 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3461 |
| [Suppes] p. 30 | Theorem 41 | nalset 4219 |
| [Suppes] p. 39 | Theorem 61 | uniss 3914 |
| [Suppes] p. 39 | Theorem 65 | uniop 4348 |
| [Suppes] p. 41 | Theorem 70 | intsn 3963 |
| [Suppes] p. 42 | Theorem 71 | intpr 3960 intprg 3961 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4575 op1stbg 4576 |
| [Suppes] p. 42 | Theorem 78 | intun 3959 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4004 dfiun2g 4002 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4005 |
| [Suppes] p. 47 | Theorem 86 | elpw 3658 elpw2 4247 elpw2g 4246 elpwg 3660 |
| [Suppes] p. 47 | Theorem 87 | pwid 3667 |
| [Suppes] p. 47 | Theorem 89 | pw0 3820 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3888 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4833 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4865 xpindir 4866 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4782 xpundir 4783 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4646 |
| [Suppes] p. 58 | Theorem 2 | relss 4813 |
| [Suppes] p. 59 | Theorem 4 | eldm 4928 eldm2 4929 eldm2g 4927 eldmg 4926 |
| [Suppes] p. 59 | Definition 3 | df-dm 4735 |
| [Suppes] p. 60 | Theorem 6 | dmin 4939 |
| [Suppes] p. 60 | Theorem 8 | rnun 5145 |
| [Suppes] p. 60 | Theorem 9 | rnin 5146 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4918 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4913 brcnvg 4911 |
| [Suppes] p. 62 | Equation 5 | elcnv 4907 elcnv2 4908 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5114 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5144 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5142 |
| [Suppes] p. 63 | Theorem 20 | co02 5250 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5002 |
| [Suppes] p. 63 | Definition 7 | df-co 4734 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4915 |
| [Suppes] p. 64 | Theorem 27 | coass 5255 |
| [Suppes] p. 65 | Theorem 31 | resundi 5026 |
| [Suppes] p. 65 | Theorem 34 | elima 5081 elima2 5082 elima3 5083 elimag 5080 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5149 |
| [Suppes] p. 66 | Theorem 40 | dminss 5151 |
| [Suppes] p. 66 | Theorem 41 | imainss 5152 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5155 |
| [Suppes] p. 81 | Definition 34 | dfec2 6708 |
| [Suppes] p. 82 | Theorem 72 | elec 6746 elecg 6745 |
| [Suppes] p. 82 | Theorem 73 | erth 6751 erth2 6752 |
| [Suppes] p. 89 | Theorem 96 | map0b 6859 |
| [Suppes] p. 89 | Theorem 97 | map0 6861 map0g 6860 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6862 |
| [Suppes] p. 89 | Theorem 99 | mapss 6863 |
| [Suppes] p. 92 | Theorem 1 | enref 6941 enrefg 6940 |
| [Suppes] p. 92 | Theorem 2 | ensym 6958 ensymb 6957 ensymi 6959 |
| [Suppes] p. 92 | Theorem 3 | entr 6961 |
| [Suppes] p. 92 | Theorem 4 | unen 6994 |
| [Suppes] p. 94 | Theorem 15 | endom 6939 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6955 |
| [Suppes] p. 94 | Theorem 17 | domtr 6962 |
| [Suppes] p. 95 | Theorem 18 | isbth 7169 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6984 fundmeng 6985 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7021 |
| [Suppes] p. 130 | Definition 3 | df-tr 4188 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4586 |
| [Suppes] p. 134 | Definition 6 | df-suc 4468 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4701 finds 4698 finds1 4700 finds2 4699 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7576 df-ltpq 7569 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4487 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2213 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2227 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2226 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2249 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6025 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3030 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3690 elpr2 3691 elprg 3689 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3685 elsn2 3703 elsn2g 3702 elsng 3684 velsn 3686 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4323 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3680 sneqr 3843 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3688 dfsn2 3683 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4534 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4329 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4307 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4538 unexg 4540 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3718 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3894 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3206 df-un 3204 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3907 uniprg 3908 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4269 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3717 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4503 elsucg 4501 sstr2 3234 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3351 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3399 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3364 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3417 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3454 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3455 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3215 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3654 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3378 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3213 dfss2 3217 sseqin2 3426 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3247 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3427 inss2 3428 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3287 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3902 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4308 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4315 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2519 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4216 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3202 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3496 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3563 difidALT 3564 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3507 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4637 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2804 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4221 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3533 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4226 ssexg 4228 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4223 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4648 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4639 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3559 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3332 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3468 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3333 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3341 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2515 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2516 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4842 xpexg 4840 xpexgALT 6298 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4732 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5394 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5554 fun11 5397 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5337 svrelfun 5395 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4917 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4919 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4737 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4738 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4734 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5191 dfrel2 5187 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4834 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4844 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4850 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4864 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5041 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5018 opelresg 5020 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5034 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5037 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5042 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5367 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5235 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5366 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5555 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2124 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5334 fv3 5663 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5275 cnvexg 5274 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4999 dmexg 4996 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5000 rnexg 4997 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5657 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5667 tz6.12 5668 tz6.12c 5670 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5631 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5329 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5330 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5332 wfo 5324 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5331 wf1 5323 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5333 wf1o 5325 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5745 eqfnfv2 5746 eqfnfv2f 5749 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5717 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5877 fnexALT 6276 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5876 resfunexgALT 6273 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5415 funimaexg 5414 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4089 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5106 iniseg 5108 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4386 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5335 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5954 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5955 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5960 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5962 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5970 |
| [TakeutiZaring] p. 35 | Notation | wtr 4187 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4451 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4191 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4674 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4478 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4482 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4590 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4465 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4584 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4650 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4680 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4189 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4609 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4585 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3921 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4468 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4512 sucidg 4513 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4599 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4466 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4604 ordelsuc 4603 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4692 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4693 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4694 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4691 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4705 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4697 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4695 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4696 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3942 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4203 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3943 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4615 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3929 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6477 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6534 tfri1d 6504 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6535 tfri2d 6505 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6536 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6471 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6455 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6635 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6631 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6628 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6632 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6680 nnaordi 6679 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4015 uniss2 3924 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6641 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6651 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6642 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6629 omsuc 6643 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6652 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6688 nnmordi 6687 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6630 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7394 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6972 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7046 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7047 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6915 isfi 6937 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7018 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6822 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7024 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7037 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1558 |
| [Tarski] p. 68 | Lemma 6 | equid 1749 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1752 |
| [Tarski] p. 70 | Lemma 14 | spim 1786 spime 1789 spimeh 1787 spimh 1785 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1554 ax-11o 1871 ax11i 1762 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1935 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1574 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2204 ax-14 2205 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 718 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 734 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 763 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 772 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 796 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 621 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 648 |
| [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 844 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2178 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 744 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 843 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 634 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 892 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 850 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 863 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 647 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 860 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 862 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 719 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 782 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 622 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 626 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 900 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 914 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 775 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 776 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 811 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 812 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 810 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1005 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 785 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 783 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 784 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 745 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 874 pm2.5gdc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 869 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 749 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 661 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 662 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 729 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 898 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 732 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 733 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 872 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 755 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 807 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 808 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 665 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 720 pm2.67 750 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 876 pm2.521gdc 875 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 754 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 901 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 922 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 818 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 819 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 912 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 761 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 965 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 966 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 967 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 760 |
| [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 700 |
| [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 867 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 866 |
| [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 695 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 601 |
| [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 762 pm3.44 722 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 606 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 792 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 878 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 879 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 897 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 701 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 960 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 764 pm4.25 765 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 825 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 735 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 774 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 799 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 609 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 829 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1006 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 823 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 979 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 957 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 786 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 821 pm4.45 791 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1529 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 964 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 904 imorr 728 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 757 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 758 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 909 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 946 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 759 pm4.56 787 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 947 oranim 788 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 692 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 893 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 693 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 908 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 894 |
| [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 834 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 751 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 607 pm4.76 608 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 717 pm4.77 806 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 789 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 910 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 714 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 915 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 958 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 959 |
| [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 559 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 605 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 916 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 919 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 918 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1433 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 835 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 911 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1438 pm5.18dc 890 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 713 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 702 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1436 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1441 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1442 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 902 |
| [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 933 pm5.6r 934 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 962 |
| [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 613 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 924 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 614 |
| [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 932 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 809 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 925 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 920 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 801 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 953 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 954 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 969 |
| [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 970 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1683 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1533 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1680 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1944 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2082 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2483 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2484 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2944 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3088 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5306 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5307 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2159 eupickbi 2162 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5334 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7398 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |