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 7303 fidcenum 7144 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7144 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7303 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13033 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7115 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7101 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13048 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13050 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13039 znnen 13006 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13051 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13052 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11026 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4631 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11155 df-pfx 11241 df-substr 11214 df-word 11101 lencl 11104 wrd0 11125 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8347 addcan2d 8352 addcan2i 8350 addcand 8351 addcani 8349 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8358 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8415 negsubd 8484 negsubi 8445 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8417 negnegd 8469 negnegi 8437 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8552 subdid 8581 subdii 8574 subdir 8553 subdird 8582 subdiri 8575 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8556 mul01d 8560 mul01i 8558 mul02 8554 mul02d 8559 mul02i 8557 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8961 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8912 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8565 mul2negd 8580 mul2negi 8573 mulneg1 8562 mulneg1d 8578 mulneg1i 8571 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14145 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8881 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9900 rpaddcld 9935 rpmulcl 9901 rpmulcld 9936 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9912 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8272 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8706 ltadd1dd 8724 ltadd1i 8670 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8760 ltmul1a 8759 ltmul1i 9088 ltmul1ii 9096 ltmul2 9024 ltmul2d 9962 ltmul2dd 9976 ltmul2i 9091 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8294 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8636 lt0neg1d 8683 ltneg 8630 ltnegd 8691 ltnegi 8661 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8613 lt2addd 8735 lt2addi 8678 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9877 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9018 recgt0d 9102 recgt0i 9074 recgt0ii 9075 |
| [Apostol] p. 22 | Definition of integers | df-z 9468 |
| [Apostol] p. 22 | Definition of rationals | df-q 9842 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7182 |
| [Apostol] p. 26 | Theorem I.29 | arch 9387 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9587 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9388 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10504 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12419 zneo 9569 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11579 sqrtthi 11667 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9134 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12594 |
| [Apostol] p. 363 | Remark | absgt0api 11694 |
| [Apostol] p. 363 | Example | abssubd 11741 abssubi 11698 |
| [ApostolNT] p. 14 | Definition | df-dvds 12336 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12352 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12376 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12372 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12366 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12368 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12353 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12354 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12359 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12393 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12395 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12397 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12572 |
| [ApostolNT] p. 16 | Definition | isprm2 12676 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12651 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13063 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12531 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12573 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12575 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12545 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12538 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12703 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12705 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 12928 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12472 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12618 |
| [ApostolNT] p. 25 | Definition | df-phi 12770 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 12800 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12781 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12785 |
| [ApostolNT] p. 38 | Remark | df-sgm 15693 |
| [ApostolNT] p. 38 | Definition | df-sgm 15693 |
| [ApostolNT] p. 104 | Definition | congr 12659 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12339 |
| [ApostolNT] p. 106 | Definition | moddvds 12347 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12426 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12427 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10591 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10628 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 10916 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12371 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12662 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 12981 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12664 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12792 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 12811 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12793 |
| [ApostolNT] p. 179 | Definition | df-lgs 15714 lgsprme0 15758 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 15759 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 15735 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 15750 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 15801 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 15820 2lgsoddprm 15829 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 15785 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 15796 |
| [ApostolNT] p. 188 | Definition | df-lgs 15714 lgs1 15760 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 15751 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 15753 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 15761 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 15762 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 619 pm2.65 663 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6010 onsucelsucexmidlem 4623 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 16508 |
| [Bauer], p. 483 | Definition | n0rf 3505 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 15687 2irrexpqap 15689 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 7056 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15364 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15354 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8813 |
| [BauerSwan], p. 14 | Remark | 0ct 7295 ctm 7297 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 16511 |
| [BauerSwan], p. 14 | Table" is defined as ` ` per | enumct 7303 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7709 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7622 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7711 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7745 addlocpr 7744 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7771 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7774 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7779 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2080 |
| [BellMachover] p. 460 | Notation | df-mo 2081 |
| [BellMachover] p. 460 | Definition | mo3 2132 mo3h 2131 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2214 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4206 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4263 |
| [BellMachover] p. 466 | Axiom Union | axun2 4528 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4636 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4477 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4639 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4590 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4462 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4683 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4708 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1473 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1471 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1474 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1469 |
| [Bollobas] p. 1 | Section I.1 | df-edg 15896 isuhgropm 15918 isusgropen 16000 isuspgropen 15999 |
| [Bollobas] p. 4 | Definition | df-wlks 16106 |
| [Bollobas] p. 5 | Definition | df-trls 16167 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 15907 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13426 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13472 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13487 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 13998 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 13933 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5917 fcofo 5918 |
| [BourbakiTop1] p. | Remark | xnegmnf 10052 xnegpnf 10051 |
| [BourbakiTop1] p. | Remark | rexneg 10053 |
| [BourbakiTop1] p. | Proposition | ishmeo 15015 |
| [BourbakiTop1] p. | Property V_i | ssnei2 14868 |
| [BourbakiTop1] p. | Property V_ii | innei 14874 |
| [BourbakiTop1] p. | Property V_iv | neissex 14876 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 14865 neiss 14861 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 14933 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15010 |
| [BourbakiTop1] p. | Property V_iii | elnei 14863 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 14709 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13426 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13472 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13669 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4148 |
| [Church] p. 129 | Section II.24 | df-ifp 984 dfifp2dc 987 |
| [Cohen] p. 301 | Remark | relogoprlem 15579 |
| [Cohen] p. 301 | Property 2 | relogmul 15580 relogmuld 15595 |
| [Cohen] p. 301 | Property 3 | relogdiv 15581 relogdivd 15596 |
| [Cohen] p. 301 | Property 4 | relogexp 15583 |
| [Cohen] p. 301 | Property 1a | log1 15577 |
| [Cohen] p. 301 | Property 1b | loge 15578 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 15676 |
| [Cohen4] p. 352 | Definition | rpelogb 15660 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 15666 |
| [Cohen4] p. 361 | Property 3 | logbrec 15671 rprelogbdiv 15668 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 15664 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 15669 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 15658 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 15659 |
| [Cohen4] p. 367 | Property | rplogbchbase 15661 |
| [Cohen4] p. 377 | Property 2 | logblt 15673 |
| [Crosilla] p. | Axiom 1 | ax-ext 2211 |
| [Crosilla] p. | Axiom 2 | ax-pr 4295 |
| [Crosilla] p. | Axiom 3 | ax-un 4526 |
| [Crosilla] p. | Axiom 4 | ax-nul 4211 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4682 |
| [Crosilla] p. | Axiom 6 | ru 3028 |
| [Crosilla] p. | Axiom 8 | ax-pow 4260 |
| [Crosilla] p. | Axiom 9 | ax-setind 4631 |
| [Crosilla], p. | Axiom 6 | ax-sep 4203 |
| [Crosilla], p. | Axiom 7 | ax-coll 4200 |
| [Crosilla], p. | Axiom 7' | repizf 4201 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4615 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6010 |
| [Crosilla], p. | Definition of ordinal | df-iord 4459 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4629 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 15907 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3200 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4685 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6812 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4210 |
| [Enderton] p. 19 | Definition | df-tp 3675 |
| [Enderton] p. 26 | Exercise 5 | unissb 3919 |
| [Enderton] p. 26 | Exercise 10 | pwel 4306 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4379 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4036 iinin2m 4035 iunin1 4031 iunin2 4030 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4034 iundif2ss 4032 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4049 |
| [Enderton] p. 33 | Exercise 25 | iununir 4050 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4057 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4573 iunpwss 4058 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4305 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4278 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4543 rnex 4996 rnexg 4993 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4937 rnuni 5144 |
| [Enderton] p. 42 | Definition of a function | dffun7 5349 dffun8 5350 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5704 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5386 |
| [Enderton] p. 44 | Definition (d) | dfima2 5074 dfima3 5075 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5709 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7409 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5895 |
| [Enderton] p. 52 | Definition | df-map 6812 |
| [Enderton] p. 53 | Exercise 21 | coass 5251 |
| [Enderton] p. 53 | Exercise 27 | dmco 5241 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5396 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5108 |
| [Enderton] p. 54 | Remark | ixpf 6882 ixpssmap 6894 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6861 |
| [Enderton] p. 56 | Theorem 3M | erref 6715 |
| [Enderton] p. 57 | Lemma 3N | erthi 6743 |
| [Enderton] p. 57 | Definition | df-ec 6697 |
| [Enderton] p. 58 | Definition | df-qs 6701 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6802 th3qcor 6801 th3qlem1 6799 th3qlem2 6800 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6697 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4934 |
| [Enderton] p. 68 | Definition of successor | df-suc 4464 |
| [Enderton] p. 71 | Definition | df-tr 4184 dftr4 4188 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4506 unisucg 4507 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4506 unisucg 4507 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4197 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4198 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6635 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6637 onasuc 6627 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6014 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6636 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6638 onmsuc 6634 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6646 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6639 nnacom 6645 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6647 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6648 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6650 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6640 nnmsucr 6649 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6689 |
| [Enderton] p. 129 | Definition | df-en 6903 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 5962 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13003 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7045 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7036 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7025 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7421 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7417 dju1en 7416 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3568 |
| [Enderton] p. 145 | Figure 38 | ffoss 5610 |
| [Enderton] p. 145 | Definition | df-dom 6904 |
| [Enderton] p. 146 | Example 1 | domen 6915 domeng 6916 |
| [Enderton] p. 146 | Example 3 | nndomo 7043 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7012 xpdom1g 7010 xpdom2g 7009 |
| [Enderton] p. 168 | Definition | df-po 4389 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4521 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4482 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4637 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4485 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4610 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4583 |
| [Enderton] p. 194 | Remark | onprc 4646 |
| [Enderton] p. 194 | Exercise 16 | suc11 4652 |
| [Enderton] p. 197 | Definition | df-card 7372 |
| [Enderton] p. 200 | Exercise 25 | tfis 4677 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4648 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4650 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4651 |
| [Geuvers], p. 1 | Remark | expap0 10819 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8783 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8822 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8784 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8139 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11751 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11759 maxle2 11760 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11761 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11764 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11765 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8750 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7555 enqer 7566 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7559 df-nqqs 7556 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7552 df-plqqs 7557 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7553 df-mqqs 7558 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7560 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7616 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7619 ltbtwnnq 7624 ltbtwnnqq 7623 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7608 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7609 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7745 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7787 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7786 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7805 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7821 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7827 ltaprlem 7826 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7824 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7780 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7800 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7789 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7788 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7796 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7846 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7934 enrer 7943 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7939 df-1r 7940 df-nr 7935 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7937 df-plr 7936 negexsr 7980 recexsrlem 7982 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7938 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9128 creur 9127 cru 8770 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8131 axcnre 8089 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11406 crimd 11525 crimi 11485 crre 11405 crred 11524 crrei 11484 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11408 remimd 11490 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11605 absval2d 11733 absval2i 11692 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11432 cjaddd 11513 cjaddi 11480 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11433 cjmuld 11514 cjmuli 11481 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11431 cjcjd 11491 cjcji 11463 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11430 cjreb 11414 cjrebd 11494 cjrebi 11466 cjred 11519 rere 11413 rereb 11411 rerebd 11493 rerebi 11465 rered 11517 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11439 addcjd 11505 addcji 11475 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11549 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11600 abscjd 11738 abscji 11696 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11612 abs00d 11734 abs00i 11693 absne0d 11735 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11644 releabsd 11739 releabsi 11697 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11617 absmuld 11742 absmuli 11699 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11603 sqabsaddi 11700 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11652 abstrid 11744 abstrii 11703 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10789 exp0 10793 expp1 10796 expp1d 10924 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 10831 expaddd 10925 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15623 cxpmuld 15648 expmul 10834 expmuld 10926 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10828 mulexpd 10938 rpmulcxp 15620 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10233 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 11874 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 11876 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 11875 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 11879 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 11872 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 11868 climcj 11869 climim 11871 climre 11870 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8207 df-xr 8206 ltxr 9998 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 11895 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10548 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14546 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15075 xmet0 15074 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15082 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15084 mstri 15184 xmettri 15083 xmstri 15183 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 14990 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15222 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 11858 addcncntop 15273 mulcn2 11860 mulcncntop 15275 subcn2 11859 subcncntop 15274 |
| [Gleason] p. 295 | Remark | bcval3 11001 bcval4 11002 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11016 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 10999 df-bc 10998 |
| [Gleason] p. 296 | Remark | bcn0 11005 bcnn 11007 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12032 |
| [Gleason] p. 308 | Equation 2 | ef0 12220 |
| [Gleason] p. 308 | Equation 3 | efcj 12221 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12226 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12230 |
| [Gleason] p. 310 | Equation 14 | sinadd 12284 |
| [Gleason] p. 310 | Equation 15 | cosadd 12285 |
| [Gleason] p. 311 | Equation 17 | sincossq 12296 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12301 sinbnd 12300 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12201 |
| [Golan] p. 1 | Remark | srgisid 13986 |
| [Golan] p. 1 | Definition | df-srg 13964 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1495 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13581 mndideu 13496 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13608 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13637 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13648 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13670 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 16588 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1465 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1466 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1468 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7428 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6660 |
| [HoTT], p. | Exercise 11.10 | neapmkv 16582 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8825 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7678 df-imp 7677 df-iplp 7676 df-reap 8743 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8839 rerecapb 9011 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6293 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7870 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16227 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 16575 dceqnconst 16574 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8108 caucvgpr 7890 caucvgprpr 7920 caucvgsr 8010 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7674 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 16580 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4390 ltpopr 7803 ltsopr 7804 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8774 reapcotr 8766 reapirr 8745 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8294 gt0add 8741 leadd1 8598 lelttr 8256 lemul1a 9026 lenlt 8243 ltadd1 8597 ltletr 8257 ltmul1 8760 reaplt 8756 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16212 |
| [Jech] p. 4 | Definition of class | cv 1394 cvjust 2224 |
| [Jech] p. 78 | Note | opthprc 4773 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1576 |
| [Kreyszig] p. 3 | Property M1 | metcl 15064 xmetcl 15063 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15071 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8836 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15153 |
| [Kreyszig] p. 19 | Remark | mopntopon 15154 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15199 mopnm 15159 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15197 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15202 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15224 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 14924 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14331 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14322 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14323 |
| [Kunen] p. 10 | Axiom 0 | a9e 1742 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4202 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6822 mapvalg 6820 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6816 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3976 |
| [Lang] p. 3 | Statement | lidrideqd 13451 mndbn0 13501 |
| [Lang] p. 3 | Definition | df-mnd 13487 |
| [Lang] p. 4 | Definition of a (finite) product | gsumsplit1r 13468 |
| [Lang] p. 5 | Equation | gsumfzreidx 13911 |
| [Lang] p. 6 | Definition | mulgnn0gsum 13702 |
| [Lang] p. 7 | Definition | dfgrp2e 13598 |
| [Levy] p. 338 | Axiom | df-clab 2216 df-clel 2225 df-cleq 2222 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1465 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1466 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1468 |
| [Margaris] p. 40 | Rule C | exlimiv 1644 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 858 |
| [Margaris] p. 49 | Definition | dfbi2 388 dfordc 897 exalim 1548 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 655 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1684 r19.2m 3579 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1600 19.3h 1599 rr19.3v 2943 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1524 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1665 alexim 1691 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1545 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1636 spsbe 1888 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1690 19.9h 1689 19.9v 1917 exlimd 1643 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1710 excomim 1709 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1711 r19.12 2637 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1692 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1514 ralbi 2663 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1601 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1602 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1650 rexbi 2664 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1712 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1503 alimd 1567 alimdh 1513 alimdv 1925 ralimdaa 2596 ralimdv 2598 ralimdva 2597 ralimdvva 2599 sbcimdv 3095 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1713 19.21 1629 19.21bi 1604 19.21h 1603 19.21ht 1627 19.21t 1628 19.21v 1919 alrimd 1656 alrimdd 1655 alrimdh 1525 alrimdv 1922 alrimi 1568 alrimih 1515 alrimiv 1920 alrimivv 1921 r19.21 2606 r19.21be 2621 r19.21bi 2618 r19.21t 2605 r19.21v 2607 ralrimd 2608 ralrimdv 2609 ralrimdva 2610 ralrimdvv 2614 ralrimdvva 2615 ralrimi 2601 ralrimiv 2602 ralrimiva 2603 ralrimivv 2611 ralrimivva 2612 ralrimivvva 2613 ralrimivw 2604 rexlimi 2641 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1927 2eximdv 1928 exim 1645 eximd 1658 eximdh 1657 eximdv 1926 rexim 2624 reximdai 2628 reximddv 2633 reximddv2 2635 reximdv 2631 reximdv2 2629 reximdva 2632 reximdvai 2630 reximi2 2626 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1724 19.23bi 1638 19.23h 1544 19.23ht 1543 19.23t 1723 19.23v 1929 19.23vv 1930 exlimd2 1641 exlimdh 1642 exlimdv 1865 exlimdvv 1944 exlimi 1640 exlimih 1639 exlimiv 1644 exlimivv 1943 r19.23 2639 r19.23v 2640 rexlimd 2645 rexlimdv 2647 rexlimdv3a 2650 rexlimdva 2648 rexlimdva2 2651 rexlimdvaa 2649 rexlimdvv 2655 rexlimdvva 2656 rexlimdvw 2652 rexlimiv 2642 rexlimiva 2643 rexlimivv 2654 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1685 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1672 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1528 19.26-3an 1529 19.26 1527 r19.26-2 2660 r19.26-3 2661 r19.26 2657 r19.26m 2662 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1607 19.27h 1606 19.27v 1946 r19.27av 2666 r19.27m 3588 r19.27mv 3589 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1609 19.28h 1608 19.28v 1947 r19.28av 2667 r19.28m 3582 r19.28mv 3585 rr19.28v 2944 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1666 19.29r 1667 19.29r2 1668 19.29x 1669 r19.29 2668 r19.29d2r 2675 r19.29r 2669 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1673 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1727 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1725 19.32r 1726 r19.32r 2677 r19.32vdc 2680 r19.32vr 2679 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1530 19.33b2 1675 19.33bdc 1676 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1730 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1670 19.35i 1671 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1719 19.36aiv 1948 19.36i 1718 r19.36av 2682 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1720 19.37aiv 1721 r19.37 2683 r19.37av 2684 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1722 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1686 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1678 19.40 1677 r19.40 2685 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1732 19.41h 1731 19.41v 1949 19.41vv 1950 19.41vvv 1951 19.41vvvv 1952 r19.41 2686 r19.41v 2687 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1734 19.42h 1733 19.42v 1953 19.42vv 1958 19.42vvv 1959 19.42vvvv 1960 r19.42v 2688 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1674 r19.43 2689 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1728 r19.44av 2690 r19.44mv 3587 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1729 r19.45av 2691 r19.45mv 3586 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2102 |
| [Megill] p. 444 | Axiom C5 | ax-17 1572 |
| [Megill] p. 445 | Lemma L12 | alequcom 1561 ax-10 1551 |
| [Megill] p. 446 | Lemma L17 | equtrr 1756 |
| [Megill] p. 446 | Lemma L19 | hbnae 1767 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1809 sbid 1820 |
| [Megill] p. 448 | Scheme C5' | ax-4 1556 |
| [Megill] p. 448 | Scheme C6' | ax-7 1494 |
| [Megill] p. 448 | Scheme C8' | ax-8 1550 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1553 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1762 |
| [Megill] p. 448 | Scheme C12' | ax-13 2202 |
| [Megill] p. 448 | Scheme C13' | ax-14 2203 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1869 |
| [Megill] p. 448 | Scheme C16' | ax-16 1860 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1776 dral2 1777 drex1 1844 drex2 1778 drsb1 1845 drsb2 1887 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2038 sbequ 1886 sbid2v 2047 |
| [Megill] p. 450 | Example in Appendix | hba1 1586 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3113 rspsbca 3114 stdpc4 1821 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3119 stdpc5 1630 |
| [Mendelson] p. 81 | Rule C | exlimiv 1644 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1749 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1816 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3529 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3530 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3445 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3493 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3446 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3336 |
| [Mendelson] p. 231 | Definition of union | unssin 3444 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4569 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3888 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4375 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4376 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4377 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3909 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4855 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5253 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4464 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7024 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6998 xpsneng 6999 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7004 xpcomeng 7005 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7007 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7001 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6814 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6979 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7029 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6848 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6980 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7420 djucomen 7419 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7418 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6628 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3427 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4810 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4811 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4147 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5248 coi2 5249 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4941 rn0 4984 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5137 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4831 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4948 rnxpm 5162 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4802 xp0 5152 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5091 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5088 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5087 imaexg 5086 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5083 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5771 funfvop 5753 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5681 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5691 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5366 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5902 dff13f 5904 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5870 funrnex 6269 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5896 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5216 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3940 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6311 df-1st 6296 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6312 df-2nd 6297 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1493 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1550 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1552 ax-11o 1869 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1873 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1494 |
| [Monk2] p. 109 | Lemma 15 | equvin 1909 equvini 1804 eqvinop 4331 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1572 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1697 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1494 |
| [Monk2] p. 114 | Lemma 22 | hba1 1586 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1598 nfia1 1626 |
| [Monk2] p. 114 | Lemma 24 | hba2 1597 nfa2 1625 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 836 dftest 16589 |
| [Munkres] p. 77 | Example 2 | distop 14796 |
| [Munkres] p. 78 | Definition of basis | df-bases 14754 isbasis3g 14757 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13330 tgval2 14762 |
| [Munkres] p. 79 | Remark | tgcl 14775 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 14769 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 14790 tgss3 14789 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 14791 basgen2 14792 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 14881 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 14823 topcld 14820 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 14824 |
| [Munkres] p. 94 | Definition of closure | clsval 14822 |
| [Munkres] p. 94 | Definition of interior | ntrval 14821 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 14899 iscn 14908 iscn2 14911 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 14941 cncnp2m 14942 cncnpi 14939 df-cnp 14900 iscnp 14910 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15225 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7084 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7352 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7340 omniwomnimkv 7355 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3315 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7323 exmidomniim 7329 finomni 7328 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7308 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 16533 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 16537 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7091 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7400 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7401 exmidfodomrlemrALT 7402 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7337 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 16519 peano4nninf 16518 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 16521 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 16529 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 16531 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 16517 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2216 rabid 2707 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2042 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2222 |
| [Quine] p. 19 | Definition 2.9 | df-v 2802 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2338 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2350 abid2f 2398 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1934 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1932 sb6 1933 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2225 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2229 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2231 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3030 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3031 dfsbcq2 3032 |
| [Quine] p. 43 | Theorem 6.8 | vex 2803 |
| [Quine] p. 43 | Theorem 6.9 | isset 2807 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2886 spcgv 2891 spcimgf 2884 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3041 spsbcd 3042 |
| [Quine] p. 44 | Theorem 6.12 | elex 2812 |
| [Quine] p. 44 | Theorem 6.13 | elab 2948 elabg 2950 elabgf 2946 |
| [Quine] p. 44 | Theorem 6.14 | noel 3496 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3732 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3674 df-sn 3673 |
| [Quine] p. 49 | Theorem 7.4 | snss 3804 snssg 3803 |
| [Quine] p. 49 | Theorem 7.5 | prss 3825 prssg 3826 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3773 prid1g 3771 prid2 3774 prid2g 3772 snid 3698 snidg 3696 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4270 snexprc 4272 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4297 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3905 unisng 3906 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3908 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3917 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3916 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5293 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5283 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5294 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5298 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5299 |
| [Quine] p. 58 | Definition 9.1 | df-op 3676 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4346 opabidw 4347 opelopab 4362 opelopaba 4356 opelopabaf 4364 opelopabf 4365 opelopabg 4358 opelopabga 4353 opelopabgf 4360 oprabid 6043 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4727 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4729 |
| [Quine] p. 64 | Definition 9.15 | df-id 4386 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5383 |
| [Quine] p. 65 | Theorem 10.4 | funi 5354 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5373 funsng 5371 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5324 |
| [Quine] p. 65 | Definition 10.2 | args 5101 dffv4g 5630 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5330 fv2 5628 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 10974 nn0opth2d 10973 nn0opthd 10972 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5410 funimaexg 5409 |
| [Roman] p. 18 | Part Preliminaries | df-rng 13933 |
| [Roman] p. 19 | Part Preliminaries | df-ring 13998 |
| [Rudin] p. 164 | Equation 27 | efcan 12224 |
| [Rudin] p. 164 | Equation 30 | efzval 12231 |
| [Rudin] p. 167 | Equation 48 | absefi 12317 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1468 |
| [Sanford] p. 39 | Rule 4 | mptxor 1466 |
| [Sanford] p. 40 | Rule 1 | mptnan 1465 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5117 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5119 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5116 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5114 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14000 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 14794 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3470 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3564 dif0 3563 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3577 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3463 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3464 |
| [Stoll] p. 20 | Remark | invdif 3447 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3677 |
| [Stoll] p. 43 | Definition | uniiun 4020 |
| [Stoll] p. 44 | Definition | intiin 4021 |
| [Stoll] p. 45 | Definition | df-iin 3969 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3968 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 894 imanst 893 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3470 |
| [Suppes] p. 22 | Theorem 2 | eq0 3511 |
| [Suppes] p. 22 | Theorem 4 | eqss 3240 eqssd 3242 eqssi 3241 |
| [Suppes] p. 23 | Theorem 5 | ss0 3533 ss0b 3532 |
| [Suppes] p. 23 | Theorem 6 | sstr 3233 |
| [Suppes] p. 25 | Theorem 12 | elin 3388 elun 3346 |
| [Suppes] p. 26 | Theorem 15 | inidm 3414 |
| [Suppes] p. 26 | Theorem 16 | in0 3527 |
| [Suppes] p. 27 | Theorem 23 | unidm 3348 |
| [Suppes] p. 27 | Theorem 24 | un0 3526 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3368 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3375 |
| [Suppes] p. 27 | Theorem 27 | unss 3379 |
| [Suppes] p. 27 | Theorem 28 | indir 3454 |
| [Suppes] p. 27 | Theorem 29 | undir 3455 |
| [Suppes] p. 28 | Theorem 32 | difid 3561 difidALT 3562 |
| [Suppes] p. 29 | Theorem 33 | difin 3442 |
| [Suppes] p. 29 | Theorem 34 | indif 3448 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3567 |
| [Suppes] p. 29 | Theorem 36 | difun2 3572 |
| [Suppes] p. 29 | Theorem 37 | difin0 3566 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3565 |
| [Suppes] p. 29 | Theorem 39 | difundi 3457 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3459 |
| [Suppes] p. 30 | Theorem 41 | nalset 4215 |
| [Suppes] p. 39 | Theorem 61 | uniss 3910 |
| [Suppes] p. 39 | Theorem 65 | uniop 4344 |
| [Suppes] p. 41 | Theorem 70 | intsn 3959 |
| [Suppes] p. 42 | Theorem 71 | intpr 3956 intprg 3957 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4571 op1stbg 4572 |
| [Suppes] p. 42 | Theorem 78 | intun 3955 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4000 dfiun2g 3998 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4001 |
| [Suppes] p. 47 | Theorem 86 | elpw 3656 elpw2 4243 elpw2g 4242 elpwg 3658 |
| [Suppes] p. 47 | Theorem 87 | pwid 3665 |
| [Suppes] p. 47 | Theorem 89 | pw0 3816 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3884 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4829 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4861 xpindir 4862 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4778 xpundir 4779 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4642 |
| [Suppes] p. 58 | Theorem 2 | relss 4809 |
| [Suppes] p. 59 | Theorem 4 | eldm 4924 eldm2 4925 eldm2g 4923 eldmg 4922 |
| [Suppes] p. 59 | Definition 3 | df-dm 4731 |
| [Suppes] p. 60 | Theorem 6 | dmin 4935 |
| [Suppes] p. 60 | Theorem 8 | rnun 5141 |
| [Suppes] p. 60 | Theorem 9 | rnin 5142 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4914 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4909 brcnvg 4907 |
| [Suppes] p. 62 | Equation 5 | elcnv 4903 elcnv2 4904 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5110 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5140 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5138 |
| [Suppes] p. 63 | Theorem 20 | co02 5246 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4998 |
| [Suppes] p. 63 | Definition 7 | df-co 4730 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4911 |
| [Suppes] p. 64 | Theorem 27 | coass 5251 |
| [Suppes] p. 65 | Theorem 31 | resundi 5022 |
| [Suppes] p. 65 | Theorem 34 | elima 5077 elima2 5078 elima3 5079 elimag 5076 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5145 |
| [Suppes] p. 66 | Theorem 40 | dminss 5147 |
| [Suppes] p. 66 | Theorem 41 | imainss 5148 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5151 |
| [Suppes] p. 81 | Definition 34 | dfec2 6698 |
| [Suppes] p. 82 | Theorem 72 | elec 6736 elecg 6735 |
| [Suppes] p. 82 | Theorem 73 | erth 6741 erth2 6742 |
| [Suppes] p. 89 | Theorem 96 | map0b 6849 |
| [Suppes] p. 89 | Theorem 97 | map0 6851 map0g 6850 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6852 |
| [Suppes] p. 89 | Theorem 99 | mapss 6853 |
| [Suppes] p. 92 | Theorem 1 | enref 6931 enrefg 6930 |
| [Suppes] p. 92 | Theorem 2 | ensym 6948 ensymb 6947 ensymi 6949 |
| [Suppes] p. 92 | Theorem 3 | entr 6951 |
| [Suppes] p. 92 | Theorem 4 | unen 6984 |
| [Suppes] p. 94 | Theorem 15 | endom 6929 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6945 |
| [Suppes] p. 94 | Theorem 17 | domtr 6952 |
| [Suppes] p. 95 | Theorem 18 | isbth 7155 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6974 fundmeng 6975 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7011 |
| [Suppes] p. 130 | Definition 3 | df-tr 4184 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4582 |
| [Suppes] p. 134 | Definition 6 | df-suc 4464 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4697 finds 4694 finds1 4696 finds2 4695 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7561 df-ltpq 7554 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4483 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2211 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2222 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2225 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2224 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2247 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6015 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3028 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3688 elpr2 3689 elprg 3687 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3683 elsn2 3701 elsn2g 3700 elsng 3682 velsn 3684 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4319 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3678 sneqr 3839 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3686 dfsn2 3681 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4530 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4325 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4303 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4534 unexg 4536 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3716 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3890 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3204 df-un 3202 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3903 uniprg 3904 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4265 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3715 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4499 elsucg 4497 sstr2 3232 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3349 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3397 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3362 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3415 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3452 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3453 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3213 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3652 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3376 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3211 dfss2 3215 sseqin2 3424 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3245 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3425 inss2 3426 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3285 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3898 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4304 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4311 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2517 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4212 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3200 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3494 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3561 difidALT 3562 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3505 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4633 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2802 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4217 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3531 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4222 ssexg 4224 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4219 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4644 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4635 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3557 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3330 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3466 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3331 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3339 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2513 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2514 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4838 xpexg 4836 xpexgALT 6288 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4728 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5389 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5548 fun11 5392 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5333 svrelfun 5390 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4913 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4915 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4733 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4734 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4730 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5187 dfrel2 5183 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4830 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4840 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4846 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4860 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5037 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5014 opelresg 5016 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5030 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5033 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5038 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5363 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5231 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5362 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5549 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2122 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5330 fv3 5656 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5271 cnvexg 5270 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4995 dmexg 4992 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4996 rnexg 4993 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5650 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5660 tz6.12 5661 tz6.12c 5663 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5624 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5325 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5326 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5328 wfo 5320 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5327 wf1 5319 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5329 wf1o 5321 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5738 eqfnfv2 5739 eqfnfv2f 5742 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5710 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5869 fnexALT 6266 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5868 resfunexgALT 6263 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5410 funimaexg 5409 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4085 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5102 iniseg 5104 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4382 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5331 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5944 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5945 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5950 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5952 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5960 |
| [TakeutiZaring] p. 35 | Notation | wtr 4183 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4447 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4187 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4670 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4474 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4478 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4586 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4461 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4580 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4646 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4676 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4185 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4605 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4581 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3917 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4464 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4508 sucidg 4509 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4595 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4462 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4600 ordelsuc 4599 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4688 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4689 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4690 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4687 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4701 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4693 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4691 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4692 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3938 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4199 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3939 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4611 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3925 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6467 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6524 tfri1d 6494 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6525 tfri2d 6495 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6526 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6461 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6445 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6625 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6621 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6618 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6622 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6670 nnaordi 6669 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4011 uniss2 3920 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6631 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6641 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6632 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6619 omsuc 6633 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6642 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6678 nnmordi 6677 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6620 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7380 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6962 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7036 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7037 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6905 isfi 6927 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7008 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6812 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7014 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7027 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1556 |
| [Tarski] p. 68 | Lemma 6 | equid 1747 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1750 |
| [Tarski] p. 70 | Lemma 14 | spim 1784 spime 1787 spimeh 1785 spimh 1783 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1552 ax-11o 1869 ax11i 1760 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1933 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1572 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2202 ax-14 2203 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 716 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 732 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 761 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 770 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 794 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 619 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 646 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 82 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 55 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 76 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 842 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2176 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 742 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 841 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 632 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 890 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 848 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 861 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 645 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 858 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 860 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 717 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 780 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 620 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 624 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 898 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 912 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 773 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 774 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 809 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 810 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 808 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1003 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 783 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 781 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 782 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 743 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 744 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 872 pm2.5gdc 871 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 867 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 745 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 746 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 659 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 660 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 727 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 896 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 730 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 731 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 870 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 753 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 805 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 806 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 663 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 718 pm2.67 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 874 pm2.521gdc 873 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 752 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 815 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 899 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 920 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 811 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 812 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 814 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 813 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 816 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 817 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 910 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 759 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 963 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 964 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 965 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 758 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 264 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 265 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 698 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 347 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 261 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 262 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 109 simplimdc 865 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 864 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 345 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 346 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 693 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 599 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 333 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 331 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 332 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 760 pm3.44 720 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 604 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 790 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 876 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 877 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 895 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 699 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 958 bitr 472 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 395 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 762 pm4.25 763 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 823 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 733 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 401 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 772 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 466 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 797 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 607 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 827 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1004 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 821 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 977 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 955 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 784 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 819 pm4.45 789 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1527 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 962 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 902 imorr 726 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 904 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 755 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 756 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 907 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 944 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 757 pm4.56 785 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 945 oranim 786 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 690 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 903 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 891 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 905 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 691 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 906 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 892 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 389 pm4.71d 393 pm4.71i 391 pm4.71r 390 pm4.71rd 394 pm4.71ri 392 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 832 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 749 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 605 pm4.76 606 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 715 pm4.77 804 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 787 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 908 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 712 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 913 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 956 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 957 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 236 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 237 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 240 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 248 impexp 263 pm4.87 557 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 603 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 914 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 915 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 917 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 916 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1431 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 833 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 909 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1436 pm5.18dc 888 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 711 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 700 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1434 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1439 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1440 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 900 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 475 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 242 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 931 pm5.6r 932 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 960 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 453 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 611 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 922 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 612 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 250 pm5.41 251 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 320 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 930 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 807 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 923 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 918 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 799 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 951 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 952 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 967 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 244 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 179 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 968 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1681 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1531 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1678 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1942 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2080 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2481 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2482 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2942 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3086 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5302 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5303 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2157 eupickbi 2160 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5330 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7384 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |