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 7374 fidcenum 7198 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7198 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7374 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13126 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7167 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7153 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13141 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13143 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13132 znnen 13099 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13144 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13145 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11101 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4641 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11234 df-pfx 11320 df-substr 11293 df-word 11180 lencl 11183 wrd0 11204 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8418 addcan2d 8423 addcan2i 8421 addcand 8422 addcani 8420 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8429 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8486 negsubd 8555 negsubi 8516 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8488 negnegd 8540 negnegi 8508 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8623 subdid 8652 subdii 8645 subdir 8624 subdird 8653 subdiri 8646 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8627 mul01d 8631 mul01i 8629 mul02 8625 mul02d 8630 mul02i 8628 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 9032 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8983 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8636 mul2negd 8651 mul2negi 8644 mulneg1 8633 mulneg1d 8649 mulneg1i 8642 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14239 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8952 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9973 rpaddcld 10008 rpmulcl 9974 rpmulcld 10009 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9985 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8343 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8777 ltadd1dd 8795 ltadd1i 8741 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8831 ltmul1a 8830 ltmul1i 9159 ltmul1ii 9167 ltmul2 9095 ltmul2d 10035 ltmul2dd 10049 ltmul2i 9162 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8365 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8707 lt0neg1d 8754 ltneg 8701 ltnegd 8762 ltnegi 8732 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8684 lt2addd 8806 lt2addi 8749 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9950 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9089 recgt0d 9173 recgt0i 9145 recgt0ii 9146 |
| [Apostol] p. 22 | Definition of integers | df-z 9541 |
| [Apostol] p. 22 | Definition of rationals | df-q 9915 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7253 |
| [Apostol] p. 26 | Theorem I.29 | arch 9458 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9660 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9459 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10579 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12512 zneo 9642 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11671 sqrtthi 11759 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9205 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12687 |
| [Apostol] p. 363 | Remark | absgt0api 11786 |
| [Apostol] p. 363 | Example | abssubd 11833 abssubi 11790 |
| [ApostolNT] p. 14 | Definition | df-dvds 12429 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12445 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12469 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12465 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12459 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12461 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12446 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12447 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12452 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12486 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12488 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12490 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12665 |
| [ApostolNT] p. 16 | Definition | isprm2 12769 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12744 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13156 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12624 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12666 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12668 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12638 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12631 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12796 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12798 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 13021 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12565 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12711 |
| [ApostolNT] p. 25 | Definition | df-phi 12863 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12893 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12874 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12878 |
| [ApostolNT] p. 38 | Remark | df-sgm 15796 |
| [ApostolNT] p. 38 | Definition | df-sgm 15796 |
| [ApostolNT] p. 104 | Definition | congr 12752 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12432 |
| [ApostolNT] p. 106 | Definition | moddvds 12440 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12519 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12520 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10666 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10703 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10991 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12464 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12755 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13074 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12757 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12885 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12904 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12886 |
| [ApostolNT] p. 179 | Definition | df-lgs 15817 lgsprme0 15861 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15862 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15838 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15853 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15904 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15923 2lgsoddprm 15932 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15888 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15899 |
| [ApostolNT] p. 188 | Definition | df-lgs 15817 lgs1 15863 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15854 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15856 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15864 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15865 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 621 pm2.65 665 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6027 onsucelsucexmidlem 4633 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16719 |
| [Bauer], p. 483 | Definition | n0rf 3509 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15787 2irrexpqap 15789 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7174 ssfiexmid 7106 ssfiexmidt 7108 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15464 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15454 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8884 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7374 |
| [BauerSwan], p. 14 | Remark | 0ct 7366 ctm 7368 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16722 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7781 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7694 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7783 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7817 addlocpr 7816 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7843 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7846 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7851 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2082 |
| [BellMachover] p. 460 | Notation | df-mo 2083 |
| [BellMachover] p. 460 | Definition | mo3 2134 mo3h 2133 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2216 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4215 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4273 |
| [BellMachover] p. 466 | Axiom Union | axun2 4538 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4646 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4487 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4649 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4600 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4472 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4693 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4718 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1476 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1474 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1477 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1472 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15999 isuhgropm 16022 isusgropen 16106 isuspgropen 16105 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16195 uhgrspansubgr 16218 |
| [Bollobas] p. 4 | Definition | df-wlks 16259 |
| [Bollobas] p. 5 | Definition | df-trls 16322 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 16011 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13519 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13565 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13580 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14092 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 14027 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5934 fcofo 5935 |
| [BourbakiTop1] p. | Remark | xnegmnf 10125 xnegpnf 10124 |
| [BourbakiTop1] p. | Remark | rexneg 10126 |
| [BourbakiTop1] p. | Proposition | ishmeo 15115 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14968 |
| [BourbakiTop1] p. | Property V_ii | innei 14974 |
| [BourbakiTop1] p. | Property V_iv | neissex 14976 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14965 neiss 14961 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 15033 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15110 |
| [BourbakiTop1] p. | Property V_iii | elnei 14963 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14809 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13519 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13565 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13762 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4157 |
| [Church] p. 129 | Section II.24 | df-ifp 987 dfifp2dc 990 |
| [Cohen] p. 301 | Remark | relogoprlem 15679 |
| [Cohen] p. 301 | Property 2 | relogmul 15680 relogmuld 15695 |
| [Cohen] p. 301 | Property 3 | relogdiv 15681 relogdivd 15696 |
| [Cohen] p. 301 | Property 4 | relogexp 15683 |
| [Cohen] p. 301 | Property 1a | log1 15677 |
| [Cohen] p. 301 | Property 1b | loge 15678 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15776 |
| [Cohen4] p. 352 | Definition | rpelogb 15760 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15766 |
| [Cohen4] p. 361 | Property 3 | logbrec 15771 rprelogbdiv 15768 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15764 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15769 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15758 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15759 |
| [Cohen4] p. 367 | Property | rplogbchbase 15761 |
| [Cohen4] p. 377 | Property 2 | logblt 15773 |
| [Crosilla] p. | Axiom 1 | ax-ext 2213 |
| [Crosilla] p. | Axiom 2 | ax-pr 4305 |
| [Crosilla] p. | Axiom 3 | ax-un 4536 |
| [Crosilla] p. | Axiom 4 | ax-nul 4220 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4692 |
| [Crosilla] p. | Axiom 6 | ru 3031 |
| [Crosilla] p. | Axiom 8 | ax-pow 4270 |
| [Crosilla] p. | Axiom 9 | ax-setind 4641 |
| [Crosilla], p. | Axiom 6 | ax-sep 4212 |
| [Crosilla], p. | Axiom 7 | ax-coll 4209 |
| [Crosilla], p. | Axiom 7' | repizf 4210 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4625 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6027 |
| [Crosilla], p. | Definition of ordinal | df-iord 4469 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4639 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16195 uhgrspansubgr 16218 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 16011 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3203 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4695 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6862 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4219 |
| [Enderton] p. 19 | Definition | df-tp 3681 |
| [Enderton] p. 26 | Exercise 5 | unissb 3928 |
| [Enderton] p. 26 | Exercise 10 | pwel 4316 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4389 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4045 iinin2m 4044 iunin1 4040 iunin2 4039 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4043 iundif2ss 4041 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4058 |
| [Enderton] p. 33 | Exercise 25 | iununir 4059 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4066 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4583 iunpwss 4067 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4315 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4288 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4553 rnex 5006 rnexg 5003 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4947 rnuni 5155 |
| [Enderton] p. 42 | Definition of a function | dffun7 5360 dffun8 5361 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5719 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5398 |
| [Enderton] p. 44 | Definition (d) | dfima2 5084 dfima3 5085 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5724 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7481 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5912 |
| [Enderton] p. 52 | Definition | df-map 6862 |
| [Enderton] p. 53 | Exercise 21 | coass 5262 |
| [Enderton] p. 53 | Exercise 27 | dmco 5252 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5408 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5119 |
| [Enderton] p. 54 | Remark | ixpf 6932 ixpssmap 6944 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6911 |
| [Enderton] p. 56 | Theorem 3M | erref 6765 |
| [Enderton] p. 57 | Lemma 3N | erthi 6793 |
| [Enderton] p. 57 | Definition | df-ec 6747 |
| [Enderton] p. 58 | Definition | df-qs 6751 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6852 th3qcor 6851 th3qlem1 6849 th3qlem2 6850 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6747 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4944 |
| [Enderton] p. 68 | Definition of successor | df-suc 4474 |
| [Enderton] p. 71 | Definition | df-tr 4193 dftr4 4197 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4516 unisucg 4517 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4516 unisucg 4517 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4206 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4207 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6685 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6687 onasuc 6677 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6031 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6686 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6688 onmsuc 6684 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6696 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6689 nnacom 6695 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6697 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6698 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6700 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6690 nnmsucr 6699 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6739 |
| [Enderton] p. 129 | Definition | df-en 6953 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5979 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13096 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7095 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7086 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7075 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7493 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7489 dju1en 7488 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3572 |
| [Enderton] p. 145 | Figure 38 | ffoss 5625 |
| [Enderton] p. 145 | Definition | df-dom 6954 |
| [Enderton] p. 146 | Example 1 | domen 6965 domeng 6966 |
| [Enderton] p. 146 | Example 3 | nndomo 7093 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7062 xpdom1g 7060 xpdom2g 7059 |
| [Enderton] p. 168 | Definition | df-po 4399 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4531 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4492 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4647 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4495 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4620 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4593 |
| [Enderton] p. 194 | Remark | onprc 4656 |
| [Enderton] p. 194 | Exercise 16 | suc11 4662 |
| [Enderton] p. 197 | Definition | df-card 7443 |
| [Enderton] p. 200 | Exercise 25 | tfis 4687 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4658 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4660 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4661 |
| [Geuvers], p. 1 | Remark | expap0 10894 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8854 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8893 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8855 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8211 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11843 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11851 maxle2 11852 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11853 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11856 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11857 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8821 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7627 enqer 7638 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7631 df-nqqs 7628 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7624 df-plqqs 7629 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7625 df-mqqs 7630 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7632 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7688 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7691 ltbtwnnq 7696 ltbtwnnqq 7695 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7680 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7681 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7817 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7859 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7858 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7877 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7893 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7899 ltaprlem 7898 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7896 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7852 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7872 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7861 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7860 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7868 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7918 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 8006 enrer 8015 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 8011 df-1r 8012 df-nr 8007 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 8009 df-plr 8008 negexsr 8052 recexsrlem 8054 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 8010 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9199 creur 9198 cru 8841 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8203 axcnre 8161 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11498 crimd 11617 crimi 11577 crre 11497 crred 11616 crrei 11576 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11500 remimd 11582 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11697 absval2d 11825 absval2i 11784 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11524 cjaddd 11605 cjaddi 11572 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11525 cjmuld 11606 cjmuli 11573 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11523 cjcjd 11583 cjcji 11555 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11522 cjreb 11506 cjrebd 11586 cjrebi 11558 cjred 11611 rere 11505 rereb 11503 rerebd 11585 rerebi 11557 rered 11609 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11531 addcjd 11597 addcji 11567 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11641 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11692 abscjd 11830 abscji 11788 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11704 abs00d 11826 abs00i 11785 absne0d 11827 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11736 releabsd 11831 releabsi 11789 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11709 absmuld 11834 absmuli 11791 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11695 sqabsaddi 11792 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11744 abstrid 11836 abstrii 11795 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10864 exp0 10868 expp1 10871 expp1d 10999 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10906 expaddd 11000 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15723 cxpmuld 15748 expmul 10909 expmuld 11001 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10903 mulexpd 11013 rpmulcxp 15720 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10307 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11966 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11968 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11967 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11971 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11964 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11960 climcj 11961 climim 11963 climre 11962 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8278 df-xr 8277 ltxr 10071 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11987 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10623 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14641 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15175 xmet0 15174 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15182 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15184 mstri 15284 xmettri 15183 xmstri 15283 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15090 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15322 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11950 addcncntop 15373 mulcn2 11952 mulcncntop 15375 subcn2 11951 subcncntop 15374 |
| [Gleason] p. 295 | Remark | bcval3 11076 bcval4 11077 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11091 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11074 df-bc 11073 |
| [Gleason] p. 296 | Remark | bcn0 11080 bcnn 11082 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12125 |
| [Gleason] p. 308 | Equation 2 | ef0 12313 |
| [Gleason] p. 308 | Equation 3 | efcj 12314 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12319 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12323 |
| [Gleason] p. 310 | Equation 14 | sinadd 12377 |
| [Gleason] p. 310 | Equation 15 | cosadd 12378 |
| [Gleason] p. 311 | Equation 17 | sincossq 12389 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12394 sinbnd 12393 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12294 |
| [Golan] p. 1 | Remark | srgisid 14080 |
| [Golan] p. 1 | Definition | df-srg 14058 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1498 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13674 mndideu 13589 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13701 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13730 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13741 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13763 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16817 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1468 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1469 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1471 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7500 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6710 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16801 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8896 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7750 df-imp 7749 df-iplp 7748 df-reap 8814 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8910 rerecapb 9082 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6309 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7942 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16435 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16794 dceqnconst 16793 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8180 caucvgpr 7962 caucvgprpr 7992 caucvgsr 8082 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7746 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16799 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4400 ltpopr 7875 ltsopr 7876 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8845 reapcotr 8837 reapirr 8816 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8365 gt0add 8812 leadd1 8669 lelttr 8327 lemul1a 9097 lenlt 8314 ltadd1 8668 ltletr 8328 ltmul1 8831 reaplt 8827 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16368 |
| [Jech] p. 4 | Definition of class | cv 1397 cvjust 2226 |
| [Jech] p. 78 | Note | opthprc 4783 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1579 |
| [Kreyszig] p. 3 | Property M1 | metcl 15164 xmetcl 15163 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15171 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8907 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15253 |
| [Kreyszig] p. 19 | Remark | mopntopon 15254 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15299 mopnm 15259 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15297 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15302 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15324 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 15024 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14426 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14417 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14418 |
| [Kunen] p. 10 | Axiom 0 | a9e 1744 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4211 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6872 mapvalg 6870 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6866 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3985 |
| [Lang] p. 3 | Statement | lidrideqd 13544 mndbn0 13594 |
| [Lang] p. 3 | Definition | df-mnd 13580 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13561 |
| [Lang] p. 5 | Equation | gsumfzreidx 14004 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13795 |
| [Lang] p. 7 | Definition | dfgrp2e 13691 |
| [Levy] p. 338 | Axiom | df-clab 2218 df-clel 2227 df-cleq 2224 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1468 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1469 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1471 |
| [Margaris] p. 40 | Rule C | exlimiv 1647 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 861 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 900 exalim 1551 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 657 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1687 r19.2m 3583 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1603 19.3h 1602 rr19.3v 2946 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1527 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1668 alexim 1694 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1548 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1639 spsbe 1890 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1693 19.9h 1692 19.9v 1919 exlimd 1646 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1712 excomim 1711 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1713 r19.12 2640 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1695 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1517 ralbi 2666 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1604 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1605 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1653 rexbi 2667 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1714 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1506 alimd 1570 alimdh 1516 alimdv 1927 ralimdaa 2599 ralimdv 2601 ralimdva 2600 ralimdvva 2602 sbcimdv 3098 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1715 19.21 1632 19.21bi 1607 19.21h 1606 19.21ht 1630 19.21t 1631 19.21v 1921 alrimd 1659 alrimdd 1658 alrimdh 1528 alrimdv 1924 alrimi 1571 alrimih 1518 alrimiv 1922 alrimivv 1923 r19.21 2609 r19.21be 2624 r19.21bi 2621 r19.21t 2608 r19.21v 2610 ralrimd 2611 ralrimdv 2612 ralrimdva 2613 ralrimdvv 2617 ralrimdvva 2618 ralrimi 2604 ralrimiv 2605 ralrimiva 2606 ralrimivv 2614 ralrimivva 2615 ralrimivvva 2616 ralrimivw 2607 rexlimi 2644 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1929 2eximdv 1930 exim 1648 eximd 1661 eximdh 1660 eximdv 1928 rexim 2627 reximdai 2631 reximddv 2636 reximddv2 2638 reximdv 2634 reximdv2 2632 reximdva 2635 reximdvai 2633 reximi2 2629 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1726 19.23bi 1641 19.23h 1547 19.23ht 1546 19.23t 1725 19.23v 1931 19.23vv 1932 exlimd2 1644 exlimdh 1645 exlimdv 1867 exlimdvv 1946 exlimi 1643 exlimih 1642 exlimiv 1647 exlimivv 1945 r19.23 2642 r19.23v 2643 rexlimd 2648 rexlimdv 2650 rexlimdv3a 2653 rexlimdva 2651 rexlimdva2 2654 rexlimdvaa 2652 rexlimdvv 2658 rexlimdvva 2659 rexlimdvw 2655 rexlimiv 2645 rexlimiva 2646 rexlimivv 2657 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1688 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1675 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1531 19.26-3an 1532 19.26 1530 r19.26-2 2663 r19.26-3 2664 r19.26 2660 r19.26m 2665 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1610 19.27h 1609 19.27v 1948 r19.27av 2669 r19.27m 3592 r19.27mv 3593 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1612 19.28h 1611 19.28v 1949 r19.28av 2670 r19.28m 3586 r19.28mv 3589 rr19.28v 2947 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1669 19.29r 1670 19.29r2 1671 19.29x 1672 r19.29 2671 r19.29d2r 2678 r19.29r 2672 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1676 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1729 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1727 19.32r 1728 r19.32r 2680 r19.32vdc 2683 r19.32vr 2682 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1533 19.33b2 1678 19.33bdc 1679 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1732 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1673 19.35i 1674 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1721 19.36aiv 1950 19.36i 1720 r19.36av 2685 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1722 19.37aiv 1723 r19.37 2686 r19.37av 2687 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1724 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1689 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1681 19.40 1680 r19.40 2688 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1734 19.41h 1733 19.41v 1951 19.41vv 1952 19.41vvv 1953 19.41vvvv 1954 r19.41 2689 r19.41v 2690 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1736 19.42h 1735 19.42v 1955 19.42vv 1960 19.42vvv 1961 19.42vvvv 1962 r19.42v 2691 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1677 r19.43 2692 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1730 r19.44av 2693 r19.44mv 3591 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1731 r19.45av 2694 r19.45mv 3590 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2104 |
| [Megill] p. 444 | Axiom C5 | ax-17 1575 |
| [Megill] p. 445 | Lemma L12 | alequcom 1564 ax-10 1554 |
| [Megill] p. 446 | Lemma L17 | equtrr 1758 |
| [Megill] p. 446 | Lemma L19 | hbnae 1769 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1811 sbid 1822 |
| [Megill] p. 448 | Scheme C5' | ax-4 1559 |
| [Megill] p. 448 | Scheme C6' | ax-7 1497 |
| [Megill] p. 448 | Scheme C8' | ax-8 1553 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1556 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1764 |
| [Megill] p. 448 | Scheme C12' | ax-13 2204 |
| [Megill] p. 448 | Scheme C13' | ax-14 2205 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1871 |
| [Megill] p. 448 | Scheme C16' | ax-16 1862 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1778 dral2 1779 drex1 1846 drex2 1780 drsb1 1847 drsb2 1889 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2040 sbequ 1888 sbid2v 2049 |
| [Megill] p. 450 | Example in Appendix | hba1 1589 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3116 rspsbca 3117 stdpc4 1823 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3122 stdpc5 1633 |
| [Mendelson] p. 81 | Rule C | exlimiv 1647 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1751 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1818 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3533 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3534 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3449 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3497 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3450 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3340 |
| [Mendelson] p. 231 | Definition of union | unssin 3448 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4579 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3897 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4385 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4386 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4387 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3918 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4865 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5264 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4474 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7074 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7048 xpsneng 7049 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7054 xpcomeng 7055 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7057 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7051 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6864 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 7029 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7079 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6898 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 7030 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7492 djucomen 7491 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7490 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6678 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3431 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4820 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4821 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4156 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5259 coi2 5260 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4951 rn0 4994 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5148 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4841 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4958 rnxpm 5173 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4812 xp0 5163 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5102 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5099 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5097 imaexg 5096 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5093 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5785 funfvop 5768 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5696 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5706 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5378 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5919 dff13f 5921 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5887 funrnex 6285 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5913 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5227 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3949 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6327 df-1st 6312 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6328 df-2nd 6313 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1496 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1553 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1555 ax-11o 1871 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1875 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1497 |
| [Monk2] p. 109 | Lemma 15 | equvin 1911 equvini 1806 eqvinop 4341 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1575 |
| [Monk2] p. 113 | Axiom C5-2 | hbn1 1700 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1497 |
| [Monk2] p. 114 | Lemma 22 | hba1 1589 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1601 nfia1 1629 |
| [Monk2] p. 114 | Lemma 24 | hba2 1600 nfa2 1628 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 839 dftest 16818 |
| [Munkres] p. 77 | Example 2 | distop 14896 |
| [Munkres] p. 78 | Definition of basis | df-bases 14854 isbasis3g 14857 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13423 tgval2 14862 |
| [Munkres] p. 79 | Remark | tgcl 14875 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14869 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14890 tgss3 14889 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14891 basgen2 14892 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14981 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14923 topcld 14920 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14924 |
| [Munkres] p. 94 | Definition of closure | clsval 14922 |
| [Munkres] p. 94 | Definition of interior | ntrval 14921 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14999 iscn 15008 iscn2 15011 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 15041 cncnp2m 15042 cncnpi 15039 df-cnp 15000 iscnp 15010 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15325 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7136 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7423 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7411 omniwomnimkv 7426 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3319 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7394 exmidomniim 7400 finomni 7399 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7379 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16747 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16751 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7143 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7472 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7473 exmidfodomrlemrALT 7474 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7408 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16733 peano4nninf 16732 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16735 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16743 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16745 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16731 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2218 rabid 2710 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2044 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2224 |
| [Quine] p. 19 | Definition 2.9 | df-v 2805 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2340 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2353 abid2f 2401 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1936 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1934 sb6 1935 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2227 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2231 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2233 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3033 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3034 dfsbcq2 3035 |
| [Quine] p. 43 | Theorem 6.8 | vex 2806 |
| [Quine] p. 43 | Theorem 6.9 | isset 2810 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2889 spcgv 2894 spcimgf 2887 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3044 spsbcd 3045 |
| [Quine] p. 44 | Theorem 6.12 | elex 2815 |
| [Quine] p. 44 | Theorem 6.13 | elab 2951 elabg 2953 elabgf 2949 |
| [Quine] p. 44 | Theorem 6.14 | noel 3500 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3738 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3680 df-sn 3679 |
| [Quine] p. 49 | Theorem 7.4 | snss 3813 snssg 3812 |
| [Quine] p. 49 | Theorem 7.5 | prss 3834 prssg 3835 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3781 prid1g 3779 prid2 3782 prid2g 3780 snid 3704 snidg 3702 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4280 snexprc 4282 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4307 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3914 unisng 3915 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3917 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3926 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3925 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5304 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5294 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5305 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5309 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5310 |
| [Quine] p. 58 | Definition 9.1 | df-op 3682 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4356 opabidw 4357 opelopab 4372 opelopaba 4366 opelopabaf 4374 opelopabf 4375 opelopabg 4368 opelopabga 4363 opelopabgf 4370 oprabid 6060 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4737 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4739 |
| [Quine] p. 64 | Definition 9.15 | df-id 4396 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5395 |
| [Quine] p. 65 | Theorem 10.4 | funi 5365 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5385 funsng 5383 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5335 |
| [Quine] p. 65 | Definition 10.2 | args 5112 dffv4g 5645 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5341 fv2 5643 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 11049 nn0opth2d 11048 nn0opthd 11047 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5422 funimaexg 5421 |
| [Roman] p. 18 | Part Preliminaries | df-rng 14027 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14092 |
| [Rudin] p. 164 | Equation 27 | efcan 12317 |
| [Rudin] p. 164 | Equation 30 | efzval 12324 |
| [Rudin] p. 167 | Equation 48 | absefi 12410 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1471 |
| [Sanford] p. 39 | Rule 4 | mptxor 1469 |
| [Sanford] p. 40 | Rule 1 | mptnan 1468 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5128 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5130 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5127 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5125 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14094 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14894 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3474 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3568 dif0 3567 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3581 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3467 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3468 |
| [Stoll] p. 20 | Remark | invdif 3451 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3683 |
| [Stoll] p. 43 | Definition | uniiun 4029 |
| [Stoll] p. 44 | Definition | intiin 4030 |
| [Stoll] p. 45 | Definition | df-iin 3978 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3977 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 897 imanst 896 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3474 |
| [Suppes] p. 22 | Theorem 2 | eq0 3515 |
| [Suppes] p. 22 | Theorem 4 | eqss 3243 eqssd 3245 eqssi 3244 |
| [Suppes] p. 23 | Theorem 5 | ss0 3537 ss0b 3536 |
| [Suppes] p. 23 | Theorem 6 | sstr 3236 |
| [Suppes] p. 25 | Theorem 12 | elin 3392 elun 3350 |
| [Suppes] p. 26 | Theorem 15 | inidm 3418 |
| [Suppes] p. 26 | Theorem 16 | in0 3531 |
| [Suppes] p. 27 | Theorem 23 | unidm 3352 |
| [Suppes] p. 27 | Theorem 24 | un0 3530 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3372 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3379 |
| [Suppes] p. 27 | Theorem 27 | unss 3383 |
| [Suppes] p. 27 | Theorem 28 | indir 3458 |
| [Suppes] p. 27 | Theorem 29 | undir 3459 |
| [Suppes] p. 28 | Theorem 32 | difid 3565 difidALT 3566 |
| [Suppes] p. 29 | Theorem 33 | difin 3446 |
| [Suppes] p. 29 | Theorem 34 | indif 3452 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3571 |
| [Suppes] p. 29 | Theorem 36 | difun2 3576 |
| [Suppes] p. 29 | Theorem 37 | difin0 3570 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3569 |
| [Suppes] p. 29 | Theorem 39 | difundi 3461 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3463 |
| [Suppes] p. 30 | Theorem 41 | nalset 4224 |
| [Suppes] p. 39 | Theorem 61 | uniss 3919 |
| [Suppes] p. 39 | Theorem 65 | uniop 4354 |
| [Suppes] p. 41 | Theorem 70 | intsn 3968 |
| [Suppes] p. 42 | Theorem 71 | intpr 3965 intprg 3966 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4581 op1stbg 4582 |
| [Suppes] p. 42 | Theorem 78 | intun 3964 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4009 dfiun2g 4007 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4010 |
| [Suppes] p. 47 | Theorem 86 | elpw 3662 elpw2 4252 elpw2g 4251 elpwg 3664 |
| [Suppes] p. 47 | Theorem 87 | pwid 3671 |
| [Suppes] p. 47 | Theorem 89 | pw0 3825 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3893 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4839 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4871 xpindir 4872 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4788 xpundir 4789 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4652 |
| [Suppes] p. 58 | Theorem 2 | relss 4819 |
| [Suppes] p. 59 | Theorem 4 | eldm 4934 eldm2 4935 eldm2g 4933 eldmg 4932 |
| [Suppes] p. 59 | Definition 3 | df-dm 4741 |
| [Suppes] p. 60 | Theorem 6 | dmin 4945 |
| [Suppes] p. 60 | Theorem 8 | rnun 5152 |
| [Suppes] p. 60 | Theorem 9 | rnin 5153 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4924 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4919 brcnvg 4917 |
| [Suppes] p. 62 | Equation 5 | elcnv 4913 elcnv2 4914 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5121 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5151 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5149 |
| [Suppes] p. 63 | Theorem 20 | co02 5257 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5008 |
| [Suppes] p. 63 | Definition 7 | df-co 4740 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4921 |
| [Suppes] p. 64 | Theorem 27 | coass 5262 |
| [Suppes] p. 65 | Theorem 31 | resundi 5032 |
| [Suppes] p. 65 | Theorem 34 | elima 5087 elima2 5088 elima3 5089 elimag 5086 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5156 |
| [Suppes] p. 66 | Theorem 40 | dminss 5158 |
| [Suppes] p. 66 | Theorem 41 | imainss 5159 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5162 |
| [Suppes] p. 81 | Definition 34 | dfec2 6748 |
| [Suppes] p. 82 | Theorem 72 | elec 6786 elecg 6785 |
| [Suppes] p. 82 | Theorem 73 | erth 6791 erth2 6792 |
| [Suppes] p. 89 | Theorem 96 | map0b 6899 |
| [Suppes] p. 89 | Theorem 97 | map0 6901 map0g 6900 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6902 |
| [Suppes] p. 89 | Theorem 99 | mapss 6903 |
| [Suppes] p. 92 | Theorem 1 | enref 6981 enrefg 6980 |
| [Suppes] p. 92 | Theorem 2 | ensym 6998 ensymb 6997 ensymi 6999 |
| [Suppes] p. 92 | Theorem 3 | entr 7001 |
| [Suppes] p. 92 | Theorem 4 | unen 7034 |
| [Suppes] p. 94 | Theorem 15 | endom 6979 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6995 |
| [Suppes] p. 94 | Theorem 17 | domtr 7002 |
| [Suppes] p. 95 | Theorem 18 | isbth 7209 |
| [Suppes] p. 98 | Exercise 4 | fundmen 7024 fundmeng 7025 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7061 |
| [Suppes] p. 130 | Definition 3 | df-tr 4193 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4592 |
| [Suppes] p. 134 | Definition 6 | df-suc 4474 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4707 finds 4704 finds1 4706 finds2 4705 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7633 df-ltpq 7626 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4493 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2213 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2227 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2226 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2249 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6032 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3031 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3694 elpr2 3695 elprg 3693 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3689 elsn2 3707 elsn2g 3706 elsng 3688 velsn 3690 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4329 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3684 sneqr 3848 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3692 dfsn2 3687 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4540 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4335 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4313 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4544 unexg 4546 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3722 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3899 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3207 df-un 3205 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3912 uniprg 3913 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4275 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3721 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4509 elsucg 4507 sstr2 3235 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3353 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3401 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3366 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3419 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3456 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3457 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3216 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3658 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3380 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3214 dfss2 3218 sseqin2 3428 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3248 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3429 inss2 3430 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3288 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3907 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4314 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4321 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2520 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4221 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3203 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3498 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3565 difidALT 3566 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3509 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4643 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2805 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4226 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3535 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4231 ssexg 4233 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4228 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4654 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4645 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3561 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3334 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3470 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3335 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3343 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2516 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2517 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4848 xpexg 4846 xpexgALT 6304 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4738 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5401 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5562 fun11 5404 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5344 svrelfun 5402 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4923 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4925 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4743 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4744 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4740 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5198 dfrel2 5194 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4840 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4850 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4856 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4870 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5047 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5024 opelresg 5026 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5040 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5043 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5048 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5374 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5242 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5373 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5563 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2124 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5341 fv3 5671 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5282 cnvexg 5281 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5005 dmexg 5002 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5006 rnexg 5003 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnvm 5098 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5665 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5675 tz6.12 5676 tz6.12c 5678 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5639 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5336 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5337 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5339 wfo 5331 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5338 wf1 5330 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5340 wf1o 5332 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5753 eqfnfv2 5754 eqfnfv2f 5757 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5725 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5884 fnexALT 6282 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5883 resfunexgALT 6279 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5422 funimaexg 5421 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4094 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5113 iniseg 5115 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4392 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5342 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5961 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5962 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5967 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5969 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5977 |
| [TakeutiZaring] p. 35 | Notation | wtr 4192 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4457 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4196 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4680 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4484 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4488 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4596 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4471 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4590 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4656 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4686 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4194 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4615 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4591 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3926 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4474 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4518 sucidg 4519 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4605 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4472 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4610 ordelsuc 4609 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4698 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4699 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4700 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4697 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4711 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4703 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4701 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4702 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3947 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4208 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3948 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4621 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3934 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6517 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6574 tfri1d 6544 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6575 tfri2d 6545 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6576 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6511 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6495 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6675 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6671 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6668 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6672 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6720 nnaordi 6719 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4020 uniss2 3929 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6681 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6691 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6682 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6669 omsuc 6683 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6692 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6728 nnmordi 6727 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6670 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7451 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 7012 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7086 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7087 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6955 isfi 6977 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7058 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6862 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7064 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7077 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1559 |
| [Tarski] p. 68 | Lemma 6 | equid 1749 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1752 |
| [Tarski] p. 70 | Lemma 14 | spim 1786 spime 1789 spimeh 1787 spimh 1785 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1555 ax-11o 1871 ax11i 1762 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1935 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1575 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2204 ax-14 2205 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 719 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 735 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 764 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 773 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 797 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 621 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 648 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 845 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2178 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 745 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 844 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 634 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 893 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 851 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 864 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 647 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 861 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 863 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 720 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 783 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 622 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 626 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 901 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 915 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 776 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 777 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 812 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 813 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 811 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1006 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 786 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 784 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 785 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 746 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 875 pm2.5gdc 874 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 870 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 749 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 750 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 661 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 662 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 730 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 899 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 733 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 734 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 756 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 808 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 809 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 665 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 721 pm2.67 751 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 877 pm2.521gdc 876 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 755 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 818 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 902 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 923 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 819 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 820 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 913 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 762 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 966 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 967 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 968 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 761 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 264 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 265 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 701 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 347 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 261 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 262 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 868 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 867 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 345 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 346 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 696 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 601 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 333 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 331 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 332 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 763 pm3.44 723 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 606 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 793 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 879 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 880 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 898 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 702 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 961 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 765 pm4.25 766 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 826 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 736 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 775 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 800 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 609 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 830 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1007 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 824 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 980 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 958 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 787 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 822 pm4.45 792 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1530 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 965 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 905 imorr 729 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 758 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 759 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 910 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 947 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 760 pm4.56 788 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 948 oranim 789 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 693 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 894 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 908 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 694 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 909 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 895 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 835 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 752 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 607 pm4.76 608 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 718 pm4.77 807 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 790 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 911 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 715 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 916 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 959 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 960 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 237 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 240 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 559 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 605 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 918 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 920 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 919 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1434 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 836 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 912 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1439 pm5.18dc 891 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 714 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 703 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1437 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1442 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1443 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 903 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 475 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 242 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 934 pm5.6r 935 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 963 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 453 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 613 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 925 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 614 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 250 pm5.41 251 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 320 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 933 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 810 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 926 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 921 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 802 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 954 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 955 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 970 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 244 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 179 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 971 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1684 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1534 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1681 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1944 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2082 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2484 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2485 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2945 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3089 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5313 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5314 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2159 eupickbi 2162 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5341 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7455 |
| [vandenDries] p. 43 | Theorem 62 | pellexlem1 15791 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |