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 7270 fidcenum 7111 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7111 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7270 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 12982 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7082 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7068 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 12997 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 12999 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 12988 znnen 12955 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13000 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13001 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 10985 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4626 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11112 df-pfx 11191 df-substr 11164 df-word 11059 lencl 11062 wrd0 11083 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8314 addcan2d 8319 addcan2i 8317 addcand 8318 addcani 8316 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8325 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8382 negsubd 8451 negsubi 8412 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8384 negnegd 8436 negnegi 8404 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8519 subdid 8548 subdii 8541 subdir 8520 subdird 8549 subdiri 8542 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8523 mul01d 8527 mul01i 8525 mul02 8521 mul02d 8526 mul02i 8524 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8928 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8879 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8532 mul2negd 8547 mul2negi 8540 mulneg1 8529 mulneg1d 8545 mulneg1i 8538 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14093 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8848 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9861 rpaddcld 9896 rpmulcl 9862 rpmulcld 9897 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9873 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8239 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8673 ltadd1dd 8691 ltadd1i 8637 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8727 ltmul1a 8726 ltmul1i 9055 ltmul1ii 9063 ltmul2 8991 ltmul2d 9923 ltmul2dd 9937 ltmul2i 9058 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8261 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8603 lt0neg1d 8650 ltneg 8597 ltnegd 8658 ltnegi 8628 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8580 lt2addd 8702 lt2addi 8645 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9838 |
| [Apostol] p. 21 | Exercise 4 | recgt0 8985 recgt0d 9069 recgt0i 9041 recgt0ii 9042 |
| [Apostol] p. 22 | Definition of integers | df-z 9435 |
| [Apostol] p. 22 | Definition of rationals | df-q 9803 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7149 |
| [Apostol] p. 26 | Theorem I.29 | arch 9354 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9554 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9355 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10463 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12368 zneo 9536 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11528 sqrtthi 11616 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9101 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12543 |
| [Apostol] p. 363 | Remark | absgt0api 11643 |
| [Apostol] p. 363 | Example | abssubd 11690 abssubi 11647 |
| [ApostolNT] p. 14 | Definition | df-dvds 12285 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12301 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12325 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12321 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12315 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12317 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12302 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12303 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12308 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12342 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12344 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12346 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12521 |
| [ApostolNT] p. 16 | Definition | isprm2 12625 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12600 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13012 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12480 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12522 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12524 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12494 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12487 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12652 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12654 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12877 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12421 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12567 |
| [ApostolNT] p. 25 | Definition | df-phi 12719 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12749 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12730 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12734 |
| [ApostolNT] p. 38 | Remark | df-sgm 15641 |
| [ApostolNT] p. 38 | Definition | df-sgm 15641 |
| [ApostolNT] p. 104 | Definition | congr 12608 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12288 |
| [ApostolNT] p. 106 | Definition | moddvds 12296 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12375 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12376 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10550 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10587 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10875 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12320 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12611 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12930 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12613 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12741 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12760 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12742 |
| [ApostolNT] p. 179 | Definition | df-lgs 15662 lgsprme0 15706 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15707 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15683 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15698 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15749 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15768 2lgsoddprm 15777 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15733 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15744 |
| [ApostolNT] p. 188 | Definition | df-lgs 15662 lgs1 15708 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15699 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15701 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15709 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15710 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 619 pm2.65 663 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5993 onsucelsucexmidlem 4618 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16294 |
| [Bauer], p. 483 | Definition | n0rf 3504 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15635 2irrexpqap 15637 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 7026 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15312 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15302 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8780 |
| [BauerSwan], p. 14 | Remark | 0ct 7262 ctm 7264 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16297 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7270 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7676 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7589 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7678 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7712 addlocpr 7711 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7738 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7741 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7746 |
| [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 4204 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4260 |
| [BellMachover] p. 466 | Axiom Union | axun2 4523 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4631 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4472 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4634 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4585 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4457 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4678 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4703 |
| [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 15844 isuhgropm 15866 isusgropen 15948 isuspgropen 15947 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15855 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13375 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13421 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13436 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13947 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13882 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5900 fcofo 5901 |
| [BourbakiTop1] p. | Remark | xnegmnf 10013 xnegpnf 10012 |
| [BourbakiTop1] p. | Remark | rexneg 10014 |
| [BourbakiTop1] p. | Proposition | ishmeo 14963 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14816 |
| [BourbakiTop1] p. | Property V_ii | innei 14822 |
| [BourbakiTop1] p. | Property V_iv | neissex 14824 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14813 neiss 14809 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14881 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 14958 |
| [BourbakiTop1] p. | Property V_iii | elnei 14811 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14657 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13375 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13421 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13618 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4146 |
| [Church] p. 129 | Section II.24 | df-ifp 984 dfifp2dc 987 |
| [Cohen] p. 301 | Remark | relogoprlem 15527 |
| [Cohen] p. 301 | Property 2 | relogmul 15528 relogmuld 15543 |
| [Cohen] p. 301 | Property 3 | relogdiv 15529 relogdivd 15544 |
| [Cohen] p. 301 | Property 4 | relogexp 15531 |
| [Cohen] p. 301 | Property 1a | log1 15525 |
| [Cohen] p. 301 | Property 1b | loge 15526 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15624 |
| [Cohen4] p. 352 | Definition | rpelogb 15608 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15614 |
| [Cohen4] p. 361 | Property 3 | logbrec 15619 rprelogbdiv 15616 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15612 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15617 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15606 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15607 |
| [Cohen4] p. 367 | Property | rplogbchbase 15609 |
| [Cohen4] p. 377 | Property 2 | logblt 15621 |
| [Crosilla] p. | Axiom 1 | ax-ext 2211 |
| [Crosilla] p. | Axiom 2 | ax-pr 4292 |
| [Crosilla] p. | Axiom 3 | ax-un 4521 |
| [Crosilla] p. | Axiom 4 | ax-nul 4209 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4677 |
| [Crosilla] p. | Axiom 6 | ru 3027 |
| [Crosilla] p. | Axiom 8 | ax-pow 4257 |
| [Crosilla] p. | Axiom 9 | ax-setind 4626 |
| [Crosilla], p. | Axiom 6 | ax-sep 4201 |
| [Crosilla], p. | Axiom 7 | ax-coll 4198 |
| [Crosilla], p. | Axiom 7' | repizf 4199 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4610 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5993 |
| [Crosilla], p. | Definition of ordinal | df-iord 4454 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4624 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15855 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3199 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4680 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6787 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4208 |
| [Enderton] p. 19 | Definition | df-tp 3674 |
| [Enderton] p. 26 | Exercise 5 | unissb 3917 |
| [Enderton] p. 26 | Exercise 10 | pwel 4303 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4374 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4034 iinin2m 4033 iunin1 4029 iunin2 4028 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4032 iundif2ss 4030 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4047 |
| [Enderton] p. 33 | Exercise 25 | iununir 4048 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4055 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4568 iunpwss 4056 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4302 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4275 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4538 rnex 4988 rnexg 4985 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4930 rnuni 5136 |
| [Enderton] p. 42 | Definition of a function | dffun7 5341 dffun8 5342 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5691 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5378 |
| [Enderton] p. 44 | Definition (d) | dfima2 5066 dfima3 5067 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5696 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7376 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5878 |
| [Enderton] p. 52 | Definition | df-map 6787 |
| [Enderton] p. 53 | Exercise 21 | coass 5243 |
| [Enderton] p. 53 | Exercise 27 | dmco 5233 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5388 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5100 |
| [Enderton] p. 54 | Remark | ixpf 6857 ixpssmap 6869 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6836 |
| [Enderton] p. 56 | Theorem 3M | erref 6690 |
| [Enderton] p. 57 | Lemma 3N | erthi 6718 |
| [Enderton] p. 57 | Definition | df-ec 6672 |
| [Enderton] p. 58 | Definition | df-qs 6676 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6777 th3qcor 6776 th3qlem1 6774 th3qlem2 6775 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6672 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4927 |
| [Enderton] p. 68 | Definition of successor | df-suc 4459 |
| [Enderton] p. 71 | Definition | df-tr 4182 dftr4 4186 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4501 unisucg 4502 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4501 unisucg 4502 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4195 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4196 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6610 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6612 onasuc 6602 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5997 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6611 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6613 onmsuc 6609 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6621 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6614 nnacom 6620 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6622 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6623 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6625 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6615 nnmsucr 6624 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6664 |
| [Enderton] p. 129 | Definition | df-en 6878 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5945 |
| [Enderton] p. 133 | Exercise 1 | xpomen 12952 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7015 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7006 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 6995 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7388 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7384 dju1en 7383 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3567 |
| [Enderton] p. 145 | Figure 38 | ffoss 5600 |
| [Enderton] p. 145 | Definition | df-dom 6879 |
| [Enderton] p. 146 | Example 1 | domen 6890 domeng 6891 |
| [Enderton] p. 146 | Example 3 | nndomo 7013 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6982 xpdom1g 6980 xpdom2g 6979 |
| [Enderton] p. 168 | Definition | df-po 4384 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4516 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4477 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4632 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4480 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4605 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4578 |
| [Enderton] p. 194 | Remark | onprc 4641 |
| [Enderton] p. 194 | Exercise 16 | suc11 4647 |
| [Enderton] p. 197 | Definition | df-card 7339 |
| [Enderton] p. 200 | Exercise 25 | tfis 4672 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4643 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4645 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4646 |
| [Geuvers], p. 1 | Remark | expap0 10778 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8750 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8789 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8751 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8106 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11700 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11708 maxle2 11709 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11710 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11713 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11714 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8717 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7522 enqer 7533 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7526 df-nqqs 7523 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7519 df-plqqs 7524 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7520 df-mqqs 7525 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7527 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7583 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7586 ltbtwnnq 7591 ltbtwnnqq 7590 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7575 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7576 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7712 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7754 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7753 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7772 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7788 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7794 ltaprlem 7793 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7791 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7747 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7767 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7756 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7755 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7763 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7813 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7901 enrer 7910 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7906 df-1r 7907 df-nr 7902 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7904 df-plr 7903 negexsr 7947 recexsrlem 7949 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7905 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9095 creur 9094 cru 8737 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8098 axcnre 8056 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11355 crimd 11474 crimi 11434 crre 11354 crred 11473 crrei 11433 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11357 remimd 11439 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11554 absval2d 11682 absval2i 11641 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11381 cjaddd 11462 cjaddi 11429 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11382 cjmuld 11463 cjmuli 11430 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11380 cjcjd 11440 cjcji 11412 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11379 cjreb 11363 cjrebd 11443 cjrebi 11415 cjred 11468 rere 11362 rereb 11360 rerebd 11442 rerebi 11414 rered 11466 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11388 addcjd 11454 addcji 11424 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11498 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11549 abscjd 11687 abscji 11645 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11561 abs00d 11683 abs00i 11642 absne0d 11684 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11593 releabsd 11688 releabsi 11646 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11566 absmuld 11691 absmuli 11648 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11552 sqabsaddi 11649 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11601 abstrid 11693 abstrii 11652 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10748 exp0 10752 expp1 10755 expp1d 10883 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10790 expaddd 10884 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15571 cxpmuld 15596 expmul 10793 expmuld 10885 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10787 mulexpd 10897 rpmulcxp 15568 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10194 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11823 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11825 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11824 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11828 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11821 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11817 climcj 11818 climim 11820 climre 11819 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8174 df-xr 8173 ltxr 9959 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11844 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10507 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14494 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15023 xmet0 15022 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15030 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15032 mstri 15132 xmettri 15031 xmstri 15131 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14938 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15170 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11807 addcncntop 15221 mulcn2 11809 mulcncntop 15223 subcn2 11808 subcncntop 15222 |
| [Gleason] p. 295 | Remark | bcval3 10960 bcval4 10961 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10975 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10958 df-bc 10957 |
| [Gleason] p. 296 | Remark | bcn0 10964 bcnn 10966 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 11981 |
| [Gleason] p. 308 | Equation 2 | ef0 12169 |
| [Gleason] p. 308 | Equation 3 | efcj 12170 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12175 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12179 |
| [Gleason] p. 310 | Equation 14 | sinadd 12233 |
| [Gleason] p. 310 | Equation 15 | cosadd 12234 |
| [Gleason] p. 311 | Equation 17 | sincossq 12245 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12250 sinbnd 12249 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12150 |
| [Golan] p. 1 | Remark | srgisid 13935 |
| [Golan] p. 1 | Definition | df-srg 13913 |
| [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 13530 mndideu 13445 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13557 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13586 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13597 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13619 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16373 |
| [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 7395 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6635 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16367 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8792 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7645 df-imp 7644 df-iplp 7643 df-reap 8710 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8806 rerecapb 8978 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6273 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7837 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16015 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16360 dceqnconst 16359 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8075 caucvgpr 7857 caucvgprpr 7887 caucvgsr 7977 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7641 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16365 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4385 ltpopr 7770 ltsopr 7771 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8741 reapcotr 8733 reapirr 8712 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8261 gt0add 8708 leadd1 8565 lelttr 8223 lemul1a 8993 lenlt 8210 ltadd1 8564 ltletr 8224 ltmul1 8727 reaplt 8723 |
| [Jech] p. 4 | Definition of class | cv 1394 cvjust 2224 |
| [Jech] p. 78 | Note | opthprc 4767 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1576 |
| [Kreyszig] p. 3 | Property M1 | metcl 15012 xmetcl 15011 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15019 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8803 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15101 |
| [Kreyszig] p. 19 | Remark | mopntopon 15102 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15147 mopnm 15107 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15145 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15150 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15172 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14872 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14279 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14270 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14271 |
| [Kunen] p. 10 | Axiom 0 | a9e 1742 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4200 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6797 mapvalg 6795 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6791 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3974 |
| [Lang] p. 3 | Statement | lidrideqd 13400 mndbn0 13450 |
| [Lang] p. 3 | Definition | df-mnd 13436 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13417 |
| [Lang] p. 5 | Equation | gsumfzreidx 13860 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13651 |
| [Lang] p. 7 | Definition | dfgrp2e 13547 |
| [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 3578 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1600 19.3h 1599 rr19.3v 2942 |
| [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 3094 |
| [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 3587 r19.27mv 3588 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1609 19.28h 1608 19.28v 1947 r19.28av 2667 r19.28m 3581 r19.28mv 3584 rr19.28v 2943 |
| [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 3586 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1729 r19.45av 2691 r19.45mv 3585 |
| [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 3112 rspsbca 3113 stdpc4 1821 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3118 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 3528 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3529 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3444 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3492 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3445 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3335 |
| [Mendelson] p. 231 | Definition of union | unssin 3443 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4564 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3886 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4370 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4371 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4372 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3907 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4848 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5245 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4459 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 6994 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6968 xpsneng 6969 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6974 xpcomeng 6975 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6977 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6971 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6789 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6954 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 6999 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6823 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6955 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7387 djucomen 7386 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7385 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6603 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3426 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4804 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4805 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4145 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5240 coi2 5241 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4934 rn0 4976 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5129 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4825 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4940 rnxpm 5154 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4796 xp0 5144 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5083 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5080 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5079 imaexg 5078 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5075 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5758 funfvop 5740 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5669 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5678 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5358 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5885 dff13f 5887 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5855 funrnex 6249 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5879 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5208 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3938 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6291 df-1st 6276 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6292 df-2nd 6277 |
| [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 4328 |
| [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 16374 |
| [Munkres] p. 77 | Example 2 | distop 14744 |
| [Munkres] p. 78 | Definition of basis | df-bases 14702 isbasis3g 14705 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13279 tgval2 14710 |
| [Munkres] p. 79 | Remark | tgcl 14723 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14717 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14738 tgss3 14737 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14739 basgen2 14740 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14829 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14771 topcld 14768 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14772 |
| [Munkres] p. 94 | Definition of closure | clsval 14770 |
| [Munkres] p. 94 | Definition of interior | ntrval 14769 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14847 iscn 14856 iscn2 14859 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14889 cncnp2m 14890 cncnpi 14887 df-cnp 14848 iscnp 14858 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15173 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7053 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7319 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7307 omniwomnimkv 7322 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3314 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7290 exmidomniim 7296 finomni 7295 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7275 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16318 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16322 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7058 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7367 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7368 exmidfodomrlemrALT 7369 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7304 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16304 peano4nninf 16303 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16306 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16314 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16316 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16302 |
| [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 2801 |
| [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 3029 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3030 dfsbcq2 3031 |
| [Quine] p. 43 | Theorem 6.8 | vex 2802 |
| [Quine] p. 43 | Theorem 6.9 | isset 2806 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2885 spcgv 2890 spcimgf 2883 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3040 spsbcd 3041 |
| [Quine] p. 44 | Theorem 6.12 | elex 2811 |
| [Quine] p. 44 | Theorem 6.13 | elab 2947 elabg 2949 elabgf 2945 |
| [Quine] p. 44 | Theorem 6.14 | noel 3495 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3731 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3673 df-sn 3672 |
| [Quine] p. 49 | Theorem 7.4 | snss 3802 snssg 3801 |
| [Quine] p. 49 | Theorem 7.5 | prss 3823 prssg 3824 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3772 prid1g 3770 prid2 3773 prid2g 3771 snid 3697 snidg 3695 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4267 snexprc 4269 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4294 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3903 unisng 3904 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3906 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3915 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3914 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5285 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5275 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5286 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5290 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5291 |
| [Quine] p. 58 | Definition 9.1 | df-op 3675 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4343 opabidw 4344 opelopab 4359 opelopaba 4353 opelopabaf 4361 opelopabf 4362 opelopabg 4355 opelopabga 4350 opelopabgf 4357 oprabid 6026 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4722 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4724 |
| [Quine] p. 64 | Definition 9.15 | df-id 4381 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5375 |
| [Quine] p. 65 | Theorem 10.4 | funi 5346 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5365 funsng 5363 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5316 |
| [Quine] p. 65 | Definition 10.2 | args 5093 dffv4g 5620 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5322 fv2 5618 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10933 nn0opth2d 10932 nn0opthd 10931 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5402 funimaexg 5401 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13882 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13947 |
| [Rudin] p. 164 | Equation 27 | efcan 12173 |
| [Rudin] p. 164 | Equation 30 | efzval 12180 |
| [Rudin] p. 167 | Equation 48 | absefi 12266 |
| [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 5109 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5111 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5108 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5106 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 13949 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14742 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3469 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3563 dif0 3562 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3576 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3462 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3463 |
| [Stoll] p. 20 | Remark | invdif 3446 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3676 |
| [Stoll] p. 43 | Definition | uniiun 4018 |
| [Stoll] p. 44 | Definition | intiin 4019 |
| [Stoll] p. 45 | Definition | df-iin 3967 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3966 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 894 imanst 893 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3469 |
| [Suppes] p. 22 | Theorem 2 | eq0 3510 |
| [Suppes] p. 22 | Theorem 4 | eqss 3239 eqssd 3241 eqssi 3240 |
| [Suppes] p. 23 | Theorem 5 | ss0 3532 ss0b 3531 |
| [Suppes] p. 23 | Theorem 6 | sstr 3232 |
| [Suppes] p. 25 | Theorem 12 | elin 3387 elun 3345 |
| [Suppes] p. 26 | Theorem 15 | inidm 3413 |
| [Suppes] p. 26 | Theorem 16 | in0 3526 |
| [Suppes] p. 27 | Theorem 23 | unidm 3347 |
| [Suppes] p. 27 | Theorem 24 | un0 3525 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3367 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3374 |
| [Suppes] p. 27 | Theorem 27 | unss 3378 |
| [Suppes] p. 27 | Theorem 28 | indir 3453 |
| [Suppes] p. 27 | Theorem 29 | undir 3454 |
| [Suppes] p. 28 | Theorem 32 | difid 3560 difidALT 3561 |
| [Suppes] p. 29 | Theorem 33 | difin 3441 |
| [Suppes] p. 29 | Theorem 34 | indif 3447 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3566 |
| [Suppes] p. 29 | Theorem 36 | difun2 3571 |
| [Suppes] p. 29 | Theorem 37 | difin0 3565 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3564 |
| [Suppes] p. 29 | Theorem 39 | difundi 3456 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3458 |
| [Suppes] p. 30 | Theorem 41 | nalset 4213 |
| [Suppes] p. 39 | Theorem 61 | uniss 3908 |
| [Suppes] p. 39 | Theorem 65 | uniop 4341 |
| [Suppes] p. 41 | Theorem 70 | intsn 3957 |
| [Suppes] p. 42 | Theorem 71 | intpr 3954 intprg 3955 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4566 op1stbg 4567 |
| [Suppes] p. 42 | Theorem 78 | intun 3953 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3998 dfiun2g 3996 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3999 |
| [Suppes] p. 47 | Theorem 86 | elpw 3655 elpw2 4240 elpw2g 4239 elpwg 3657 |
| [Suppes] p. 47 | Theorem 87 | pwid 3664 |
| [Suppes] p. 47 | Theorem 89 | pw0 3814 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3882 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4823 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4854 xpindir 4855 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4772 xpundir 4773 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4637 |
| [Suppes] p. 58 | Theorem 2 | relss 4803 |
| [Suppes] p. 59 | Theorem 4 | eldm 4917 eldm2 4918 eldm2g 4916 eldmg 4915 |
| [Suppes] p. 59 | Definition 3 | df-dm 4726 |
| [Suppes] p. 60 | Theorem 6 | dmin 4928 |
| [Suppes] p. 60 | Theorem 8 | rnun 5133 |
| [Suppes] p. 60 | Theorem 9 | rnin 5134 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4907 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4902 brcnvg 4900 |
| [Suppes] p. 62 | Equation 5 | elcnv 4896 elcnv2 4897 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5102 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5132 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5130 |
| [Suppes] p. 63 | Theorem 20 | co02 5238 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4990 |
| [Suppes] p. 63 | Definition 7 | df-co 4725 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4904 |
| [Suppes] p. 64 | Theorem 27 | coass 5243 |
| [Suppes] p. 65 | Theorem 31 | resundi 5014 |
| [Suppes] p. 65 | Theorem 34 | elima 5069 elima2 5070 elima3 5071 elimag 5068 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5137 |
| [Suppes] p. 66 | Theorem 40 | dminss 5139 |
| [Suppes] p. 66 | Theorem 41 | imainss 5140 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5143 |
| [Suppes] p. 81 | Definition 34 | dfec2 6673 |
| [Suppes] p. 82 | Theorem 72 | elec 6711 elecg 6710 |
| [Suppes] p. 82 | Theorem 73 | erth 6716 erth2 6717 |
| [Suppes] p. 89 | Theorem 96 | map0b 6824 |
| [Suppes] p. 89 | Theorem 97 | map0 6826 map0g 6825 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6827 |
| [Suppes] p. 89 | Theorem 99 | mapss 6828 |
| [Suppes] p. 92 | Theorem 1 | enref 6906 enrefg 6905 |
| [Suppes] p. 92 | Theorem 2 | ensym 6923 ensymb 6922 ensymi 6924 |
| [Suppes] p. 92 | Theorem 3 | entr 6926 |
| [Suppes] p. 92 | Theorem 4 | unen 6959 |
| [Suppes] p. 94 | Theorem 15 | endom 6904 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6920 |
| [Suppes] p. 94 | Theorem 17 | domtr 6927 |
| [Suppes] p. 95 | Theorem 18 | isbth 7122 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6949 fundmeng 6950 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6981 |
| [Suppes] p. 130 | Definition 3 | df-tr 4182 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4577 |
| [Suppes] p. 134 | Definition 6 | df-suc 4459 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4692 finds 4689 finds1 4691 finds2 4690 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7528 df-ltpq 7521 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4478 |
| [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 5998 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3027 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3687 elpr2 3688 elprg 3686 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3682 elsn2 3700 elsn2g 3699 elsng 3681 velsn 3683 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4316 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3677 sneqr 3837 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3685 dfsn2 3680 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4525 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4322 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4300 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4529 unexg 4531 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3715 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3888 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3203 df-un 3201 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3901 uniprg 3902 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4262 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3714 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4494 elsucg 4492 sstr2 3231 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3348 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3396 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3361 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3414 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3451 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3452 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3212 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3651 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3375 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3210 dfss2 3214 sseqin2 3423 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3244 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3424 inss2 3425 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3284 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3896 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4301 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4308 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2517 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4210 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3199 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3493 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3560 difidALT 3561 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3504 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4628 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2801 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4215 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3530 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4220 ssexg 4222 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4217 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4639 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4630 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3556 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3329 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3465 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3330 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3338 |
| [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 4831 xpexg 4830 xpexgALT 6268 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4723 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5381 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5538 fun11 5384 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5325 svrelfun 5382 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4906 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4908 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4728 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4729 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4725 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5179 dfrel2 5175 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4824 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4833 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4839 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4853 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5029 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5006 opelresg 5008 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5022 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5025 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5030 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5355 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5223 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5354 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5539 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2122 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5322 fv3 5646 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5263 cnvexg 5262 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4987 dmexg 4984 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4988 rnexg 4985 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5640 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5650 tz6.12 5651 tz6.12c 5653 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5614 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5317 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5318 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5320 wfo 5312 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5319 wf1 5311 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5321 wf1o 5313 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5725 eqfnfv2 5726 eqfnfv2f 5729 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5697 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5854 fnexALT 6246 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5853 resfunexgALT 6243 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5402 funimaexg 5401 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4083 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5094 iniseg 5096 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4377 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5323 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5927 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5928 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5933 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5935 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5943 |
| [TakeutiZaring] p. 35 | Notation | wtr 4181 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4442 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4185 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4665 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4469 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4473 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4581 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4456 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4575 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4641 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4671 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4183 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4600 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4576 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3915 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4459 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4503 sucidg 4504 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4590 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4457 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4595 ordelsuc 4594 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4683 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4684 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4685 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4682 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4696 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4688 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4686 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4687 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3936 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4197 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3937 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4606 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3923 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6444 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6501 tfri1d 6471 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6502 tfri2d 6472 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6503 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6438 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6422 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6600 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6596 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6593 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6597 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6645 nnaordi 6644 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4009 uniss2 3918 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6606 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6616 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6607 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6594 omsuc 6608 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6617 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6653 nnmordi 6652 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6595 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7347 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6937 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7006 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7007 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6880 isfi 6902 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6978 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6787 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 6984 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 6997 |
| [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 2941 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3085 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5294 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5295 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2157 eupickbi 2160 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5322 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7351 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |