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 7456 fidcenum 7273 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7273 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7456 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13368 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7239 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7225 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13383 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13385 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13374 znnen 13341 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13386 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13387 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11231 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4684 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11375 df-pfx 11461 df-substr 11434 df-word 11321 lencl 11324 wrd0 11345 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8508 addcan2d 8513 addcan2i 8511 addcand 8512 addcani 8510 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8519 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8576 negsubd 8645 negsubi 8606 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8578 negnegd 8630 negnegi 8598 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8714 subdid 8743 subdii 8736 subdir 8715 subdird 8744 subdiri 8737 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8718 mul01d 8722 mul01i 8720 mul02 8716 mul02d 8721 mul02i 8719 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 9126 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 9077 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8727 mul2negd 8742 mul2negi 8735 mulneg1 8724 mulneg1d 8740 mulneg1i 8733 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14535 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 9046 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 10089 rpaddcld 10124 rpmulcl 10090 rpmulcld 10125 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 10101 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8432 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8868 ltadd1dd 8886 ltadd1i 8832 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8923 ltmul1a 8922 ltmul1i 9253 ltmul1ii 9261 ltmul2 9189 ltmul2d 10151 ltmul2dd 10165 ltmul2i 9256 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8455 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8798 lt0neg1d 8845 ltneg 8792 ltnegd 8853 ltnegi 8823 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8775 lt2addd 8898 lt2addi 8840 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 10066 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9183 recgt0d 9267 recgt0i 9239 recgt0ii 9240 |
| [Apostol] p. 22 | Definition of integers | df-z 9650 |
| [Apostol] p. 22 | Definition of rationals | df-q 10030 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7335 |
| [Apostol] p. 26 | Theorem I.29 | arch 9565 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9770 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9566 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10702 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12657 zneo 9752 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11813 sqrtthi 11902 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9310 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12832 |
| [Apostol] p. 363 | Remark | absgt0api 11929 |
| [Apostol] p. 363 | Example | abssubd 11976 abssubi 11933 |
| [ApostolNT] p. 8 | Definition | df-ppi 16198 |
| [ApostolNT] p. 14 | Definition | df-dvds 12574 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12590 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12614 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12610 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12604 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12606 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12591 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12592 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12597 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12631 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12633 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12635 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12810 |
| [ApostolNT] p. 16 | Definition | isprm2 12914 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12889 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13398 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12769 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12811 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12813 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12783 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12776 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12942 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12944 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 13170 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12710 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12856 |
| [ApostolNT] p. 25 | Definition | df-phi 13012 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 13042 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 13023 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 13027 |
| [ApostolNT] p. 38 | Remark | df-sgm 16199 |
| [ApostolNT] p. 38 | Definition | df-sgm 16199 |
| [ApostolNT] p. 75 | Definition | df-cht 16197 |
| [ApostolNT] p. 104 | Definition | congr 12897 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12577 |
| [ApostolNT] p. 106 | Definition | moddvds 12585 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12664 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12665 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10793 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10830 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 11119 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12609 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12900 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13224 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12902 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 13034 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 13053 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 13035 |
| [ApostolNT] p. 179 | Definition | df-lgs 16283 lgsprme0 16327 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 16328 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 16304 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 16319 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 16370 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 16389 2lgsoddprm 16398 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 16354 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 16365 |
| [ApostolNT] p. 188 | Definition | df-lgs 16283 lgs1 16329 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 16320 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 16322 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 16330 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 16331 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 625 pm2.65 669 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6084 onsucelsucexmidlem 4676 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 17193 |
| [Bauer], p. 483 | Definition | n0rf 3534 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 16173 2irrexpqap 16175 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7246 ssfiexmid 7178 ssfiexmidt 7180 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15845 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15835 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8976 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7456 |
| [BauerSwan], p. 14 | Remark | 0ct 7448 ctm 7450 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 17196 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7869 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7782 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7871 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7905 addlocpr 7904 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7931 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7934 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7939 |
| [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 4254 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4314 |
| [BellMachover] p. 466 | Axiom Union | axun2 4580 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4689 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4529 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4692 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4643 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4514 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4736 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4761 |
| [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 16465 isuhgropm 16488 isusgropen 16572 isuspgropen 16571 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16661 uhgrspansubgr 16684 |
| [Bollobas] p. 4 | Definition | df-wlks 16725 |
| [Bollobas] p. 5 | Definition | df-trls 16788 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 16477 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13729 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13770 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13783 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14386 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 14316 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5989 fcofo 5990 |
| [BourbakiTop1] p. | Remark | xnegmnf 10242 xnegpnf 10241 |
| [BourbakiTop1] p. | Remark | rexneg 10243 |
| [BourbakiTop1] p. | Proposition | ishmeo 15496 |
| [BourbakiTop1] p. | Property V_i | ssnei2 15349 |
| [BourbakiTop1] p. | Property V_ii | innei 15355 |
| [BourbakiTop1] p. | Property V_iv | neissex 15357 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 15346 neiss 15342 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 15414 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15491 |
| [BourbakiTop1] p. | Property V_iii | elnei 15344 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 15190 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13729 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13770 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13957 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4194 |
| [Church] p. 129 | Section II.24 | df-ifp 991 dfifp2dc 994 |
| [Cohen] p. 301 | Remark | relogoprlem 16062 |
| [Cohen] p. 301 | Property 2 | relogmul 16063 relogmuld 16078 |
| [Cohen] p. 301 | Property 3 | relogdiv 16064 relogdivd 16079 |
| [Cohen] p. 301 | Property 4 | relogexp 16066 |
| [Cohen] p. 301 | Property 1a | log1 16059 |
| [Cohen] p. 301 | Property 1b | loge 16060 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 16162 |
| [Cohen4] p. 352 | Definition | rpelogb 16146 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 16152 |
| [Cohen4] p. 361 | Property 3 | logbrec 16157 rprelogbdiv 16154 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 16150 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 16155 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 16144 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 16145 |
| [Cohen4] p. 367 | Property | rplogbchbase 16147 |
| [Cohen4] p. 377 | Property 2 | logblt 16159 |
| [Crosilla] p. | Axiom 1 | ax-ext 2220 |
| [Crosilla] p. | Axiom 2 | ax-pr 4346 |
| [Crosilla] p. | Axiom 3 | ax-un 4578 |
| [Crosilla] p. | Axiom 4 | ax-nul 4259 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4735 |
| [Crosilla] p. | Axiom 6 | ru 3050 |
| [Crosilla] p. | Axiom 8 | ax-pow 4311 |
| [Crosilla] p. | Axiom 9 | ax-setind 4684 |
| [Crosilla], p. | Axiom 6 | ax-sep 4249 |
| [Crosilla], p. | Axiom 7 | ax-coll 4246 |
| [Crosilla], p. | Axiom 7' | repizf 4247 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4668 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6084 |
| [Crosilla], p. | Definition of ordinal | df-iord 4511 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4682 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16661 uhgrspansubgr 16684 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 16477 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3222 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4738 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6924 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4258 |
| [Enderton] p. 19 | Definition | df-tp 3717 |
| [Enderton] p. 26 | Exercise 5 | unissb 3965 |
| [Enderton] p. 26 | Exercise 10 | pwel 4358 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4431 |
| [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 4626 iunpwss 4104 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4357 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4329 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4596 rnex 5050 rnexg 5047 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4991 rnuni 5199 |
| [Enderton] p. 42 | Definition of a function | dffun7 5404 dffun8 5405 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5767 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5442 |
| [Enderton] p. 44 | Definition (d) | dfima2 5128 dfima3 5129 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5774 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7563 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5967 |
| [Enderton] p. 52 | Definition | df-map 6924 |
| [Enderton] p. 53 | Exercise 21 | coass 5306 |
| [Enderton] p. 53 | Exercise 27 | dmco 5296 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5452 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5163 |
| [Enderton] p. 54 | Remark | ixpf 7002 ixpssmap 7014 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6981 |
| [Enderton] p. 56 | Theorem 3M | erref 6827 |
| [Enderton] p. 57 | Lemma 3N | erthi 6855 |
| [Enderton] p. 57 | Definition | df-ec 6809 |
| [Enderton] p. 58 | Definition | df-qs 6813 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6914 th3qcor 6913 th3qlem1 6911 th3qlem2 6912 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6809 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4988 |
| [Enderton] p. 68 | Definition of successor | df-suc 4516 |
| [Enderton] p. 71 | Definition | df-tr 4230 dftr4 4234 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4558 unisucg 4559 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4558 unisucg 4559 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4243 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4244 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6747 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6749 onasuc 6739 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6088 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6748 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6750 onmsuc 6746 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6758 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6751 nnacom 6757 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6759 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6760 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6762 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6752 nnmsucr 6761 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6801 |
| [Enderton] p. 129 | Definition | df-en 7023 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6036 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13338 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7167 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7158 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7146 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7575 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7571 dju1en 7570 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3603 |
| [Enderton] p. 145 | Figure 38 | ffoss 5672 |
| [Enderton] p. 145 | Definition | df-dom 7024 |
| [Enderton] p. 146 | Example 1 | domen 7035 domeng 7036 |
| [Enderton] p. 146 | Example 3 | nndomo 7165 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7133 xpdom1g 7131 xpdom2g 7130 |
| [Enderton] p. 168 | Definition | df-po 4441 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4573 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4534 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4690 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4537 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4663 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4636 |
| [Enderton] p. 194 | Remark | onprc 4699 |
| [Enderton] p. 194 | Exercise 16 | suc11 4705 |
| [Enderton] p. 197 | Definition | df-card 7525 |
| [Enderton] p. 200 | Exercise 25 | tfis 4730 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4701 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4703 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4704 |
| [Geuvers], p. 1 | Remark | expap0 11021 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8946 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8985 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8947 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8299 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11986 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11994 maxle2 11995 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11996 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11999 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 12000 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8913 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7715 enqer 7726 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7719 df-nqqs 7716 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7712 df-plqqs 7717 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7713 df-mqqs 7718 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7720 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7776 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7779 ltbtwnnq 7784 ltbtwnnqq 7783 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7768 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7769 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7905 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7947 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7946 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7965 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7981 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7987 ltaprlem 7986 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7984 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7940 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7960 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7949 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7948 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7956 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 8006 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 8094 enrer 8103 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 8099 df-1r 8100 df-nr 8095 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 8097 df-plr 8096 negexsr 8140 recexsrlem 8142 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 8098 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9293 creur 9292 cru 8933 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8291 axcnre 8249 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11639 crimd 11759 crimi 11719 crre 11638 crred 11758 crrei 11718 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11641 remimd 11724 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11839 absval2d 11968 absval2i 11927 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11665 cjaddd 11747 cjaddi 11714 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11666 cjmuld 11748 cjmuli 11715 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11664 cjcjd 11725 cjcji 11697 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11663 cjreb 11647 cjrebd 11728 cjrebi 11700 cjred 11753 rere 11646 rereb 11644 rerebd 11727 rerebi 11699 rered 11751 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11672 addcjd 11739 addcji 11709 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11783 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11834 abscjd 11973 abscji 11931 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11846 abs00d 11969 abs00i 11928 absne0d 11970 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11879 releabsd 11974 releabsi 11932 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11851 absmuld 11977 absmuli 11934 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11837 sqabsaddi 11935 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11887 abstrid 11979 abstrii 11938 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10991 exp0 10995 expp1 10998 expp1d 11127 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 11033 expaddd 11128 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 16109 cxpmuld 16134 expmul 11036 expmuld 11129 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 11030 mulexpd 11141 rpmulcxp 16106 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10424 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 12111 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 12113 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 12112 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 12116 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 12109 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 12105 climcj 12106 climim 12108 climre 12107 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8366 df-xr 8365 ltxr 10188 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 12132 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10750 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14966 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15556 xmet0 15555 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15563 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15565 mstri 15665 xmettri 15564 xmstri 15664 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15471 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15703 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 12095 addcncntop 15754 mulcn2 12097 mulcncntop 15756 subcn2 12096 subcncntop 15755 |
| [Gleason] p. 295 | Remark | bcval3 11205 bcval4 11206 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11220 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11203 df-bc 11202 |
| [Gleason] p. 296 | Remark | bcn0 11209 bcnn 11211 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12270 |
| [Gleason] p. 308 | Equation 2 | ef0 12458 |
| [Gleason] p. 308 | Equation 3 | efcj 12459 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12464 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12468 |
| [Gleason] p. 310 | Equation 14 | sinadd 12522 |
| [Gleason] p. 310 | Equation 15 | cosadd 12523 |
| [Gleason] p. 311 | Equation 17 | sincossq 12534 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12539 sinbnd 12538 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12439 |
| [Golan] p. 1 | Remark | srgisid 14374 |
| [Golan] p. 1 | Definition | df-srg 14352 |
| [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 13869 mndideu 13792 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13896 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13925 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13936 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13958 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 17291 |
| [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 7582 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6772 |
| [HoTT], p. | Exercise 11.10 | neapmkv 17285 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8988 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7838 df-imp 7837 df-iplp 7836 df-reap 8906 |
| [HoTT], p. | Theorem 11.2.4 | recapb 9004 rerecapb 9176 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6371 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 8030 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16901 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 17278 dceqnconst 17277 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8268 caucvgpr 8050 caucvgprpr 8080 caucvgsr 8170 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7834 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 17283 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4442 ltpopr 7963 ltsopr 7964 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8937 reapcotr 8929 reapirr 8908 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8455 gt0add 8904 leadd1 8760 lelttr 8415 lemul1a 9191 lenlt 8402 ltadd1 8759 ltletr 8416 ltmul1 8923 reaplt 8919 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16834 |
| [Jech] p. 4 | Definition of class | cv 1401 cvjust 2233 |
| [Jech] p. 78 | Note | opthprc 4826 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1583 |
| [Kreyszig] p. 3 | Property M1 | metcl 15545 xmetcl 15544 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15552 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 9001 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15634 |
| [Kreyszig] p. 19 | Remark | mopntopon 15635 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15680 mopnm 15640 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15678 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15683 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15705 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 15405 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14751 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14742 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14743 |
| [Kunen] p. 10 | Axiom 0 | a9e 1748 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4248 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6934 mapvalg 6932 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6928 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4022 |
| [Lang] p. 3 | Statement | lidrideqd 13754 mndbn0 13797 |
| [Lang] p. 3 | Definition | df-mnd 13783 |
| [Lang] p. 4 | Definition of a (finite) product | gzsumsplit1r 13768 |
| [Lang] p. 5 | Equation | gzsumreidx 14225 |
| [Lang] p. 6 | Definition | mulgnn0gzsum 13984 |
| [Lang] p. 7 | Definition | dfgrp2e 13886 |
| [Lang2] p. 3 | Notations | df-ind 9297 |
| [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 4622 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3934 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4427 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4428 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4429 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3955 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4909 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5308 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4516 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7145 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7119 xpsneng 7120 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7125 xpcomeng 7126 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7128 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7122 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6926 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 7100 mapsnend 7099 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 7151 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7150 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6967 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 7101 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7574 djucomen 7573 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7572 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6740 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3453 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4863 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4864 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4193 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5303 coi2 5304 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4995 rn0 5038 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5192 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4884 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 5002 rnxpm 5217 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4855 xp0 5207 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5146 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5143 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5141 imaexg 5140 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5137 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5838 funfvop 5821 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5744 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5754 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5422 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5974 dff13f 5976 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5940 funrnex 6343 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5968 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5271 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3986 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6389 df-1st 6374 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6390 df-2nd 6375 |
| [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 4383 |
| [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 17292 |
| [Munkres] p. 77 | Example 2 | distop 15277 |
| [Munkres] p. 78 | Definition of basis | df-bases 15235 isbasis3g 15238 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13667 tgval2 15243 |
| [Munkres] p. 79 | Remark | tgcl 15256 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 15250 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 15271 tgss3 15270 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 15272 basgen2 15273 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 15362 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 15304 topcld 15301 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 15305 |
| [Munkres] p. 94 | Definition of closure | clsval 15303 |
| [Munkres] p. 94 | Definition of interior | ntrval 15302 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 15380 iscn 15389 iscn2 15392 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 15422 cncnp2m 15423 cncnpi 15420 df-cnp 15381 iscnp 15391 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15706 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7208 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7505 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7493 omniwomnimkv 7508 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3339 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7476 exmidomniim 7482 finomni 7481 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7461 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 17230 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 17234 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7215 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7554 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7555 exmidfodomrlemrALT 7556 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7490 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 17216 peano4nninf 17215 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 17218 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 17226 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 17228 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 17214 |
| [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 4321 snexprc 4323 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4349 |
| [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 5348 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5338 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5349 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5353 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5354 |
| [Quine] p. 58 | Definition 9.1 | df-op 3718 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4398 opabidw 4399 opelopab 4414 opelopaba 4408 opelopabaf 4416 opelopabf 4417 opelopabg 4410 opelopabga 4405 opelopabgf 4412 oprabid 6117 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4780 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4782 |
| [Quine] p. 64 | Definition 9.15 | df-id 4438 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5439 |
| [Quine] p. 65 | Theorem 10.4 | funi 5409 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5429 funsng 5427 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5379 |
| [Quine] p. 65 | Definition 10.2 | args 5156 dffv4g 5692 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5385 fv2 5690 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 11178 nn0opth2d 11177 nn0opthd 11176 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5466 funimaexg 5465 |
| [Roman] p. 18 | Part Preliminaries | df-rng 14316 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14386 |
| [Rudin] p. 164 | Equation 27 | efcan 12462 |
| [Rudin] p. 164 | Equation 30 | efzval 12469 |
| [Rudin] p. 167 | Equation 48 | absefi 12555 |
| [Russell1905] p. 482 | Example of "the father | dfalseu2 17344 |
| [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 5172 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5174 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5171 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5169 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14388 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 15275 |
| [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 4263 |
| [Suppes] p. 39 | Theorem 61 | uniss 3956 |
| [Suppes] p. 39 | Theorem 65 | uniop 4396 |
| [Suppes] p. 41 | Theorem 70 | intsn 4005 |
| [Suppes] p. 42 | Theorem 71 | intpr 4002 intprg 4003 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4624 op1stbg 4625 |
| [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 4293 elpw2g 4292 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 4882 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4915 xpindir 4916 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4831 xpundir 4832 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4695 |
| [Suppes] p. 58 | Theorem 2 | relss 4862 |
| [Suppes] p. 59 | Theorem 4 | eldm 4978 eldm2 4979 eldm2g 4977 eldmg 4976 |
| [Suppes] p. 59 | Definition 3 | df-dm 4784 |
| [Suppes] p. 60 | Theorem 6 | dmin 4989 |
| [Suppes] p. 60 | Theorem 8 | rnun 5196 |
| [Suppes] p. 60 | Theorem 9 | rnin 5197 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4968 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4963 brcnvg 4961 |
| [Suppes] p. 62 | Equation 5 | elcnv 4957 elcnv2 4958 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5165 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5195 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5193 |
| [Suppes] p. 63 | Theorem 20 | co02 5301 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5052 |
| [Suppes] p. 63 | Definition 7 | df-co 4783 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4965 |
| [Suppes] p. 64 | Theorem 27 | coass 5306 |
| [Suppes] p. 65 | Theorem 31 | resundi 5076 |
| [Suppes] p. 65 | Theorem 34 | elima 5131 elima2 5132 elima3 5133 elimag 5130 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5200 |
| [Suppes] p. 66 | Theorem 40 | dminss 5202 |
| [Suppes] p. 66 | Theorem 41 | imainss 5203 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5206 |
| [Suppes] p. 81 | Definition 34 | dfec2 6810 |
| [Suppes] p. 82 | Theorem 72 | elec 6848 elecg 6847 |
| [Suppes] p. 82 | Theorem 73 | erth 6853 erth2 6854 |
| [Suppes] p. 89 | Theorem 96 | map0b 6968 |
| [Suppes] p. 89 | Theorem 97 | map0 6971 map0g 6969 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6972 mapsnd 6970 |
| [Suppes] p. 89 | Theorem 99 | mapss 6973 |
| [Suppes] p. 92 | Theorem 1 | enref 7051 enrefg 7050 |
| [Suppes] p. 92 | Theorem 2 | ensym 7068 ensymb 7067 ensymi 7069 |
| [Suppes] p. 92 | Theorem 3 | entr 7071 |
| [Suppes] p. 92 | Theorem 4 | unen 7105 |
| [Suppes] p. 94 | Theorem 15 | endom 7049 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 7065 |
| [Suppes] p. 94 | Theorem 17 | domtr 7072 |
| [Suppes] p. 95 | Theorem 18 | isbth 7284 |
| [Suppes] p. 98 | Exercise 4 | fundmen 7094 fundmeng 7095 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7132 |
| [Suppes] p. 130 | Definition 3 | df-tr 4230 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4635 |
| [Suppes] p. 134 | Definition 6 | df-suc 4516 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4750 finds 4747 finds1 4749 finds2 4748 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7721 df-ltpq 7714 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4535 |
| [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 6089 |
| [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 4371 |
| [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 4583 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4377 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4355 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4587 unexg 4589 |
| [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 4316 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3757 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4551 elsucg 4549 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 4356 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4363 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2537 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4260 |
| [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 4686 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2823 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4265 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3561 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4270 ssexg 4272 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4267 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4697 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4688 |
| [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 4891 xpexg 4889 xpexgALT 6366 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4781 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5445 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5609 fun11 5448 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5388 svrelfun 5446 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4967 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4969 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4786 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4787 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4783 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5242 dfrel2 5238 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4883 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4894 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4900 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4914 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5091 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5068 opelresg 5070 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5084 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5087 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5092 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5418 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5286 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5417 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5610 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2131 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5385 fv3 5718 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5326 cnvexg 5325 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5049 dmexg 5046 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5050 rnexg 5047 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnvm 5142 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5712 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5722 tz6.12 5723 tz6.12c 5725 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5686 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5380 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5381 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5383 wfo 5375 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5382 wf1 5374 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5384 wf1o 5376 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5806 eqfnfv2 5807 eqfnfv2f 5810 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5775 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5937 fnexALT 6340 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5936 resfunexgALT 6337 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5466 funimaexg 5465 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4131 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5157 iniseg 5159 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4434 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5386 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 6016 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 6017 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 6022 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 6024 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 6032 |
| [TakeutiZaring] p. 35 | Notation | wtr 4229 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4499 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4233 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4723 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4526 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4530 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4639 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4513 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4633 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4699 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4729 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4231 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4658 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4634 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3963 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4516 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4560 sucidg 4561 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4648 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4514 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4653 ordelsuc 4652 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4741 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4742 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4743 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4740 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4754 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4746 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4744 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4745 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3984 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4245 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3985 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4664 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3971 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6579 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6636 tfri1d 6606 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6637 tfri2d 6607 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6638 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6573 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6557 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6737 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6733 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6730 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6734 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6782 nnaordi 6781 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4057 uniss2 3966 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6743 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6753 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6744 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6731 omsuc 6745 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6754 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6790 nnmordi 6789 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6732 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7533 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 7082 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7158 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7159 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 7025 isfi 7047 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7129 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6924 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7135 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7148 |
| [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 5357 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5358 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2166 eupickbi 2169 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5385 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7537 |
| [vandenDries] p. 43 | Theorem 62 | pellexlem1 16190 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |