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 7313 fidcenum 7154 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7154 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7313 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13045 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7123 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7109 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13060 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13062 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13051 znnen 13018 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13063 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13064 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11037 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4635 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11167 df-pfx 11253 df-substr 11226 df-word 11113 lencl 11116 wrd0 11137 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8358 addcan2d 8363 addcan2i 8361 addcand 8362 addcani 8360 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8369 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8426 negsubd 8495 negsubi 8456 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8428 negnegd 8480 negnegi 8448 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8563 subdid 8592 subdii 8585 subdir 8564 subdird 8593 subdiri 8586 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8567 mul01d 8571 mul01i 8569 mul02 8565 mul02d 8570 mul02i 8568 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8972 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8923 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8576 mul2negd 8591 mul2negi 8584 mulneg1 8573 mulneg1d 8589 mulneg1i 8582 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14157 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8892 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9911 rpaddcld 9946 rpmulcl 9912 rpmulcld 9947 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9923 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8283 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8717 ltadd1dd 8735 ltadd1i 8681 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8771 ltmul1a 8770 ltmul1i 9099 ltmul1ii 9107 ltmul2 9035 ltmul2d 9973 ltmul2dd 9987 ltmul2i 9102 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8305 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8647 lt0neg1d 8694 ltneg 8641 ltnegd 8702 ltnegi 8672 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8624 lt2addd 8746 lt2addi 8689 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9888 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9029 recgt0d 9113 recgt0i 9085 recgt0ii 9086 |
| [Apostol] p. 22 | Definition of integers | df-z 9479 |
| [Apostol] p. 22 | Definition of rationals | df-q 9853 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7192 |
| [Apostol] p. 26 | Theorem I.29 | arch 9398 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9598 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9399 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10515 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12431 zneo 9580 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11591 sqrtthi 11679 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9145 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12606 |
| [Apostol] p. 363 | Remark | absgt0api 11706 |
| [Apostol] p. 363 | Example | abssubd 11753 abssubi 11710 |
| [ApostolNT] p. 14 | Definition | df-dvds 12348 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12364 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12388 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12384 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12378 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12380 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12365 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12366 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12371 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12405 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12407 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12409 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12584 |
| [ApostolNT] p. 16 | Definition | isprm2 12688 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12663 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13075 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12543 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12585 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12587 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12557 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12550 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12715 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12717 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12940 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12484 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12630 |
| [ApostolNT] p. 25 | Definition | df-phi 12782 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12812 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12793 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12797 |
| [ApostolNT] p. 38 | Remark | df-sgm 15705 |
| [ApostolNT] p. 38 | Definition | df-sgm 15705 |
| [ApostolNT] p. 104 | Definition | congr 12671 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12351 |
| [ApostolNT] p. 106 | Definition | moddvds 12359 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12438 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12439 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10602 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10639 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10927 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12383 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12674 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12993 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12676 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12804 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12823 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12805 |
| [ApostolNT] p. 179 | Definition | df-lgs 15726 lgsprme0 15770 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15771 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15747 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15762 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15813 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15832 2lgsoddprm 15841 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15797 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15808 |
| [ApostolNT] p. 188 | Definition | df-lgs 15726 lgs1 15772 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15763 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15765 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15773 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15774 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 621 pm2.65 665 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6016 onsucelsucexmidlem 4627 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16598 |
| [Bauer], p. 483 | Definition | n0rf 3507 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15699 2irrexpqap 15701 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7130 ssfiexmid 7062 ssfiexmidt 7064 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15376 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15366 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8824 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7313 |
| [BauerSwan], p. 14 | Remark | 0ct 7305 ctm 7307 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16601 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7720 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7633 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7722 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7756 addlocpr 7755 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7782 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7785 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7790 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2082 |
| [BellMachover] p. 460 | Notation | df-mo 2083 |
| [BellMachover] p. 460 | Definition | mo3 2134 mo3h 2133 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2216 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4210 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4267 |
| [BellMachover] p. 466 | Axiom Union | axun2 4532 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4640 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4481 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4643 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4594 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4466 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4687 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4712 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1475 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1473 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1476 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1471 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15908 isuhgropm 15931 isusgropen 16015 isuspgropen 16014 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16104 uhgrspansubgr 16127 |
| [Bollobas] p. 4 | Definition | df-wlks 16168 |
| [Bollobas] p. 5 | Definition | df-trls 16231 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15920 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13438 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13484 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13499 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14010 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13945 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5923 fcofo 5924 |
| [BourbakiTop1] p. | Remark | xnegmnf 10063 xnegpnf 10062 |
| [BourbakiTop1] p. | Remark | rexneg 10064 |
| [BourbakiTop1] p. | Proposition | ishmeo 15027 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14880 |
| [BourbakiTop1] p. | Property V_ii | innei 14886 |
| [BourbakiTop1] p. | Property V_iv | neissex 14888 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14877 neiss 14873 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14945 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15022 |
| [BourbakiTop1] p. | Property V_iii | elnei 14875 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14721 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13438 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13484 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13681 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4152 |
| [Church] p. 129 | Section II.24 | df-ifp 986 dfifp2dc 989 |
| [Cohen] p. 301 | Remark | relogoprlem 15591 |
| [Cohen] p. 301 | Property 2 | relogmul 15592 relogmuld 15607 |
| [Cohen] p. 301 | Property 3 | relogdiv 15593 relogdivd 15608 |
| [Cohen] p. 301 | Property 4 | relogexp 15595 |
| [Cohen] p. 301 | Property 1a | log1 15589 |
| [Cohen] p. 301 | Property 1b | loge 15590 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15688 |
| [Cohen4] p. 352 | Definition | rpelogb 15672 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15678 |
| [Cohen4] p. 361 | Property 3 | logbrec 15683 rprelogbdiv 15680 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15676 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15681 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15670 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15671 |
| [Cohen4] p. 367 | Property | rplogbchbase 15673 |
| [Cohen4] p. 377 | Property 2 | logblt 15685 |
| [Crosilla] p. | Axiom 1 | ax-ext 2213 |
| [Crosilla] p. | Axiom 2 | ax-pr 4299 |
| [Crosilla] p. | Axiom 3 | ax-un 4530 |
| [Crosilla] p. | Axiom 4 | ax-nul 4215 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4686 |
| [Crosilla] p. | Axiom 6 | ru 3030 |
| [Crosilla] p. | Axiom 8 | ax-pow 4264 |
| [Crosilla] p. | Axiom 9 | ax-setind 4635 |
| [Crosilla], p. | Axiom 6 | ax-sep 4207 |
| [Crosilla], p. | Axiom 7 | ax-coll 4204 |
| [Crosilla], p. | Axiom 7' | repizf 4205 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4619 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6016 |
| [Crosilla], p. | Definition of ordinal | df-iord 4463 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4633 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16104 uhgrspansubgr 16127 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15920 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3202 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4689 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6818 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4214 |
| [Enderton] p. 19 | Definition | df-tp 3677 |
| [Enderton] p. 26 | Exercise 5 | unissb 3923 |
| [Enderton] p. 26 | Exercise 10 | pwel 4310 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4383 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4040 iinin2m 4039 iunin1 4035 iunin2 4034 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4038 iundif2ss 4036 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4053 |
| [Enderton] p. 33 | Exercise 25 | iununir 4054 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4061 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4577 iunpwss 4062 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4309 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4282 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4547 rnex 5000 rnexg 4997 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4941 rnuni 5148 |
| [Enderton] p. 42 | Definition of a function | dffun7 5353 dffun8 5354 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5710 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5391 |
| [Enderton] p. 44 | Definition (d) | dfima2 5078 dfima3 5079 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5715 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7420 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5901 |
| [Enderton] p. 52 | Definition | df-map 6818 |
| [Enderton] p. 53 | Exercise 21 | coass 5255 |
| [Enderton] p. 53 | Exercise 27 | dmco 5245 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5401 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5112 |
| [Enderton] p. 54 | Remark | ixpf 6888 ixpssmap 6900 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6867 |
| [Enderton] p. 56 | Theorem 3M | erref 6721 |
| [Enderton] p. 57 | Lemma 3N | erthi 6749 |
| [Enderton] p. 57 | Definition | df-ec 6703 |
| [Enderton] p. 58 | Definition | df-qs 6707 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6808 th3qcor 6807 th3qlem1 6805 th3qlem2 6806 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6703 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4938 |
| [Enderton] p. 68 | Definition of successor | df-suc 4468 |
| [Enderton] p. 71 | Definition | df-tr 4188 dftr4 4192 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4510 unisucg 4511 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4510 unisucg 4511 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4201 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4202 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6641 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6643 onasuc 6633 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6020 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6642 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6644 onmsuc 6640 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6652 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6645 nnacom 6651 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6653 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6654 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6656 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6646 nnmsucr 6655 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6695 |
| [Enderton] p. 129 | Definition | df-en 6909 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5968 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13015 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7051 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7042 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7031 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7432 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7428 dju1en 7427 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3570 |
| [Enderton] p. 145 | Figure 38 | ffoss 5616 |
| [Enderton] p. 145 | Definition | df-dom 6910 |
| [Enderton] p. 146 | Example 1 | domen 6921 domeng 6922 |
| [Enderton] p. 146 | Example 3 | nndomo 7049 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7018 xpdom1g 7016 xpdom2g 7015 |
| [Enderton] p. 168 | Definition | df-po 4393 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4525 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4486 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4641 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4489 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4614 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4587 |
| [Enderton] p. 194 | Remark | onprc 4650 |
| [Enderton] p. 194 | Exercise 16 | suc11 4656 |
| [Enderton] p. 197 | Definition | df-card 7382 |
| [Enderton] p. 200 | Exercise 25 | tfis 4681 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4652 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4654 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4655 |
| [Geuvers], p. 1 | Remark | expap0 10830 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8794 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8833 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8795 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8150 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11763 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11771 maxle2 11772 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11773 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11776 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11777 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8761 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7566 enqer 7577 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7570 df-nqqs 7567 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7563 df-plqqs 7568 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7564 df-mqqs 7569 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7571 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7627 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7630 ltbtwnnq 7635 ltbtwnnqq 7634 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7619 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7620 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7756 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7798 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7797 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7816 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7832 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7838 ltaprlem 7837 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7835 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7791 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7811 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7800 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7799 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7807 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7857 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7945 enrer 7954 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7950 df-1r 7951 df-nr 7946 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7948 df-plr 7947 negexsr 7991 recexsrlem 7993 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7949 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9139 creur 9138 cru 8781 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8142 axcnre 8100 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11418 crimd 11537 crimi 11497 crre 11417 crred 11536 crrei 11496 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11420 remimd 11502 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11617 absval2d 11745 absval2i 11704 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11444 cjaddd 11525 cjaddi 11492 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11445 cjmuld 11526 cjmuli 11493 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11443 cjcjd 11503 cjcji 11475 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11442 cjreb 11426 cjrebd 11506 cjrebi 11478 cjred 11531 rere 11425 rereb 11423 rerebd 11505 rerebi 11477 rered 11529 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11451 addcjd 11517 addcji 11487 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11561 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11612 abscjd 11750 abscji 11708 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11624 abs00d 11746 abs00i 11705 absne0d 11747 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11656 releabsd 11751 releabsi 11709 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11629 absmuld 11754 absmuli 11711 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11615 sqabsaddi 11712 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11664 abstrid 11756 abstrii 11715 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10800 exp0 10804 expp1 10807 expp1d 10935 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10842 expaddd 10936 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15635 cxpmuld 15660 expmul 10845 expmuld 10937 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10839 mulexpd 10949 rpmulcxp 15632 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10244 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11886 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11888 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11887 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11891 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11884 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11880 climcj 11881 climim 11883 climre 11882 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8218 df-xr 8217 ltxr 10009 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11907 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10559 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14558 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15087 xmet0 15086 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15094 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15096 mstri 15196 xmettri 15095 xmstri 15195 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15002 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15234 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11870 addcncntop 15285 mulcn2 11872 mulcncntop 15287 subcn2 11871 subcncntop 15286 |
| [Gleason] p. 295 | Remark | bcval3 11012 bcval4 11013 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11027 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11010 df-bc 11009 |
| [Gleason] p. 296 | Remark | bcn0 11016 bcnn 11018 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12044 |
| [Gleason] p. 308 | Equation 2 | ef0 12232 |
| [Gleason] p. 308 | Equation 3 | efcj 12233 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12238 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12242 |
| [Gleason] p. 310 | Equation 14 | sinadd 12296 |
| [Gleason] p. 310 | Equation 15 | cosadd 12297 |
| [Gleason] p. 311 | Equation 17 | sincossq 12308 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12313 sinbnd 12312 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12213 |
| [Golan] p. 1 | Remark | srgisid 13998 |
| [Golan] p. 1 | Definition | df-srg 13976 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1497 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13593 mndideu 13508 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13620 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13649 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13660 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13682 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16685 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1467 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1468 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1470 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7439 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6666 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16672 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8836 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7689 df-imp 7688 df-iplp 7687 df-reap 8754 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8850 rerecapb 9022 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6299 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7881 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16317 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16665 dceqnconst 16664 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8119 caucvgpr 7901 caucvgprpr 7931 caucvgsr 8021 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7685 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16670 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4394 ltpopr 7814 ltsopr 7815 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8785 reapcotr 8777 reapirr 8756 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8305 gt0add 8752 leadd1 8609 lelttr 8267 lemul1a 9037 lenlt 8254 ltadd1 8608 ltletr 8268 ltmul1 8771 reaplt 8767 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16277 |
| [Jech] p. 4 | Definition of class | cv 1396 cvjust 2226 |
| [Jech] p. 78 | Note | opthprc 4777 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1578 |
| [Kreyszig] p. 3 | Property M1 | metcl 15076 xmetcl 15075 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15083 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8847 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15165 |
| [Kreyszig] p. 19 | Remark | mopntopon 15166 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15211 mopnm 15171 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15209 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15214 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15236 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14936 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14343 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14334 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14335 |
| [Kunen] p. 10 | Axiom 0 | a9e 1744 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4206 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6828 mapvalg 6826 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6822 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3980 |
| [Lang] p. 3 | Statement | lidrideqd 13463 mndbn0 13513 |
| [Lang] p. 3 | Definition | df-mnd 13499 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13480 |
| [Lang] p. 5 | Equation | gsumfzreidx 13923 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13714 |
| [Lang] p. 7 | Definition | dfgrp2e 13610 |
| [Levy] p. 338 | Axiom | df-clab 2218 df-clel 2227 df-cleq 2224 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1467 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1468 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1470 |
| [Margaris] p. 40 | Rule C | exlimiv 1646 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 860 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 899 exalim 1550 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 657 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1686 r19.2m 3581 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1602 19.3h 1601 rr19.3v 2945 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1526 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1667 alexim 1693 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1547 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1638 spsbe 1890 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1692 19.9h 1691 19.9v 1919 exlimd 1645 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1712 excomim 1711 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1713 r19.12 2639 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1694 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1516 ralbi 2665 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1603 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1604 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1652 rexbi 2666 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1714 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1505 alimd 1569 alimdh 1515 alimdv 1927 ralimdaa 2598 ralimdv 2600 ralimdva 2599 ralimdvva 2601 sbcimdv 3097 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1715 19.21 1631 19.21bi 1606 19.21h 1605 19.21ht 1629 19.21t 1630 19.21v 1921 alrimd 1658 alrimdd 1657 alrimdh 1527 alrimdv 1924 alrimi 1570 alrimih 1517 alrimiv 1922 alrimivv 1923 r19.21 2608 r19.21be 2623 r19.21bi 2620 r19.21t 2607 r19.21v 2609 ralrimd 2610 ralrimdv 2611 ralrimdva 2612 ralrimdvv 2616 ralrimdvva 2617 ralrimi 2603 ralrimiv 2604 ralrimiva 2605 ralrimivv 2613 ralrimivva 2614 ralrimivvva 2615 ralrimivw 2606 rexlimi 2643 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1929 2eximdv 1930 exim 1647 eximd 1660 eximdh 1659 eximdv 1928 rexim 2626 reximdai 2630 reximddv 2635 reximddv2 2637 reximdv 2633 reximdv2 2631 reximdva 2634 reximdvai 2632 reximi2 2628 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1726 19.23bi 1640 19.23h 1546 19.23ht 1545 19.23t 1725 19.23v 1931 19.23vv 1932 exlimd2 1643 exlimdh 1644 exlimdv 1867 exlimdvv 1946 exlimi 1642 exlimih 1641 exlimiv 1646 exlimivv 1945 r19.23 2641 r19.23v 2642 rexlimd 2647 rexlimdv 2649 rexlimdv3a 2652 rexlimdva 2650 rexlimdva2 2653 rexlimdvaa 2651 rexlimdvv 2657 rexlimdvva 2658 rexlimdvw 2654 rexlimiv 2644 rexlimiva 2645 rexlimivv 2656 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1687 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1674 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1530 19.26-3an 1531 19.26 1529 r19.26-2 2662 r19.26-3 2663 r19.26 2659 r19.26m 2664 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1609 19.27h 1608 19.27v 1948 r19.27av 2668 r19.27m 3590 r19.27mv 3591 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1611 19.28h 1610 19.28v 1949 r19.28av 2669 r19.28m 3584 r19.28mv 3587 rr19.28v 2946 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1668 19.29r 1669 19.29r2 1670 19.29x 1671 r19.29 2670 r19.29d2r 2677 r19.29r 2671 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1675 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1729 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1727 19.32r 1728 r19.32r 2679 r19.32vdc 2682 r19.32vr 2681 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1532 19.33b2 1677 19.33bdc 1678 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1732 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1672 19.35i 1673 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1721 19.36aiv 1950 19.36i 1720 r19.36av 2684 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1722 19.37aiv 1723 r19.37 2685 r19.37av 2686 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1724 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1688 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1680 19.40 1679 r19.40 2687 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1734 19.41h 1733 19.41v 1951 19.41vv 1952 19.41vvv 1953 19.41vvvv 1954 r19.41 2688 r19.41v 2689 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1736 19.42h 1735 19.42v 1955 19.42vv 1960 19.42vvv 1961 19.42vvvv 1962 r19.42v 2690 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1676 r19.43 2691 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1730 r19.44av 2692 r19.44mv 3589 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1731 r19.45av 2693 r19.45mv 3588 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2104 |
| [Megill] p. 444 | Axiom C5 | ax-17 1574 |
| [Megill] p. 445 | Lemma L12 | alequcom 1563 ax-10 1553 |
| [Megill] p. 446 | Lemma L17 | equtrr 1758 |
| [Megill] p. 446 | Lemma L19 | hbnae 1769 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1811 sbid 1822 |
| [Megill] p. 448 | Scheme C5' | ax-4 1558 |
| [Megill] p. 448 | Scheme C6' | ax-7 1496 |
| [Megill] p. 448 | Scheme C8' | ax-8 1552 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1555 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1764 |
| [Megill] p. 448 | Scheme C12' | ax-13 2204 |
| [Megill] p. 448 | Scheme C13' | ax-14 2205 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1871 |
| [Megill] p. 448 | Scheme C16' | ax-16 1862 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1778 dral2 1779 drex1 1846 drex2 1780 drsb1 1847 drsb2 1889 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2040 sbequ 1888 sbid2v 2049 |
| [Megill] p. 450 | Example in Appendix | hba1 1588 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3115 rspsbca 3116 stdpc4 1823 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3121 stdpc5 1632 |
| [Mendelson] p. 81 | Rule C | exlimiv 1646 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1751 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1818 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3531 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3532 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3447 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3495 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3448 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3338 |
| [Mendelson] p. 231 | Definition of union | unssin 3446 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4573 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3892 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4379 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4380 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4381 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3913 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4859 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5257 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4468 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7030 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7004 xpsneng 7005 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7010 xpcomeng 7011 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7013 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7007 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6820 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6985 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7035 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6854 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6986 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7431 djucomen 7430 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7429 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6634 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3429 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4814 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4815 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4151 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5252 coi2 5253 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4945 rn0 4988 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5141 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4835 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4952 rnxpm 5166 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4806 xp0 5156 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5095 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5092 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5091 imaexg 5090 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5087 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5777 funfvop 5759 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5687 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5697 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5371 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5908 dff13f 5910 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5876 funrnex 6275 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5902 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5220 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3944 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6317 df-1st 6302 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6318 df-2nd 6303 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1495 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1552 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1554 ax-11o 1871 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1875 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1496 |
| [Monk2] p. 109 | Lemma 15 | equvin 1911 equvini 1806 eqvinop 4335 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1574 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1699 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1496 |
| [Monk2] p. 114 | Lemma 22 | hba1 1588 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1600 nfia1 1628 |
| [Monk2] p. 114 | Lemma 24 | hba2 1599 nfa2 1627 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 838 dftest 16686 |
| [Munkres] p. 77 | Example 2 | distop 14808 |
| [Munkres] p. 78 | Definition of basis | df-bases 14766 isbasis3g 14769 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13342 tgval2 14774 |
| [Munkres] p. 79 | Remark | tgcl 14787 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14781 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14802 tgss3 14801 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14803 basgen2 14804 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14893 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14835 topcld 14832 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14836 |
| [Munkres] p. 94 | Definition of closure | clsval 14834 |
| [Munkres] p. 94 | Definition of interior | ntrval 14833 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14911 iscn 14920 iscn2 14923 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14953 cncnp2m 14954 cncnpi 14951 df-cnp 14912 iscnp 14922 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15237 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7092 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7362 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7350 omniwomnimkv 7365 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3317 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7333 exmidomniim 7339 finomni 7338 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7318 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16623 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16627 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7099 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7411 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7412 exmidfodomrlemrALT 7413 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7347 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16609 peano4nninf 16608 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16611 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16619 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16621 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16607 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2218 rabid 2709 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2044 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2224 |
| [Quine] p. 19 | Definition 2.9 | df-v 2804 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2340 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2352 abid2f 2400 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1936 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1934 sb6 1935 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2227 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2231 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2233 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3032 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3033 dfsbcq2 3034 |
| [Quine] p. 43 | Theorem 6.8 | vex 2805 |
| [Quine] p. 43 | Theorem 6.9 | isset 2809 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2888 spcgv 2893 spcimgf 2886 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3043 spsbcd 3044 |
| [Quine] p. 44 | Theorem 6.12 | elex 2814 |
| [Quine] p. 44 | Theorem 6.13 | elab 2950 elabg 2952 elabgf 2948 |
| [Quine] p. 44 | Theorem 6.14 | noel 3498 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3734 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3676 df-sn 3675 |
| [Quine] p. 49 | Theorem 7.4 | snss 3808 snssg 3807 |
| [Quine] p. 49 | Theorem 7.5 | prss 3829 prssg 3830 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3777 prid1g 3775 prid2 3778 prid2g 3776 snid 3700 snidg 3698 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4274 snexprc 4276 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4301 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3909 unisng 3910 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3912 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3921 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3920 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5297 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5287 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5298 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5302 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5303 |
| [Quine] p. 58 | Definition 9.1 | df-op 3678 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4350 opabidw 4351 opelopab 4366 opelopaba 4360 opelopabaf 4368 opelopabf 4369 opelopabg 4362 opelopabga 4357 opelopabgf 4364 oprabid 6049 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4731 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4733 |
| [Quine] p. 64 | Definition 9.15 | df-id 4390 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5388 |
| [Quine] p. 65 | Theorem 10.4 | funi 5358 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5378 funsng 5376 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5328 |
| [Quine] p. 65 | Definition 10.2 | args 5105 dffv4g 5636 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5334 fv2 5634 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10985 nn0opth2d 10984 nn0opthd 10983 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5415 funimaexg 5414 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13945 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14010 |
| [Rudin] p. 164 | Equation 27 | efcan 12236 |
| [Rudin] p. 164 | Equation 30 | efzval 12243 |
| [Rudin] p. 167 | Equation 48 | absefi 12329 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1470 |
| [Sanford] p. 39 | Rule 4 | mptxor 1468 |
| [Sanford] p. 40 | Rule 1 | mptnan 1467 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5121 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5123 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5120 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5118 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14012 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14806 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3472 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3566 dif0 3565 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3579 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3465 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3466 |
| [Stoll] p. 20 | Remark | invdif 3449 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3679 |
| [Stoll] p. 43 | Definition | uniiun 4024 |
| [Stoll] p. 44 | Definition | intiin 4025 |
| [Stoll] p. 45 | Definition | df-iin 3973 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3972 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 896 imanst 895 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3472 |
| [Suppes] p. 22 | Theorem 2 | eq0 3513 |
| [Suppes] p. 22 | Theorem 4 | eqss 3242 eqssd 3244 eqssi 3243 |
| [Suppes] p. 23 | Theorem 5 | ss0 3535 ss0b 3534 |
| [Suppes] p. 23 | Theorem 6 | sstr 3235 |
| [Suppes] p. 25 | Theorem 12 | elin 3390 elun 3348 |
| [Suppes] p. 26 | Theorem 15 | inidm 3416 |
| [Suppes] p. 26 | Theorem 16 | in0 3529 |
| [Suppes] p. 27 | Theorem 23 | unidm 3350 |
| [Suppes] p. 27 | Theorem 24 | un0 3528 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3370 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3377 |
| [Suppes] p. 27 | Theorem 27 | unss 3381 |
| [Suppes] p. 27 | Theorem 28 | indir 3456 |
| [Suppes] p. 27 | Theorem 29 | undir 3457 |
| [Suppes] p. 28 | Theorem 32 | difid 3563 difidALT 3564 |
| [Suppes] p. 29 | Theorem 33 | difin 3444 |
| [Suppes] p. 29 | Theorem 34 | indif 3450 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3569 |
| [Suppes] p. 29 | Theorem 36 | difun2 3574 |
| [Suppes] p. 29 | Theorem 37 | difin0 3568 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3567 |
| [Suppes] p. 29 | Theorem 39 | difundi 3459 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3461 |
| [Suppes] p. 30 | Theorem 41 | nalset 4219 |
| [Suppes] p. 39 | Theorem 61 | uniss 3914 |
| [Suppes] p. 39 | Theorem 65 | uniop 4348 |
| [Suppes] p. 41 | Theorem 70 | intsn 3963 |
| [Suppes] p. 42 | Theorem 71 | intpr 3960 intprg 3961 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4575 op1stbg 4576 |
| [Suppes] p. 42 | Theorem 78 | intun 3959 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4004 dfiun2g 4002 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4005 |
| [Suppes] p. 47 | Theorem 86 | elpw 3658 elpw2 4247 elpw2g 4246 elpwg 3660 |
| [Suppes] p. 47 | Theorem 87 | pwid 3667 |
| [Suppes] p. 47 | Theorem 89 | pw0 3820 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3888 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4833 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4865 xpindir 4866 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4782 xpundir 4783 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4646 |
| [Suppes] p. 58 | Theorem 2 | relss 4813 |
| [Suppes] p. 59 | Theorem 4 | eldm 4928 eldm2 4929 eldm2g 4927 eldmg 4926 |
| [Suppes] p. 59 | Definition 3 | df-dm 4735 |
| [Suppes] p. 60 | Theorem 6 | dmin 4939 |
| [Suppes] p. 60 | Theorem 8 | rnun 5145 |
| [Suppes] p. 60 | Theorem 9 | rnin 5146 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4918 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4913 brcnvg 4911 |
| [Suppes] p. 62 | Equation 5 | elcnv 4907 elcnv2 4908 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5114 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5144 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5142 |
| [Suppes] p. 63 | Theorem 20 | co02 5250 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5002 |
| [Suppes] p. 63 | Definition 7 | df-co 4734 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4915 |
| [Suppes] p. 64 | Theorem 27 | coass 5255 |
| [Suppes] p. 65 | Theorem 31 | resundi 5026 |
| [Suppes] p. 65 | Theorem 34 | elima 5081 elima2 5082 elima3 5083 elimag 5080 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5149 |
| [Suppes] p. 66 | Theorem 40 | dminss 5151 |
| [Suppes] p. 66 | Theorem 41 | imainss 5152 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5155 |
| [Suppes] p. 81 | Definition 34 | dfec2 6704 |
| [Suppes] p. 82 | Theorem 72 | elec 6742 elecg 6741 |
| [Suppes] p. 82 | Theorem 73 | erth 6747 erth2 6748 |
| [Suppes] p. 89 | Theorem 96 | map0b 6855 |
| [Suppes] p. 89 | Theorem 97 | map0 6857 map0g 6856 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6858 |
| [Suppes] p. 89 | Theorem 99 | mapss 6859 |
| [Suppes] p. 92 | Theorem 1 | enref 6937 enrefg 6936 |
| [Suppes] p. 92 | Theorem 2 | ensym 6954 ensymb 6953 ensymi 6955 |
| [Suppes] p. 92 | Theorem 3 | entr 6957 |
| [Suppes] p. 92 | Theorem 4 | unen 6990 |
| [Suppes] p. 94 | Theorem 15 | endom 6935 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6951 |
| [Suppes] p. 94 | Theorem 17 | domtr 6958 |
| [Suppes] p. 95 | Theorem 18 | isbth 7165 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6980 fundmeng 6981 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7017 |
| [Suppes] p. 130 | Definition 3 | df-tr 4188 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4586 |
| [Suppes] p. 134 | Definition 6 | df-suc 4468 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4701 finds 4698 finds1 4700 finds2 4699 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7572 df-ltpq 7565 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4487 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2213 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2227 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2226 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2249 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6021 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3030 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3690 elpr2 3691 elprg 3689 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3685 elsn2 3703 elsn2g 3702 elsng 3684 velsn 3686 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4323 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3680 sneqr 3843 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3688 dfsn2 3683 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4534 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4329 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4307 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4538 unexg 4540 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3718 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3894 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3206 df-un 3204 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3907 uniprg 3908 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4269 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3717 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4503 elsucg 4501 sstr2 3234 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3351 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3399 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3364 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3417 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3454 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3455 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3215 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3654 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3378 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3213 dfss2 3217 sseqin2 3426 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3247 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3427 inss2 3428 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3287 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3902 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4308 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4315 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2519 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4216 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3202 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3496 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3563 difidALT 3564 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3507 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4637 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2804 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4221 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3533 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4226 ssexg 4228 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4223 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4648 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4639 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3559 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3332 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3468 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3333 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3341 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2515 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2516 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4842 xpexg 4840 xpexgALT 6294 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4732 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5394 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5553 fun11 5397 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5337 svrelfun 5395 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4917 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4919 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4737 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4738 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4734 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5191 dfrel2 5187 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4834 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4844 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4850 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4864 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5041 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5018 opelresg 5020 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5034 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5037 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5042 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5367 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5235 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5366 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5554 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2124 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5334 fv3 5662 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5275 cnvexg 5274 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4999 dmexg 4996 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5000 rnexg 4997 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5656 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5666 tz6.12 5667 tz6.12c 5669 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5630 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5329 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5330 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5332 wfo 5324 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5331 wf1 5323 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5333 wf1o 5325 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5744 eqfnfv2 5745 eqfnfv2f 5748 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5716 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5875 fnexALT 6272 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5874 resfunexgALT 6269 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5415 funimaexg 5414 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4089 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5106 iniseg 5108 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4386 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5335 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5950 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5951 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5956 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5958 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5966 |
| [TakeutiZaring] p. 35 | Notation | wtr 4187 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4451 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4191 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4674 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4478 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4482 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4590 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4465 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4584 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4650 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4680 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4189 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4609 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4585 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3921 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4468 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4512 sucidg 4513 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4599 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4466 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4604 ordelsuc 4603 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4692 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4693 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4694 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4691 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4705 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4697 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4695 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4696 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3942 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4203 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3943 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4615 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3929 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6473 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6530 tfri1d 6500 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6531 tfri2d 6501 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6532 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6467 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6451 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6631 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6627 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6624 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6628 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6676 nnaordi 6675 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4015 uniss2 3924 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6637 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6647 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6638 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6625 omsuc 6639 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6648 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6684 nnmordi 6683 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6626 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7390 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6968 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7042 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7043 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6911 isfi 6933 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7014 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6818 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7020 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7033 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1558 |
| [Tarski] p. 68 | Lemma 6 | equid 1749 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1752 |
| [Tarski] p. 70 | Lemma 14 | spim 1786 spime 1789 spimeh 1787 spimh 1785 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1554 ax-11o 1871 ax11i 1762 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1935 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1574 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2204 ax-14 2205 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 718 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 734 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 763 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 772 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 796 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 621 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 648 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 844 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2178 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 744 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 843 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 634 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 892 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 850 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 863 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 647 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 860 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 862 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 719 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 782 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 622 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 626 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 900 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 914 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 775 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 776 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 811 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 812 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 810 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1005 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 785 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 783 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 784 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 745 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 874 pm2.5gdc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 869 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 749 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 661 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 662 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 729 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 898 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 732 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 733 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 872 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 755 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 807 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 808 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 665 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 720 pm2.67 750 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 876 pm2.521gdc 875 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 754 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 901 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 922 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 818 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 819 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 912 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 761 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 965 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 966 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 967 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 760 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 264 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 265 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 700 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 347 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 261 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 262 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 867 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 866 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 345 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 346 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 695 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 601 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 333 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 331 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 332 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 762 pm3.44 722 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 606 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 792 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 878 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 879 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 897 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 701 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 960 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 764 pm4.25 765 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 825 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 735 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 774 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 799 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 609 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 829 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1006 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 823 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 979 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 957 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 786 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 821 pm4.45 791 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1529 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 964 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 904 imorr 728 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 757 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 758 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 909 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 946 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 759 pm4.56 787 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 947 oranim 788 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 692 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 893 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 693 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 908 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 894 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 834 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 751 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 607 pm4.76 608 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 717 pm4.77 806 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 789 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 910 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 714 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 915 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 958 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 959 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 237 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 240 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 559 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 605 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 916 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 919 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 918 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1433 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 835 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 911 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1438 pm5.18dc 890 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 713 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 702 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1436 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1441 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1442 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 902 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 475 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 242 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 933 pm5.6r 934 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 962 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 453 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 613 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 924 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 614 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 250 pm5.41 251 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 320 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 932 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 809 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 925 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 920 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 801 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 953 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 954 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 969 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 244 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 179 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 970 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1683 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1533 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1680 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1944 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2082 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2483 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2484 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2944 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3088 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5306 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5307 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2159 eupickbi 2162 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5334 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7394 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |