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 7461 fidcenum 7278 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7278 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7461 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13374 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7243 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7229 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13389 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13391 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13380 znnen 13347 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13392 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13393 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11237 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4686 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11381 df-pfx 11467 df-substr 11440 df-word 11327 lencl 11330 wrd0 11351 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8513 addcan2d 8518 addcan2i 8516 addcand 8517 addcani 8515 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8524 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8581 negsubd 8650 negsubi 8611 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8583 negnegd 8635 negnegi 8603 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8719 subdid 8748 subdii 8741 subdir 8720 subdird 8749 subdiri 8742 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8723 mul01d 8727 mul01i 8725 mul02 8721 mul02d 8726 mul02i 8724 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 9131 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 9082 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8732 mul2negd 8747 mul2negi 8740 mulneg1 8729 mulneg1d 8745 mulneg1i 8738 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14560 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 9051 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 10095 rpaddcld 10130 rpmulcl 10096 rpmulcld 10131 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 10107 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8437 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8873 ltadd1dd 8891 ltadd1i 8837 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8928 ltmul1a 8927 ltmul1i 9258 ltmul1ii 9266 ltmul2 9194 ltmul2d 10157 ltmul2dd 10171 ltmul2i 9261 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8460 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8803 lt0neg1d 8850 ltneg 8797 ltnegd 8858 ltnegi 8828 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8780 lt2addd 8903 lt2addi 8845 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 10072 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9188 recgt0d 9272 recgt0i 9244 recgt0ii 9245 |
| [Apostol] p. 22 | Definition of integers | df-z 9656 |
| [Apostol] p. 22 | Definition of rationals | df-q 10036 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7340 |
| [Apostol] p. 26 | Theorem I.29 | arch 9571 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9776 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9572 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10708 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12663 zneo 9758 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11819 sqrtthi 11908 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9316 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12838 |
| [Apostol] p. 363 | Remark | absgt0api 11935 |
| [Apostol] p. 363 | Example | abssubd 11982 abssubi 11939 |
| [ApostolNT] p. 8 | Definition | df-ppi 16237 |
| [ApostolNT] p. 14 | Definition | df-dvds 12580 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12596 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12620 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12616 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12610 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12612 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12597 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12598 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12603 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12637 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12639 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12641 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12816 |
| [ApostolNT] p. 16 | Definition | isprm2 12920 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12895 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13404 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12775 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12817 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12819 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12789 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12782 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12948 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12950 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 13176 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12716 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12862 |
| [ApostolNT] p. 25 | Definition | df-phi 13018 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 13048 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 13029 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 13033 |
| [ApostolNT] p. 38 | Remark | df-sgm 16238 |
| [ApostolNT] p. 38 | Definition | df-sgm 16238 |
| [ApostolNT] p. 75 | Definition | df-cht 16236 |
| [ApostolNT] p. 104 | Definition | congr 12903 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12583 |
| [ApostolNT] p. 106 | Definition | moddvds 12591 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12670 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12671 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10799 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10836 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 11125 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12615 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12906 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13230 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12908 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 13040 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 13059 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 13041 |
| [ApostolNT] p. 179 | Definition | df-lgs 16322 lgsprme0 16366 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 16367 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 16343 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 16358 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 16409 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 16428 2lgsoddprm 16437 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 16393 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 16404 |
| [ApostolNT] p. 188 | Definition | df-lgs 16322 lgs1 16368 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 16359 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 16361 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 16369 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 16370 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 625 pm2.65 669 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6087 onsucelsucexmidlem 4678 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 17232 |
| [Bauer], p. 483 | Definition | n0rf 3534 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 16212 2irrexpqap 16214 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7250 ssfiexmid 7182 ssfiexmidt 7184 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15879 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15869 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8981 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7461 |
| [BauerSwan], p. 14 | Remark | 0ct 7453 ctm 7455 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 17235 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7874 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7787 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7876 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7910 addlocpr 7909 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7936 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7939 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7944 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 2089 |
| [BellMachover] p. 460 | Notation | df-mo 2090 |
| [BellMachover] p. 460 | Definition | mo3 2141 mo3h 2140 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2223 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 4256 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4316 |
| [BellMachover] p. 466 | Axiom Union | axun2 4582 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4691 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4531 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4694 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4645 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4516 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4738 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4763 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1480 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1478 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1481 |
| [Bobzien] p. 117 | Conclusion the contradictory | stoic1a 1476 |
| [Bollobas] p. 1 | Section I.1 | df-edg 16504 isuhgropm 16527 isusgropen 16611 isuspgropen 16610 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16700 uhgrspansubgr 16723 |
| [Bollobas] p. 4 | Definition | df-wlks 16764 |
| [Bollobas] p. 5 | Definition | df-trls 16827 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 16516 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13735 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13776 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13789 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14409 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 14339 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5992 fcofo 5993 |
| [BourbakiTop1] p. | Remark | xnegmnf 10248 xnegpnf 10247 |
| [BourbakiTop1] p. | Remark | rexneg 10249 |
| [BourbakiTop1] p. | Proposition | ishmeo 15530 |
| [BourbakiTop1] p. | Property V_i | ssnei2 15383 |
| [BourbakiTop1] p. | Property V_ii | innei 15389 |
| [BourbakiTop1] p. | Property V_iv | neissex 15391 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 15380 neiss 15376 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 15448 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15525 |
| [BourbakiTop1] p. | Property V_iii | elnei 15378 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 15224 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13735 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13776 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13963 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4195 |
| [Church] p. 129 | Section II.24 | df-ifp 991 dfifp2dc 994 |
| [Cohen] p. 301 | Remark | relogoprlem 16098 |
| [Cohen] p. 301 | Property 2 | relogmul 16099 relogmuld 16114 |
| [Cohen] p. 301 | Property 3 | relogdiv 16100 relogdivd 16115 |
| [Cohen] p. 301 | Property 4 | relogexp 16102 |
| [Cohen] p. 301 | Property 1a | log1 16095 |
| [Cohen] p. 301 | Property 1b | loge 16096 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 16201 |
| [Cohen4] p. 352 | Definition | rpelogb 16185 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 16191 |
| [Cohen4] p. 361 | Property 3 | logbrec 16196 rprelogbdiv 16193 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 16189 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 16194 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 16183 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 16184 |
| [Cohen4] p. 367 | Property | rplogbchbase 16186 |
| [Cohen4] p. 377 | Property 2 | logblt 16198 |
| [Crosilla] p. | Axiom 1 | ax-ext 2220 |
| [Crosilla] p. | Axiom 2 | ax-pr 4348 |
| [Crosilla] p. | Axiom 3 | ax-un 4580 |
| [Crosilla] p. | Axiom 4 | ax-nul 4261 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4737 |
| [Crosilla] p. | Axiom 6 | ru 3050 |
| [Crosilla] p. | Axiom 8 | ax-pow 4313 |
| [Crosilla] p. | Axiom 9 | ax-setind 4686 |
| [Crosilla], p. | Axiom 6 | ax-sep 4251 |
| [Crosilla], p. | Axiom 7 | ax-coll 4248 |
| [Crosilla], p. | Axiom 7' | repizf 4249 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4670 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6087 |
| [Crosilla], p. | Definition of ordinal | df-iord 4513 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4684 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16700 uhgrspansubgr 16723 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 16516 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3222 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4740 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6928 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4260 |
| [Enderton] p. 19 | Definition | df-tp 3717 |
| [Enderton] p. 26 | Exercise 5 | unissb 3965 |
| [Enderton] p. 26 | Exercise 10 | pwel 4360 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4433 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4082 iinin2m 4081 iunin1 4077 iunin2 4076 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4080 iundif2ss 4078 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4095 |
| [Enderton] p. 33 | Exercise 25 | iununir 4096 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4103 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4628 iunpwss 4104 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4359 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4331 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4598 rnex 5052 rnexg 5049 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4993 rnuni 5202 |
| [Enderton] p. 42 | Definition of a function | dffun7 5407 dffun8 5408 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5770 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5445 |
| [Enderton] p. 44 | Definition (d) | dfima2 5131 dfima3 5132 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5777 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7568 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5970 |
| [Enderton] p. 52 | Definition | df-map 6928 |
| [Enderton] p. 53 | Exercise 21 | coass 5309 |
| [Enderton] p. 53 | Exercise 27 | dmco 5299 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5455 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5166 |
| [Enderton] p. 54 | Remark | ixpf 7006 ixpssmap 7018 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6985 |
| [Enderton] p. 56 | Theorem 3M | erref 6831 |
| [Enderton] p. 57 | Lemma 3N | erthi 6859 |
| [Enderton] p. 57 | Definition | df-ec 6813 |
| [Enderton] p. 58 | Definition | df-qs 6817 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6918 th3qcor 6917 th3qlem1 6915 th3qlem2 6916 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6813 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4990 |
| [Enderton] p. 68 | Definition of successor | df-suc 4518 |
| [Enderton] p. 71 | Definition | df-tr 4232 dftr4 4236 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4560 unisucg 4561 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4560 unisucg 4561 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4245 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4246 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6751 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6753 onasuc 6743 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6091 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6752 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6754 onmsuc 6750 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6762 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6755 nnacom 6761 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6763 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6764 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6766 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6756 nnmsucr 6765 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6805 |
| [Enderton] p. 129 | Definition | df-en 7027 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6039 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13344 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7171 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7162 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7150 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7580 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7576 dju1en 7575 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3603 |
| [Enderton] p. 145 | Figure 38 | ffoss 5675 |
| [Enderton] p. 145 | Definition | df-dom 7028 |
| [Enderton] p. 146 | Example 1 | domen 7039 domeng 7040 |
| [Enderton] p. 146 | Example 3 | nndomo 7169 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7137 xpdom1g 7135 xpdom2g 7134 |
| [Enderton] p. 168 | Definition | df-po 4443 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4575 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4536 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4692 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4539 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4665 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4638 |
| [Enderton] p. 194 | Remark | onprc 4701 |
| [Enderton] p. 194 | Exercise 16 | suc11 4707 |
| [Enderton] p. 197 | Definition | df-card 7530 |
| [Enderton] p. 200 | Exercise 25 | tfis 4732 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4703 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4705 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4706 |
| [Geuvers], p. 1 | Remark | expap0 11027 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8951 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8990 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8952 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8304 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11992 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 12000 maxle2 12001 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 12002 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 12005 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 12006 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8918 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7720 enqer 7731 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7724 df-nqqs 7721 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7717 df-plqqs 7722 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7718 df-mqqs 7723 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7725 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7781 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7784 ltbtwnnq 7789 ltbtwnnqq 7788 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7773 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7774 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7910 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7952 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7951 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7970 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7986 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7992 ltaprlem 7991 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7989 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7945 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7965 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7954 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7953 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7961 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 8011 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 8099 enrer 8108 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 8104 df-1r 8105 df-nr 8100 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 8102 df-plr 8101 negexsr 8145 recexsrlem 8147 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 8103 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9298 creur 9297 cru 8938 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8296 axcnre 8254 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11645 crimd 11765 crimi 11725 crre 11644 crred 11764 crrei 11724 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11647 remimd 11730 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11845 absval2d 11974 absval2i 11933 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11671 cjaddd 11753 cjaddi 11720 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11672 cjmuld 11754 cjmuli 11721 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11670 cjcjd 11731 cjcji 11703 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11669 cjreb 11653 cjrebd 11734 cjrebi 11706 cjred 11759 rere 11652 rereb 11650 rerebd 11733 rerebi 11705 rered 11757 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11678 addcjd 11745 addcji 11715 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11789 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11840 abscjd 11979 abscji 11937 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11852 abs00d 11975 abs00i 11934 absne0d 11976 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11885 releabsd 11980 releabsi 11938 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11857 absmuld 11983 absmuli 11940 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11843 sqabsaddi 11941 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11893 abstrid 11985 abstrii 11944 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10997 exp0 11001 expp1 11004 expp1d 11133 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 11039 expaddd 11134 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 16145 cxpmuld 16172 expmul 11042 expmuld 11135 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 11036 mulexpd 11147 rpmulcxp 16142 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10430 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 12117 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 12119 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 12118 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 12122 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 12115 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 12111 climcj 12112 climim 12114 climre 12113 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8371 df-xr 8370 ltxr 10194 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 12138 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10756 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14991 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15590 xmet0 15589 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15597 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15599 mstri 15699 xmettri 15598 xmstri 15698 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15505 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15737 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 12101 addcncntop 15788 mulcn2 12103 mulcncntop 15790 subcn2 12102 subcncntop 15789 |
| [Gleason] p. 295 | Remark | bcval3 11211 bcval4 11212 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11226 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11209 df-bc 11208 |
| [Gleason] p. 296 | Remark | bcn0 11215 bcnn 11217 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12276 |
| [Gleason] p. 308 | Equation 2 | ef0 12464 |
| [Gleason] p. 308 | Equation 3 | efcj 12465 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12470 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12474 |
| [Gleason] p. 310 | Equation 14 | sinadd 12528 |
| [Gleason] p. 310 | Equation 15 | cosadd 12529 |
| [Gleason] p. 311 | Equation 17 | sincossq 12540 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12545 sinbnd 12544 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12445 |
| [Golan] p. 1 | Remark | srgisid 14397 |
| [Golan] p. 1 | Definition | df-srg 14375 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 5 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1502 |
| [Herstein] p. 55 | Lemma 2.2.1(a) | grpideu 13875 mndideu 13798 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13902 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13931 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13942 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13964 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 17331 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1472 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1473 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1475 |
| [HoTT], p. | Lemma 10.4.1 | exmidontriim 7587 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6776 |
| [HoTT], p. | Exercise 11.10 | neapmkv 17325 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8993 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7843 df-imp 7842 df-iplp 7841 df-reap 8911 |
| [HoTT], p. | Theorem 11.2.4 | recapb 9009 rerecapb 9181 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6375 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 8035 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16940 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 17318 dceqnconst 17317 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8273 caucvgpr 8055 caucvgprpr 8085 caucvgsr 8175 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7839 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 17323 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4444 ltpopr 7968 ltsopr 7969 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8942 reapcotr 8934 reapirr 8913 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8460 gt0add 8909 leadd1 8765 lelttr 8420 lemul1a 9196 lenlt 8407 ltadd1 8764 ltletr 8421 ltmul1 8928 reaplt 8924 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16873 |
| [Jech] p. 4 | Definition of class | cv 1401 cvjust 2233 |
| [Jech] p. 78 | Note | opthprc 4828 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1583 |
| [Kreyszig] p. 3 | Property M1 | metcl 15579 xmetcl 15578 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15586 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 9006 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15668 |
| [Kreyszig] p. 19 | Remark | mopntopon 15669 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15714 mopnm 15674 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15712 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15717 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15739 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 15439 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14776 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14767 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14768 |
| [Kunen] p. 10 | Axiom 0 | a9e 1748 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4250 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6938 mapvalg 6936 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6932 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4022 |
| [Lang] p. 3 | Statement | lidrideqd 13760 mndbn0 13803 |
| [Lang] p. 3 | Definition | df-mnd 13789 |
| [Lang] p. 4 | Definition of a (finite) product | gzsumsplit1r 13774 |
| [Lang] p. 5 | Equation | gzsumreidx 14231 |
| [Lang] p. 6 | Definition | mulgnn0gzsum 13990 |
| [Lang] p. 7 | Definition | dfgrp2e 13892 |
| [Lang2] p. 3 | Notations | df-ind 9303 |
| [Levy] p. 338 | Axiom | df-clab 2225 df-clel 2234 df-cleq 2231 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1472 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1473 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1475 |
| [Margaris] p. 40 | Rule C | exlimiv 1651 |
| [Margaris] p. 49 | Axiom A1 | ax-1 6 |
| [Margaris] p. 49 | Axiom A2 | ax-2 7 |
| [Margaris] p. 49 | Axiom A3 | condc 865 |
| [Margaris] p. 49 | Definition | dfbi2 392 dfordc 904 exalim 1555 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 45 |
| [Margaris] p. 60 | Theorem 8 | jcn 661 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1691 r19.2m 3614 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1607 19.3h 1606 rr19.3v 2965 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1531 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1672 alexim 1698 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1552 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1643 spsbe 1895 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1697 19.9h 1696 19.9v 1924 exlimd 1650 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1716 excomim 1715 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1717 r19.12 2657 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1699 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1521 ralbi 2683 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1608 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1609 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1657 rexbi 2684 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1718 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1510 alimd 1574 alimdh 1520 alimdv 1932 ralimdaa 2616 ralimdv 2618 ralimdva 2617 ralimdvva 2619 sbcimdv 3117 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1719 19.21 1636 19.21bi 1611 19.21h 1610 19.21ht 1634 19.21t 1635 19.21v 1926 alrimd 1663 alrimdd 1662 alrimdh 1532 alrimdv 1929 alrimi 1575 alrimih 1522 alrimiv 1927 alrimivv 1928 r19.21 2626 r19.21be 2641 r19.21bi 2638 r19.21t 2625 r19.21v 2627 ralrimd 2628 ralrimdv 2629 ralrimdva 2630 ralrimdvv 2634 ralrimdvva 2635 ralrimi 2621 ralrimiv 2622 ralrimiva 2623 ralrimivv 2631 ralrimivva 2632 ralrimivvva 2633 ralrimivw 2624 rexlimi 2661 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1934 2eximdv 1935 exim 1652 eximd 1665 eximdh 1664 eximdv 1933 rexim 2644 reximdai 2648 reximddv 2653 reximddv2 2655 reximdv 2651 reximdv2 2649 reximdva 2652 reximdvai 2650 reximi2 2646 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1730 19.23bi 1645 19.23h 1551 19.23ht 1550 19.23t 1729 19.23v 1936 19.23vv 1937 exlimd2 1648 exlimdh 1649 exlimdv 1872 exlimdvv 1953 exlimi 1647 exlimih 1646 exlimiv 1651 exlimivv 1952 r19.23 2659 r19.23v 2660 rexlimd 2665 rexlimdv 2667 rexlimdv3a 2670 rexlimdva 2668 rexlimdva2 2671 rexlimdvaa 2669 rexlimdvv 2675 rexlimdvva 2676 rexlimdvw 2672 rexlimiv 2662 rexlimiva 2663 rexlimivv 2674 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1692 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1679 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1535 19.26-3an 1536 19.26 1534 r19.26-2 2680 r19.26-3 2681 r19.26 2677 r19.26m 2682 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1614 19.27h 1613 19.27v 1955 r19.27av 2686 r19.27m 3623 r19.27mv 3624 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1616 19.28h 1615 19.28v 1956 r19.28av 2687 r19.28m 3617 r19.28mv 3620 rr19.28v 2966 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1673 19.29r 1674 19.29r2 1675 19.29x 1676 r19.29 2688 r19.29d2r 2695 r19.29r 2689 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1680 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1733 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1731 19.32r 1732 r19.32r 2697 r19.32vdc 2700 r19.32vr 2699 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1537 19.33b2 1682 19.33bdc 1683 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1736 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1677 19.35i 1678 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1725 19.36aiv 1957 19.36i 1724 r19.36av 2702 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1726 19.37aiv 1727 r19.37 2703 r19.37av 2704 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1728 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1693 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1685 19.40 1684 r19.40 2705 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1738 19.41h 1737 19.41v 1958 19.41vv 1959 19.41vvv 1960 19.41vvvv 1961 r19.41 2706 r19.41v 2707 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1740 19.42h 1739 19.42v 1962 19.42vv 1967 19.42vvv 1968 19.42vvvv 1969 r19.42v 2708 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1681 r19.43 2709 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1734 r19.44av 2710 r19.44mv 3622 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1735 r19.45av 2711 r19.45mv 3621 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 2111 |
| [Megill] p. 444 | Axiom C5 | ax-17 1579 |
| [Megill] p. 445 | Lemma L12 | alequcom 1568 ax-10 1558 |
| [Megill] p. 446 | Lemma L17 | equtrr 1762 |
| [Megill] p. 446 | Lemma L19 | hbnae 1773 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1816 sbid 1827 |
| [Megill] p. 448 | Scheme C5' | ax-4 1563 |
| [Megill] p. 448 | Scheme C6' | ax-7 1501 |
| [Megill] p. 448 | Scheme C8' | ax-8 1557 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1560 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1768 |
| [Megill] p. 448 | Scheme C12' | ax-13 2211 |
| [Megill] p. 448 | Scheme C13' | ax-14 2212 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1876 |
| [Megill] p. 448 | Scheme C16' | ax-16 1867 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1783 dral2 1784 drex1 1851 drex2 1785 drsb1 1852 drsb2 1894 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 2047 sbequ 1893 sbid2v 2056 |
| [Megill] p. 450 | Example in Appendix | hba1 1593 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 3135 rspsbca 3136 stdpc4 1828 |
| [Mendelson] p. 69 | Axiom 5 | ra5 3141 stdpc5 1637 |
| [Mendelson] p. 81 | Rule C | exlimiv 1651 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1755 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1823 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3559 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3560 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3471 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3521 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3472 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3360 |
| [Mendelson] p. 231 | Definition of union | unssin 3470 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4624 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3934 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4429 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4430 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4431 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3955 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4911 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5311 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4518 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7149 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7123 xpsneng 7124 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7129 xpcomeng 7130 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7132 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7126 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6930 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 7104 mapsnend 7103 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 7155 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7154 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6971 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 7105 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7579 djucomen 7578 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7577 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6744 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3453 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4865 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4866 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4194 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5306 coi2 5307 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4997 rn0 5040 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5195 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4886 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 5004 rnxpm 5220 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4857 xp0 5210 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5149 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5146 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5144 imaexg 5143 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5140 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5841 funfvop 5824 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5747 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5757 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5425 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5977 dff13f 5979 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5943 funrnex 6347 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5971 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5274 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3986 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6393 df-1st 6378 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6394 df-2nd 6379 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1500 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1557 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1559 ax-11o 1876 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1880 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1501 |
| [Monk2] p. 109 | Lemma 15 | equvin 1916 equvini 1811 eqvinop 4385 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1579 |
| [Monk2] p. 113 | Axiom C5-2 | hbn1 1704 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1501 |
| [Monk2] p. 114 | Lemma 22 | hba1 1593 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1605 nfia1 1633 |
| [Monk2] p. 114 | Lemma 24 | hba2 1604 nfa2 1632 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 843 dftest 17332 |
| [Munkres] p. 77 | Example 2 | distop 15311 |
| [Munkres] p. 78 | Definition of basis | df-bases 15269 isbasis3g 15272 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13673 tgval2 15277 |
| [Munkres] p. 79 | Remark | tgcl 15290 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 15284 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 15305 tgss3 15304 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 15306 basgen2 15307 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 15396 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 15338 topcld 15335 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 15339 |
| [Munkres] p. 94 | Definition of closure | clsval 15337 |
| [Munkres] p. 94 | Definition of interior | ntrval 15336 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 15414 iscn 15423 iscn2 15426 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 15456 cncnp2m 15457 cncnpi 15454 df-cnp 15415 iscnp 15425 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15740 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7212 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7510 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7498 omniwomnimkv 7513 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3339 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7481 exmidomniim 7487 finomni 7486 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7466 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 17270 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 17274 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7219 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7559 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7560 exmidfodomrlemrALT 7561 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7495 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 17256 peano4nninf 17255 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 17258 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 17266 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 17268 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 17254 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2225 rabid 2727 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 2051 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2231 |
| [Quine] p. 19 | Definition 2.9 | df-v 2823 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2347 eqabb 2374 |
| [Quine] p. 35 | Theorem 5.2 | abid1 2372 abid2 2361 abid2f 2418 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1942 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1940 sb6 1941 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2234 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2238 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2240 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 3052 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 3053 dfsbcq2 3054 |
| [Quine] p. 43 | Theorem 6.8 | vex 2824 |
| [Quine] p. 43 | Theorem 6.9 | isset 2828 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2907 spcgv 2912 spcimgf 2905 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 3063 spsbcd 3064 |
| [Quine] p. 44 | Theorem 6.12 | elex 2833 |
| [Quine] p. 44 | Theorem 6.13 | elab 2970 elabg 2972 elabgf 2968 |
| [Quine] p. 44 | Theorem 6.14 | noel 3525 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3774 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3716 df-sn 3715 |
| [Quine] p. 49 | Theorem 7.4 | snss 3850 snssg 3849 |
| [Quine] p. 49 | Theorem 7.5 | prss 3871 prssg 3872 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3817 prid1g 3815 prid2 3818 prid2g 3816 snid 3740 snidg 3738 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4323 snexprc 4325 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4351 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3951 unisng 3952 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3954 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3963 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3962 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5351 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5341 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5352 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5356 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5357 |
| [Quine] p. 58 | Definition 9.1 | df-op 3718 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4400 opabidw 4401 opelopab 4416 opelopaba 4410 opelopabaf 4418 opelopabf 4419 opelopabg 4412 opelopabga 4407 opelopabgf 4414 oprabid 6120 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4782 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4784 |
| [Quine] p. 64 | Definition 9.15 | df-id 4440 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5442 |
| [Quine] p. 65 | Theorem 10.4 | funi 5412 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5432 funsng 5430 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5382 |
| [Quine] p. 65 | Definition 10.2 | args 5159 dffv4g 5695 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5388 fv2 5693 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 11184 nn0opth2d 11183 nn0opthd 11182 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5469 funimaexg 5468 |
| [Roman] p. 18 | Part Preliminaries | df-rng 14339 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14409 |
| [Rudin] p. 164 | Equation 27 | efcan 12468 |
| [Rudin] p. 164 | Equation 30 | efzval 12475 |
| [Rudin] p. 167 | Equation 48 | absefi 12561 |
| [Russell1905] p. 482 | Example of "the father | dfalseu2 17384 |
| [Sanford] p. 39 | Remark | ax-mp 5 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1475 |
| [Sanford] p. 39 | Rule 4 | mptxor 1473 |
| [Sanford] p. 40 | Rule 1 | mptnan 1472 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 5175 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5177 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5174 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5172 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14411 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 15309 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3496 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3597 dif0 3596 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3612 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3489 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3490 |
| [Stoll] p. 20 | Remark | invdif 3473 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3719 |
| [Stoll] p. 43 | Definition | uniiun 4066 |
| [Stoll] p. 44 | Definition | intiin 4067 |
| [Stoll] p. 45 | Definition | df-iin 4015 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4014 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 901 imanst 900 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3496 |
| [Suppes] p. 22 | Theorem 2 | eq0 3540 |
| [Suppes] p. 22 | Theorem 4 | eqss 3263 eqssd 3265 eqssi 3264 |
| [Suppes] p. 23 | Theorem 5 | ss0 3563 ss0b 3562 |
| [Suppes] p. 23 | Theorem 6 | sstr 3256 |
| [Suppes] p. 25 | Theorem 12 | elin 3412 elun 3370 |
| [Suppes] p. 26 | Theorem 15 | inidm 3440 |
| [Suppes] p. 26 | Theorem 16 | in0 3557 |
| [Suppes] p. 27 | Theorem 23 | unidm 3372 |
| [Suppes] p. 27 | Theorem 24 | un0 3556 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3392 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3399 |
| [Suppes] p. 27 | Theorem 27 | unss 3403 |
| [Suppes] p. 27 | Theorem 28 | indir 3480 |
| [Suppes] p. 27 | Theorem 29 | undir 3481 |
| [Suppes] p. 28 | Theorem 32 | difid 3594 difidALT 3595 |
| [Suppes] p. 29 | Theorem 33 | difin 3468 |
| [Suppes] p. 29 | Theorem 34 | indif 3474 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3602 |
| [Suppes] p. 29 | Theorem 36 | difun2 3607 |
| [Suppes] p. 29 | Theorem 37 | difin0 3601 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3599 |
| [Suppes] p. 29 | Theorem 39 | difundi 3483 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3485 |
| [Suppes] p. 30 | Theorem 41 | nalset 4265 |
| [Suppes] p. 39 | Theorem 61 | uniss 3956 |
| [Suppes] p. 39 | Theorem 65 | uniop 4398 |
| [Suppes] p. 41 | Theorem 70 | intsn 4005 |
| [Suppes] p. 42 | Theorem 71 | intpr 4002 intprg 4003 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4626 op1stbg 4627 |
| [Suppes] p. 42 | Theorem 78 | intun 4001 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4046 dfiun2g 4044 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4047 |
| [Suppes] p. 47 | Theorem 86 | elpw 3694 elpw2 4295 elpw2g 4294 elpwg 3696 |
| [Suppes] p. 47 | Theorem 87 | pwid 3707 |
| [Suppes] p. 47 | Theorem 89 | pw0 3862 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3930 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4884 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4917 xpindir 4918 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4833 xpundir 4834 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4697 |
| [Suppes] p. 58 | Theorem 2 | relss 4864 |
| [Suppes] p. 59 | Theorem 4 | eldm 4980 eldm2 4981 eldm2g 4979 eldmg 4978 |
| [Suppes] p. 59 | Definition 3 | df-dm 4786 |
| [Suppes] p. 60 | Theorem 6 | dmin 4991 |
| [Suppes] p. 60 | Theorem 8 | rnun 5199 |
| [Suppes] p. 60 | Theorem 9 | rnin 5200 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4970 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4965 brcnvg 4963 |
| [Suppes] p. 62 | Equation 5 | elcnv 4959 elcnv2 4960 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5168 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5198 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5196 |
| [Suppes] p. 63 | Theorem 20 | co02 5304 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5054 |
| [Suppes] p. 63 | Definition 7 | df-co 4785 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4967 |
| [Suppes] p. 64 | Theorem 27 | coass 5309 |
| [Suppes] p. 65 | Theorem 31 | resundi 5078 |
| [Suppes] p. 65 | Theorem 34 | elima 5134 elima2 5135 elima3 5136 elimag 5133 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5203 |
| [Suppes] p. 66 | Theorem 40 | dminss 5205 |
| [Suppes] p. 66 | Theorem 41 | imainss 5206 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5209 |
| [Suppes] p. 81 | Definition 34 | dfec2 6814 |
| [Suppes] p. 82 | Theorem 72 | elec 6852 elecg 6851 |
| [Suppes] p. 82 | Theorem 73 | erth 6857 erth2 6858 |
| [Suppes] p. 89 | Theorem 96 | map0b 6972 |
| [Suppes] p. 89 | Theorem 97 | map0 6975 map0g 6973 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6976 mapsnd 6974 |
| [Suppes] p. 89 | Theorem 99 | mapss 6977 |
| [Suppes] p. 92 | Theorem 1 | enref 7055 enrefg 7054 |
| [Suppes] p. 92 | Theorem 2 | ensym 7072 ensymb 7071 ensymi 7073 |
| [Suppes] p. 92 | Theorem 3 | entr 7075 |
| [Suppes] p. 92 | Theorem 4 | unen 7109 |
| [Suppes] p. 94 | Theorem 15 | endom 7053 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 7069 |
| [Suppes] p. 94 | Theorem 17 | domtr 7076 |
| [Suppes] p. 95 | Theorem 18 | isbth 7289 |
| [Suppes] p. 98 | Exercise 4 | fundmen 7098 fundmeng 7099 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7136 |
| [Suppes] p. 130 | Definition 3 | df-tr 4232 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4637 |
| [Suppes] p. 134 | Definition 6 | df-suc 4518 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4752 finds 4749 finds1 4751 finds2 4750 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7726 df-ltpq 7719 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4537 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2220 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2231 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2234 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2233 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2256 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 6092 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3050 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3730 elpr2 3731 elprg 3729 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3725 elsn2 3743 elsn2g 3742 elsng 3724 velsn 3726 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4373 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3720 sneqr 3885 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3728 dfsn2 3723 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4585 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4379 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4357 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4589 unexg 4591 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3758 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3936 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3226 df-un 3224 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3949 uniprg 3950 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4318 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3757 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4553 elsucg 4551 sstr2 3255 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3373 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3421 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3386 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3441 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3478 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3479 |
| [TakeutiZaring] p. 17 | Definition 5.9 | ssalel 3235 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3690 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3400 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 3233 dfss2 3237 sseqin2 3450 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3268 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3451 inss2 3452 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3308 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3944 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4358 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4365 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2537 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4262 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 3222 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3523 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3594 difidALT 3595 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3534 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4688 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2823 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4267 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3561 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4272 ssexg 4274 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4269 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4699 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4690 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3589 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3354 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3492 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3355 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3363 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2533 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2534 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4893 xpexg 4891 xpexgALT 6370 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4783 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5448 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5612 fun11 5451 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5391 svrelfun 5449 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4969 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4971 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4788 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4789 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4785 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5245 dfrel2 5241 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4885 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4896 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4902 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4916 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5093 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5070 opelresg 5072 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5086 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5089 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5094 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5421 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5289 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5420 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5613 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2131 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5388 fv3 5721 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5329 cnvexg 5328 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5051 dmexg 5048 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5052 rnexg 5049 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnvm 5145 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5715 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5725 tz6.12 5726 tz6.12c 5728 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5689 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5383 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5384 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5386 wfo 5378 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5385 wf1 5377 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5387 wf1o 5379 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5809 eqfnfv2 5810 eqfnfv2f 5813 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5778 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5940 fnexALT 6344 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5939 resfunexgALT 6341 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5469 funimaexg 5468 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4132 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5160 iniseg 5162 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4436 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5389 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 6019 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 6020 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 6025 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 6027 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 6035 |
| [TakeutiZaring] p. 35 | Notation | wtr 4231 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4501 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4235 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4725 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4528 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4532 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4641 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4515 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4635 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4701 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4731 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4233 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4660 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4636 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3963 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4518 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4562 sucidg 4563 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4650 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4516 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4655 ordelsuc 4654 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4743 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4744 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4745 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4742 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4756 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4748 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4746 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4747 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3984 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4247 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3985 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4666 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3971 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6583 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6640 tfri1d 6610 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6641 tfri2d 6611 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6642 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6577 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6561 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6741 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6737 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6734 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6738 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6786 nnaordi 6785 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4057 uniss2 3966 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6747 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6757 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6748 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6735 omsuc 6749 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6758 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6794 nnmordi 6793 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6736 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7538 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 7086 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7162 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7163 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 7029 isfi 7051 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7133 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6928 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7139 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7152 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1563 |
| [Tarski] p. 68 | Lemma 6 | equid 1753 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1756 |
| [Tarski] p. 70 | Lemma 14 | spim 1791 spime 1794 spimeh 1792 spimh 1790 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1559 ax-11o 1876 ax11i 1766 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1941 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1579 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 2211 ax-14 2212 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 723 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 739 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 768 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 777 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 801 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 625 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 6 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 652 |
| [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 849 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2185 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 749 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 848 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 638 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 897 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 855 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 868 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 651 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 865 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 867 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 724 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 787 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 626 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 630 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 905 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 919 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 40 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 780 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 781 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 816 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 817 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 815 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 1010 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 790 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 788 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 789 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 53 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 750 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 751 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 879 pm2.5gdc 878 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 874 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 752 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 753 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 754 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 665 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 666 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 734 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 903 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 737 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 738 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 877 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 760 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 812 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 813 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 669 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 725 pm2.67 755 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 881 pm2.521gdc 880 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 759 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 822 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 906 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 927 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 818 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 819 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 821 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 820 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 7 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 823 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 824 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 77 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 917 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 101 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 766 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 139 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 970 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 971 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 972 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 765 |
| [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 705 |
| [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 872 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 110 simprimdc 871 |
| [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 700 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 605 |
| [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 767 pm3.44 727 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | anim12 344 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 610 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 797 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 883 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 171 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 884 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 902 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 706 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 140 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 965 bitr 476 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 399 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 769 pm4.25 770 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 266 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 830 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 740 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 405 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 779 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 470 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 804 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 613 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 834 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 1011 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 828 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 984 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 962 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 791 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 826 pm4.45 796 pm4.45im 334 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1534 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 969 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 909 imorr 733 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 319 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 911 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 762 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 763 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 914 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 951 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 764 pm4.56 792 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 952 oranim 793 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 697 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 910 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 898 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 912 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 698 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 913 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 899 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 393 pm4.71d 397 pm4.71i 395 pm4.71r 394 pm4.71rd 398 pm4.71ri 396 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 839 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 300 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 756 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 611 pm4.76 612 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 722 pm4.77 811 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 794 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 915 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 719 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 920 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 963 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 964 |
| [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 563 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 609 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 921 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 922 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 924 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 923 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1438 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 840 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 916 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1443 pm5.18dc 895 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 718 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 707 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1441 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1446 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1447 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 907 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 479 |
| [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 938 pm5.6r 939 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 967 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 348 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 457 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 617 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 929 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 618 |
| [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 937 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 814 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 930 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 925 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 806 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 958 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 959 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 974 |
| [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 975 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1688 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1538 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1685 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1951 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 2089 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2501 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2502 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2964 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 3108 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 5360 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5361 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2166 eupickbi 2169 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5388 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7542 |
| [vandenDries] p. 43 | Theorem 62 | pellexlem1 16229 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |