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 7405 fidcenum 7225 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7225 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7405 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13165 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7191 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7177 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13180 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13182 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13171 znnen 13138 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13183 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13184 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11134 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4658 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11272 df-pfx 11358 df-substr 11331 df-word 11218 lencl 11221 wrd0 11242 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8449 addcan2d 8454 addcan2i 8452 addcand 8453 addcani 8451 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8460 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8517 negsubd 8586 negsubi 8547 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8519 negnegd 8571 negnegi 8539 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8654 subdid 8683 subdii 8676 subdir 8655 subdird 8684 subdiri 8677 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8658 mul01d 8662 mul01i 8660 mul02 8656 mul02d 8661 mul02i 8659 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 9063 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 9014 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8667 mul2negd 8682 mul2negi 8675 mulneg1 8664 mulneg1d 8680 mulneg1i 8673 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14278 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8983 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 10006 rpaddcld 10041 rpmulcl 10007 rpmulcld 10042 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 10018 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8374 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8808 ltadd1dd 8826 ltadd1i 8772 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8862 ltmul1a 8861 ltmul1i 9190 ltmul1ii 9198 ltmul2 9126 ltmul2d 10068 ltmul2dd 10082 ltmul2i 9193 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8396 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8738 lt0neg1d 8785 ltneg 8732 ltnegd 8793 ltnegi 8763 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8715 lt2addd 8837 lt2addi 8780 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9983 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9120 recgt0d 9204 recgt0i 9176 recgt0ii 9177 |
| [Apostol] p. 22 | Definition of integers | df-z 9574 |
| [Apostol] p. 22 | Definition of rationals | df-q 9948 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7284 |
| [Apostol] p. 26 | Theorem I.29 | arch 9489 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9693 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9490 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10612 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12550 zneo 9675 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11709 sqrtthi 11797 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9236 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12725 |
| [Apostol] p. 363 | Remark | absgt0api 11824 |
| [Apostol] p. 363 | Example | abssubd 11871 abssubi 11828 |
| [ApostolNT] p. 14 | Definition | df-dvds 12467 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12483 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12507 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12503 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12497 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12499 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12484 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12485 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12490 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12524 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12526 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12528 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12703 |
| [ApostolNT] p. 16 | Definition | isprm2 12807 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12782 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13195 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12662 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12704 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12706 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12676 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12669 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12834 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12836 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 13059 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12603 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12749 |
| [ApostolNT] p. 25 | Definition | df-phi 12901 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12931 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12912 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12916 |
| [ApostolNT] p. 38 | Remark | df-sgm 15837 |
| [ApostolNT] p. 38 | Definition | df-sgm 15837 |
| [ApostolNT] p. 104 | Definition | congr 12790 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12470 |
| [ApostolNT] p. 106 | Definition | moddvds 12478 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12557 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12558 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10699 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10736 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 11024 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12502 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12793 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13112 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12795 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12923 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12942 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12924 |
| [ApostolNT] p. 179 | Definition | df-lgs 15858 lgsprme0 15902 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15903 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15879 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15894 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15945 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15964 2lgsoddprm 15973 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15929 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15940 |
| [ApostolNT] p. 188 | Definition | df-lgs 15858 lgs1 15904 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15895 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15897 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15905 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15906 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 621 pm2.65 665 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6048 onsucelsucexmidlem 4650 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16758 |
| [Bauer], p. 483 | Definition | n0rf 3520 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15828 2irrexpqap 15830 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7198 ssfiexmid 7130 ssfiexmidt 7132 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15505 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15495 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8915 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7405 |
| [BauerSwan], p. 14 | Remark | 0ct 7397 ctm 7399 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16761 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7812 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7725 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7814 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7848 addlocpr 7847 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7874 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7877 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7882 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2083 |
| [BellMachover] p. 460 | Notation | df-mo 2084 |
| [BellMachover] p. 460 | Definition | mo3 2135 mo3h 2134 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2217 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4230 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4289 |
| [BellMachover] p. 466 | Axiom Union | axun2 4555 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4663 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4504 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4666 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4617 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4489 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4710 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4735 |
| [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 16040 isuhgropm 16063 isusgropen 16147 isuspgropen 16146 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16236 uhgrspansubgr 16259 |
| [Bollobas] p. 4 | Definition | df-wlks 16300 |
| [Bollobas] p. 5 | Definition | df-trls 16363 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 16052 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13558 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13604 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13619 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14131 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 14066 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5955 fcofo 5956 |
| [BourbakiTop1] p. | Remark | xnegmnf 10158 xnegpnf 10157 |
| [BourbakiTop1] p. | Remark | rexneg 10159 |
| [BourbakiTop1] p. | Proposition | ishmeo 15156 |
| [BourbakiTop1] p. | Property V_i | ssnei2 15009 |
| [BourbakiTop1] p. | Property V_ii | innei 15015 |
| [BourbakiTop1] p. | Property V_iv | neissex 15017 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 15006 neiss 15002 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 15074 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15151 |
| [BourbakiTop1] p. | Property V_iii | elnei 15004 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14850 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13558 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13604 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13801 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4172 |
| [Church] p. 129 | Section II.24 | df-ifp 987 dfifp2dc 990 |
| [Cohen] p. 301 | Remark | relogoprlem 15720 |
| [Cohen] p. 301 | Property 2 | relogmul 15721 relogmuld 15736 |
| [Cohen] p. 301 | Property 3 | relogdiv 15722 relogdivd 15737 |
| [Cohen] p. 301 | Property 4 | relogexp 15724 |
| [Cohen] p. 301 | Property 1a | log1 15718 |
| [Cohen] p. 301 | Property 1b | loge 15719 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15817 |
| [Cohen4] p. 352 | Definition | rpelogb 15801 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15807 |
| [Cohen4] p. 361 | Property 3 | logbrec 15812 rprelogbdiv 15809 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15805 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15810 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15799 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15800 |
| [Cohen4] p. 367 | Property | rplogbchbase 15802 |
| [Cohen4] p. 377 | Property 2 | logblt 15814 |
| [Crosilla] p. | Axiom 1 | ax-ext 2214 |
| [Crosilla] p. | Axiom 2 | ax-pr 4321 |
| [Crosilla] p. | Axiom 3 | ax-un 4553 |
| [Crosilla] p. | Axiom 4 | ax-nul 4235 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4709 |
| [Crosilla] p. | Axiom 6 | ru 3040 |
| [Crosilla] p. | Axiom 8 | ax-pow 4286 |
| [Crosilla] p. | Axiom 9 | ax-setind 4658 |
| [Crosilla], p. | Axiom 6 | ax-sep 4227 |
| [Crosilla], p. | Axiom 7 | ax-coll 4224 |
| [Crosilla], p. | Axiom 7' | repizf 4225 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4642 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6048 |
| [Crosilla], p. | Definition of ordinal | df-iord 4486 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4656 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16236 uhgrspansubgr 16259 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 16052 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3212 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4712 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6883 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4234 |
| [Enderton] p. 19 | Definition | df-tp 3696 |
| [Enderton] p. 26 | Exercise 5 | unissb 3943 |
| [Enderton] p. 26 | Exercise 10 | pwel 4333 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4406 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4060 iinin2m 4059 iunin1 4055 iunin2 4054 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4058 iundif2ss 4056 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4073 |
| [Enderton] p. 33 | Exercise 25 | iununir 4074 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4081 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4600 iunpwss 4082 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4332 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4304 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4570 rnex 5024 rnexg 5021 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4965 rnuni 5173 |
| [Enderton] p. 42 | Definition of a function | dffun7 5378 dffun8 5379 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5740 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5416 |
| [Enderton] p. 44 | Definition (d) | dfima2 5102 dfima3 5103 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5745 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7512 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5933 |
| [Enderton] p. 52 | Definition | df-map 6883 |
| [Enderton] p. 53 | Exercise 21 | coass 5280 |
| [Enderton] p. 53 | Exercise 27 | dmco 5270 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5426 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5137 |
| [Enderton] p. 54 | Remark | ixpf 6954 ixpssmap 6966 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6933 |
| [Enderton] p. 56 | Theorem 3M | erref 6786 |
| [Enderton] p. 57 | Lemma 3N | erthi 6814 |
| [Enderton] p. 57 | Definition | df-ec 6768 |
| [Enderton] p. 58 | Definition | df-qs 6772 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6873 th3qcor 6872 th3qlem1 6870 th3qlem2 6871 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6768 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4962 |
| [Enderton] p. 68 | Definition of successor | df-suc 4491 |
| [Enderton] p. 71 | Definition | df-tr 4208 dftr4 4212 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4533 unisucg 4534 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4533 unisucg 4534 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4221 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4222 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6706 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6708 onasuc 6698 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6052 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6707 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6709 onmsuc 6705 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6717 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6710 nnacom 6716 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6718 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6719 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6721 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6711 nnmsucr 6720 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6760 |
| [Enderton] p. 129 | Definition | df-en 6975 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6000 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13135 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7119 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7110 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7098 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7524 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7520 dju1en 7519 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3584 |
| [Enderton] p. 145 | Figure 38 | ffoss 5646 |
| [Enderton] p. 145 | Definition | df-dom 6976 |
| [Enderton] p. 146 | Example 1 | domen 6987 domeng 6988 |
| [Enderton] p. 146 | Example 3 | nndomo 7117 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7085 xpdom1g 7083 xpdom2g 7082 |
| [Enderton] p. 168 | Definition | df-po 4416 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4548 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4509 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4664 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4512 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4637 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4610 |
| [Enderton] p. 194 | Remark | onprc 4673 |
| [Enderton] p. 194 | Exercise 16 | suc11 4679 |
| [Enderton] p. 197 | Definition | df-card 7474 |
| [Enderton] p. 200 | Exercise 25 | tfis 4704 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4675 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4677 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4678 |
| [Geuvers], p. 1 | Remark | expap0 10927 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8885 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8924 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8886 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8242 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11881 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11889 maxle2 11890 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11891 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11894 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11895 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8852 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7658 enqer 7669 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7662 df-nqqs 7659 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7655 df-plqqs 7660 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7656 df-mqqs 7661 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7663 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7719 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7722 ltbtwnnq 7727 ltbtwnnqq 7726 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7711 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7712 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7848 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7890 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7889 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7908 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7924 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7930 ltaprlem 7929 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7927 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7883 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7903 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7892 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7891 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7899 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7949 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 8037 enrer 8046 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 8042 df-1r 8043 df-nr 8038 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 8040 df-plr 8039 negexsr 8083 recexsrlem 8085 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 8041 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9230 creur 9229 cru 8872 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8234 axcnre 8192 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11536 crimd 11655 crimi 11615 crre 11535 crred 11654 crrei 11614 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11538 remimd 11620 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11735 absval2d 11863 absval2i 11822 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11562 cjaddd 11643 cjaddi 11610 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11563 cjmuld 11644 cjmuli 11611 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11561 cjcjd 11621 cjcji 11593 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11560 cjreb 11544 cjrebd 11624 cjrebi 11596 cjred 11649 rere 11543 rereb 11541 rerebd 11623 rerebi 11595 rered 11647 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11569 addcjd 11635 addcji 11605 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11679 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11730 abscjd 11868 abscji 11826 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11742 abs00d 11864 abs00i 11823 absne0d 11865 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11774 releabsd 11869 releabsi 11827 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11747 absmuld 11872 absmuli 11829 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11733 sqabsaddi 11830 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11782 abstrid 11874 abstrii 11833 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10897 exp0 10901 expp1 10904 expp1d 11032 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10939 expaddd 11033 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15764 cxpmuld 15789 expmul 10942 expmuld 11034 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10936 mulexpd 11046 rpmulcxp 15761 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10340 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 12004 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 12006 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 12005 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 12009 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 12002 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11998 climcj 11999 climim 12001 climre 12000 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8309 df-xr 8308 ltxr 10104 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 12025 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10656 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14680 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15216 xmet0 15215 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15223 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15225 mstri 15325 xmettri 15224 xmstri 15324 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15131 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15363 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11988 addcncntop 15414 mulcn2 11990 mulcncntop 15416 subcn2 11989 subcncntop 15415 |
| [Gleason] p. 295 | Remark | bcval3 11109 bcval4 11110 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11124 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11107 df-bc 11106 |
| [Gleason] p. 296 | Remark | bcn0 11113 bcnn 11115 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12163 |
| [Gleason] p. 308 | Equation 2 | ef0 12351 |
| [Gleason] p. 308 | Equation 3 | efcj 12352 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12357 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12361 |
| [Gleason] p. 310 | Equation 14 | sinadd 12415 |
| [Gleason] p. 310 | Equation 15 | cosadd 12416 |
| [Gleason] p. 311 | Equation 17 | sincossq 12427 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12432 sinbnd 12431 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12332 |
| [Golan] p. 1 | Remark | srgisid 14119 |
| [Golan] p. 1 | Definition | df-srg 14097 |
| [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 13713 mndideu 13628 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13740 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13769 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13780 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13802 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16856 |
| [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 7531 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6731 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16840 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8927 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7781 df-imp 7780 df-iplp 7779 df-reap 8845 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8941 rerecapb 9113 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6330 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7973 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16476 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16833 dceqnconst 16832 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8211 caucvgpr 7993 caucvgprpr 8023 caucvgsr 8113 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7777 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16838 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4417 ltpopr 7906 ltsopr 7907 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8876 reapcotr 8868 reapirr 8847 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8396 gt0add 8843 leadd1 8700 lelttr 8358 lemul1a 9128 lenlt 8345 ltadd1 8699 ltletr 8359 ltmul1 8862 reaplt 8858 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16409 |
| [Jech] p. 4 | Definition of class | cv 1397 cvjust 2227 |
| [Jech] p. 78 | Note | opthprc 4800 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1579 |
| [Kreyszig] p. 3 | Property M1 | metcl 15205 xmetcl 15204 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15212 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8938 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15294 |
| [Kreyszig] p. 19 | Remark | mopntopon 15295 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15340 mopnm 15300 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15338 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15343 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15365 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 15065 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14465 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14456 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14457 |
| [Kunen] p. 10 | Axiom 0 | a9e 1744 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4226 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6893 mapvalg 6891 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6887 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4000 |
| [Lang] p. 3 | Statement | lidrideqd 13583 mndbn0 13633 |
| [Lang] p. 3 | Definition | df-mnd 13619 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13600 |
| [Lang] p. 5 | Equation | gsumfzreidx 14043 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13834 |
| [Lang] p. 7 | Definition | dfgrp2e 13730 |
| [Levy] p. 338 | Axiom | df-clab 2219 df-clel 2228 df-cleq 2225 |
| [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 3595 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1603 19.3h 1602 rr19.3v 2955 |
| [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 2649 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1695 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1517 ralbi 2675 |
| [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 2676 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1714 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1506 alimd 1570 alimdh 1516 alimdv 1928 ralimdaa 2608 ralimdv 2610 ralimdva 2609 ralimdvva 2611 sbcimdv 3107 |
| [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 2618 r19.21be 2633 r19.21bi 2630 r19.21t 2617 r19.21v 2619 ralrimd 2620 ralrimdv 2621 ralrimdva 2622 ralrimdvv 2626 ralrimdvva 2627 ralrimi 2613 ralrimiv 2614 ralrimiva 2615 ralrimivv 2623 ralrimivva 2624 ralrimivvva 2625 ralrimivw 2616 rexlimi 2653 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1930 2eximdv 1931 exim 1648 eximd 1661 eximdh 1660 eximdv 1929 rexim 2636 reximdai 2640 reximddv 2645 reximddv2 2647 reximdv 2643 reximdv2 2641 reximdva 2644 reximdvai 2642 reximi2 2638 |
| [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 1947 exlimi 1643 exlimih 1642 exlimiv 1647 exlimivv 1946 r19.23 2651 r19.23v 2652 rexlimd 2657 rexlimdv 2659 rexlimdv3a 2662 rexlimdva 2660 rexlimdva2 2663 rexlimdvaa 2661 rexlimdvv 2667 rexlimdvva 2668 rexlimdvw 2664 rexlimiv 2654 rexlimiva 2655 rexlimivv 2666 |
| [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 2672 r19.26-3 2673 r19.26 2669 r19.26m 2674 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1610 19.27h 1609 19.27v 1949 r19.27av 2678 r19.27m 3604 r19.27mv 3605 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1612 19.28h 1611 19.28v 1950 r19.28av 2679 r19.28m 3598 r19.28mv 3601 rr19.28v 2956 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1669 19.29r 1670 19.29r2 1671 19.29x 1672 r19.29 2680 r19.29d2r 2687 r19.29r 2681 |
| [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 2689 r19.32vdc 2692 r19.32vr 2691 |
| [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 1951 19.36i 1720 r19.36av 2694 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1722 19.37aiv 1723 r19.37 2695 r19.37av 2696 |
| [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 2697 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1734 19.41h 1733 19.41v 1952 19.41vv 1953 19.41vvv 1954 19.41vvvv 1955 r19.41 2698 r19.41v 2699 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1736 19.42h 1735 19.42v 1956 19.42vv 1961 19.42vvv 1962 19.42vvvv 1963 r19.42v 2700 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1677 r19.43 2701 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1730 r19.44av 2702 r19.44mv 3603 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1731 r19.45av 2703 r19.45mv 3602 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2105 |
| [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 2205 |
| [Megill] p. 448 | Scheme C13' | ax-14 2206 |
| [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 2041 sbequ 1889 sbid2v 2050 |
| [Megill] p. 450 | Example in Appendix | hba1 1589 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3125 rspsbca 3126 stdpc4 1824 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3131 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 3544 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3545 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3460 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3508 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3461 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3349 |
| [Mendelson] p. 231 | Definition of union | unssin 3459 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4596 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3912 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4402 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4403 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4404 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3933 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4883 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5282 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4491 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7097 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7071 xpsneng 7072 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7077 xpcomeng 7078 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7080 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7074 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6885 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 7052 mapsnend 7051 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 7103 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7102 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6919 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 7053 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7523 djucomen 7522 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7521 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6699 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3442 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4837 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4838 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4171 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5277 coi2 5278 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4969 rn0 5012 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5166 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4858 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4976 rnxpm 5191 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4829 xp0 5181 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5120 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5117 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5115 imaexg 5114 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5111 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5806 funfvop 5789 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5717 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5727 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5396 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5940 dff13f 5942 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5908 funrnex 6306 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5934 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5245 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3964 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6348 df-1st 6333 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6349 df-2nd 6334 |
| [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 4358 |
| [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 16857 |
| [Munkres] p. 77 | Example 2 | distop 14937 |
| [Munkres] p. 78 | Definition of basis | df-bases 14895 isbasis3g 14898 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13462 tgval2 14903 |
| [Munkres] p. 79 | Remark | tgcl 14916 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14910 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14931 tgss3 14930 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14932 basgen2 14933 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 15022 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14964 topcld 14961 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14965 |
| [Munkres] p. 94 | Definition of closure | clsval 14963 |
| [Munkres] p. 94 | Definition of interior | ntrval 14962 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 15040 iscn 15049 iscn2 15052 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 15082 cncnp2m 15083 cncnpi 15080 df-cnp 15041 iscnp 15051 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15366 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7160 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7454 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7442 omniwomnimkv 7457 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3328 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7425 exmidomniim 7431 finomni 7430 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7410 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16786 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16790 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7167 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7503 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7504 exmidfodomrlemrALT 7505 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7439 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16772 peano4nninf 16771 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16774 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16782 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16784 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16770 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2219 rabid 2719 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2045 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2225 |
| [Quine] p. 19 | Definition 2.9 | df-v 2814 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2341 eqabb 2368 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2366 abid2 2355 abid2f 2410 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1937 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1935 sb6 1936 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2228 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2232 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2234 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3042 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3043 dfsbcq2 3044 |
| [Quine] p. 43 | Theorem 6.8 | vex 2815 |
| [Quine] p. 43 | Theorem 6.9 | isset 2819 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2898 spcgv 2903 spcimgf 2896 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3053 spsbcd 3054 |
| [Quine] p. 44 | Theorem 6.12 | elex 2824 |
| [Quine] p. 44 | Theorem 6.13 | elab 2960 elabg 2962 elabgf 2958 |
| [Quine] p. 44 | Theorem 6.14 | noel 3511 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3753 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3695 df-sn 3694 |
| [Quine] p. 49 | Theorem 7.4 | snss 3828 snssg 3827 |
| [Quine] p. 49 | Theorem 7.5 | prss 3849 prssg 3850 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3796 prid1g 3794 prid2 3797 prid2g 3795 snid 3719 snidg 3717 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4296 snexprc 4298 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4324 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3929 unisng 3930 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3932 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3941 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3940 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5322 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5312 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5323 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5327 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5328 |
| [Quine] p. 58 | Definition 9.1 | df-op 3697 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4373 opabidw 4374 opelopab 4389 opelopaba 4383 opelopabaf 4391 opelopabf 4392 opelopabg 4385 opelopabga 4380 opelopabgf 4387 oprabid 6081 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4754 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4756 |
| [Quine] p. 64 | Definition 9.15 | df-id 4413 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5413 |
| [Quine] p. 65 | Theorem 10.4 | funi 5383 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5403 funsng 5401 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5353 |
| [Quine] p. 65 | Definition 10.2 | args 5130 dffv4g 5666 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5359 fv2 5664 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 11082 nn0opth2d 11081 nn0opthd 11080 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5440 funimaexg 5439 |
| [Roman] p. 18 | Part Preliminaries | df-rng 14066 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14131 |
| [Rudin] p. 164 | Equation 27 | efcan 12355 |
| [Rudin] p. 164 | Equation 30 | efzval 12362 |
| [Rudin] p. 167 | Equation 48 | absefi 12448 |
| [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 5146 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5148 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5145 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5143 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14133 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14935 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3485 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3579 dif0 3578 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3593 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3478 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3479 |
| [Stoll] p. 20 | Remark | invdif 3462 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3698 |
| [Stoll] p. 43 | Definition | uniiun 4044 |
| [Stoll] p. 44 | Definition | intiin 4045 |
| [Stoll] p. 45 | Definition | df-iin 3993 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3992 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 897 imanst 896 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3485 |
| [Suppes] p. 22 | Theorem 2 | eq0 3526 |
| [Suppes] p. 22 | Theorem 4 | eqss 3252 eqssd 3254 eqssi 3253 |
| [Suppes] p. 23 | Theorem 5 | ss0 3548 ss0b 3547 |
| [Suppes] p. 23 | Theorem 6 | sstr 3245 |
| [Suppes] p. 25 | Theorem 12 | elin 3401 elun 3359 |
| [Suppes] p. 26 | Theorem 15 | inidm 3429 |
| [Suppes] p. 26 | Theorem 16 | in0 3542 |
| [Suppes] p. 27 | Theorem 23 | unidm 3361 |
| [Suppes] p. 27 | Theorem 24 | un0 3541 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3381 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3388 |
| [Suppes] p. 27 | Theorem 27 | unss 3392 |
| [Suppes] p. 27 | Theorem 28 | indir 3469 |
| [Suppes] p. 27 | Theorem 29 | undir 3470 |
| [Suppes] p. 28 | Theorem 32 | difid 3576 difidALT 3577 |
| [Suppes] p. 29 | Theorem 33 | difin 3457 |
| [Suppes] p. 29 | Theorem 34 | indif 3463 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3583 |
| [Suppes] p. 29 | Theorem 36 | difun2 3588 |
| [Suppes] p. 29 | Theorem 37 | difin0 3582 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3580 |
| [Suppes] p. 29 | Theorem 39 | difundi 3472 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3474 |
| [Suppes] p. 30 | Theorem 41 | nalset 4239 |
| [Suppes] p. 39 | Theorem 61 | uniss 3934 |
| [Suppes] p. 39 | Theorem 65 | uniop 4371 |
| [Suppes] p. 41 | Theorem 70 | intsn 3983 |
| [Suppes] p. 42 | Theorem 71 | intpr 3980 intprg 3981 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4598 op1stbg 4599 |
| [Suppes] p. 42 | Theorem 78 | intun 3979 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4024 dfiun2g 4022 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4025 |
| [Suppes] p. 47 | Theorem 86 | elpw 3674 elpw2 4268 elpw2g 4267 elpwg 3676 |
| [Suppes] p. 47 | Theorem 87 | pwid 3686 |
| [Suppes] p. 47 | Theorem 89 | pw0 3840 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3908 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4856 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4889 xpindir 4890 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4805 xpundir 4806 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4669 |
| [Suppes] p. 58 | Theorem 2 | relss 4836 |
| [Suppes] p. 59 | Theorem 4 | eldm 4952 eldm2 4953 eldm2g 4951 eldmg 4950 |
| [Suppes] p. 59 | Definition 3 | df-dm 4758 |
| [Suppes] p. 60 | Theorem 6 | dmin 4963 |
| [Suppes] p. 60 | Theorem 8 | rnun 5170 |
| [Suppes] p. 60 | Theorem 9 | rnin 5171 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4942 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4937 brcnvg 4935 |
| [Suppes] p. 62 | Equation 5 | elcnv 4931 elcnv2 4932 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5139 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5169 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5167 |
| [Suppes] p. 63 | Theorem 20 | co02 5275 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5026 |
| [Suppes] p. 63 | Definition 7 | df-co 4757 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4939 |
| [Suppes] p. 64 | Theorem 27 | coass 5280 |
| [Suppes] p. 65 | Theorem 31 | resundi 5050 |
| [Suppes] p. 65 | Theorem 34 | elima 5105 elima2 5106 elima3 5107 elimag 5104 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5174 |
| [Suppes] p. 66 | Theorem 40 | dminss 5176 |
| [Suppes] p. 66 | Theorem 41 | imainss 5177 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5180 |
| [Suppes] p. 81 | Definition 34 | dfec2 6769 |
| [Suppes] p. 82 | Theorem 72 | elec 6807 elecg 6806 |
| [Suppes] p. 82 | Theorem 73 | erth 6812 erth2 6813 |
| [Suppes] p. 89 | Theorem 96 | map0b 6920 |
| [Suppes] p. 89 | Theorem 97 | map0 6923 map0g 6921 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6924 mapsnd 6922 |
| [Suppes] p. 89 | Theorem 99 | mapss 6925 |
| [Suppes] p. 92 | Theorem 1 | enref 7003 enrefg 7002 |
| [Suppes] p. 92 | Theorem 2 | ensym 7020 ensymb 7019 ensymi 7021 |
| [Suppes] p. 92 | Theorem 3 | entr 7023 |
| [Suppes] p. 92 | Theorem 4 | unen 7057 |
| [Suppes] p. 94 | Theorem 15 | endom 7001 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 7017 |
| [Suppes] p. 94 | Theorem 17 | domtr 7024 |
| [Suppes] p. 95 | Theorem 18 | isbth 7236 |
| [Suppes] p. 98 | Exercise 4 | fundmen 7046 fundmeng 7047 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7084 |
| [Suppes] p. 130 | Definition 3 | df-tr 4208 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4609 |
| [Suppes] p. 134 | Definition 6 | df-suc 4491 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4724 finds 4721 finds1 4723 finds2 4722 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7664 df-ltpq 7657 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4510 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2214 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2225 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2228 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2227 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2250 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6053 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3040 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3709 elpr2 3710 elprg 3708 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3704 elsn2 3722 elsn2g 3721 elsng 3703 velsn 3705 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4346 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3699 sneqr 3863 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3707 dfsn2 3702 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4557 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4352 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4330 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4561 unexg 4563 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3737 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3914 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3216 df-un 3214 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3927 uniprg 3928 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4291 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3736 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4526 elsucg 4524 sstr2 3244 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3362 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3410 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3375 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3430 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3467 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3468 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3225 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3670 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3389 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3223 dfss2 3227 sseqin2 3439 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3257 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3440 inss2 3441 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3297 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3922 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4331 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4338 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2529 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4236 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3212 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3509 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3576 difidALT 3577 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3520 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4660 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2814 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4241 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3546 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4246 ssexg 4248 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4243 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4671 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4662 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3572 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3343 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3481 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3344 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3352 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2525 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2526 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4865 xpexg 4863 xpexgALT 6325 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4755 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5419 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5583 fun11 5422 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5362 svrelfun 5420 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4941 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4943 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4760 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4761 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4757 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5216 dfrel2 5212 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4857 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4868 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4874 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4888 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5065 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5042 opelresg 5044 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5058 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5061 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5066 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5392 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5260 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5391 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5584 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2125 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5359 fv3 5692 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5300 cnvexg 5299 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5023 dmexg 5020 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5024 rnexg 5021 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnvm 5116 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5686 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5696 tz6.12 5697 tz6.12c 5699 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5660 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5354 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5355 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5357 wfo 5349 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5356 wf1 5348 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5358 wf1o 5350 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5774 eqfnfv2 5775 eqfnfv2f 5778 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5746 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5905 fnexALT 6303 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5904 resfunexgALT 6300 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5440 funimaexg 5439 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4109 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5131 iniseg 5133 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4409 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5360 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5982 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5983 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5988 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5990 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5998 |
| [TakeutiZaring] p. 35 | Notation | wtr 4207 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4474 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4211 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4697 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4501 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4505 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4613 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4488 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4607 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4673 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4703 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4209 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4632 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4608 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3941 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4491 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4535 sucidg 4536 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4622 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4489 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4627 ordelsuc 4626 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4715 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4716 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4717 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4714 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4728 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4720 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4718 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4719 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3962 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4223 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3963 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4638 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3949 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6538 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6595 tfri1d 6565 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6596 tfri2d 6566 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6597 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6532 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6516 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6696 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6692 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6689 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6693 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6741 nnaordi 6740 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4035 uniss2 3944 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6702 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6712 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6703 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6690 omsuc 6704 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6713 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6749 nnmordi 6748 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6691 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7482 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 7034 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7110 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7111 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6977 isfi 6999 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7081 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6883 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7087 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7100 |
| [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 1936 |
| [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 2205 ax-14 2206 |
| [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 2179 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 1945 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2083 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2493 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2494 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2954 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3098 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5331 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5332 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2160 eupickbi 2163 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5359 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7486 |
| [vandenDries] p. 43 | Theorem 62 | pellexlem1 15832 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |