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 7293 fidcenum 7134 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7134 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7293 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13012 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7105 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7091 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13027 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13029 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13018 znnen 12985 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13030 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13031 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11010 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4629 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11139 df-pfx 11221 df-substr 11194 df-word 11085 lencl 11088 wrd0 11109 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8337 addcan2d 8342 addcan2i 8340 addcand 8341 addcani 8339 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8348 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8405 negsubd 8474 negsubi 8435 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8407 negnegd 8459 negnegi 8427 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8542 subdid 8571 subdii 8564 subdir 8543 subdird 8572 subdiri 8565 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8546 mul01d 8550 mul01i 8548 mul02 8544 mul02d 8549 mul02i 8547 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8951 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8902 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8555 mul2negd 8570 mul2negi 8563 mulneg1 8552 mulneg1d 8568 mulneg1i 8561 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14124 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8871 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9885 rpaddcld 9920 rpmulcl 9886 rpmulcld 9921 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9897 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8262 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8696 ltadd1dd 8714 ltadd1i 8660 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8750 ltmul1a 8749 ltmul1i 9078 ltmul1ii 9086 ltmul2 9014 ltmul2d 9947 ltmul2dd 9961 ltmul2i 9081 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8284 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8626 lt0neg1d 8673 ltneg 8620 ltnegd 8681 ltnegi 8651 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8603 lt2addd 8725 lt2addi 8668 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9862 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9008 recgt0d 9092 recgt0i 9064 recgt0ii 9065 |
| [Apostol] p. 22 | Definition of integers | df-z 9458 |
| [Apostol] p. 22 | Definition of rationals | df-q 9827 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7172 |
| [Apostol] p. 26 | Theorem I.29 | arch 9377 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9577 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9378 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10488 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12398 zneo 9559 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11558 sqrtthi 11646 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9124 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12573 |
| [Apostol] p. 363 | Remark | absgt0api 11673 |
| [Apostol] p. 363 | Example | abssubd 11720 abssubi 11677 |
| [ApostolNT] p. 14 | Definition | df-dvds 12315 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12331 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12355 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12351 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12345 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12347 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12332 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12333 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12338 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12372 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12374 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12376 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12551 |
| [ApostolNT] p. 16 | Definition | isprm2 12655 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12630 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13042 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12510 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12552 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12554 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12524 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12517 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12682 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12684 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12907 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12451 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12597 |
| [ApostolNT] p. 25 | Definition | df-phi 12749 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12779 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12760 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12764 |
| [ApostolNT] p. 38 | Remark | df-sgm 15672 |
| [ApostolNT] p. 38 | Definition | df-sgm 15672 |
| [ApostolNT] p. 104 | Definition | congr 12638 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12318 |
| [ApostolNT] p. 106 | Definition | moddvds 12326 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12405 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12406 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10575 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10612 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10900 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12350 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12641 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12960 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12643 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12771 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12790 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12772 |
| [ApostolNT] p. 179 | Definition | df-lgs 15693 lgsprme0 15737 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15738 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15714 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15729 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15780 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15799 2lgsoddprm 15808 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15764 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15775 |
| [ApostolNT] p. 188 | Definition | df-lgs 15693 lgs1 15739 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15730 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15732 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15740 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15741 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 619 pm2.65 663 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6006 onsucelsucexmidlem 4621 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16450 |
| [Bauer], p. 483 | Definition | n0rf 3504 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15666 2irrexpqap 15668 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 7046 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15343 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15333 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8803 |
| [BauerSwan], p. 14 | Remark | 0ct 7285 ctm 7287 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16453 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7293 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7699 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7612 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7701 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7735 addlocpr 7734 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7761 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7764 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7769 |
| [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 4205 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4261 |
| [BellMachover] p. 466 | Axiom Union | axun2 4526 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4634 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4475 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4637 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4588 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4460 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4681 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4706 |
| [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 15875 isuhgropm 15897 isusgropen 15979 isuspgropen 15978 |
| [Bollobas] p. 4 | Definition | df-wlks 16064 |
| [Bollobas] p. 5 | Definition | df-trls 16125 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15886 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13405 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13451 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13466 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13977 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13912 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5913 fcofo 5914 |
| [BourbakiTop1] p. | Remark | xnegmnf 10037 xnegpnf 10036 |
| [BourbakiTop1] p. | Remark | rexneg 10038 |
| [BourbakiTop1] p. | Proposition | ishmeo 14994 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14847 |
| [BourbakiTop1] p. | Property V_ii | innei 14853 |
| [BourbakiTop1] p. | Property V_iv | neissex 14855 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14844 neiss 14840 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14912 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 14989 |
| [BourbakiTop1] p. | Property V_iii | elnei 14842 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14688 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13405 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13451 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13648 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4147 |
| [Church] p. 129 | Section II.24 | df-ifp 984 dfifp2dc 987 |
| [Cohen] p. 301 | Remark | relogoprlem 15558 |
| [Cohen] p. 301 | Property 2 | relogmul 15559 relogmuld 15574 |
| [Cohen] p. 301 | Property 3 | relogdiv 15560 relogdivd 15575 |
| [Cohen] p. 301 | Property 4 | relogexp 15562 |
| [Cohen] p. 301 | Property 1a | log1 15556 |
| [Cohen] p. 301 | Property 1b | loge 15557 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15655 |
| [Cohen4] p. 352 | Definition | rpelogb 15639 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15645 |
| [Cohen4] p. 361 | Property 3 | logbrec 15650 rprelogbdiv 15647 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15643 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15648 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15637 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15638 |
| [Cohen4] p. 367 | Property | rplogbchbase 15640 |
| [Cohen4] p. 377 | Property 2 | logblt 15652 |
| [Crosilla] p. | Axiom 1 | ax-ext 2211 |
| [Crosilla] p. | Axiom 2 | ax-pr 4293 |
| [Crosilla] p. | Axiom 3 | ax-un 4524 |
| [Crosilla] p. | Axiom 4 | ax-nul 4210 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4680 |
| [Crosilla] p. | Axiom 6 | ru 3027 |
| [Crosilla] p. | Axiom 8 | ax-pow 4258 |
| [Crosilla] p. | Axiom 9 | ax-setind 4629 |
| [Crosilla], p. | Axiom 6 | ax-sep 4202 |
| [Crosilla], p. | Axiom 7 | ax-coll 4199 |
| [Crosilla], p. | Axiom 7' | repizf 4200 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4613 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6006 |
| [Crosilla], p. | Definition of ordinal | df-iord 4457 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4627 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15886 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3199 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4683 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6805 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4209 |
| [Enderton] p. 19 | Definition | df-tp 3674 |
| [Enderton] p. 26 | Exercise 5 | unissb 3918 |
| [Enderton] p. 26 | Exercise 10 | pwel 4304 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4377 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4035 iinin2m 4034 iunin1 4030 iunin2 4029 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4033 iundif2ss 4031 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4048 |
| [Enderton] p. 33 | Exercise 25 | iununir 4049 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4056 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4571 iunpwss 4057 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4303 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4276 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4541 rnex 4992 rnexg 4989 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4933 rnuni 5140 |
| [Enderton] p. 42 | Definition of a function | dffun7 5345 dffun8 5346 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5700 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5382 |
| [Enderton] p. 44 | Definition (d) | dfima2 5070 dfima3 5071 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5705 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7399 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5891 |
| [Enderton] p. 52 | Definition | df-map 6805 |
| [Enderton] p. 53 | Exercise 21 | coass 5247 |
| [Enderton] p. 53 | Exercise 27 | dmco 5237 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5392 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5104 |
| [Enderton] p. 54 | Remark | ixpf 6875 ixpssmap 6887 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6854 |
| [Enderton] p. 56 | Theorem 3M | erref 6708 |
| [Enderton] p. 57 | Lemma 3N | erthi 6736 |
| [Enderton] p. 57 | Definition | df-ec 6690 |
| [Enderton] p. 58 | Definition | df-qs 6694 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6795 th3qcor 6794 th3qlem1 6792 th3qlem2 6793 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6690 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4930 |
| [Enderton] p. 68 | Definition of successor | df-suc 4462 |
| [Enderton] p. 71 | Definition | df-tr 4183 dftr4 4187 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4504 unisucg 4505 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4504 unisucg 4505 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4196 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4197 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6628 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6630 onasuc 6620 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6010 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6629 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6631 onmsuc 6627 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6639 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6632 nnacom 6638 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6640 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6641 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6643 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6633 nnmsucr 6642 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6682 |
| [Enderton] p. 129 | Definition | df-en 6896 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5958 |
| [Enderton] p. 133 | Exercise 1 | xpomen 12982 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7035 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7026 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7015 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7411 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7407 dju1en 7406 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3567 |
| [Enderton] p. 145 | Figure 38 | ffoss 5606 |
| [Enderton] p. 145 | Definition | df-dom 6897 |
| [Enderton] p. 146 | Example 1 | domen 6908 domeng 6909 |
| [Enderton] p. 146 | Example 3 | nndomo 7033 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7002 xpdom1g 7000 xpdom2g 6999 |
| [Enderton] p. 168 | Definition | df-po 4387 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4519 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4480 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4635 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4483 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4608 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4581 |
| [Enderton] p. 194 | Remark | onprc 4644 |
| [Enderton] p. 194 | Exercise 16 | suc11 4650 |
| [Enderton] p. 197 | Definition | df-card 7362 |
| [Enderton] p. 200 | Exercise 25 | tfis 4675 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4646 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4648 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4649 |
| [Geuvers], p. 1 | Remark | expap0 10803 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8773 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8812 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8774 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8129 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11730 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11738 maxle2 11739 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11740 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11743 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11744 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8740 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7545 enqer 7556 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7549 df-nqqs 7546 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7542 df-plqqs 7547 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7543 df-mqqs 7548 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7550 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7606 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7609 ltbtwnnq 7614 ltbtwnnqq 7613 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7598 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7599 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7735 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7777 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7776 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7795 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7811 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7817 ltaprlem 7816 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7814 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7770 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7790 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7779 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7778 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7786 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7836 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7924 enrer 7933 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7929 df-1r 7930 df-nr 7925 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7927 df-plr 7926 negexsr 7970 recexsrlem 7972 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7928 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9118 creur 9117 cru 8760 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8121 axcnre 8079 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11385 crimd 11504 crimi 11464 crre 11384 crred 11503 crrei 11463 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11387 remimd 11469 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11584 absval2d 11712 absval2i 11671 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11411 cjaddd 11492 cjaddi 11459 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11412 cjmuld 11493 cjmuli 11460 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11410 cjcjd 11470 cjcji 11442 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11409 cjreb 11393 cjrebd 11473 cjrebi 11445 cjred 11498 rere 11392 rereb 11390 rerebd 11472 rerebi 11444 rered 11496 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11418 addcjd 11484 addcji 11454 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11528 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11579 abscjd 11717 abscji 11675 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11591 abs00d 11713 abs00i 11672 absne0d 11714 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11623 releabsd 11718 releabsi 11676 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11596 absmuld 11721 absmuli 11678 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11582 sqabsaddi 11679 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11631 abstrid 11723 abstrii 11682 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10773 exp0 10777 expp1 10780 expp1d 10908 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10815 expaddd 10909 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15602 cxpmuld 15627 expmul 10818 expmuld 10910 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10812 mulexpd 10922 rpmulcxp 15599 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10218 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11853 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11855 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11854 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11858 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11851 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11847 climcj 11848 climim 11850 climre 11849 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8197 df-xr 8196 ltxr 9983 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11874 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10532 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14525 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15054 xmet0 15053 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15061 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15063 mstri 15163 xmettri 15062 xmstri 15162 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14969 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15201 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11837 addcncntop 15252 mulcn2 11839 mulcncntop 15254 subcn2 11838 subcncntop 15253 |
| [Gleason] p. 295 | Remark | bcval3 10985 bcval4 10986 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11000 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10983 df-bc 10982 |
| [Gleason] p. 296 | Remark | bcn0 10989 bcnn 10991 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12011 |
| [Gleason] p. 308 | Equation 2 | ef0 12199 |
| [Gleason] p. 308 | Equation 3 | efcj 12200 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12205 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12209 |
| [Gleason] p. 310 | Equation 14 | sinadd 12263 |
| [Gleason] p. 310 | Equation 15 | cosadd 12264 |
| [Gleason] p. 311 | Equation 17 | sincossq 12275 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12280 sinbnd 12279 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12180 |
| [Golan] p. 1 | Remark | srgisid 13965 |
| [Golan] p. 1 | Definition | df-srg 13943 |
| [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 13560 mndideu 13475 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13587 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13616 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13627 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13649 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16530 |
| [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 7418 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6653 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16524 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8815 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7668 df-imp 7667 df-iplp 7666 df-reap 8733 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8829 rerecapb 9001 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6289 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7860 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16168 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16517 dceqnconst 16516 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8098 caucvgpr 7880 caucvgprpr 7910 caucvgsr 8000 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7664 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16522 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4388 ltpopr 7793 ltsopr 7794 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8764 reapcotr 8756 reapirr 8735 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8284 gt0add 8731 leadd1 8588 lelttr 8246 lemul1a 9016 lenlt 8233 ltadd1 8587 ltletr 8247 ltmul1 8750 reaplt 8746 |
| [Jech] p. 4 | Definition of class | cv 1394 cvjust 2224 |
| [Jech] p. 78 | Note | opthprc 4770 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1576 |
| [Kreyszig] p. 3 | Property M1 | metcl 15043 xmetcl 15042 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15050 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8826 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15132 |
| [Kreyszig] p. 19 | Remark | mopntopon 15133 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15178 mopnm 15138 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15176 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15181 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15203 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14903 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14310 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14301 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14302 |
| [Kunen] p. 10 | Axiom 0 | a9e 1742 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4201 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6815 mapvalg 6813 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6809 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3975 |
| [Lang] p. 3 | Statement | lidrideqd 13430 mndbn0 13480 |
| [Lang] p. 3 | Definition | df-mnd 13466 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13447 |
| [Lang] p. 5 | Equation | gsumfzreidx 13890 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13681 |
| [Lang] p. 7 | Definition | dfgrp2e 13577 |
| [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 4567 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3887 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4373 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4374 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4375 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3908 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4851 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5249 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4462 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7014 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6988 xpsneng 6989 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6994 xpcomeng 6995 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6997 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6991 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6807 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6972 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7019 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6841 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6973 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7410 djucomen 7409 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7408 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6621 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3426 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4807 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4808 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4146 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5244 coi2 5245 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4937 rn0 4980 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5133 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4828 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4944 rnxpm 5158 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4799 xp0 5148 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5087 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5084 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5083 imaexg 5082 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5079 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5767 funfvop 5749 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5677 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5687 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5362 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5898 dff13f 5900 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5866 funrnex 6265 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5892 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5212 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3939 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6307 df-1st 6292 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6308 df-2nd 6293 |
| [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 4329 |
| [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 16531 |
| [Munkres] p. 77 | Example 2 | distop 14775 |
| [Munkres] p. 78 | Definition of basis | df-bases 14733 isbasis3g 14736 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13309 tgval2 14741 |
| [Munkres] p. 79 | Remark | tgcl 14754 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14748 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14769 tgss3 14768 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14770 basgen2 14771 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14860 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14802 topcld 14799 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14803 |
| [Munkres] p. 94 | Definition of closure | clsval 14801 |
| [Munkres] p. 94 | Definition of interior | ntrval 14800 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14878 iscn 14887 iscn2 14890 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14920 cncnp2m 14921 cncnpi 14918 df-cnp 14879 iscnp 14889 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15204 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7074 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7342 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7330 omniwomnimkv 7345 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3314 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7313 exmidomniim 7319 finomni 7318 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7298 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16475 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16479 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7081 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7390 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7391 exmidfodomrlemrALT 7392 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7327 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16461 peano4nninf 16460 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16463 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16471 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16473 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16459 |
| [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 3803 snssg 3802 |
| [Quine] p. 49 | Theorem 7.5 | prss 3824 prssg 3825 |
| [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 4268 snexprc 4270 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4295 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3904 unisng 3905 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3907 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3916 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3915 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5289 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5279 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5290 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5294 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5295 |
| [Quine] p. 58 | Definition 9.1 | df-op 3675 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4344 opabidw 4345 opelopab 4360 opelopaba 4354 opelopabaf 4362 opelopabf 4363 opelopabg 4356 opelopabga 4351 opelopabgf 4358 oprabid 6039 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4725 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4727 |
| [Quine] p. 64 | Definition 9.15 | df-id 4384 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5379 |
| [Quine] p. 65 | Theorem 10.4 | funi 5350 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5369 funsng 5367 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5320 |
| [Quine] p. 65 | Definition 10.2 | args 5097 dffv4g 5626 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5326 fv2 5624 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10958 nn0opth2d 10957 nn0opthd 10956 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5406 funimaexg 5405 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13912 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13977 |
| [Rudin] p. 164 | Equation 27 | efcan 12203 |
| [Rudin] p. 164 | Equation 30 | efzval 12210 |
| [Rudin] p. 167 | Equation 48 | absefi 12296 |
| [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 5113 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5115 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5112 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5110 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 13979 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14773 |
| [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 4019 |
| [Stoll] p. 44 | Definition | intiin 4020 |
| [Stoll] p. 45 | Definition | df-iin 3968 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3967 |
| [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 4214 |
| [Suppes] p. 39 | Theorem 61 | uniss 3909 |
| [Suppes] p. 39 | Theorem 65 | uniop 4342 |
| [Suppes] p. 41 | Theorem 70 | intsn 3958 |
| [Suppes] p. 42 | Theorem 71 | intpr 3955 intprg 3956 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4569 op1stbg 4570 |
| [Suppes] p. 42 | Theorem 78 | intun 3954 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3999 dfiun2g 3997 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4000 |
| [Suppes] p. 47 | Theorem 86 | elpw 3655 elpw2 4241 elpw2g 4240 elpwg 3657 |
| [Suppes] p. 47 | Theorem 87 | pwid 3664 |
| [Suppes] p. 47 | Theorem 89 | pw0 3815 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3883 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4826 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4857 xpindir 4858 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4775 xpundir 4776 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4640 |
| [Suppes] p. 58 | Theorem 2 | relss 4806 |
| [Suppes] p. 59 | Theorem 4 | eldm 4920 eldm2 4921 eldm2g 4919 eldmg 4918 |
| [Suppes] p. 59 | Definition 3 | df-dm 4729 |
| [Suppes] p. 60 | Theorem 6 | dmin 4931 |
| [Suppes] p. 60 | Theorem 8 | rnun 5137 |
| [Suppes] p. 60 | Theorem 9 | rnin 5138 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4910 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4905 brcnvg 4903 |
| [Suppes] p. 62 | Equation 5 | elcnv 4899 elcnv2 4900 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5106 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5136 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5134 |
| [Suppes] p. 63 | Theorem 20 | co02 5242 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4994 |
| [Suppes] p. 63 | Definition 7 | df-co 4728 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4907 |
| [Suppes] p. 64 | Theorem 27 | coass 5247 |
| [Suppes] p. 65 | Theorem 31 | resundi 5018 |
| [Suppes] p. 65 | Theorem 34 | elima 5073 elima2 5074 elima3 5075 elimag 5072 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5141 |
| [Suppes] p. 66 | Theorem 40 | dminss 5143 |
| [Suppes] p. 66 | Theorem 41 | imainss 5144 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5147 |
| [Suppes] p. 81 | Definition 34 | dfec2 6691 |
| [Suppes] p. 82 | Theorem 72 | elec 6729 elecg 6728 |
| [Suppes] p. 82 | Theorem 73 | erth 6734 erth2 6735 |
| [Suppes] p. 89 | Theorem 96 | map0b 6842 |
| [Suppes] p. 89 | Theorem 97 | map0 6844 map0g 6843 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6845 |
| [Suppes] p. 89 | Theorem 99 | mapss 6846 |
| [Suppes] p. 92 | Theorem 1 | enref 6924 enrefg 6923 |
| [Suppes] p. 92 | Theorem 2 | ensym 6941 ensymb 6940 ensymi 6942 |
| [Suppes] p. 92 | Theorem 3 | entr 6944 |
| [Suppes] p. 92 | Theorem 4 | unen 6977 |
| [Suppes] p. 94 | Theorem 15 | endom 6922 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6938 |
| [Suppes] p. 94 | Theorem 17 | domtr 6945 |
| [Suppes] p. 95 | Theorem 18 | isbth 7145 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6967 fundmeng 6968 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7001 |
| [Suppes] p. 130 | Definition 3 | df-tr 4183 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4580 |
| [Suppes] p. 134 | Definition 6 | df-suc 4462 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4695 finds 4692 finds1 4694 finds2 4693 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7551 df-ltpq 7544 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4481 |
| [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 6011 |
| [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 4317 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3677 sneqr 3838 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3685 dfsn2 3680 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4528 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4323 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4301 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4532 unexg 4534 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3715 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3889 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3203 df-un 3201 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3902 uniprg 3903 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4263 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3714 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4497 elsucg 4495 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 3897 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4302 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4309 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2517 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4211 |
| [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 4631 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2801 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4216 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3530 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4221 ssexg 4223 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4218 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4642 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4633 |
| [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 4834 xpexg 4833 xpexgALT 6284 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4726 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5385 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5544 fun11 5388 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5329 svrelfun 5386 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4909 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4911 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4731 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4732 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4728 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5183 dfrel2 5179 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4827 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4836 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4842 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4856 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5033 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5010 opelresg 5012 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5026 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5029 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5034 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5359 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5227 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5358 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5545 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2122 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5326 fv3 5652 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5267 cnvexg 5266 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4991 dmexg 4988 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4992 rnexg 4989 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5646 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5656 tz6.12 5657 tz6.12c 5659 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5620 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5321 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5322 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5324 wfo 5316 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5323 wf1 5315 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5325 wf1o 5317 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5734 eqfnfv2 5735 eqfnfv2f 5738 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5706 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5865 fnexALT 6262 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5864 resfunexgALT 6259 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5406 funimaexg 5405 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4084 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5098 iniseg 5100 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4380 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5327 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5940 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5941 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5946 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5948 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5956 |
| [TakeutiZaring] p. 35 | Notation | wtr 4182 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4445 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4186 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4668 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4472 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4476 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4584 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4459 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4578 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4644 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4674 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4184 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4603 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4579 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3916 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4462 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4506 sucidg 4507 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4593 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4460 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4598 ordelsuc 4597 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4686 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4687 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4688 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4685 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4699 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4691 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4689 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4690 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3937 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4198 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3938 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4609 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3924 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6460 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6517 tfri1d 6487 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6518 tfri2d 6488 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6519 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6454 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6438 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6618 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6614 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6611 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6615 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6663 nnaordi 6662 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4010 uniss2 3919 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6624 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6634 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6625 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6612 omsuc 6626 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6635 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6671 nnmordi 6670 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6613 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7370 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6955 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7026 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7027 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6898 isfi 6920 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6998 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6805 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7004 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7017 |
| [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 5298 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5299 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2157 eupickbi 2160 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5326 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7374 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |