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 7408 fidcenum 7228 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7228 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7408 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13193 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7194 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7180 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13208 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13210 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13199 znnen 13166 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13211 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13212 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11143 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4661 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11283 df-pfx 11369 df-substr 11342 df-word 11229 lencl 11232 wrd0 11253 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8455 addcan2d 8460 addcan2i 8458 addcand 8459 addcani 8457 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8466 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8523 negsubd 8592 negsubi 8553 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8525 negnegd 8577 negnegi 8545 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8660 subdid 8689 subdii 8682 subdir 8661 subdird 8690 subdiri 8683 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8664 mul01d 8668 mul01i 8666 mul02 8662 mul02d 8667 mul02i 8665 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 9069 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 9020 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8673 mul2negd 8688 mul2negi 8681 mulneg1 8670 mulneg1d 8686 mulneg1i 8679 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14306 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8989 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 10013 rpaddcld 10048 rpmulcl 10014 rpmulcld 10049 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 10025 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8380 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8814 ltadd1dd 8832 ltadd1i 8778 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8868 ltmul1a 8867 ltmul1i 9196 ltmul1ii 9204 ltmul2 9132 ltmul2d 10075 ltmul2dd 10089 ltmul2i 9199 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8402 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8744 lt0neg1d 8791 ltneg 8738 ltnegd 8799 ltnegi 8769 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8721 lt2addd 8843 lt2addi 8786 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9990 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9126 recgt0d 9210 recgt0i 9182 recgt0ii 9183 |
| [Apostol] p. 22 | Definition of integers | df-z 9580 |
| [Apostol] p. 22 | Definition of rationals | df-q 9955 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7287 |
| [Apostol] p. 26 | Theorem I.29 | arch 9495 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9700 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9496 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10620 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12561 zneo 9682 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11720 sqrtthi 11808 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9242 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12736 |
| [Apostol] p. 363 | Remark | absgt0api 11835 |
| [Apostol] p. 363 | Example | abssubd 11882 abssubi 11839 |
| [ApostolNT] p. 14 | Definition | df-dvds 12478 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12494 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12518 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12514 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12508 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12510 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12495 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12496 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12501 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12535 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12537 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12539 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12714 |
| [ApostolNT] p. 16 | Definition | isprm2 12818 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12793 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13223 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12673 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12715 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12717 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12687 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12680 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12845 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12847 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 13070 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12614 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12760 |
| [ApostolNT] p. 25 | Definition | df-phi 12912 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12942 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12923 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12927 |
| [ApostolNT] p. 38 | Remark | df-sgm 15867 |
| [ApostolNT] p. 38 | Definition | df-sgm 15867 |
| [ApostolNT] p. 104 | Definition | congr 12801 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12481 |
| [ApostolNT] p. 106 | Definition | moddvds 12489 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12568 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12569 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10707 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10744 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 11032 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12513 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12804 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13123 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12806 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12934 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12953 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12935 |
| [ApostolNT] p. 179 | Definition | df-lgs 15888 lgsprme0 15932 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15933 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15909 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15924 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15975 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15994 2lgsoddprm 16003 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15959 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15970 |
| [ApostolNT] p. 188 | Definition | df-lgs 15888 lgs1 15934 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15925 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15927 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15935 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15936 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 621 pm2.65 665 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6051 onsucelsucexmidlem 4653 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16788 |
| [Bauer], p. 483 | Definition | n0rf 3523 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15858 2irrexpqap 15860 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7201 ssfiexmid 7133 ssfiexmidt 7135 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15535 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15525 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8921 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7408 |
| [BauerSwan], p. 14 | Remark | 0ct 7400 ctm 7402 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16791 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7818 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7731 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7820 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7854 addlocpr 7853 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7880 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7883 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7888 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2085 |
| [BellMachover] p. 460 | Notation | df-mo 2086 |
| [BellMachover] p. 460 | Definition | mo3 2137 mo3h 2136 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2219 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4233 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4292 |
| [BellMachover] p. 466 | Axiom Union | axun2 4558 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4666 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4507 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4669 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4620 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4492 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4713 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4738 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1476 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1474 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1477 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1472 |
| [Bollobas] p. 1 | Section I.1 | df-edg 16070 isuhgropm 16093 isusgropen 16177 isuspgropen 16176 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16266 uhgrspansubgr 16289 |
| [Bollobas] p. 4 | Definition | df-wlks 16330 |
| [Bollobas] p. 5 | Definition | df-trls 16393 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 16082 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13586 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13632 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13647 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14159 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 14094 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5958 fcofo 5959 |
| [BourbakiTop1] p. | Remark | xnegmnf 10165 xnegpnf 10164 |
| [BourbakiTop1] p. | Remark | rexneg 10166 |
| [BourbakiTop1] p. | Proposition | ishmeo 15186 |
| [BourbakiTop1] p. | Property V_i | ssnei2 15039 |
| [BourbakiTop1] p. | Property V_ii | innei 15045 |
| [BourbakiTop1] p. | Property V_iv | neissex 15047 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 15036 neiss 15032 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 15104 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15181 |
| [BourbakiTop1] p. | Property V_iii | elnei 15034 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14880 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13586 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13632 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13829 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4175 |
| [Church] p. 129 | Section II.24 | df-ifp 987 dfifp2dc 990 |
| [Cohen] p. 301 | Remark | relogoprlem 15750 |
| [Cohen] p. 301 | Property 2 | relogmul 15751 relogmuld 15766 |
| [Cohen] p. 301 | Property 3 | relogdiv 15752 relogdivd 15767 |
| [Cohen] p. 301 | Property 4 | relogexp 15754 |
| [Cohen] p. 301 | Property 1a | log1 15748 |
| [Cohen] p. 301 | Property 1b | loge 15749 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15847 |
| [Cohen4] p. 352 | Definition | rpelogb 15831 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15837 |
| [Cohen4] p. 361 | Property 3 | logbrec 15842 rprelogbdiv 15839 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15835 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15840 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15829 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15830 |
| [Cohen4] p. 367 | Property | rplogbchbase 15832 |
| [Cohen4] p. 377 | Property 2 | logblt 15844 |
| [Crosilla] p. | Axiom 1 | ax-ext 2216 |
| [Crosilla] p. | Axiom 2 | ax-pr 4324 |
| [Crosilla] p. | Axiom 3 | ax-un 4556 |
| [Crosilla] p. | Axiom 4 | ax-nul 4238 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4712 |
| [Crosilla] p. | Axiom 6 | ru 3043 |
| [Crosilla] p. | Axiom 8 | ax-pow 4289 |
| [Crosilla] p. | Axiom 9 | ax-setind 4661 |
| [Crosilla], p. | Axiom 6 | ax-sep 4230 |
| [Crosilla], p. | Axiom 7 | ax-coll 4227 |
| [Crosilla], p. | Axiom 7' | repizf 4228 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4645 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6051 |
| [Crosilla], p. | Definition of ordinal | df-iord 4489 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4659 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16266 uhgrspansubgr 16289 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 16082 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3215 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4715 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6886 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4237 |
| [Enderton] p. 19 | Definition | df-tp 3699 |
| [Enderton] p. 26 | Exercise 5 | unissb 3946 |
| [Enderton] p. 26 | Exercise 10 | pwel 4336 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4409 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4063 iinin2m 4062 iunin1 4058 iunin2 4057 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4061 iundif2ss 4059 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4076 |
| [Enderton] p. 33 | Exercise 25 | iununir 4077 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4084 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4603 iunpwss 4085 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4335 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4307 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4573 rnex 5027 rnexg 5024 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4968 rnuni 5176 |
| [Enderton] p. 42 | Definition of a function | dffun7 5381 dffun8 5382 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5743 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5419 |
| [Enderton] p. 44 | Definition (d) | dfima2 5105 dfima3 5106 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5748 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7515 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5936 |
| [Enderton] p. 52 | Definition | df-map 6886 |
| [Enderton] p. 53 | Exercise 21 | coass 5283 |
| [Enderton] p. 53 | Exercise 27 | dmco 5273 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5429 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5140 |
| [Enderton] p. 54 | Remark | ixpf 6957 ixpssmap 6969 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6936 |
| [Enderton] p. 56 | Theorem 3M | erref 6789 |
| [Enderton] p. 57 | Lemma 3N | erthi 6817 |
| [Enderton] p. 57 | Definition | df-ec 6771 |
| [Enderton] p. 58 | Definition | df-qs 6775 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6876 th3qcor 6875 th3qlem1 6873 th3qlem2 6874 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6771 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4965 |
| [Enderton] p. 68 | Definition of successor | df-suc 4494 |
| [Enderton] p. 71 | Definition | df-tr 4211 dftr4 4215 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4536 unisucg 4537 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4536 unisucg 4537 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4224 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4225 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6709 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6711 onasuc 6701 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6055 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6710 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6712 onmsuc 6708 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6720 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6713 nnacom 6719 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6721 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6722 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6724 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6714 nnmsucr 6723 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6763 |
| [Enderton] p. 129 | Definition | df-en 6978 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6003 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13163 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7122 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7113 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7101 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7527 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7523 dju1en 7522 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3587 |
| [Enderton] p. 145 | Figure 38 | ffoss 5649 |
| [Enderton] p. 145 | Definition | df-dom 6979 |
| [Enderton] p. 146 | Example 1 | domen 6990 domeng 6991 |
| [Enderton] p. 146 | Example 3 | nndomo 7120 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7088 xpdom1g 7086 xpdom2g 7085 |
| [Enderton] p. 168 | Definition | df-po 4419 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4551 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4512 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4667 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4515 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4640 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4613 |
| [Enderton] p. 194 | Remark | onprc 4676 |
| [Enderton] p. 194 | Exercise 16 | suc11 4682 |
| [Enderton] p. 197 | Definition | df-card 7477 |
| [Enderton] p. 200 | Exercise 25 | tfis 4707 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4678 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4680 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4681 |
| [Geuvers], p. 1 | Remark | expap0 10935 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8891 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8930 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8892 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8248 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11892 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11900 maxle2 11901 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11902 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11905 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11906 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8858 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7664 enqer 7675 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7668 df-nqqs 7665 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7661 df-plqqs 7666 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7662 df-mqqs 7667 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7669 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7725 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7728 ltbtwnnq 7733 ltbtwnnqq 7732 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7717 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7718 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7854 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7896 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7895 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7914 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7930 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7936 ltaprlem 7935 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7933 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7889 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7909 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7898 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7897 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7905 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7955 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 8043 enrer 8052 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 8048 df-1r 8049 df-nr 8044 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 8046 df-plr 8045 negexsr 8089 recexsrlem 8091 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 8047 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9236 creur 9235 cru 8878 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8240 axcnre 8198 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11547 crimd 11666 crimi 11626 crre 11546 crred 11665 crrei 11625 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11549 remimd 11631 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11746 absval2d 11874 absval2i 11833 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11573 cjaddd 11654 cjaddi 11621 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11574 cjmuld 11655 cjmuli 11622 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11572 cjcjd 11632 cjcji 11604 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11571 cjreb 11555 cjrebd 11635 cjrebi 11607 cjred 11660 rere 11554 rereb 11552 rerebd 11634 rerebi 11606 rered 11658 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11580 addcjd 11646 addcji 11616 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11690 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11741 abscjd 11879 abscji 11837 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11753 abs00d 11875 abs00i 11834 absne0d 11876 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11785 releabsd 11880 releabsi 11838 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11758 absmuld 11883 absmuli 11840 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11744 sqabsaddi 11841 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11793 abstrid 11885 abstrii 11844 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10905 exp0 10909 expp1 10912 expp1d 11040 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10947 expaddd 11041 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15794 cxpmuld 15819 expmul 10950 expmuld 11042 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10944 mulexpd 11054 rpmulcxp 15791 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10347 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 12015 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 12017 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 12016 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 12020 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 12013 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 12009 climcj 12010 climim 12012 climre 12011 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8315 df-xr 8314 ltxr 10111 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 12036 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10664 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14710 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15246 xmet0 15245 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15253 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15255 mstri 15355 xmettri 15254 xmstri 15354 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15161 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15393 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11999 addcncntop 15444 mulcn2 12001 mulcncntop 15446 subcn2 12000 subcncntop 15445 |
| [Gleason] p. 295 | Remark | bcval3 11117 bcval4 11118 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11132 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11115 df-bc 11114 |
| [Gleason] p. 296 | Remark | bcn0 11121 bcnn 11123 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12174 |
| [Gleason] p. 308 | Equation 2 | ef0 12362 |
| [Gleason] p. 308 | Equation 3 | efcj 12363 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12368 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12372 |
| [Gleason] p. 310 | Equation 14 | sinadd 12426 |
| [Gleason] p. 310 | Equation 15 | cosadd 12427 |
| [Gleason] p. 311 | Equation 17 | sincossq 12438 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12443 sinbnd 12442 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12343 |
| [Golan] p. 1 | Remark | srgisid 14147 |
| [Golan] p. 1 | Definition | df-srg 14125 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1498 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13741 mndideu 13656 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13768 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13797 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13808 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13830 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16888 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1468 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1469 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1471 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7534 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6734 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16871 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8933 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7787 df-imp 7786 df-iplp 7785 df-reap 8851 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8947 rerecapb 9119 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6333 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7979 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16506 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16864 dceqnconst 16863 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8217 caucvgpr 7999 caucvgprpr 8029 caucvgsr 8119 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7783 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16869 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4420 ltpopr 7912 ltsopr 7913 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8882 reapcotr 8874 reapirr 8853 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8402 gt0add 8849 leadd1 8706 lelttr 8364 lemul1a 9134 lenlt 8351 ltadd1 8705 ltletr 8365 ltmul1 8868 reaplt 8864 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16439 |
| [Jech] p. 4 | Definition of class | cv 1397 cvjust 2229 |
| [Jech] p. 78 | Note | opthprc 4803 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1579 |
| [Kreyszig] p. 3 | Property M1 | metcl 15235 xmetcl 15234 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15242 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8944 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15324 |
| [Kreyszig] p. 19 | Remark | mopntopon 15325 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15370 mopnm 15330 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15368 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15373 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15395 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 15095 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14495 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14486 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14487 |
| [Kunen] p. 10 | Axiom 0 | a9e 1744 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4229 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6896 mapvalg 6894 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6890 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4003 |
| [Lang] p. 3 | Statement | lidrideqd 13611 mndbn0 13661 |
| [Lang] p. 3 | Definition | df-mnd 13647 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13628 |
| [Lang] p. 5 | Equation | gsumfzreidx 14071 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13862 |
| [Lang] p. 7 | Definition | dfgrp2e 13758 |
| [Levy] p. 338 | Axiom | df-clab 2221 df-clel 2230 df-cleq 2227 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1468 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1469 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1471 |
| [Margaris] p. 40 | Rule C | exlimiv 1647 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 861 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 900 exalim 1551 |
| [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 1687 r19.2m 3598 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1603 19.3h 1602 rr19.3v 2958 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1527 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1668 alexim 1694 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1548 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1639 spsbe 1891 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1693 19.9h 1692 19.9v 1920 exlimd 1646 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1712 excomim 1711 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1713 r19.12 2651 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1695 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1517 ralbi 2677 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1604 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1605 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1653 rexbi 2678 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1714 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1506 alimd 1570 alimdh 1516 alimdv 1928 ralimdaa 2610 ralimdv 2612 ralimdva 2611 ralimdvva 2613 sbcimdv 3110 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1715 19.21 1632 19.21bi 1607 19.21h 1606 19.21ht 1630 19.21t 1631 19.21v 1922 alrimd 1659 alrimdd 1658 alrimdh 1528 alrimdv 1925 alrimi 1571 alrimih 1518 alrimiv 1923 alrimivv 1924 r19.21 2620 r19.21be 2635 r19.21bi 2632 r19.21t 2619 r19.21v 2621 ralrimd 2622 ralrimdv 2623 ralrimdva 2624 ralrimdvv 2628 ralrimdvva 2629 ralrimi 2615 ralrimiv 2616 ralrimiva 2617 ralrimivv 2625 ralrimivva 2626 ralrimivvva 2627 ralrimivw 2618 rexlimi 2655 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1930 2eximdv 1931 exim 1648 eximd 1661 eximdh 1660 eximdv 1929 rexim 2638 reximdai 2642 reximddv 2647 reximddv2 2649 reximdv 2645 reximdv2 2643 reximdva 2646 reximdvai 2644 reximi2 2640 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1726 19.23bi 1641 19.23h 1547 19.23ht 1546 19.23t 1725 19.23v 1932 19.23vv 1933 exlimd2 1644 exlimdh 1645 exlimdv 1868 exlimdvv 1949 exlimi 1643 exlimih 1642 exlimiv 1647 exlimivv 1948 r19.23 2653 r19.23v 2654 rexlimd 2659 rexlimdv 2661 rexlimdv3a 2664 rexlimdva 2662 rexlimdva2 2665 rexlimdvaa 2663 rexlimdvv 2669 rexlimdvva 2670 rexlimdvw 2666 rexlimiv 2656 rexlimiva 2657 rexlimivv 2668 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1688 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1675 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1531 19.26-3an 1532 19.26 1530 r19.26-2 2674 r19.26-3 2675 r19.26 2671 r19.26m 2676 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1610 19.27h 1609 19.27v 1951 r19.27av 2680 r19.27m 3607 r19.27mv 3608 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1612 19.28h 1611 19.28v 1952 r19.28av 2681 r19.28m 3601 r19.28mv 3604 rr19.28v 2959 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1669 19.29r 1670 19.29r2 1671 19.29x 1672 r19.29 2682 r19.29d2r 2689 r19.29r 2683 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1676 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1729 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1727 19.32r 1728 r19.32r 2691 r19.32vdc 2694 r19.32vr 2693 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1533 19.33b2 1678 19.33bdc 1679 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1732 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1673 19.35i 1674 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1721 19.36aiv 1953 19.36i 1720 r19.36av 2696 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1722 19.37aiv 1723 r19.37 2697 r19.37av 2698 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1724 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1689 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1681 19.40 1680 r19.40 2699 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1734 19.41h 1733 19.41v 1954 19.41vv 1955 19.41vvv 1956 19.41vvvv 1957 r19.41 2700 r19.41v 2701 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1736 19.42h 1735 19.42v 1958 19.42vv 1963 19.42vvv 1964 19.42vvvv 1965 r19.42v 2702 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1677 r19.43 2703 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1730 r19.44av 2704 r19.44mv 3606 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1731 r19.45av 2705 r19.45mv 3605 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2107 |
| [Megill] p. 444 | Axiom C5 | ax-17 1575 |
| [Megill] p. 445 | Lemma L12 | alequcom 1564 ax-10 1554 |
| [Megill] p. 446 | Lemma L17 | equtrr 1758 |
| [Megill] p. 446 | Lemma L19 | hbnae 1769 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1812 sbid 1823 |
| [Megill] p. 448 | Scheme C5' | ax-4 1559 |
| [Megill] p. 448 | Scheme C6' | ax-7 1497 |
| [Megill] p. 448 | Scheme C8' | ax-8 1553 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1556 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1764 |
| [Megill] p. 448 | Scheme C12' | ax-13 2207 |
| [Megill] p. 448 | Scheme C13' | ax-14 2208 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1872 |
| [Megill] p. 448 | Scheme C16' | ax-16 1863 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1779 dral2 1780 drex1 1847 drex2 1781 drsb1 1848 drsb2 1890 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2043 sbequ 1889 sbid2v 2052 |
| [Megill] p. 450 | Example in Appendix | hba1 1589 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3128 rspsbca 3129 stdpc4 1824 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3134 stdpc5 1633 |
| [Mendelson] p. 81 | Rule C | exlimiv 1647 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1751 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1819 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3547 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3548 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3463 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3511 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3464 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3352 |
| [Mendelson] p. 231 | Definition of union | unssin 3462 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4599 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3915 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4405 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4406 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4407 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3936 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4886 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5285 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4494 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7100 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7074 xpsneng 7075 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7080 xpcomeng 7081 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7083 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7077 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6888 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 7055 mapsnend 7054 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 7106 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7105 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6922 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 7056 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7526 djucomen 7525 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7524 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6702 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3445 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4840 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4841 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4174 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5280 coi2 5281 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4972 rn0 5015 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5169 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4861 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4979 rnxpm 5194 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4832 xp0 5184 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5123 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5120 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5118 imaexg 5117 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5114 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5809 funfvop 5792 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5720 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5730 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5399 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5943 dff13f 5945 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5911 funrnex 6309 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5937 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5248 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3967 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6351 df-1st 6336 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6352 df-2nd 6337 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1496 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1553 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1555 ax-11o 1872 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1876 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1497 |
| [Monk2] p. 109 | Lemma 15 | equvin 1912 equvini 1807 eqvinop 4361 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1575 |
| [Monk2] p. 113 | Axiom C5-2 | hbn1 1700 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1497 |
| [Monk2] p. 114 | Lemma 22 | hba1 1589 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1601 nfia1 1629 |
| [Monk2] p. 114 | Lemma 24 | hba2 1600 nfa2 1628 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 839 dftest 16889 |
| [Munkres] p. 77 | Example 2 | distop 14967 |
| [Munkres] p. 78 | Definition of basis | df-bases 14925 isbasis3g 14928 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13490 tgval2 14933 |
| [Munkres] p. 79 | Remark | tgcl 14946 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14940 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14961 tgss3 14960 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14962 basgen2 14963 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 15052 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14994 topcld 14991 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14995 |
| [Munkres] p. 94 | Definition of closure | clsval 14993 |
| [Munkres] p. 94 | Definition of interior | ntrval 14992 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 15070 iscn 15079 iscn2 15082 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 15112 cncnp2m 15113 cncnpi 15110 df-cnp 15071 iscnp 15081 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15396 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7163 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7457 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7445 omniwomnimkv 7460 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3331 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7428 exmidomniim 7434 finomni 7433 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7413 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16816 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16820 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7170 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7506 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7507 exmidfodomrlemrALT 7508 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7442 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16802 peano4nninf 16801 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16804 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16812 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16814 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16800 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2221 rabid 2721 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2047 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2227 |
| [Quine] p. 19 | Definition 2.9 | df-v 2817 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2343 eqabb 2370 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2368 abid2 2357 abid2f 2412 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1938 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1936 sb6 1937 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2230 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2234 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2236 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3045 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3046 dfsbcq2 3047 |
| [Quine] p. 43 | Theorem 6.8 | vex 2818 |
| [Quine] p. 43 | Theorem 6.9 | isset 2822 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2901 spcgv 2906 spcimgf 2899 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3056 spsbcd 3057 |
| [Quine] p. 44 | Theorem 6.12 | elex 2827 |
| [Quine] p. 44 | Theorem 6.13 | elab 2963 elabg 2965 elabgf 2961 |
| [Quine] p. 44 | Theorem 6.14 | noel 3514 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3756 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3698 df-sn 3697 |
| [Quine] p. 49 | Theorem 7.4 | snss 3831 snssg 3830 |
| [Quine] p. 49 | Theorem 7.5 | prss 3852 prssg 3853 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3799 prid1g 3797 prid2 3800 prid2g 3798 snid 3722 snidg 3720 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4299 snexprc 4301 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4327 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3932 unisng 3933 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3935 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3944 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3943 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5325 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5315 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5326 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5330 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5331 |
| [Quine] p. 58 | Definition 9.1 | df-op 3700 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4376 opabidw 4377 opelopab 4392 opelopaba 4386 opelopabaf 4394 opelopabf 4395 opelopabg 4388 opelopabga 4383 opelopabgf 4390 oprabid 6084 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4757 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4759 |
| [Quine] p. 64 | Definition 9.15 | df-id 4416 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5416 |
| [Quine] p. 65 | Theorem 10.4 | funi 5386 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5406 funsng 5404 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5356 |
| [Quine] p. 65 | Definition 10.2 | args 5133 dffv4g 5669 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5362 fv2 5667 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 11090 nn0opth2d 11089 nn0opthd 11088 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5443 funimaexg 5442 |
| [Roman] p. 18 | Part Preliminaries | df-rng 14094 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14159 |
| [Rudin] p. 164 | Equation 27 | efcan 12366 |
| [Rudin] p. 164 | Equation 30 | efzval 12373 |
| [Rudin] p. 167 | Equation 48 | absefi 12459 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1471 |
| [Sanford] p. 39 | Rule 4 | mptxor 1469 |
| [Sanford] p. 40 | Rule 1 | mptnan 1468 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5149 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5151 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5148 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5146 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14161 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14965 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3488 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3582 dif0 3581 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3596 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3481 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3482 |
| [Stoll] p. 20 | Remark | invdif 3465 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3701 |
| [Stoll] p. 43 | Definition | uniiun 4047 |
| [Stoll] p. 44 | Definition | intiin 4048 |
| [Stoll] p. 45 | Definition | df-iin 3996 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3995 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 897 imanst 896 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3488 |
| [Suppes] p. 22 | Theorem 2 | eq0 3529 |
| [Suppes] p. 22 | Theorem 4 | eqss 3255 eqssd 3257 eqssi 3256 |
| [Suppes] p. 23 | Theorem 5 | ss0 3551 ss0b 3550 |
| [Suppes] p. 23 | Theorem 6 | sstr 3248 |
| [Suppes] p. 25 | Theorem 12 | elin 3404 elun 3362 |
| [Suppes] p. 26 | Theorem 15 | inidm 3432 |
| [Suppes] p. 26 | Theorem 16 | in0 3545 |
| [Suppes] p. 27 | Theorem 23 | unidm 3364 |
| [Suppes] p. 27 | Theorem 24 | un0 3544 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3384 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3391 |
| [Suppes] p. 27 | Theorem 27 | unss 3395 |
| [Suppes] p. 27 | Theorem 28 | indir 3472 |
| [Suppes] p. 27 | Theorem 29 | undir 3473 |
| [Suppes] p. 28 | Theorem 32 | difid 3579 difidALT 3580 |
| [Suppes] p. 29 | Theorem 33 | difin 3460 |
| [Suppes] p. 29 | Theorem 34 | indif 3466 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3586 |
| [Suppes] p. 29 | Theorem 36 | difun2 3591 |
| [Suppes] p. 29 | Theorem 37 | difin0 3585 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3583 |
| [Suppes] p. 29 | Theorem 39 | difundi 3475 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3477 |
| [Suppes] p. 30 | Theorem 41 | nalset 4242 |
| [Suppes] p. 39 | Theorem 61 | uniss 3937 |
| [Suppes] p. 39 | Theorem 65 | uniop 4374 |
| [Suppes] p. 41 | Theorem 70 | intsn 3986 |
| [Suppes] p. 42 | Theorem 71 | intpr 3983 intprg 3984 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4601 op1stbg 4602 |
| [Suppes] p. 42 | Theorem 78 | intun 3982 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4027 dfiun2g 4025 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4028 |
| [Suppes] p. 47 | Theorem 86 | elpw 3677 elpw2 4271 elpw2g 4270 elpwg 3679 |
| [Suppes] p. 47 | Theorem 87 | pwid 3689 |
| [Suppes] p. 47 | Theorem 89 | pw0 3843 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3911 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4859 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4892 xpindir 4893 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4808 xpundir 4809 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4672 |
| [Suppes] p. 58 | Theorem 2 | relss 4839 |
| [Suppes] p. 59 | Theorem 4 | eldm 4955 eldm2 4956 eldm2g 4954 eldmg 4953 |
| [Suppes] p. 59 | Definition 3 | df-dm 4761 |
| [Suppes] p. 60 | Theorem 6 | dmin 4966 |
| [Suppes] p. 60 | Theorem 8 | rnun 5173 |
| [Suppes] p. 60 | Theorem 9 | rnin 5174 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4945 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4940 brcnvg 4938 |
| [Suppes] p. 62 | Equation 5 | elcnv 4934 elcnv2 4935 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5142 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5172 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5170 |
| [Suppes] p. 63 | Theorem 20 | co02 5278 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5029 |
| [Suppes] p. 63 | Definition 7 | df-co 4760 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4942 |
| [Suppes] p. 64 | Theorem 27 | coass 5283 |
| [Suppes] p. 65 | Theorem 31 | resundi 5053 |
| [Suppes] p. 65 | Theorem 34 | elima 5108 elima2 5109 elima3 5110 elimag 5107 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5177 |
| [Suppes] p. 66 | Theorem 40 | dminss 5179 |
| [Suppes] p. 66 | Theorem 41 | imainss 5180 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5183 |
| [Suppes] p. 81 | Definition 34 | dfec2 6772 |
| [Suppes] p. 82 | Theorem 72 | elec 6810 elecg 6809 |
| [Suppes] p. 82 | Theorem 73 | erth 6815 erth2 6816 |
| [Suppes] p. 89 | Theorem 96 | map0b 6923 |
| [Suppes] p. 89 | Theorem 97 | map0 6926 map0g 6924 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6927 mapsnd 6925 |
| [Suppes] p. 89 | Theorem 99 | mapss 6928 |
| [Suppes] p. 92 | Theorem 1 | enref 7006 enrefg 7005 |
| [Suppes] p. 92 | Theorem 2 | ensym 7023 ensymb 7022 ensymi 7024 |
| [Suppes] p. 92 | Theorem 3 | entr 7026 |
| [Suppes] p. 92 | Theorem 4 | unen 7060 |
| [Suppes] p. 94 | Theorem 15 | endom 7004 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 7020 |
| [Suppes] p. 94 | Theorem 17 | domtr 7027 |
| [Suppes] p. 95 | Theorem 18 | isbth 7239 |
| [Suppes] p. 98 | Exercise 4 | fundmen 7049 fundmeng 7050 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7087 |
| [Suppes] p. 130 | Definition 3 | df-tr 4211 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4612 |
| [Suppes] p. 134 | Definition 6 | df-suc 4494 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4727 finds 4724 finds1 4726 finds2 4725 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7670 df-ltpq 7663 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4513 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2216 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2227 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2230 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2229 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2252 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6056 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3043 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3712 elpr2 3713 elprg 3711 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3707 elsn2 3725 elsn2g 3724 elsng 3706 velsn 3708 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4349 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3702 sneqr 3866 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3710 dfsn2 3705 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4560 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4355 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4333 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4564 unexg 4566 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3740 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3917 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3219 df-un 3217 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3930 uniprg 3931 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4294 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3739 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4529 elsucg 4527 sstr2 3247 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3365 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3413 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3378 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3433 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3470 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3471 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3228 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3673 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3392 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3226 dfss2 3230 sseqin2 3442 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3260 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3443 inss2 3444 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3300 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3925 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4334 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4341 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2531 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4239 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3215 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3512 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3579 difidALT 3580 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3523 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4663 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2817 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4244 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3549 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4249 ssexg 4251 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4246 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4674 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4665 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3575 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3346 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3484 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3347 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3355 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2527 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2528 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4868 xpexg 4866 xpexgALT 6328 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4758 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5422 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5586 fun11 5425 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5365 svrelfun 5423 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4944 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4946 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4763 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4764 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4760 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5219 dfrel2 5215 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4860 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4871 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4877 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4891 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5068 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5045 opelresg 5047 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5061 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5064 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5069 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5395 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5263 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5394 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5587 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2127 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5362 fv3 5695 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5303 cnvexg 5302 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5026 dmexg 5023 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5027 rnexg 5024 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnvm 5119 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5689 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5699 tz6.12 5700 tz6.12c 5702 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5663 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5357 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5358 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5360 wfo 5352 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5359 wf1 5351 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5361 wf1o 5353 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5777 eqfnfv2 5778 eqfnfv2f 5781 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5749 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5908 fnexALT 6306 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5907 resfunexgALT 6303 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5443 funimaexg 5442 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4112 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5134 iniseg 5136 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4412 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5363 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5985 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5986 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5991 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5993 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 6001 |
| [TakeutiZaring] p. 35 | Notation | wtr 4210 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4477 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4214 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4700 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4504 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4508 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4616 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4491 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4610 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4676 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4706 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4212 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4635 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4611 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3944 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4494 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4538 sucidg 4539 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4625 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4492 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4630 ordelsuc 4629 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4718 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4719 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4720 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4717 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4731 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4723 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4721 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4722 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3965 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4226 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3966 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4641 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3952 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6541 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6598 tfri1d 6568 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6599 tfri2d 6569 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6600 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6535 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6519 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6699 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6695 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6692 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6696 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6744 nnaordi 6743 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4038 uniss2 3947 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6705 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6715 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6706 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6693 omsuc 6707 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6716 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6752 nnmordi 6751 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6694 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7485 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 7037 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7113 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7114 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6980 isfi 7002 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7084 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6886 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7090 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7103 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1559 |
| [Tarski] p. 68 | Lemma 6 | equid 1749 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1752 |
| [Tarski] p. 70 | Lemma 14 | spim 1787 spime 1790 spimeh 1788 spimh 1786 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1555 ax-11o 1872 ax11i 1762 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1937 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1575 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2207 ax-14 2208 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 719 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 735 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 764 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 773 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 797 |
| [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 845 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2181 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 745 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 844 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 634 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 893 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 851 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 864 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 647 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 861 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 863 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 720 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 783 |
| [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 901 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 915 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 776 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 777 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 812 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 813 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 811 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1006 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 786 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 784 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 785 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 746 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 875 pm2.5gdc 874 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 870 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 749 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 750 |
| [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 730 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 899 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 733 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 734 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 756 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 808 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 809 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 665 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 721 pm2.67 751 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 877 pm2.521gdc 876 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 755 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 818 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 902 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 923 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 819 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 820 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 913 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 762 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 966 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 967 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 968 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 761 |
| [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 701 |
| [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 868 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 867 |
| [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 696 |
| [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 763 pm3.44 723 |
| [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 793 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 879 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 880 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 898 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 702 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 961 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 765 pm4.25 766 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 826 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 736 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 775 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 800 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 609 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 830 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1007 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 824 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 980 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 958 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 787 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 822 pm4.45 792 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1530 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 965 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 905 imorr 729 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 758 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 759 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 910 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 947 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 760 pm4.56 788 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 948 oranim 789 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 693 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 894 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 908 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 694 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 909 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 895 |
| [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 835 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 752 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 607 pm4.76 608 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 718 pm4.77 807 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 790 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 911 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 715 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 916 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 959 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 960 |
| [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 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 918 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 920 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 919 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1434 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 836 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 912 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1439 pm5.18dc 891 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 714 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 703 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1437 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1442 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1443 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 903 |
| [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 934 pm5.6r 935 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 963 |
| [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 925 |
| [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 933 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 810 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 926 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 921 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 802 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 954 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 955 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 970 |
| [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 971 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1684 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1534 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1681 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1947 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2085 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2495 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2496 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2957 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3101 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5334 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5335 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2162 eupickbi 2165 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5362 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7489 |
| [vandenDries] p. 43 | Theorem 62 | pellexlem1 15862 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |