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 7308 fidcenum 7149 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7149 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7308 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13039 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7119 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7105 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13054 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13056 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13045 znnen 13012 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13057 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13058 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11031 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4633 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11161 df-pfx 11247 df-substr 11220 df-word 11107 lencl 11110 wrd0 11131 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8352 addcan2d 8357 addcan2i 8355 addcand 8356 addcani 8354 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8363 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8420 negsubd 8489 negsubi 8450 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8422 negnegd 8474 negnegi 8442 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8557 subdid 8586 subdii 8579 subdir 8558 subdird 8587 subdiri 8580 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8561 mul01d 8565 mul01i 8563 mul02 8559 mul02d 8564 mul02i 8562 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8966 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8917 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8570 mul2negd 8585 mul2negi 8578 mulneg1 8567 mulneg1d 8583 mulneg1i 8576 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14151 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8886 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9905 rpaddcld 9940 rpmulcl 9906 rpmulcld 9941 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9917 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8277 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8711 ltadd1dd 8729 ltadd1i 8675 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8765 ltmul1a 8764 ltmul1i 9093 ltmul1ii 9101 ltmul2 9029 ltmul2d 9967 ltmul2dd 9981 ltmul2i 9096 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8299 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8641 lt0neg1d 8688 ltneg 8635 ltnegd 8696 ltnegi 8666 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8618 lt2addd 8740 lt2addi 8683 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9882 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9023 recgt0d 9107 recgt0i 9079 recgt0ii 9080 |
| [Apostol] p. 22 | Definition of integers | df-z 9473 |
| [Apostol] p. 22 | Definition of rationals | df-q 9847 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7187 |
| [Apostol] p. 26 | Theorem I.29 | arch 9392 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9592 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9393 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10509 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12425 zneo 9574 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11585 sqrtthi 11673 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9139 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12600 |
| [Apostol] p. 363 | Remark | absgt0api 11700 |
| [Apostol] p. 363 | Example | abssubd 11747 abssubi 11704 |
| [ApostolNT] p. 14 | Definition | df-dvds 12342 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12358 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12382 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12378 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12372 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12374 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12359 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12360 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12365 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12399 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12401 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12403 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12578 |
| [ApostolNT] p. 16 | Definition | isprm2 12682 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12657 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13069 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12537 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12579 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12581 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12551 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12544 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12709 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12711 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12934 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12478 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12624 |
| [ApostolNT] p. 25 | Definition | df-phi 12776 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12806 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12787 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12791 |
| [ApostolNT] p. 38 | Remark | df-sgm 15699 |
| [ApostolNT] p. 38 | Definition | df-sgm 15699 |
| [ApostolNT] p. 104 | Definition | congr 12665 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12345 |
| [ApostolNT] p. 106 | Definition | moddvds 12353 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12432 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12433 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10596 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10633 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10921 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12377 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12668 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12987 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12670 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12798 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12817 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12799 |
| [ApostolNT] p. 179 | Definition | df-lgs 15720 lgsprme0 15764 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15765 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15741 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15756 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15807 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15826 2lgsoddprm 15835 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15791 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15802 |
| [ApostolNT] p. 188 | Definition | df-lgs 15720 lgs1 15766 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15757 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15759 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15767 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15768 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 619 pm2.65 663 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6012 onsucelsucexmidlem 4625 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16548 |
| [Bauer], p. 483 | Definition | n0rf 3505 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15693 2irrexpqap 15695 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7125 ssfiexmid 7058 ssfiexmidt 7060 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15370 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15360 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8818 |
| [BauerSwan], p. 14 | Remark | 0ct 7300 ctm 7302 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16551 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7308 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7714 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7627 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7716 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7750 addlocpr 7749 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7776 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7779 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7784 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2080 |
| [BellMachover] p. 460 | Notation | df-mo 2081 |
| [BellMachover] p. 460 | Definition | mo3 2132 mo3h 2131 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2214 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4208 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4265 |
| [BellMachover] p. 466 | Axiom Union | axun2 4530 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4638 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4479 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4641 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4592 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4464 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4685 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4710 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1473 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1471 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1474 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1469 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15902 isuhgropm 15925 isusgropen 16009 isuspgropen 16008 |
| [Bollobas] p. 4 | Definition | df-wlks 16129 |
| [Bollobas] p. 5 | Definition | df-trls 16190 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15914 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13432 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13478 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13493 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14004 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13939 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5919 fcofo 5920 |
| [BourbakiTop1] p. | Remark | xnegmnf 10057 xnegpnf 10056 |
| [BourbakiTop1] p. | Remark | rexneg 10058 |
| [BourbakiTop1] p. | Proposition | ishmeo 15021 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14874 |
| [BourbakiTop1] p. | Property V_ii | innei 14880 |
| [BourbakiTop1] p. | Property V_iv | neissex 14882 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14871 neiss 14867 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14939 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15016 |
| [BourbakiTop1] p. | Property V_iii | elnei 14869 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14715 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13432 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13478 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13675 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4150 |
| [Church] p. 129 | Section II.24 | df-ifp 984 dfifp2dc 987 |
| [Cohen] p. 301 | Remark | relogoprlem 15585 |
| [Cohen] p. 301 | Property 2 | relogmul 15586 relogmuld 15601 |
| [Cohen] p. 301 | Property 3 | relogdiv 15587 relogdivd 15602 |
| [Cohen] p. 301 | Property 4 | relogexp 15589 |
| [Cohen] p. 301 | Property 1a | log1 15583 |
| [Cohen] p. 301 | Property 1b | loge 15584 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15682 |
| [Cohen4] p. 352 | Definition | rpelogb 15666 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15672 |
| [Cohen4] p. 361 | Property 3 | logbrec 15677 rprelogbdiv 15674 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15670 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15675 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15664 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15665 |
| [Cohen4] p. 367 | Property | rplogbchbase 15667 |
| [Cohen4] p. 377 | Property 2 | logblt 15679 |
| [Crosilla] p. | Axiom 1 | ax-ext 2211 |
| [Crosilla] p. | Axiom 2 | ax-pr 4297 |
| [Crosilla] p. | Axiom 3 | ax-un 4528 |
| [Crosilla] p. | Axiom 4 | ax-nul 4213 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4684 |
| [Crosilla] p. | Axiom 6 | ru 3028 |
| [Crosilla] p. | Axiom 8 | ax-pow 4262 |
| [Crosilla] p. | Axiom 9 | ax-setind 4633 |
| [Crosilla], p. | Axiom 6 | ax-sep 4205 |
| [Crosilla], p. | Axiom 7 | ax-coll 4202 |
| [Crosilla], p. | Axiom 7' | repizf 4203 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4617 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6012 |
| [Crosilla], p. | Definition of ordinal | df-iord 4461 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4631 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15914 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3200 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4687 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6814 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4212 |
| [Enderton] p. 19 | Definition | df-tp 3675 |
| [Enderton] p. 26 | Exercise 5 | unissb 3921 |
| [Enderton] p. 26 | Exercise 10 | pwel 4308 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4381 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4038 iinin2m 4037 iunin1 4033 iunin2 4032 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4036 iundif2ss 4034 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4051 |
| [Enderton] p. 33 | Exercise 25 | iununir 4052 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4059 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4575 iunpwss 4060 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4307 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4280 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4545 rnex 4998 rnexg 4995 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4939 rnuni 5146 |
| [Enderton] p. 42 | Definition of a function | dffun7 5351 dffun8 5352 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5706 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5388 |
| [Enderton] p. 44 | Definition (d) | dfima2 5076 dfima3 5077 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5711 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7414 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5897 |
| [Enderton] p. 52 | Definition | df-map 6814 |
| [Enderton] p. 53 | Exercise 21 | coass 5253 |
| [Enderton] p. 53 | Exercise 27 | dmco 5243 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5398 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5110 |
| [Enderton] p. 54 | Remark | ixpf 6884 ixpssmap 6896 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6863 |
| [Enderton] p. 56 | Theorem 3M | erref 6717 |
| [Enderton] p. 57 | Lemma 3N | erthi 6745 |
| [Enderton] p. 57 | Definition | df-ec 6699 |
| [Enderton] p. 58 | Definition | df-qs 6703 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6804 th3qcor 6803 th3qlem1 6801 th3qlem2 6802 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6699 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4936 |
| [Enderton] p. 68 | Definition of successor | df-suc 4466 |
| [Enderton] p. 71 | Definition | df-tr 4186 dftr4 4190 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4508 unisucg 4509 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4508 unisucg 4509 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4199 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4200 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6637 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6639 onasuc 6629 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6016 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6638 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6640 onmsuc 6636 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6648 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6641 nnacom 6647 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6649 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6650 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6652 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6642 nnmsucr 6651 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6691 |
| [Enderton] p. 129 | Definition | df-en 6905 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5964 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13009 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7047 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7038 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7027 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7426 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7422 dju1en 7421 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3568 |
| [Enderton] p. 145 | Figure 38 | ffoss 5612 |
| [Enderton] p. 145 | Definition | df-dom 6906 |
| [Enderton] p. 146 | Example 1 | domen 6917 domeng 6918 |
| [Enderton] p. 146 | Example 3 | nndomo 7045 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7014 xpdom1g 7012 xpdom2g 7011 |
| [Enderton] p. 168 | Definition | df-po 4391 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4523 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4484 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4639 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4487 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4612 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4585 |
| [Enderton] p. 194 | Remark | onprc 4648 |
| [Enderton] p. 194 | Exercise 16 | suc11 4654 |
| [Enderton] p. 197 | Definition | df-card 7377 |
| [Enderton] p. 200 | Exercise 25 | tfis 4679 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4650 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4652 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4653 |
| [Geuvers], p. 1 | Remark | expap0 10824 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8788 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8827 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8789 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8144 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11757 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11765 maxle2 11766 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11767 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11770 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11771 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8755 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7560 enqer 7571 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7564 df-nqqs 7561 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7557 df-plqqs 7562 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7558 df-mqqs 7563 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7565 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7621 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7624 ltbtwnnq 7629 ltbtwnnqq 7628 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7613 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7614 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7750 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7792 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7791 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7810 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7826 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7832 ltaprlem 7831 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7829 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7785 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7805 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7794 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7793 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7801 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7851 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7939 enrer 7948 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7944 df-1r 7945 df-nr 7940 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7942 df-plr 7941 negexsr 7985 recexsrlem 7987 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7943 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9133 creur 9132 cru 8775 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8136 axcnre 8094 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11412 crimd 11531 crimi 11491 crre 11411 crred 11530 crrei 11490 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11414 remimd 11496 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11611 absval2d 11739 absval2i 11698 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11438 cjaddd 11519 cjaddi 11486 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11439 cjmuld 11520 cjmuli 11487 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11437 cjcjd 11497 cjcji 11469 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11436 cjreb 11420 cjrebd 11500 cjrebi 11472 cjred 11525 rere 11419 rereb 11417 rerebd 11499 rerebi 11471 rered 11523 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11445 addcjd 11511 addcji 11481 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11555 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11606 abscjd 11744 abscji 11702 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11618 abs00d 11740 abs00i 11699 absne0d 11741 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11650 releabsd 11745 releabsi 11703 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11623 absmuld 11748 absmuli 11705 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11609 sqabsaddi 11706 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11658 abstrid 11750 abstrii 11709 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10794 exp0 10798 expp1 10801 expp1d 10929 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10836 expaddd 10930 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15629 cxpmuld 15654 expmul 10839 expmuld 10931 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10833 mulexpd 10943 rpmulcxp 15626 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10238 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11880 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11882 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11881 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11885 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11878 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11874 climcj 11875 climim 11877 climre 11876 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8212 df-xr 8211 ltxr 10003 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11901 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10553 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14552 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15081 xmet0 15080 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15088 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15090 mstri 15190 xmettri 15089 xmstri 15189 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14996 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15228 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11864 addcncntop 15279 mulcn2 11866 mulcncntop 15281 subcn2 11865 subcncntop 15280 |
| [Gleason] p. 295 | Remark | bcval3 11006 bcval4 11007 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11021 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11004 df-bc 11003 |
| [Gleason] p. 296 | Remark | bcn0 11010 bcnn 11012 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12038 |
| [Gleason] p. 308 | Equation 2 | ef0 12226 |
| [Gleason] p. 308 | Equation 3 | efcj 12227 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12232 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12236 |
| [Gleason] p. 310 | Equation 14 | sinadd 12290 |
| [Gleason] p. 310 | Equation 15 | cosadd 12291 |
| [Gleason] p. 311 | Equation 17 | sincossq 12302 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12307 sinbnd 12306 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12207 |
| [Golan] p. 1 | Remark | srgisid 13992 |
| [Golan] p. 1 | Definition | df-srg 13970 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1495 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13587 mndideu 13502 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13614 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13643 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13654 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13676 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16628 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1465 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1466 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1468 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7433 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6662 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16622 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8830 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7683 df-imp 7682 df-iplp 7681 df-reap 8748 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8844 rerecapb 9016 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6295 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7875 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16267 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16615 dceqnconst 16614 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8113 caucvgpr 7895 caucvgprpr 7925 caucvgsr 8015 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7679 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16620 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4392 ltpopr 7808 ltsopr 7809 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8779 reapcotr 8771 reapirr 8750 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8299 gt0add 8746 leadd1 8603 lelttr 8261 lemul1a 9031 lenlt 8248 ltadd1 8602 ltletr 8262 ltmul1 8765 reaplt 8761 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16236 |
| [Jech] p. 4 | Definition of class | cv 1394 cvjust 2224 |
| [Jech] p. 78 | Note | opthprc 4775 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1576 |
| [Kreyszig] p. 3 | Property M1 | metcl 15070 xmetcl 15069 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15077 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8841 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15159 |
| [Kreyszig] p. 19 | Remark | mopntopon 15160 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15205 mopnm 15165 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15203 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15208 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15230 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14930 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14337 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14328 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14329 |
| [Kunen] p. 10 | Axiom 0 | a9e 1742 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4204 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6824 mapvalg 6822 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6818 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3978 |
| [Lang] p. 3 | Statement | lidrideqd 13457 mndbn0 13507 |
| [Lang] p. 3 | Definition | df-mnd 13493 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13474 |
| [Lang] p. 5 | Equation | gsumfzreidx 13917 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13708 |
| [Lang] p. 7 | Definition | dfgrp2e 13604 |
| [Levy] p. 338 | Axiom | df-clab 2216 df-clel 2225 df-cleq 2222 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1465 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1466 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1468 |
| [Margaris] p. 40 | Rule C | exlimiv 1644 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 858 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 897 exalim 1548 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 655 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1684 r19.2m 3579 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1600 19.3h 1599 rr19.3v 2943 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1524 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1665 alexim 1691 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1545 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1636 spsbe 1888 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1690 19.9h 1689 19.9v 1917 exlimd 1643 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1710 excomim 1709 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1711 r19.12 2637 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1692 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1514 ralbi 2663 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1601 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1602 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1650 rexbi 2664 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1712 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1503 alimd 1567 alimdh 1513 alimdv 1925 ralimdaa 2596 ralimdv 2598 ralimdva 2597 ralimdvva 2599 sbcimdv 3095 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1713 19.21 1629 19.21bi 1604 19.21h 1603 19.21ht 1627 19.21t 1628 19.21v 1919 alrimd 1656 alrimdd 1655 alrimdh 1525 alrimdv 1922 alrimi 1568 alrimih 1515 alrimiv 1920 alrimivv 1921 r19.21 2606 r19.21be 2621 r19.21bi 2618 r19.21t 2605 r19.21v 2607 ralrimd 2608 ralrimdv 2609 ralrimdva 2610 ralrimdvv 2614 ralrimdvva 2615 ralrimi 2601 ralrimiv 2602 ralrimiva 2603 ralrimivv 2611 ralrimivva 2612 ralrimivvva 2613 ralrimivw 2604 rexlimi 2641 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1927 2eximdv 1928 exim 1645 eximd 1658 eximdh 1657 eximdv 1926 rexim 2624 reximdai 2628 reximddv 2633 reximddv2 2635 reximdv 2631 reximdv2 2629 reximdva 2632 reximdvai 2630 reximi2 2626 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1724 19.23bi 1638 19.23h 1544 19.23ht 1543 19.23t 1723 19.23v 1929 19.23vv 1930 exlimd2 1641 exlimdh 1642 exlimdv 1865 exlimdvv 1944 exlimi 1640 exlimih 1639 exlimiv 1644 exlimivv 1943 r19.23 2639 r19.23v 2640 rexlimd 2645 rexlimdv 2647 rexlimdv3a 2650 rexlimdva 2648 rexlimdva2 2651 rexlimdvaa 2649 rexlimdvv 2655 rexlimdvva 2656 rexlimdvw 2652 rexlimiv 2642 rexlimiva 2643 rexlimivv 2654 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1685 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1672 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1528 19.26-3an 1529 19.26 1527 r19.26-2 2660 r19.26-3 2661 r19.26 2657 r19.26m 2662 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1607 19.27h 1606 19.27v 1946 r19.27av 2666 r19.27m 3588 r19.27mv 3589 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1609 19.28h 1608 19.28v 1947 r19.28av 2667 r19.28m 3582 r19.28mv 3585 rr19.28v 2944 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1666 19.29r 1667 19.29r2 1668 19.29x 1669 r19.29 2668 r19.29d2r 2675 r19.29r 2669 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1673 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1727 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1725 19.32r 1726 r19.32r 2677 r19.32vdc 2680 r19.32vr 2679 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1530 19.33b2 1675 19.33bdc 1676 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1730 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1670 19.35i 1671 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1719 19.36aiv 1948 19.36i 1718 r19.36av 2682 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1720 19.37aiv 1721 r19.37 2683 r19.37av 2684 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1722 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1686 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1678 19.40 1677 r19.40 2685 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1732 19.41h 1731 19.41v 1949 19.41vv 1950 19.41vvv 1951 19.41vvvv 1952 r19.41 2686 r19.41v 2687 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1734 19.42h 1733 19.42v 1953 19.42vv 1958 19.42vvv 1959 19.42vvvv 1960 r19.42v 2688 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1674 r19.43 2689 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1728 r19.44av 2690 r19.44mv 3587 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1729 r19.45av 2691 r19.45mv 3586 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2102 |
| [Megill] p. 444 | Axiom C5 | ax-17 1572 |
| [Megill] p. 445 | Lemma L12 | alequcom 1561 ax-10 1551 |
| [Megill] p. 446 | Lemma L17 | equtrr 1756 |
| [Megill] p. 446 | Lemma L19 | hbnae 1767 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1809 sbid 1820 |
| [Megill] p. 448 | Scheme C5' | ax-4 1556 |
| [Megill] p. 448 | Scheme C6' | ax-7 1494 |
| [Megill] p. 448 | Scheme C8' | ax-8 1550 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1553 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1762 |
| [Megill] p. 448 | Scheme C12' | ax-13 2202 |
| [Megill] p. 448 | Scheme C13' | ax-14 2203 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1869 |
| [Megill] p. 448 | Scheme C16' | ax-16 1860 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1776 dral2 1777 drex1 1844 drex2 1778 drsb1 1845 drsb2 1887 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2038 sbequ 1886 sbid2v 2047 |
| [Megill] p. 450 | Example in Appendix | hba1 1586 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3113 rspsbca 3114 stdpc4 1821 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3119 stdpc5 1630 |
| [Mendelson] p. 81 | Rule C | exlimiv 1644 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1749 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1816 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3529 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3530 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3445 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3493 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3446 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3336 |
| [Mendelson] p. 231 | Definition of union | unssin 3444 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4571 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3890 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4377 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4378 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4379 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3911 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4857 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5255 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4466 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7026 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7000 xpsneng 7001 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7006 xpcomeng 7007 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7009 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7003 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6816 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6981 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7031 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6850 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6982 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7425 djucomen 7424 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7423 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6630 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3427 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4812 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4813 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4149 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5250 coi2 5251 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4943 rn0 4986 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5139 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4833 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4950 rnxpm 5164 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4804 xp0 5154 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5093 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5090 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5089 imaexg 5088 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5085 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5773 funfvop 5755 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5683 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5693 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5368 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5904 dff13f 5906 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5872 funrnex 6271 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5898 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5218 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3942 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6313 df-1st 6298 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6314 df-2nd 6299 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1493 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1550 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1552 ax-11o 1869 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1873 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1494 |
| [Monk2] p. 109 | Lemma 15 | equvin 1909 equvini 1804 eqvinop 4333 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1572 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1697 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1494 |
| [Monk2] p. 114 | Lemma 22 | hba1 1586 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1598 nfia1 1626 |
| [Monk2] p. 114 | Lemma 24 | hba2 1597 nfa2 1625 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 836 dftest 16629 |
| [Munkres] p. 77 | Example 2 | distop 14802 |
| [Munkres] p. 78 | Definition of basis | df-bases 14760 isbasis3g 14763 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13336 tgval2 14768 |
| [Munkres] p. 79 | Remark | tgcl 14781 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14775 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14796 tgss3 14795 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14797 basgen2 14798 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14887 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14829 topcld 14826 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14830 |
| [Munkres] p. 94 | Definition of closure | clsval 14828 |
| [Munkres] p. 94 | Definition of interior | ntrval 14827 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14905 iscn 14914 iscn2 14917 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14947 cncnp2m 14948 cncnpi 14945 df-cnp 14906 iscnp 14916 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15231 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7088 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7357 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7345 omniwomnimkv 7360 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3315 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7328 exmidomniim 7334 finomni 7333 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7313 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16573 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16577 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7095 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7405 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7406 exmidfodomrlemrALT 7407 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7342 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16559 peano4nninf 16558 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16561 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16569 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16571 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16557 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2216 rabid 2707 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2042 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2222 |
| [Quine] p. 19 | Definition 2.9 | df-v 2802 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2338 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2350 abid2f 2398 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1934 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1932 sb6 1933 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2225 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2229 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2231 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3030 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3031 dfsbcq2 3032 |
| [Quine] p. 43 | Theorem 6.8 | vex 2803 |
| [Quine] p. 43 | Theorem 6.9 | isset 2807 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2886 spcgv 2891 spcimgf 2884 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3041 spsbcd 3042 |
| [Quine] p. 44 | Theorem 6.12 | elex 2812 |
| [Quine] p. 44 | Theorem 6.13 | elab 2948 elabg 2950 elabgf 2946 |
| [Quine] p. 44 | Theorem 6.14 | noel 3496 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3732 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3674 df-sn 3673 |
| [Quine] p. 49 | Theorem 7.4 | snss 3806 snssg 3805 |
| [Quine] p. 49 | Theorem 7.5 | prss 3827 prssg 3828 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3775 prid1g 3773 prid2 3776 prid2g 3774 snid 3698 snidg 3696 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4272 snexprc 4274 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4299 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3907 unisng 3908 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3910 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3919 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3918 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5295 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5285 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5296 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5300 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5301 |
| [Quine] p. 58 | Definition 9.1 | df-op 3676 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4348 opabidw 4349 opelopab 4364 opelopaba 4358 opelopabaf 4366 opelopabf 4367 opelopabg 4360 opelopabga 4355 opelopabgf 4362 oprabid 6045 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4729 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4731 |
| [Quine] p. 64 | Definition 9.15 | df-id 4388 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5385 |
| [Quine] p. 65 | Theorem 10.4 | funi 5356 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5375 funsng 5373 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5326 |
| [Quine] p. 65 | Definition 10.2 | args 5103 dffv4g 5632 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5332 fv2 5630 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10979 nn0opth2d 10978 nn0opthd 10977 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5412 funimaexg 5411 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13939 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14004 |
| [Rudin] p. 164 | Equation 27 | efcan 12230 |
| [Rudin] p. 164 | Equation 30 | efzval 12237 |
| [Rudin] p. 167 | Equation 48 | absefi 12323 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1468 |
| [Sanford] p. 39 | Rule 4 | mptxor 1466 |
| [Sanford] p. 40 | Rule 1 | mptnan 1465 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5119 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5121 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5118 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5116 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14006 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14800 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3470 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3564 dif0 3563 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3577 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3463 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3464 |
| [Stoll] p. 20 | Remark | invdif 3447 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3677 |
| [Stoll] p. 43 | Definition | uniiun 4022 |
| [Stoll] p. 44 | Definition | intiin 4023 |
| [Stoll] p. 45 | Definition | df-iin 3971 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3970 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 894 imanst 893 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3470 |
| [Suppes] p. 22 | Theorem 2 | eq0 3511 |
| [Suppes] p. 22 | Theorem 4 | eqss 3240 eqssd 3242 eqssi 3241 |
| [Suppes] p. 23 | Theorem 5 | ss0 3533 ss0b 3532 |
| [Suppes] p. 23 | Theorem 6 | sstr 3233 |
| [Suppes] p. 25 | Theorem 12 | elin 3388 elun 3346 |
| [Suppes] p. 26 | Theorem 15 | inidm 3414 |
| [Suppes] p. 26 | Theorem 16 | in0 3527 |
| [Suppes] p. 27 | Theorem 23 | unidm 3348 |
| [Suppes] p. 27 | Theorem 24 | un0 3526 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3368 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3375 |
| [Suppes] p. 27 | Theorem 27 | unss 3379 |
| [Suppes] p. 27 | Theorem 28 | indir 3454 |
| [Suppes] p. 27 | Theorem 29 | undir 3455 |
| [Suppes] p. 28 | Theorem 32 | difid 3561 difidALT 3562 |
| [Suppes] p. 29 | Theorem 33 | difin 3442 |
| [Suppes] p. 29 | Theorem 34 | indif 3448 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3567 |
| [Suppes] p. 29 | Theorem 36 | difun2 3572 |
| [Suppes] p. 29 | Theorem 37 | difin0 3566 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3565 |
| [Suppes] p. 29 | Theorem 39 | difundi 3457 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3459 |
| [Suppes] p. 30 | Theorem 41 | nalset 4217 |
| [Suppes] p. 39 | Theorem 61 | uniss 3912 |
| [Suppes] p. 39 | Theorem 65 | uniop 4346 |
| [Suppes] p. 41 | Theorem 70 | intsn 3961 |
| [Suppes] p. 42 | Theorem 71 | intpr 3958 intprg 3959 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4573 op1stbg 4574 |
| [Suppes] p. 42 | Theorem 78 | intun 3957 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4002 dfiun2g 4000 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4003 |
| [Suppes] p. 47 | Theorem 86 | elpw 3656 elpw2 4245 elpw2g 4244 elpwg 3658 |
| [Suppes] p. 47 | Theorem 87 | pwid 3665 |
| [Suppes] p. 47 | Theorem 89 | pw0 3818 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3886 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4831 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4863 xpindir 4864 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4780 xpundir 4781 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4644 |
| [Suppes] p. 58 | Theorem 2 | relss 4811 |
| [Suppes] p. 59 | Theorem 4 | eldm 4926 eldm2 4927 eldm2g 4925 eldmg 4924 |
| [Suppes] p. 59 | Definition 3 | df-dm 4733 |
| [Suppes] p. 60 | Theorem 6 | dmin 4937 |
| [Suppes] p. 60 | Theorem 8 | rnun 5143 |
| [Suppes] p. 60 | Theorem 9 | rnin 5144 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4916 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4911 brcnvg 4909 |
| [Suppes] p. 62 | Equation 5 | elcnv 4905 elcnv2 4906 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5112 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5142 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5140 |
| [Suppes] p. 63 | Theorem 20 | co02 5248 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5000 |
| [Suppes] p. 63 | Definition 7 | df-co 4732 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4913 |
| [Suppes] p. 64 | Theorem 27 | coass 5253 |
| [Suppes] p. 65 | Theorem 31 | resundi 5024 |
| [Suppes] p. 65 | Theorem 34 | elima 5079 elima2 5080 elima3 5081 elimag 5078 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5147 |
| [Suppes] p. 66 | Theorem 40 | dminss 5149 |
| [Suppes] p. 66 | Theorem 41 | imainss 5150 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5153 |
| [Suppes] p. 81 | Definition 34 | dfec2 6700 |
| [Suppes] p. 82 | Theorem 72 | elec 6738 elecg 6737 |
| [Suppes] p. 82 | Theorem 73 | erth 6743 erth2 6744 |
| [Suppes] p. 89 | Theorem 96 | map0b 6851 |
| [Suppes] p. 89 | Theorem 97 | map0 6853 map0g 6852 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6854 |
| [Suppes] p. 89 | Theorem 99 | mapss 6855 |
| [Suppes] p. 92 | Theorem 1 | enref 6933 enrefg 6932 |
| [Suppes] p. 92 | Theorem 2 | ensym 6950 ensymb 6949 ensymi 6951 |
| [Suppes] p. 92 | Theorem 3 | entr 6953 |
| [Suppes] p. 92 | Theorem 4 | unen 6986 |
| [Suppes] p. 94 | Theorem 15 | endom 6931 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6947 |
| [Suppes] p. 94 | Theorem 17 | domtr 6954 |
| [Suppes] p. 95 | Theorem 18 | isbth 7160 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6976 fundmeng 6977 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7013 |
| [Suppes] p. 130 | Definition 3 | df-tr 4186 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4584 |
| [Suppes] p. 134 | Definition 6 | df-suc 4466 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4699 finds 4696 finds1 4698 finds2 4697 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7566 df-ltpq 7559 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4485 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2211 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2222 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2225 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2247 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6017 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3028 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3688 elpr2 3689 elprg 3687 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3683 elsn2 3701 elsn2g 3700 elsng 3682 velsn 3684 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4321 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3678 sneqr 3841 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3686 dfsn2 3681 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4532 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4327 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4305 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4536 unexg 4538 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3716 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3892 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3204 df-un 3202 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3905 uniprg 3906 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4267 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3715 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4501 elsucg 4499 sstr2 3232 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3349 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3397 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3362 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3415 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3452 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3453 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3213 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3652 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3376 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3211 dfss2 3215 sseqin2 3424 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3245 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3425 inss2 3426 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3285 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3900 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4306 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4313 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2517 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4214 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3200 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3494 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3561 difidALT 3562 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3505 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4635 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2802 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4219 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3531 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4224 ssexg 4226 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4221 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4646 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4637 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3557 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3330 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3466 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3331 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3339 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2513 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2514 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4840 xpexg 4838 xpexgALT 6290 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4730 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5391 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5550 fun11 5394 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5335 svrelfun 5392 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4915 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4917 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4735 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4736 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4732 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5189 dfrel2 5185 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4832 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4842 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4848 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4862 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5039 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5016 opelresg 5018 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5032 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5035 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5040 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5365 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5233 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5364 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5551 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2122 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5332 fv3 5658 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5273 cnvexg 5272 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4997 dmexg 4994 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4998 rnexg 4995 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5652 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5662 tz6.12 5663 tz6.12c 5665 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5626 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5327 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5328 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5330 wfo 5322 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5329 wf1 5321 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5331 wf1o 5323 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5740 eqfnfv2 5741 eqfnfv2f 5744 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5712 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5871 fnexALT 6268 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5870 resfunexgALT 6265 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5412 funimaexg 5411 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4087 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5104 iniseg 5106 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4384 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5333 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5946 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5947 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5952 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5954 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5962 |
| [TakeutiZaring] p. 35 | Notation | wtr 4185 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4449 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4189 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4672 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4476 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4480 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4588 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4463 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4582 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4648 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4678 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4187 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4607 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4583 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3919 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4466 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4510 sucidg 4511 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4597 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4464 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4602 ordelsuc 4601 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4690 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4691 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4692 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4689 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4703 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4695 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4693 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4694 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3940 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4201 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3941 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4613 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3927 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6469 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6526 tfri1d 6496 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6527 tfri2d 6497 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6528 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6463 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6447 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6627 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6623 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6620 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6624 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6672 nnaordi 6671 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4013 uniss2 3922 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6633 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6643 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6634 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6621 omsuc 6635 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6644 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6680 nnmordi 6679 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6622 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7385 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6964 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7038 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7039 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6907 isfi 6929 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7010 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6814 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7016 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7029 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1556 |
| [Tarski] p. 68 | Lemma 6 | equid 1747 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1750 |
| [Tarski] p. 70 | Lemma 14 | spim 1784 spime 1787 spimeh 1785 spimh 1783 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1552 ax-11o 1869 ax11i 1760 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1933 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1572 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2202 ax-14 2203 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 716 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 732 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 761 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 770 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 794 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 619 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 646 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 842 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2176 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 742 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 841 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 632 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 890 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 848 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 861 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 645 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 858 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 860 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 717 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 780 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 620 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 624 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 898 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 912 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 773 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 774 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 809 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 810 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 808 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1003 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 783 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 781 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 782 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 743 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 744 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 872 pm2.5gdc 871 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 867 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 745 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 659 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 660 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 727 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 896 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 730 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 731 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 870 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 753 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 805 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 806 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 663 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 718 pm2.67 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 874 pm2.521gdc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 752 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 899 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 920 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 811 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 812 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 910 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 759 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 963 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 964 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 965 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 758 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 264 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 265 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 698 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 347 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 261 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 262 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 865 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 864 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 345 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 346 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 693 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 599 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 333 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 331 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 332 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 760 pm3.44 720 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 604 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 790 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 876 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 877 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 895 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 699 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 958 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 762 pm4.25 763 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 823 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 733 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 772 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 797 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 607 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 827 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1004 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 821 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 977 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 955 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 784 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 819 pm4.45 789 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1527 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 962 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 902 imorr 726 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 904 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 755 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 756 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 944 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 757 pm4.56 785 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 945 oranim 786 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 690 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 903 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 891 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 691 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 892 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 832 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 749 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 605 pm4.76 606 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 715 pm4.77 804 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 787 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 908 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 712 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 913 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 956 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 957 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 237 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 240 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 557 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 603 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 914 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 915 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 916 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1431 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 833 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 909 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1436 pm5.18dc 888 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 711 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 700 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1434 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1439 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1440 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 900 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 475 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 242 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 931 pm5.6r 932 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 960 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 453 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 611 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 922 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 612 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 250 pm5.41 251 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 320 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 930 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 807 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 923 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 918 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 799 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 951 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 952 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 967 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 244 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 179 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 968 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1681 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1531 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1678 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1942 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2080 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2481 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2482 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2942 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3086 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5304 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5305 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2157 eupickbi 2160 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5332 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7389 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |