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 7314 fidcenum 7155 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7155 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7314 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13048 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7124 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7110 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13063 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13065 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13054 znnen 13021 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13066 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13067 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11039 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4635 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11169 df-pfx 11255 df-substr 11228 df-word 11115 lencl 11118 wrd0 11139 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8359 addcan2d 8364 addcan2i 8362 addcand 8363 addcani 8361 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8370 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8427 negsubd 8496 negsubi 8457 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8429 negnegd 8481 negnegi 8449 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8564 subdid 8593 subdii 8586 subdir 8565 subdird 8594 subdiri 8587 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8568 mul01d 8572 mul01i 8570 mul02 8566 mul02d 8571 mul02i 8569 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8973 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8924 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8577 mul2negd 8592 mul2negi 8585 mulneg1 8574 mulneg1d 8590 mulneg1i 8583 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14161 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8893 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9912 rpaddcld 9947 rpmulcl 9913 rpmulcld 9948 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9924 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8284 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8718 ltadd1dd 8736 ltadd1i 8682 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8772 ltmul1a 8771 ltmul1i 9100 ltmul1ii 9108 ltmul2 9036 ltmul2d 9974 ltmul2dd 9988 ltmul2i 9103 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8306 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8648 lt0neg1d 8695 ltneg 8642 ltnegd 8703 ltnegi 8673 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8625 lt2addd 8747 lt2addi 8690 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9889 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9030 recgt0d 9114 recgt0i 9086 recgt0ii 9087 |
| [Apostol] p. 22 | Definition of integers | df-z 9480 |
| [Apostol] p. 22 | Definition of rationals | df-q 9854 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7193 |
| [Apostol] p. 26 | Theorem I.29 | arch 9399 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9599 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9400 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10517 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12434 zneo 9581 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11593 sqrtthi 11681 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9146 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12609 |
| [Apostol] p. 363 | Remark | absgt0api 11708 |
| [Apostol] p. 363 | Example | abssubd 11755 abssubi 11712 |
| [ApostolNT] p. 14 | Definition | df-dvds 12351 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12367 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12391 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12387 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12381 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12383 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12368 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12369 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12374 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12408 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12410 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12412 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12587 |
| [ApostolNT] p. 16 | Definition | isprm2 12691 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12666 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13078 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12546 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12588 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12590 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12560 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12553 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12718 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12720 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12943 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12487 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12633 |
| [ApostolNT] p. 25 | Definition | df-phi 12785 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12815 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12796 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12800 |
| [ApostolNT] p. 38 | Remark | df-sgm 15709 |
| [ApostolNT] p. 38 | Definition | df-sgm 15709 |
| [ApostolNT] p. 104 | Definition | congr 12674 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12354 |
| [ApostolNT] p. 106 | Definition | moddvds 12362 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12441 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12442 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10604 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10641 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10929 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12386 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12677 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12996 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12679 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12807 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12826 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12808 |
| [ApostolNT] p. 179 | Definition | df-lgs 15730 lgsprme0 15774 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15775 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15751 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15766 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15817 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15836 2lgsoddprm 15845 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15801 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15812 |
| [ApostolNT] p. 188 | Definition | df-lgs 15730 lgs1 15776 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15767 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15769 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15777 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15778 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 621 pm2.65 665 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6017 onsucelsucexmidlem 4627 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16615 |
| [Bauer], p. 483 | Definition | n0rf 3507 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15703 2irrexpqap 15705 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7131 ssfiexmid 7063 ssfiexmidt 7065 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15380 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15370 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8825 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7314 |
| [BauerSwan], p. 14 | Remark | 0ct 7306 ctm 7308 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16618 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7721 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7634 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7723 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7757 addlocpr 7756 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7783 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7786 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7791 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2082 |
| [BellMachover] p. 460 | Notation | df-mo 2083 |
| [BellMachover] p. 460 | Definition | mo3 2134 mo3h 2133 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2216 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4210 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4267 |
| [BellMachover] p. 466 | Axiom Union | axun2 4532 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4640 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4481 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4643 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4594 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4466 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4687 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4712 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1475 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1473 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1476 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1471 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15912 isuhgropm 15935 isusgropen 16019 isuspgropen 16018 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16108 uhgrspansubgr 16131 |
| [Bollobas] p. 4 | Definition | df-wlks 16172 |
| [Bollobas] p. 5 | Definition | df-trls 16235 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15924 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13441 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13487 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13502 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14014 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13949 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5924 fcofo 5925 |
| [BourbakiTop1] p. | Remark | xnegmnf 10064 xnegpnf 10063 |
| [BourbakiTop1] p. | Remark | rexneg 10065 |
| [BourbakiTop1] p. | Proposition | ishmeo 15031 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14884 |
| [BourbakiTop1] p. | Property V_ii | innei 14890 |
| [BourbakiTop1] p. | Property V_iv | neissex 14892 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14881 neiss 14877 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14949 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15026 |
| [BourbakiTop1] p. | Property V_iii | elnei 14879 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14725 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13441 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13487 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13684 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4152 |
| [Church] p. 129 | Section II.24 | df-ifp 986 dfifp2dc 989 |
| [Cohen] p. 301 | Remark | relogoprlem 15595 |
| [Cohen] p. 301 | Property 2 | relogmul 15596 relogmuld 15611 |
| [Cohen] p. 301 | Property 3 | relogdiv 15597 relogdivd 15612 |
| [Cohen] p. 301 | Property 4 | relogexp 15599 |
| [Cohen] p. 301 | Property 1a | log1 15593 |
| [Cohen] p. 301 | Property 1b | loge 15594 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15692 |
| [Cohen4] p. 352 | Definition | rpelogb 15676 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15682 |
| [Cohen4] p. 361 | Property 3 | logbrec 15687 rprelogbdiv 15684 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15680 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15685 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15674 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15675 |
| [Cohen4] p. 367 | Property | rplogbchbase 15677 |
| [Cohen4] p. 377 | Property 2 | logblt 15689 |
| [Crosilla] p. | Axiom 1 | ax-ext 2213 |
| [Crosilla] p. | Axiom 2 | ax-pr 4299 |
| [Crosilla] p. | Axiom 3 | ax-un 4530 |
| [Crosilla] p. | Axiom 4 | ax-nul 4215 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4686 |
| [Crosilla] p. | Axiom 6 | ru 3030 |
| [Crosilla] p. | Axiom 8 | ax-pow 4264 |
| [Crosilla] p. | Axiom 9 | ax-setind 4635 |
| [Crosilla], p. | Axiom 6 | ax-sep 4207 |
| [Crosilla], p. | Axiom 7 | ax-coll 4204 |
| [Crosilla], p. | Axiom 7' | repizf 4205 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4619 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6017 |
| [Crosilla], p. | Definition of ordinal | df-iord 4463 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4633 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16108 uhgrspansubgr 16131 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15924 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3202 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4689 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6819 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4214 |
| [Enderton] p. 19 | Definition | df-tp 3677 |
| [Enderton] p. 26 | Exercise 5 | unissb 3923 |
| [Enderton] p. 26 | Exercise 10 | pwel 4310 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4383 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4040 iinin2m 4039 iunin1 4035 iunin2 4034 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4038 iundif2ss 4036 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4053 |
| [Enderton] p. 33 | Exercise 25 | iununir 4054 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4061 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4577 iunpwss 4062 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4309 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4282 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4547 rnex 5000 rnexg 4997 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4941 rnuni 5148 |
| [Enderton] p. 42 | Definition of a function | dffun7 5353 dffun8 5354 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5710 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5391 |
| [Enderton] p. 44 | Definition (d) | dfima2 5078 dfima3 5079 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5715 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7421 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5902 |
| [Enderton] p. 52 | Definition | df-map 6819 |
| [Enderton] p. 53 | Exercise 21 | coass 5255 |
| [Enderton] p. 53 | Exercise 27 | dmco 5245 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5401 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5112 |
| [Enderton] p. 54 | Remark | ixpf 6889 ixpssmap 6901 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6868 |
| [Enderton] p. 56 | Theorem 3M | erref 6722 |
| [Enderton] p. 57 | Lemma 3N | erthi 6750 |
| [Enderton] p. 57 | Definition | df-ec 6704 |
| [Enderton] p. 58 | Definition | df-qs 6708 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6809 th3qcor 6808 th3qlem1 6806 th3qlem2 6807 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6704 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4938 |
| [Enderton] p. 68 | Definition of successor | df-suc 4468 |
| [Enderton] p. 71 | Definition | df-tr 4188 dftr4 4192 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4510 unisucg 4511 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4510 unisucg 4511 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4201 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4202 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6642 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6644 onasuc 6634 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6021 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6643 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6645 onmsuc 6641 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6653 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6646 nnacom 6652 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6654 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6655 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6657 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6647 nnmsucr 6656 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6696 |
| [Enderton] p. 129 | Definition | df-en 6910 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5969 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13018 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7052 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7043 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7032 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7433 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7429 dju1en 7428 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3570 |
| [Enderton] p. 145 | Figure 38 | ffoss 5616 |
| [Enderton] p. 145 | Definition | df-dom 6911 |
| [Enderton] p. 146 | Example 1 | domen 6922 domeng 6923 |
| [Enderton] p. 146 | Example 3 | nndomo 7050 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7019 xpdom1g 7017 xpdom2g 7016 |
| [Enderton] p. 168 | Definition | df-po 4393 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4525 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4486 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4641 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4489 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4614 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4587 |
| [Enderton] p. 194 | Remark | onprc 4650 |
| [Enderton] p. 194 | Exercise 16 | suc11 4656 |
| [Enderton] p. 197 | Definition | df-card 7383 |
| [Enderton] p. 200 | Exercise 25 | tfis 4681 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4652 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4654 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4655 |
| [Geuvers], p. 1 | Remark | expap0 10832 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8795 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8834 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8796 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8151 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11765 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11773 maxle2 11774 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11775 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11778 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11779 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8762 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7567 enqer 7578 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7571 df-nqqs 7568 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7564 df-plqqs 7569 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7565 df-mqqs 7570 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7572 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7628 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7631 ltbtwnnq 7636 ltbtwnnqq 7635 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7620 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7621 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7757 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7799 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7798 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7817 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7833 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7839 ltaprlem 7838 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7836 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7792 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7812 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7801 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7800 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7808 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7858 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7946 enrer 7955 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7951 df-1r 7952 df-nr 7947 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7949 df-plr 7948 negexsr 7992 recexsrlem 7994 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7950 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9140 creur 9139 cru 8782 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8143 axcnre 8101 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11420 crimd 11539 crimi 11499 crre 11419 crred 11538 crrei 11498 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11422 remimd 11504 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11619 absval2d 11747 absval2i 11706 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11446 cjaddd 11527 cjaddi 11494 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11447 cjmuld 11528 cjmuli 11495 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11445 cjcjd 11505 cjcji 11477 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11444 cjreb 11428 cjrebd 11508 cjrebi 11480 cjred 11533 rere 11427 rereb 11425 rerebd 11507 rerebi 11479 rered 11531 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11453 addcjd 11519 addcji 11489 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11563 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11614 abscjd 11752 abscji 11710 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11626 abs00d 11748 abs00i 11707 absne0d 11749 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11658 releabsd 11753 releabsi 11711 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11631 absmuld 11756 absmuli 11713 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11617 sqabsaddi 11714 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11666 abstrid 11758 abstrii 11717 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10802 exp0 10806 expp1 10809 expp1d 10937 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10844 expaddd 10938 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15639 cxpmuld 15664 expmul 10847 expmuld 10939 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10841 mulexpd 10951 rpmulcxp 15636 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10245 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11888 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11890 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11889 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11893 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11886 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11882 climcj 11883 climim 11885 climre 11884 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8219 df-xr 8218 ltxr 10010 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11909 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10561 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14562 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15091 xmet0 15090 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15098 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15100 mstri 15200 xmettri 15099 xmstri 15199 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15006 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15238 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11872 addcncntop 15289 mulcn2 11874 mulcncntop 15291 subcn2 11873 subcncntop 15290 |
| [Gleason] p. 295 | Remark | bcval3 11014 bcval4 11015 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11029 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11012 df-bc 11011 |
| [Gleason] p. 296 | Remark | bcn0 11018 bcnn 11020 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12047 |
| [Gleason] p. 308 | Equation 2 | ef0 12235 |
| [Gleason] p. 308 | Equation 3 | efcj 12236 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12241 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12245 |
| [Gleason] p. 310 | Equation 14 | sinadd 12299 |
| [Gleason] p. 310 | Equation 15 | cosadd 12300 |
| [Gleason] p. 311 | Equation 17 | sincossq 12311 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12316 sinbnd 12315 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12216 |
| [Golan] p. 1 | Remark | srgisid 14002 |
| [Golan] p. 1 | Definition | df-srg 13980 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1497 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13596 mndideu 13511 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13623 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13652 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13663 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13685 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16705 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1467 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1468 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1470 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7440 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6667 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16689 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8837 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7690 df-imp 7689 df-iplp 7688 df-reap 8755 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8851 rerecapb 9023 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6300 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7882 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16334 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16682 dceqnconst 16681 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8120 caucvgpr 7902 caucvgprpr 7932 caucvgsr 8022 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7686 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16687 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4394 ltpopr 7815 ltsopr 7816 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8786 reapcotr 8778 reapirr 8757 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8306 gt0add 8753 leadd1 8610 lelttr 8268 lemul1a 9038 lenlt 8255 ltadd1 8609 ltletr 8269 ltmul1 8772 reaplt 8768 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16281 |
| [Jech] p. 4 | Definition of class | cv 1396 cvjust 2226 |
| [Jech] p. 78 | Note | opthprc 4777 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1578 |
| [Kreyszig] p. 3 | Property M1 | metcl 15080 xmetcl 15079 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15087 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8848 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15169 |
| [Kreyszig] p. 19 | Remark | mopntopon 15170 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15215 mopnm 15175 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15213 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15218 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15240 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14940 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14347 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14338 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14339 |
| [Kunen] p. 10 | Axiom 0 | a9e 1744 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4206 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6829 mapvalg 6827 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6823 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3980 |
| [Lang] p. 3 | Statement | lidrideqd 13466 mndbn0 13516 |
| [Lang] p. 3 | Definition | df-mnd 13502 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13483 |
| [Lang] p. 5 | Equation | gsumfzreidx 13926 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13717 |
| [Lang] p. 7 | Definition | dfgrp2e 13613 |
| [Levy] p. 338 | Axiom | df-clab 2218 df-clel 2227 df-cleq 2224 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1467 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1468 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1470 |
| [Margaris] p. 40 | Rule C | exlimiv 1646 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 860 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 899 exalim 1550 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 657 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1686 r19.2m 3581 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1602 19.3h 1601 rr19.3v 2945 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1526 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1667 alexim 1693 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1547 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1638 spsbe 1890 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1692 19.9h 1691 19.9v 1919 exlimd 1645 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1712 excomim 1711 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1713 r19.12 2639 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1694 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1516 ralbi 2665 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1603 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1604 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1652 rexbi 2666 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1714 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1505 alimd 1569 alimdh 1515 alimdv 1927 ralimdaa 2598 ralimdv 2600 ralimdva 2599 ralimdvva 2601 sbcimdv 3097 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1715 19.21 1631 19.21bi 1606 19.21h 1605 19.21ht 1629 19.21t 1630 19.21v 1921 alrimd 1658 alrimdd 1657 alrimdh 1527 alrimdv 1924 alrimi 1570 alrimih 1517 alrimiv 1922 alrimivv 1923 r19.21 2608 r19.21be 2623 r19.21bi 2620 r19.21t 2607 r19.21v 2609 ralrimd 2610 ralrimdv 2611 ralrimdva 2612 ralrimdvv 2616 ralrimdvva 2617 ralrimi 2603 ralrimiv 2604 ralrimiva 2605 ralrimivv 2613 ralrimivva 2614 ralrimivvva 2615 ralrimivw 2606 rexlimi 2643 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1929 2eximdv 1930 exim 1647 eximd 1660 eximdh 1659 eximdv 1928 rexim 2626 reximdai 2630 reximddv 2635 reximddv2 2637 reximdv 2633 reximdv2 2631 reximdva 2634 reximdvai 2632 reximi2 2628 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1726 19.23bi 1640 19.23h 1546 19.23ht 1545 19.23t 1725 19.23v 1931 19.23vv 1932 exlimd2 1643 exlimdh 1644 exlimdv 1867 exlimdvv 1946 exlimi 1642 exlimih 1641 exlimiv 1646 exlimivv 1945 r19.23 2641 r19.23v 2642 rexlimd 2647 rexlimdv 2649 rexlimdv3a 2652 rexlimdva 2650 rexlimdva2 2653 rexlimdvaa 2651 rexlimdvv 2657 rexlimdvva 2658 rexlimdvw 2654 rexlimiv 2644 rexlimiva 2645 rexlimivv 2656 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1687 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1674 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1530 19.26-3an 1531 19.26 1529 r19.26-2 2662 r19.26-3 2663 r19.26 2659 r19.26m 2664 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1609 19.27h 1608 19.27v 1948 r19.27av 2668 r19.27m 3590 r19.27mv 3591 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1611 19.28h 1610 19.28v 1949 r19.28av 2669 r19.28m 3584 r19.28mv 3587 rr19.28v 2946 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1668 19.29r 1669 19.29r2 1670 19.29x 1671 r19.29 2670 r19.29d2r 2677 r19.29r 2671 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1675 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1729 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1727 19.32r 1728 r19.32r 2679 r19.32vdc 2682 r19.32vr 2681 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1532 19.33b2 1677 19.33bdc 1678 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1732 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1672 19.35i 1673 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1721 19.36aiv 1950 19.36i 1720 r19.36av 2684 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1722 19.37aiv 1723 r19.37 2685 r19.37av 2686 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1724 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1688 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1680 19.40 1679 r19.40 2687 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1734 19.41h 1733 19.41v 1951 19.41vv 1952 19.41vvv 1953 19.41vvvv 1954 r19.41 2688 r19.41v 2689 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1736 19.42h 1735 19.42v 1955 19.42vv 1960 19.42vvv 1961 19.42vvvv 1962 r19.42v 2690 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1676 r19.43 2691 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1730 r19.44av 2692 r19.44mv 3589 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1731 r19.45av 2693 r19.45mv 3588 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2104 |
| [Megill] p. 444 | Axiom C5 | ax-17 1574 |
| [Megill] p. 445 | Lemma L12 | alequcom 1563 ax-10 1553 |
| [Megill] p. 446 | Lemma L17 | equtrr 1758 |
| [Megill] p. 446 | Lemma L19 | hbnae 1769 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1811 sbid 1822 |
| [Megill] p. 448 | Scheme C5' | ax-4 1558 |
| [Megill] p. 448 | Scheme C6' | ax-7 1496 |
| [Megill] p. 448 | Scheme C8' | ax-8 1552 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1555 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1764 |
| [Megill] p. 448 | Scheme C12' | ax-13 2204 |
| [Megill] p. 448 | Scheme C13' | ax-14 2205 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1871 |
| [Megill] p. 448 | Scheme C16' | ax-16 1862 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1778 dral2 1779 drex1 1846 drex2 1780 drsb1 1847 drsb2 1889 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2040 sbequ 1888 sbid2v 2049 |
| [Megill] p. 450 | Example in Appendix | hba1 1588 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3115 rspsbca 3116 stdpc4 1823 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3121 stdpc5 1632 |
| [Mendelson] p. 81 | Rule C | exlimiv 1646 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1751 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1818 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3531 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3532 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3447 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3495 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3448 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3338 |
| [Mendelson] p. 231 | Definition of union | unssin 3446 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4573 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3892 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4379 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4380 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4381 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3913 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4859 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5257 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4468 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7031 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7005 xpsneng 7006 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7011 xpcomeng 7012 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7014 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7008 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6821 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6986 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7036 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6855 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6987 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7432 djucomen 7431 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7430 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6635 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3429 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4814 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4815 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4151 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5252 coi2 5253 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4945 rn0 4988 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5141 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4835 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4952 rnxpm 5166 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4806 xp0 5156 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5095 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5092 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5091 imaexg 5090 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5087 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5777 funfvop 5759 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5687 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5697 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5371 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5909 dff13f 5911 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5877 funrnex 6276 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5903 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5220 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3944 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6318 df-1st 6303 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6319 df-2nd 6304 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1495 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1552 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1554 ax-11o 1871 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1875 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1496 |
| [Monk2] p. 109 | Lemma 15 | equvin 1911 equvini 1806 eqvinop 4335 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1574 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1699 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1496 |
| [Monk2] p. 114 | Lemma 22 | hba1 1588 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1600 nfia1 1628 |
| [Monk2] p. 114 | Lemma 24 | hba2 1599 nfa2 1627 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 838 dftest 16706 |
| [Munkres] p. 77 | Example 2 | distop 14812 |
| [Munkres] p. 78 | Definition of basis | df-bases 14770 isbasis3g 14773 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13345 tgval2 14778 |
| [Munkres] p. 79 | Remark | tgcl 14791 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14785 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14806 tgss3 14805 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14807 basgen2 14808 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14897 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14839 topcld 14836 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14840 |
| [Munkres] p. 94 | Definition of closure | clsval 14838 |
| [Munkres] p. 94 | Definition of interior | ntrval 14837 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14915 iscn 14924 iscn2 14927 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14957 cncnp2m 14958 cncnpi 14955 df-cnp 14916 iscnp 14926 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15241 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7093 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7363 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7351 omniwomnimkv 7366 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3317 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7334 exmidomniim 7340 finomni 7339 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7319 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16640 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16644 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7100 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7412 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7413 exmidfodomrlemrALT 7414 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7348 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16626 peano4nninf 16625 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16628 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16636 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16638 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16624 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2218 rabid 2709 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2044 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2224 |
| [Quine] p. 19 | Definition 2.9 | df-v 2804 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2340 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2352 abid2f 2400 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1936 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1934 sb6 1935 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2227 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2231 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2233 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3032 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3033 dfsbcq2 3034 |
| [Quine] p. 43 | Theorem 6.8 | vex 2805 |
| [Quine] p. 43 | Theorem 6.9 | isset 2809 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2888 spcgv 2893 spcimgf 2886 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3043 spsbcd 3044 |
| [Quine] p. 44 | Theorem 6.12 | elex 2814 |
| [Quine] p. 44 | Theorem 6.13 | elab 2950 elabg 2952 elabgf 2948 |
| [Quine] p. 44 | Theorem 6.14 | noel 3498 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3734 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3676 df-sn 3675 |
| [Quine] p. 49 | Theorem 7.4 | snss 3808 snssg 3807 |
| [Quine] p. 49 | Theorem 7.5 | prss 3829 prssg 3830 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3777 prid1g 3775 prid2 3778 prid2g 3776 snid 3700 snidg 3698 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4274 snexprc 4276 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4301 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3909 unisng 3910 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3912 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3921 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3920 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5297 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5287 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5298 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5302 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5303 |
| [Quine] p. 58 | Definition 9.1 | df-op 3678 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4350 opabidw 4351 opelopab 4366 opelopaba 4360 opelopabaf 4368 opelopabf 4369 opelopabg 4362 opelopabga 4357 opelopabgf 4364 oprabid 6050 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4731 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4733 |
| [Quine] p. 64 | Definition 9.15 | df-id 4390 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5388 |
| [Quine] p. 65 | Theorem 10.4 | funi 5358 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5378 funsng 5376 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5328 |
| [Quine] p. 65 | Definition 10.2 | args 5105 dffv4g 5636 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5334 fv2 5634 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10987 nn0opth2d 10986 nn0opthd 10985 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5415 funimaexg 5414 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13949 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14014 |
| [Rudin] p. 164 | Equation 27 | efcan 12239 |
| [Rudin] p. 164 | Equation 30 | efzval 12246 |
| [Rudin] p. 167 | Equation 48 | absefi 12332 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1470 |
| [Sanford] p. 39 | Rule 4 | mptxor 1468 |
| [Sanford] p. 40 | Rule 1 | mptnan 1467 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5121 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5123 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5120 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5118 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14016 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14810 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3472 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3566 dif0 3565 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3579 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3465 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3466 |
| [Stoll] p. 20 | Remark | invdif 3449 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3679 |
| [Stoll] p. 43 | Definition | uniiun 4024 |
| [Stoll] p. 44 | Definition | intiin 4025 |
| [Stoll] p. 45 | Definition | df-iin 3973 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3972 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 896 imanst 895 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3472 |
| [Suppes] p. 22 | Theorem 2 | eq0 3513 |
| [Suppes] p. 22 | Theorem 4 | eqss 3242 eqssd 3244 eqssi 3243 |
| [Suppes] p. 23 | Theorem 5 | ss0 3535 ss0b 3534 |
| [Suppes] p. 23 | Theorem 6 | sstr 3235 |
| [Suppes] p. 25 | Theorem 12 | elin 3390 elun 3348 |
| [Suppes] p. 26 | Theorem 15 | inidm 3416 |
| [Suppes] p. 26 | Theorem 16 | in0 3529 |
| [Suppes] p. 27 | Theorem 23 | unidm 3350 |
| [Suppes] p. 27 | Theorem 24 | un0 3528 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3370 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3377 |
| [Suppes] p. 27 | Theorem 27 | unss 3381 |
| [Suppes] p. 27 | Theorem 28 | indir 3456 |
| [Suppes] p. 27 | Theorem 29 | undir 3457 |
| [Suppes] p. 28 | Theorem 32 | difid 3563 difidALT 3564 |
| [Suppes] p. 29 | Theorem 33 | difin 3444 |
| [Suppes] p. 29 | Theorem 34 | indif 3450 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3569 |
| [Suppes] p. 29 | Theorem 36 | difun2 3574 |
| [Suppes] p. 29 | Theorem 37 | difin0 3568 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3567 |
| [Suppes] p. 29 | Theorem 39 | difundi 3459 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3461 |
| [Suppes] p. 30 | Theorem 41 | nalset 4219 |
| [Suppes] p. 39 | Theorem 61 | uniss 3914 |
| [Suppes] p. 39 | Theorem 65 | uniop 4348 |
| [Suppes] p. 41 | Theorem 70 | intsn 3963 |
| [Suppes] p. 42 | Theorem 71 | intpr 3960 intprg 3961 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4575 op1stbg 4576 |
| [Suppes] p. 42 | Theorem 78 | intun 3959 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4004 dfiun2g 4002 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4005 |
| [Suppes] p. 47 | Theorem 86 | elpw 3658 elpw2 4247 elpw2g 4246 elpwg 3660 |
| [Suppes] p. 47 | Theorem 87 | pwid 3667 |
| [Suppes] p. 47 | Theorem 89 | pw0 3820 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3888 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4833 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4865 xpindir 4866 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4782 xpundir 4783 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4646 |
| [Suppes] p. 58 | Theorem 2 | relss 4813 |
| [Suppes] p. 59 | Theorem 4 | eldm 4928 eldm2 4929 eldm2g 4927 eldmg 4926 |
| [Suppes] p. 59 | Definition 3 | df-dm 4735 |
| [Suppes] p. 60 | Theorem 6 | dmin 4939 |
| [Suppes] p. 60 | Theorem 8 | rnun 5145 |
| [Suppes] p. 60 | Theorem 9 | rnin 5146 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4918 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4913 brcnvg 4911 |
| [Suppes] p. 62 | Equation 5 | elcnv 4907 elcnv2 4908 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5114 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5144 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5142 |
| [Suppes] p. 63 | Theorem 20 | co02 5250 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5002 |
| [Suppes] p. 63 | Definition 7 | df-co 4734 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4915 |
| [Suppes] p. 64 | Theorem 27 | coass 5255 |
| [Suppes] p. 65 | Theorem 31 | resundi 5026 |
| [Suppes] p. 65 | Theorem 34 | elima 5081 elima2 5082 elima3 5083 elimag 5080 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5149 |
| [Suppes] p. 66 | Theorem 40 | dminss 5151 |
| [Suppes] p. 66 | Theorem 41 | imainss 5152 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5155 |
| [Suppes] p. 81 | Definition 34 | dfec2 6705 |
| [Suppes] p. 82 | Theorem 72 | elec 6743 elecg 6742 |
| [Suppes] p. 82 | Theorem 73 | erth 6748 erth2 6749 |
| [Suppes] p. 89 | Theorem 96 | map0b 6856 |
| [Suppes] p. 89 | Theorem 97 | map0 6858 map0g 6857 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6859 |
| [Suppes] p. 89 | Theorem 99 | mapss 6860 |
| [Suppes] p. 92 | Theorem 1 | enref 6938 enrefg 6937 |
| [Suppes] p. 92 | Theorem 2 | ensym 6955 ensymb 6954 ensymi 6956 |
| [Suppes] p. 92 | Theorem 3 | entr 6958 |
| [Suppes] p. 92 | Theorem 4 | unen 6991 |
| [Suppes] p. 94 | Theorem 15 | endom 6936 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6952 |
| [Suppes] p. 94 | Theorem 17 | domtr 6959 |
| [Suppes] p. 95 | Theorem 18 | isbth 7166 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6981 fundmeng 6982 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7018 |
| [Suppes] p. 130 | Definition 3 | df-tr 4188 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4586 |
| [Suppes] p. 134 | Definition 6 | df-suc 4468 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4701 finds 4698 finds1 4700 finds2 4699 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7573 df-ltpq 7566 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4487 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2213 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2227 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2226 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2249 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6022 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3030 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3690 elpr2 3691 elprg 3689 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3685 elsn2 3703 elsn2g 3702 elsng 3684 velsn 3686 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4323 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3680 sneqr 3843 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3688 dfsn2 3683 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4534 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4329 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4307 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4538 unexg 4540 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3718 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3894 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3206 df-un 3204 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3907 uniprg 3908 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4269 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3717 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4503 elsucg 4501 sstr2 3234 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3351 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3399 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3364 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3417 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3454 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3455 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3215 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3654 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3378 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3213 dfss2 3217 sseqin2 3426 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3247 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3427 inss2 3428 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3287 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3902 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4308 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4315 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2519 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4216 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3202 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3496 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3563 difidALT 3564 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3507 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4637 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2804 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4221 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3533 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4226 ssexg 4228 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4223 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4648 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4639 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3559 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3332 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3468 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3333 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3341 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2515 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2516 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4842 xpexg 4840 xpexgALT 6295 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4732 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5394 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5553 fun11 5397 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5337 svrelfun 5395 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4917 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4919 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4737 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4738 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4734 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5191 dfrel2 5187 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4834 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4844 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4850 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4864 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5041 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5018 opelresg 5020 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5034 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5037 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5042 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5367 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5235 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5366 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5554 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2124 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5334 fv3 5662 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5275 cnvexg 5274 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4999 dmexg 4996 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5000 rnexg 4997 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5656 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5666 tz6.12 5667 tz6.12c 5669 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5630 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5329 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5330 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5332 wfo 5324 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5331 wf1 5323 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5333 wf1o 5325 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5744 eqfnfv2 5745 eqfnfv2f 5748 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5716 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5876 fnexALT 6273 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5875 resfunexgALT 6270 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5415 funimaexg 5414 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4089 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5106 iniseg 5108 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4386 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5335 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5951 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5952 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5957 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5959 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5967 |
| [TakeutiZaring] p. 35 | Notation | wtr 4187 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4451 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4191 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4674 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4478 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4482 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4590 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4465 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4584 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4650 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4680 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4189 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4609 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4585 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3921 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4468 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4512 sucidg 4513 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4599 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4466 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4604 ordelsuc 4603 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4692 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4693 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4694 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4691 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4705 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4697 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4695 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4696 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3942 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4203 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3943 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4615 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3929 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6474 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6531 tfri1d 6501 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6532 tfri2d 6502 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6533 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6468 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6452 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6632 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6628 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6625 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6629 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6677 nnaordi 6676 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4015 uniss2 3924 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6638 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6648 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6639 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6626 omsuc 6640 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6649 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6685 nnmordi 6684 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6627 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7391 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6969 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7043 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7044 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6912 isfi 6934 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7015 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6819 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7021 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7034 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1558 |
| [Tarski] p. 68 | Lemma 6 | equid 1749 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1752 |
| [Tarski] p. 70 | Lemma 14 | spim 1786 spime 1789 spimeh 1787 spimh 1785 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1554 ax-11o 1871 ax11i 1762 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1935 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1574 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2204 ax-14 2205 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 718 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 734 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 763 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 772 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 796 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 621 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 648 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 844 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2178 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 744 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 843 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 634 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 892 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 850 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 863 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 647 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 860 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 862 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 719 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 782 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 622 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 626 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 900 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 914 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 775 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 776 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 811 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 812 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 810 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1005 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 785 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 783 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 784 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 745 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 874 pm2.5gdc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 869 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 749 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 661 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 662 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 729 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 898 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 732 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 733 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 872 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 755 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 807 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 808 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 665 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 720 pm2.67 750 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 876 pm2.521gdc 875 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 754 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 901 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 922 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 818 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 819 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 912 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 761 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 965 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 966 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 967 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 760 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 264 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 265 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 700 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 347 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 261 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 262 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 867 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 866 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 345 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 346 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 695 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 601 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 333 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 331 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 332 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 762 pm3.44 722 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 606 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 792 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 878 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 879 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 897 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 701 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 960 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 764 pm4.25 765 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 825 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 735 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 774 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 799 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 609 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 829 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1006 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 823 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 979 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 957 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 786 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 821 pm4.45 791 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1529 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 964 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 904 imorr 728 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 757 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 758 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 909 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 946 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 759 pm4.56 787 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 947 oranim 788 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 692 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 893 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 693 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 908 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 894 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 834 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 751 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 607 pm4.76 608 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 717 pm4.77 806 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 789 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 910 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 714 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 915 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 958 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 959 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 237 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 240 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 559 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 605 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 916 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 919 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 918 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1433 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 835 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 911 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1438 pm5.18dc 890 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 713 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 702 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1436 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1441 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1442 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 902 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 475 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 242 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 933 pm5.6r 934 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 962 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 453 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 613 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 924 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 614 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 250 pm5.41 251 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 320 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 932 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 809 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 925 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 920 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 801 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 953 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 954 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 969 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 244 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 179 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 970 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1683 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1533 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1680 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1944 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2082 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2483 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2484 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2944 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3088 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5306 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5307 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2159 eupickbi 2162 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5334 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7395 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |