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 7449 fidcenum 7267 |
| [AczelRathjen], p. 72 | Proposition 8.1.11 | fidcenum 7267 |
| [AczelRathjen], p. 73 | Lemma 8.1.14 | enumct 7449 |
| [AczelRathjen], p. 73 | Corollary 8.1.13 | ennnfone 13299 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 7233 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 7219 |
| [AczelRathjen], p. 74 | Theorem 8.1.19 | ctiunct 13314 |
| [AczelRathjen], p. 75 | Corollary 8.1.20 | unct 13316 |
| [AczelRathjen], p. 75 | Corollary 8.1.23 | qnnen 13305 znnen 13272 |
| [AczelRathjen], p. 77 | Lemma 8.1.27 | omctfn 13317 |
| [AczelRathjen], p. 78 | Theorem 8.1.28 | omiunct 13318 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 11198 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4682 |
| [AhoHopUll] p. 318 | Section 9.1 | df-concat 11342 df-pfx 11428 df-substr 11401 df-word 11288 lencl 11291 wrd0 11312 |
| [Apostol] p. 18 | Theorem I.1 | addcan 8500 addcan2d 8505 addcan2i 8503 addcand 8504 addcani 8502 |
| [Apostol] p. 18 | Theorem I.2 | negeu 8511 |
| [Apostol] p. 18 | Theorem I.3 | negsub 8568 negsubd 8637 negsubi 8598 |
| [Apostol] p. 18 | Theorem I.4 | negneg 8570 negnegd 8622 negnegi 8590 |
| [Apostol] p. 18 | Theorem I.5 | subdi 8706 subdid 8735 subdii 8728 subdir 8707 subdird 8736 subdiri 8729 |
| [Apostol] p. 18 | Theorem I.6 | mul01 8710 mul01d 8714 mul01i 8712 mul02 8708 mul02d 8713 mul02i 8711 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 9117 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 9068 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 8719 mul2negd 8734 mul2negi 8727 mulneg1 8716 mulneg1d 8732 mulneg1i 8725 |
| [Apostol] p. 18 | Theorem I.14 | rdivmuldivd 14434 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 9037 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 10061 rpaddcld 10096 rpmulcl 10062 rpmulcld 10097 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 10073 |
| [Apostol] p. 20 | Theorem I.17 | lttri 8424 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 8860 ltadd1dd 8878 ltadd1i 8824 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 8914 ltmul1a 8913 ltmul1i 9244 ltmul1ii 9252 ltmul2 9180 ltmul2d 10123 ltmul2dd 10137 ltmul2i 9247 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 8447 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 8790 lt0neg1d 8837 ltneg 8784 ltnegd 8845 ltnegi 8815 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 8767 lt2addd 8889 lt2addi 8832 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 10038 |
| [Apostol] p. 21 | Exercise 4 | recgt0 9174 recgt0d 9258 recgt0i 9230 recgt0ii 9231 |
| [Apostol] p. 22 | Definition of integers | df-z 9628 |
| [Apostol] p. 22 | Definition of rationals | df-q 10003 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 7328 |
| [Apostol] p. 26 | Theorem I.29 | arch 9543 |
| [Apostol] p. 28 | Exercise 2 | btwnz 9748 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 9544 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 10674 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 12621 zneo 9730 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 11780 sqrtthi 11868 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 9290 |
| [Apostol] p. 34 | Theorem I.37 (well-ordering principle) | nnwodc 12796 |
| [Apostol] p. 363 | Remark | absgt0api 11895 |
| [Apostol] p. 363 | Example | abssubd 11942 abssubi 11899 |
| [ApostolNT] p. 14 | Definition | df-dvds 12538 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 12554 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 12578 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 12574 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 12568 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 12570 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 12555 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 12556 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 12561 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 12595 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 12597 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 12599 |
| [ApostolNT] p. 15 | Definition | dfgcd2 12774 |
| [ApostolNT] p. 16 | Definition | isprm2 12878 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 12853 |
| [ApostolNT] p. 16 | Theorem 1.7 | prminf 13329 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 12733 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 12775 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 12777 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 12747 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 12740 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 12905 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 12907 |
| [ApostolNT] p. 17 | Theorem 1.10 | 1arith2 13130 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 12674 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucalg 12820 |
| [ApostolNT] p. 25 | Definition | df-phi 12972 |
| [ApostolNT] p. 26 | Theorem 2.2 | phisum 13002 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 12983 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 12987 |
| [ApostolNT] p. 38 | Remark | df-sgm 16079 |
| [ApostolNT] p. 38 | Definition | df-sgm 16079 |
| [ApostolNT] p. 104 | Definition | congr 12861 |
| [ApostolNT] p. 106 | Remark | dvdsval3 12541 |
| [ApostolNT] p. 106 | Definition | moddvds 12549 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 12628 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 12629 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 10761 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 10798 |
| [ApostolNT] p. 107 | Theorem 5.2(c) | modqexp 11087 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 12573 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 12864 |
| [ApostolNT] p. 109 | Theorem 5.6 | gcdmodi 13183 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 12866 |
| [ApostolNT] p. 113 | Theorem 5.17 | eulerth 12994 |
| [ApostolNT] p. 113 | Theorem 5.18 | vfermltl 13013 |
| [ApostolNT] p. 114 | Theorem 5.19 | fermltl 12995 |
| [ApostolNT] p. 179 | Definition | df-lgs 16100 lgsprme0 16144 |
| [ApostolNT] p. 180 | Example 1 | 1lgs 16145 |
| [ApostolNT] p. 180 | Theorem 9.2 | lgsvalmod 16121 |
| [ApostolNT] p. 180 | Theorem 9.3 | lgsdirprm 16136 |
| [ApostolNT] p. 181 | Theorem 9.4 | m1lgs 16187 |
| [ApostolNT] p. 181 | Theorem 9.5 | 2lgs 16206 2lgsoddprm 16215 |
| [ApostolNT] p. 182 | Theorem 9.6 | gausslemma2d 16171 |
| [ApostolNT] p. 185 | Theorem 9.8 | lgsquad 16182 |
| [ApostolNT] p. 188 | Definition | df-lgs 16100 lgs1 16146 |
| [ApostolNT] p. 188 | Theorem 9.9(a) | lgsdir 16137 |
| [ApostolNT] p. 188 | Theorem 9.9(b) | lgsdi 16139 |
| [ApostolNT] p. 188 | Theorem 9.9(c) | lgsmodeq 16147 |
| [ApostolNT] p. 188 | Theorem 9.9(d) | lgsmulsqcoprm 16148 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 625 pm2.65 669 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 6078 onsucelsucexmidlem 4674 |
| [Bauer], p. 481 | Section 1.1 | pwtrufal 17010 |
| [Bauer], p. 483 | Definition | n0rf 3534 |
| [Bauer], p. 483 | Theorem 1.2 | 2irrexpq 16061 2irrexpqap 16063 |
| [Bauer], p. 485 | Theorem 2.1 | exmidssfi 7240 ssfiexmid 7172 ssfiexmidt 7174 |
| [Bauer], p. 493 | Section 5.1 | ivthdich 15737 |
| [Bauer], p. 494 | Theorem 5.5 | ivthinc 15727 |
| [BauerHanson], p. 27 | Proposition 5.2 | cnstab 8967 |
| [BauerSwan], p. 3 | Definition on page 14:3 | enumct 7449 |
| [BauerSwan], p. 14 | Remark | 0ct 7441 ctm 7443 |
| [BauerSwan], p. 14 | Proposition 2.6 | subctctexmid 17013 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 7862 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 7775 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 7864 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 7898 addlocpr 7897 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7924 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7927 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7932 |
| [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 4252 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 4312 |
| [BellMachover] p. 466 | Axiom Union | axun2 4578 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4687 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4527 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4690 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4641 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4512 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4734 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4759 |
| [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 16282 isuhgropm 16305 isusgropen 16389 isuspgropen 16388 |
| [Bollobas] p. 2 | Section I.1 | df-subgr 16478 uhgrspansubgr 16501 |
| [Bollobas] p. 4 | Definition | df-wlks 16542 |
| [Bollobas] p. 5 | Definition | df-trls 16605 |
| [Bollobas] p. 7 | Section I.1 | df-ushgrm 16294 |
| [BourbakiAlg1] p. 1 | Definition 1 | df-mgm 13659 |
| [BourbakiAlg1] p. 4 | Definition 5 | df-sgrp 13700 |
| [BourbakiAlg1] p. 12 | Definition 2 | df-mnd 13713 |
| [BourbakiAlg1] p. 92 | Definition 1 | df-ring 14285 |
| [BourbakiAlg1] p. 93 | Section I.8.1 | df-rng 14215 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5983 fcofo 5984 |
| [BourbakiTop1] p. | Remark | xnegmnf 10214 xnegpnf 10213 |
| [BourbakiTop1] p. | Remark | rexneg 10215 |
| [BourbakiTop1] p. | Proposition | ishmeo 15388 |
| [BourbakiTop1] p. | Property V_i | ssnei2 15241 |
| [BourbakiTop1] p. | Property V_ii | innei 15247 |
| [BourbakiTop1] p. | Property V_iv | neissex 15249 |
| [BourbakiTop1] p. | Proposition 1 | neipsm 15238 neiss 15234 |
| [BourbakiTop1] p. | Proposition 2 | cnptopco 15306 |
| [BourbakiTop1] p. | Proposition 4 | imasnopn 15383 |
| [BourbakiTop1] p. | Property V_iii | elnei 15236 |
| [BourbakiTop1] p. | Definition is due to Bourbaki (Def. 1 | df-top 15082 |
| [Bruck] p. 1 | Section I.1 | df-mgm 13659 |
| [Bruck] p. 23 | Section II.1 | df-sgrp 13700 |
| [Bruck] p. 28 | Theorem 3.2 | dfgrp3m 13887 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 4192 |
| [Church] p. 129 | Section II.24 | df-ifp 991 dfifp2dc 994 |
| [Cohen] p. 301 | Remark | relogoprlem 15952 |
| [Cohen] p. 301 | Property 2 | relogmul 15953 relogmuld 15968 |
| [Cohen] p. 301 | Property 3 | relogdiv 15954 relogdivd 15969 |
| [Cohen] p. 301 | Property 4 | relogexp 15956 |
| [Cohen] p. 301 | Property 1a | log1 15950 |
| [Cohen] p. 301 | Property 1b | loge 15951 |
| [Cohen4] p. 348 | Observation | relogbcxpbap 16050 |
| [Cohen4] p. 352 | Definition | rpelogb 16034 |
| [Cohen4] p. 361 | Property 2 | rprelogbmul 16040 |
| [Cohen4] p. 361 | Property 3 | logbrec 16045 rprelogbdiv 16042 |
| [Cohen4] p. 361 | Property 4 | rplogbreexp 16038 |
| [Cohen4] p. 361 | Property 6 | relogbexpap 16043 |
| [Cohen4] p. 361 | Property 1(a) | rplogbid1 16032 |
| [Cohen4] p. 361 | Property 1(b) | rplogb1 16033 |
| [Cohen4] p. 367 | Property | rplogbchbase 16035 |
| [Cohen4] p. 377 | Property 2 | logblt 16047 |
| [Crosilla] p. | Axiom 1 | ax-ext 2220 |
| [Crosilla] p. | Axiom 2 | ax-pr 4344 |
| [Crosilla] p. | Axiom 3 | ax-un 4576 |
| [Crosilla] p. | Axiom 4 | ax-nul 4257 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4733 |
| [Crosilla] p. | Axiom 6 | ru 3050 |
| [Crosilla] p. | Axiom 8 | ax-pow 4309 |
| [Crosilla] p. | Axiom 9 | ax-setind 4682 |
| [Crosilla], p. | Axiom 6 | ax-sep 4247 |
| [Crosilla], p. | Axiom 7 | ax-coll 4244 |
| [Crosilla], p. | Axiom 7' | repizf 4245 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4666 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 6078 |
| [Crosilla], p. | Definition of ordinal | df-iord 4509 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4680 |
| [Diestel] p. 4 | Section 1.1 | df-subgr 16478 uhgrspansubgr 16501 |
| [Diestel] p. 27 | Section 1.10 | df-ushgrm 16294 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 3222 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4736 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6918 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 4256 |
| [Enderton] p. 19 | Definition | df-tp 3716 |
| [Enderton] p. 26 | Exercise 5 | unissb 3963 |
| [Enderton] p. 26 | Exercise 10 | pwel 4356 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4429 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 4080 iinin2m 4079 iunin1 4075 iunin2 4074 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 4078 iundif2ss 4076 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 4093 |
| [Enderton] p. 33 | Exercise 25 | iununir 4094 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 4101 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4624 iunpwss 4102 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4355 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 4327 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4594 rnex 5048 rnexg 5045 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4989 rnuni 5197 |
| [Enderton] p. 42 | Definition of a function | dffun7 5402 dffun8 5403 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5764 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5440 |
| [Enderton] p. 44 | Definition (d) | dfima2 5126 dfima3 5127 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5771 |
| [Enderton] p. 49 | Axiom of Choice (first form) | df-ac 7556 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5961 |
| [Enderton] p. 52 | Definition | df-map 6918 |
| [Enderton] p. 53 | Exercise 21 | coass 5304 |
| [Enderton] p. 53 | Exercise 27 | dmco 5294 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5450 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 5161 |
| [Enderton] p. 54 | Remark | ixpf 6996 ixpssmap 7008 |
| [Enderton] p. 54 | Definition of infinite Cartesian product | df-ixp 6975 |
| [Enderton] p. 56 | Theorem 3M | erref 6821 |
| [Enderton] p. 57 | Lemma 3N | erthi 6849 |
| [Enderton] p. 57 | Definition | df-ec 6803 |
| [Enderton] p. 58 | Definition | df-qs 6807 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6908 th3qcor 6907 th3qlem1 6905 th3qlem2 6906 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6803 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4986 |
| [Enderton] p. 68 | Definition of successor | df-suc 4514 |
| [Enderton] p. 71 | Definition | df-tr 4228 dftr4 4232 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4556 unisucg 4557 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4556 unisucg 4557 |
| [Enderton] p. 73 | Exercise 5(a) | truni 4241 |
| [Enderton] p. 73 | Exercise 5(b) | trint 4242 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6741 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6743 onasuc 6733 |
| [Enderton] p. 79 | Definition of operation value | df-ov 6082 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6742 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6744 onmsuc 6740 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6752 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6745 nnacom 6751 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6753 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6754 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6756 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6746 nnmsucr 6755 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6795 |
| [Enderton] p. 129 | Definition | df-en 7017 |
| [Enderton] p. 132 | Theorem 6B(b) | canth 6030 |
| [Enderton] p. 133 | Exercise 1 | xpomen 13269 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 7161 |
| [Enderton] p. 136 | Corollary 6E | nneneq 7152 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 7140 |
| [Enderton] p. 142 | Theorem 6I(3) | xpdjuen 7568 |
| [Enderton] p. 143 | Theorem 6J | dju0en 7564 dju1en 7563 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3603 |
| [Enderton] p. 145 | Figure 38 | ffoss 5670 |
| [Enderton] p. 145 | Definition | df-dom 7018 |
| [Enderton] p. 146 | Example 1 | domen 7029 domeng 7030 |
| [Enderton] p. 146 | Example 3 | nndomo 7159 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 7127 xpdom1g 7125 xpdom2g 7124 |
| [Enderton] p. 168 | Definition | df-po 4439 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4571 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4532 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4688 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4535 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4661 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4634 |
| [Enderton] p. 194 | Remark | onprc 4697 |
| [Enderton] p. 194 | Exercise 16 | suc11 4703 |
| [Enderton] p. 197 | Definition | df-card 7518 |
| [Enderton] p. 200 | Exercise 25 | tfis 4728 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4699 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4701 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4702 |
| [Geuvers], p. 1 | Remark | expap0 10989 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 8937 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8976 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 8938 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 8292 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 11952 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 11960 maxle2 11961 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 11962 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 11965 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 11966 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 8904 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 7708 enqer 7719 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 7712 df-nqqs 7709 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 7705 df-plqqs 7710 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 7706 df-mqqs 7711 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 7713 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 7769 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 7772 ltbtwnnq 7777 ltbtwnnqq 7776 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 7761 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 7762 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 7898 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7940 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7939 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7958 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7974 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7980 ltaprlem 7979 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7977 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7933 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7953 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7942 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7941 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7949 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7999 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 8087 enrer 8096 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 8092 df-1r 8093 df-nr 8088 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 8090 df-plr 8089 negexsr 8133 recexsrlem 8135 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 8091 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 9284 creur 9283 cru 8924 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 8284 axcnre 8242 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 11606 crimd 11726 crimi 11686 crre 11605 crred 11725 crrei 11685 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 11608 remimd 11691 |
| [Gleason] p. 133 | Definition 10.36 | absval2 11806 absval2d 11934 absval2i 11893 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 11632 cjaddd 11714 cjaddi 11681 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 11633 cjmuld 11715 cjmuli 11682 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 11631 cjcjd 11692 cjcji 11664 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 11630 cjreb 11614 cjrebd 11695 cjrebi 11667 cjred 11720 rere 11613 rereb 11611 rerebd 11694 rerebi 11666 rered 11718 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 11639 addcjd 11706 addcji 11676 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 11750 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 11801 abscjd 11939 abscji 11897 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 11813 abs00d 11935 abs00i 11894 absne0d 11936 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 11845 releabsd 11940 releabsi 11898 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 11818 absmuld 11943 absmuli 11900 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 11804 sqabsaddi 11901 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 11853 abstrid 11945 abstrii 11904 |
| [Gleason] p. 134 | Definition 10-4.1 | df-exp 10959 exp0 10963 expp1 10966 expp1d 11095 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 11001 expaddd 11096 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | cxpmul 15997 cxpmuld 16022 expmul 11004 expmuld 11097 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 10998 mulexpd 11109 rpmulcxp 15994 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 10396 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 12075 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 12077 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 12076 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 12080 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 12073 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 12069 climcj 12070 climim 12072 climre 12071 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 8359 df-xr 8358 ltxr 10160 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 12096 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 10718 |
| [Gleason] p. 223 | Definition 14-1.1 | df-met 14865 |
| [Gleason] p. 223 | Definition 14-1.1(a) | met0 15448 xmet0 15447 |
| [Gleason] p. 223 | Definition 14-1.1(c) | metsym 15455 |
| [Gleason] p. 223 | Definition 14-1.1(d) | mettri 15457 mstri 15557 xmettri 15456 xmstri 15556 |
| [Gleason] p. 230 | Proposition 14-2.6 | txlm 15363 |
| [Gleason] p. 240 | Proposition 14-4.2 | metcnp3 15595 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 12059 addcncntop 15646 mulcn2 12061 mulcncntop 15648 subcn2 12060 subcncntop 15647 |
| [Gleason] p. 295 | Remark | bcval3 11172 bcval4 11173 |
| [Gleason] p. 295 | Equation 2 | bcpasc 11187 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 11170 df-bc 11169 |
| [Gleason] p. 296 | Remark | bcn0 11176 bcnn 11178 |
| [Gleason] p. 296 | Theorem 15-2.8 | binom 12234 |
| [Gleason] p. 308 | Equation 2 | ef0 12422 |
| [Gleason] p. 308 | Equation 3 | efcj 12423 |
| [Gleason] p. 309 | Corollary 15-4.3 | efne0 12428 |
| [Gleason] p. 309 | Corollary 15-4.4 | efexp 12432 |
| [Gleason] p. 310 | Equation 14 | sinadd 12486 |
| [Gleason] p. 310 | Equation 15 | cosadd 12487 |
| [Gleason] p. 311 | Equation 17 | sincossq 12498 |
| [Gleason] p. 311 | Equation 18 | cosbnd 12503 sinbnd 12502 |
| [Gleason] p. 311 | Definition of ` ` | df-pi 12403 |
| [Golan] p. 1 | Remark | srgisid 14273 |
| [Golan] p. 1 | Definition | df-srg 14251 |
| [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 13799 mndideu 13722 |
| [Herstein] p. 55 | Lemma 2.2.1(b) | grpinveu 13826 |
| [Herstein] p. 55 | Lemma 2.2.1(c) | grpinvinv 13855 |
| [Herstein] p. 55 | Lemma 2.2.1(d) | grpinvadd 13866 |
| [Herstein] p. 57 | Exercise 1 | dfgrp3me 13888 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 17098 |
| [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 7575 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6766 |
| [HoTT], p. | Exercise 11.10 | neapmkv 17092 |
| [HoTT], p. | Exercise 11.11 | mulap0bd 8979 |
| [HoTT], p. | Section 11.2.1 | df-iltp 7831 df-imp 7830 df-iplp 7829 df-reap 8897 |
| [HoTT], p. | Theorem 11.2.4 | recapb 8995 rerecapb 9167 |
| [HoTT], p. | Corollary 3.9.2 | uchoice 6365 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 8023 |
| [HoTT], p. | Corollary 11.4.3 | conventions 16718 |
| [HoTT], p. | Exercise 11.6(i) | dcapnconst 17085 dceqnconst 17084 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 8261 caucvgpr 8043 caucvgprpr 8073 caucvgsr 8163 |
| [HoTT], p. | Definition 11.2.1 | df-inp 7827 |
| [HoTT], p. | Exercise 11.6(ii) | nconstwlpo 17090 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4440 ltpopr 7956 ltsopr 7957 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 8928 reapcotr 8920 reapirr 8899 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 8447 gt0add 8895 leadd1 8752 lelttr 8408 lemul1a 9182 lenlt 8395 ltadd1 8751 ltletr 8409 ltmul1 8914 reaplt 8910 |
| [Huneke] p. 2 | Statement | df-clwwlknon 16651 |
| [Jech] p. 4 | Definition of class | cv 1401 cvjust 2233 |
| [Jech] p. 78 | Note | opthprc 4824 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1583 |
| [Kreyszig] p. 3 | Property M1 | metcl 15437 xmetcl 15436 |
| [Kreyszig] p. 4 | Property M2 | meteq0 15444 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8992 |
| [Kreyszig] p. 18 | Definition 1.3-2 | mopnval 15526 |
| [Kreyszig] p. 19 | Remark | mopntopon 15527 |
| [Kreyszig] p. 19 | Theorem T1 | mopn0 15572 mopnm 15532 |
| [Kreyszig] p. 19 | Theorem T2 | unimopn 15570 |
| [Kreyszig] p. 19 | Definition of neighborhood | neibl 15575 |
| [Kreyszig] p. 20 | Definition 1.3-3 | metcnp2 15597 |
| [Kreyszig] p. 25 | Definition 1.4-1 | lmbr 15297 |
| [Kreyszig] p. 51 | Equation 2 | lmodvneg1 14650 |
| [Kreyszig] p. 51 | Equation 1a | lmod0vs 14641 |
| [Kreyszig] p. 51 | Equation 1b | lmodvs0 14642 |
| [Kunen] p. 10 | Axiom 0 | a9e 1748 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 4246 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6928 mapvalg 6926 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6922 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 4020 |
| [Lang] p. 3 | Statement | lidrideqd 13684 mndbn0 13727 |
| [Lang] p. 3 | Definition | df-mnd 13713 |
| [Lang] p. 4 | Definition of a (finite) product | gzsumsplit1r 13698 |
| [Lang] p. 5 | Equation | gzsumreidx 14124 |
| [Lang] p. 6 | Definition | mulgnn0gzsum 13914 |
| [Lang] p. 7 | Definition | dfgrp2e 13816 |
| [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 4620 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3932 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4425 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4426 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4427 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3953 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4907 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 5306 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4514 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 7139 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 7113 xpsneng 7114 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 7119 xpcomeng 7120 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 7122 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 7116 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6920 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 7094 mapsnend 7093 |
| [Mendelson] p. 255 | Exercise 4.45 | mapunen 7145 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 7144 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6961 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 7095 |
| [Mendelson] p. 258 | Exercise 4.56(c) | djuassen 7567 djucomen 7566 |
| [Mendelson] p. 258 | Exercise 4.56(g) | xp2dju 7565 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6734 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3453 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4861 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4862 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 4191 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 5301 coi2 5302 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4993 rn0 5036 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 5190 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4882 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 5000 rnxpm 5215 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4853 xp0 5205 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 5144 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 5141 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 5139 imaexg 5138 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 5135 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5832 funfvop 5815 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5741 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5751 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5420 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5968 dff13f 5970 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5934 funrnex 6337 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5962 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 5269 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3984 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 6383 df-1st 6368 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 6384 df-2nd 6369 |
| [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 4381 |
| [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 17099 |
| [Munkres] p. 77 | Example 2 | distop 15169 |
| [Munkres] p. 78 | Definition of basis | df-bases 15127 isbasis3g 15130 |
| [Munkres] p. 78 | Definition of a topology generated by a basis | df-topgen 13597 tgval2 15135 |
| [Munkres] p. 79 | Remark | tgcl 15148 |
| [Munkres] p. 80 | Lemma 2.1 | tgval3 15142 |
| [Munkres] p. 80 | Lemma 2.2 | tgss2 15163 tgss3 15162 |
| [Munkres] p. 81 | Lemma 2.3 | basgen 15164 basgen2 15165 |
| [Munkres] p. 89 | Definition of subspace topology | resttop 15254 |
| [Munkres] p. 93 | Theorem 6.1(1) | 0cld 15196 topcld 15193 |
| [Munkres] p. 93 | Theorem 6.1(3) | uncld 15197 |
| [Munkres] p. 94 | Definition of closure | clsval 15195 |
| [Munkres] p. 94 | Definition of interior | ntrval 15194 |
| [Munkres] p. 102 | Definition of continuous function | df-cn 15272 iscn 15281 iscn2 15284 |
| [Munkres] p. 107 | Theorem 7.2(g) | cncnp 15314 cncnp2m 15315 cncnpi 15312 df-cnp 15273 iscnp 15283 |
| [Munkres] p. 127 | Theorem 10.1 | metcn 15598 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 7202 |
| [Pierik], p. 9 | Definition 2.4 | df-womni 7498 |
| [Pierik], p. 9 | Definition 2.5 | df-markov 7486 omniwomnimkv 7501 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3339 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 7469 exmidomniim 7475 finomni 7474 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 7454 |
| [Pradic2025], p. 2 | Section 1.1 | nnnninfen 17038 |
| [PradicBrown2022], p. 1 | Theorem 1 | exmidsbthr 17042 |
| [PradicBrown2022], p. 2 | Remark | exmidpw 7209 |
| [PradicBrown2022], p. 2 | Proposition 1.1 | exmidfodomrlemim 7547 |
| [PradicBrown2022], p. 2 | Proposition 1.2 | exmidfodomrlemr 7548 exmidfodomrlemrALT 7549 |
| [PradicBrown2022], p. 4 | Lemma 3.2 | fodjuomni 7483 |
| [PradicBrown2022], p. 5 | Lemma 3.4 | peano3nninf 17024 peano4nninf 17023 |
| [PradicBrown2022], p. 5 | Lemma 3.5 | nninfall 17026 |
| [PradicBrown2022], p. 5 | Theorem 3.6 | nninfsel 17034 |
| [PradicBrown2022], p. 5 | Corollary 3.7 | nninfomni 17036 |
| [PradicBrown2022], p. 5 | Definition 3.3 | nnsf 17022 |
| [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 3773 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3715 df-sn 3714 |
| [Quine] p. 49 | Theorem 7.4 | snss 3848 snssg 3847 |
| [Quine] p. 49 | Theorem 7.5 | prss 3869 prssg 3870 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3816 prid1g 3814 prid2 3817 prid2g 3815 snid 3739 snidg 3737 |
| [Quine] p. 51 | Theorem 7.12 | snexg 4319 snexprc 4321 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4347 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3949 unisng 3950 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3952 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3961 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3960 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 5346 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 5336 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 5347 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 5351 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 5352 |
| [Quine] p. 58 | Definition 9.1 | df-op 3717 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4396 opabidw 4397 opelopab 4412 opelopaba 4406 opelopabaf 4414 opelopabf 4415 opelopabg 4408 opelopabga 4403 opelopabgf 4410 oprabid 6111 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4778 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4780 |
| [Quine] p. 64 | Definition 9.15 | df-id 4436 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5437 |
| [Quine] p. 65 | Theorem 10.4 | funi 5407 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5427 funsng 5425 |
| [Quine] p. 65 | Definition 10.1 | df-fun 5377 |
| [Quine] p. 65 | Definition 10.2 | args 5154 dffv4g 5690 |
| [Quine] p. 68 | Definition 10.11 | df-fv 5383 fv2 5688 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 11145 nn0opth2d 11144 nn0opthd 11143 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5464 funimaexg 5463 |
| [Roman] p. 18 | Part Preliminaries | df-rng 14215 |
| [Roman] p. 19 | Part Preliminaries | df-ring 14285 |
| [Rudin] p. 164 | Equation 27 | efcan 12426 |
| [Rudin] p. 164 | Equation 30 | efzval 12433 |
| [Rudin] p. 167 | Equation 48 | absefi 12519 |
| [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 5170 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 5172 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 5169 |
| [Schechter] p. 51 | Definition of transitivity | cotr 5167 |
| [Schechter] p. 187 | Definition of "ring with unit" | isring 14287 |
| [Schechter] p. 428 | Definition 15.35 | bastop1 15167 |
| [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 3718 |
| [Stoll] p. 43 | Definition | uniiun 4064 |
| [Stoll] p. 44 | Definition | intiin 4065 |
| [Stoll] p. 45 | Definition | df-iin 4013 |
| [Stoll] p. 45 | Definition indexed union | df-iun 4012 |
| [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 4261 |
| [Suppes] p. 39 | Theorem 61 | uniss 3954 |
| [Suppes] p. 39 | Theorem 65 | uniop 4394 |
| [Suppes] p. 41 | Theorem 70 | intsn 4003 |
| [Suppes] p. 42 | Theorem 71 | intpr 4000 intprg 4001 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4622 op1stbg 4623 |
| [Suppes] p. 42 | Theorem 78 | intun 3999 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 4044 dfiun2g 4042 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 4045 |
| [Suppes] p. 47 | Theorem 86 | elpw 3694 elpw2 4291 elpw2g 4290 elpwg 3696 |
| [Suppes] p. 47 | Theorem 87 | pwid 3706 |
| [Suppes] p. 47 | Theorem 89 | pw0 3860 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3928 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4880 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4913 xpindir 4914 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4829 xpundir 4830 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4693 |
| [Suppes] p. 58 | Theorem 2 | relss 4860 |
| [Suppes] p. 59 | Theorem 4 | eldm 4976 eldm2 4977 eldm2g 4975 eldmg 4974 |
| [Suppes] p. 59 | Definition 3 | df-dm 4782 |
| [Suppes] p. 60 | Theorem 6 | dmin 4987 |
| [Suppes] p. 60 | Theorem 8 | rnun 5194 |
| [Suppes] p. 60 | Theorem 9 | rnin 5195 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4966 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4961 brcnvg 4959 |
| [Suppes] p. 62 | Equation 5 | elcnv 4955 elcnv2 4956 |
| [Suppes] p. 62 | Theorem 12 | relcnv 5163 |
| [Suppes] p. 62 | Theorem 15 | cnvin 5193 |
| [Suppes] p. 62 | Theorem 16 | cnvun 5191 |
| [Suppes] p. 63 | Theorem 20 | co02 5299 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 5050 |
| [Suppes] p. 63 | Definition 7 | df-co 4781 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4963 |
| [Suppes] p. 64 | Theorem 27 | coass 5304 |
| [Suppes] p. 65 | Theorem 31 | resundi 5074 |
| [Suppes] p. 65 | Theorem 34 | elima 5129 elima2 5130 elima3 5131 elimag 5128 |
| [Suppes] p. 65 | Theorem 35 | imaundi 5198 |
| [Suppes] p. 66 | Theorem 40 | dminss 5200 |
| [Suppes] p. 66 | Theorem 41 | imainss 5201 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 5204 |
| [Suppes] p. 81 | Definition 34 | dfec2 6804 |
| [Suppes] p. 82 | Theorem 72 | elec 6842 elecg 6841 |
| [Suppes] p. 82 | Theorem 73 | erth 6847 erth2 6848 |
| [Suppes] p. 89 | Theorem 96 | map0b 6962 |
| [Suppes] p. 89 | Theorem 97 | map0 6965 map0g 6963 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6966 mapsnd 6964 |
| [Suppes] p. 89 | Theorem 99 | mapss 6967 |
| [Suppes] p. 92 | Theorem 1 | enref 7045 enrefg 7044 |
| [Suppes] p. 92 | Theorem 2 | ensym 7062 ensymb 7061 ensymi 7063 |
| [Suppes] p. 92 | Theorem 3 | entr 7065 |
| [Suppes] p. 92 | Theorem 4 | unen 7099 |
| [Suppes] p. 94 | Theorem 15 | endom 7043 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 7059 |
| [Suppes] p. 94 | Theorem 17 | domtr 7066 |
| [Suppes] p. 95 | Theorem 18 | isbth 7278 |
| [Suppes] p. 98 | Exercise 4 | fundmen 7088 fundmeng 7089 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 7126 |
| [Suppes] p. 130 | Definition 3 | df-tr 4228 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4633 |
| [Suppes] p. 134 | Definition 6 | df-suc 4514 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4748 finds 4745 finds1 4747 finds2 4746 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 7714 df-ltpq 7707 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4533 |
| [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 6083 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 3050 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3729 elpr2 3730 elprg 3728 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3724 elsn2 3742 elsn2g 3741 elsng 3723 velsn 3725 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4369 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3719 sneqr 3883 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3727 dfsn2 3722 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4581 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4375 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4353 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4585 unexg 4587 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3757 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3934 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 3226 df-un 3224 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3947 uniprg 3948 |
| [TakeutiZaring] p. 17 | Axiom 4 | vpwex 4314 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3756 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4549 elsucg 4547 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 3942 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4354 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4361 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2537 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 4258 |
| [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 4684 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2823 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 4263 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3561 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 4268 ssexg 4270 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 4265 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4695 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4686 |
| [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 4889 xpexg 4887 xpexgALT 6360 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4779 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5443 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5607 fun11 5446 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 5386 svrelfun 5444 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4965 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4967 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4784 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4785 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4781 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 5240 dfrel2 5236 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4881 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4892 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4898 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4912 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 5089 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 5066 opelresg 5068 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 5082 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 5085 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 5090 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5416 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 5284 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5415 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5608 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 2131 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 5383 fv3 5716 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 5324 cnvexg 5323 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 5047 dmexg 5044 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 5048 rnexg 5045 |
| [TakeutiZaring] p. 26 | Corollary 6.9(2) | xpexcnvm 5140 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5710 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5720 tz6.12 5721 tz6.12c 5723 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5684 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 5378 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 5379 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 5381 wfo 5373 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 5380 wf1 5372 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 5382 wf1o 5374 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5800 eqfnfv2 5801 eqfnfv2f 5804 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5772 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5931 fnexALT 6334 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5930 resfunexgALT 6331 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5464 funimaexg 5463 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 4129 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 5155 iniseg 5157 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4432 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 5384 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 6010 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 6011 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 6016 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 6018 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 6026 |
| [TakeutiZaring] p. 35 | Notation | wtr 4227 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4497 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 4231 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4721 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4524 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4528 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4637 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4511 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4631 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4697 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4727 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 4229 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4656 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4632 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3961 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4514 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4558 sucidg 4559 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | onsuc 4646 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4512 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4651 ordelsuc 4650 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4739 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4740 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4741 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4738 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4752 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4744 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4742 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4743 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3982 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 4243 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3983 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4662 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3969 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6573 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6630 tfri1d 6600 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6631 tfri2d 6601 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6632 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 6567 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 6551 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6731 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6727 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6724 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6728 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6776 nnaordi 6775 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 4055 uniss2 3964 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6737 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6747 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6738 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6725 omsuc 6739 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6748 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6784 nnmordi 6783 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6726 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 7526 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 7076 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 7152 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 7153 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 7019 isfi 7041 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 7123 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6918 |
| [TakeutiZaring] p. 96 | Proposition 10.44 | pw2f1odc 7129 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 7142 |
| [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 5355 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 5356 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2166 eupickbi 2169 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 5383 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 7530 |
| [vandenDries] p. 43 | Theorem 62 | pellexlem1 16074 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |