Bibliographic Cross-References
|
|
Intuitionistic Logic Explorer Bibliographic Cross-References |
|
| Mirrors > Home > ILE Home > Bibliographic Cross-References | ||
| Bibliographic Reference | Description | Intuitionistic Logic Explorer Page(s) |
|---|---|---|
| [ than ] equality." ([Geuvers], p. 1 | Partness is more basic | expap0 9821 |
| [AczelRathjen], p. 74 | Lemma 8.1.16 | xpfi 6564 |
| [AczelRathjen], p. 74 | Remark 8.1.17 | unfiexmid 6554 |
| [AczelRathjen], p. 80 | Corollary 8.2.4 | df-ihash 10018 |
| [AczelRathjen], p. 183 | Chapter 20 | ax-setind 4315 |
| [Apostol] p. 18 | Theorem I.1 | addcan 7564 addcan2d 7569 addcan2i 7567 addcand 7568 addcani 7566 |
| [Apostol] p. 18 | Theorem I.2 | negeu 7575 |
| [Apostol] p. 18 | Theorem I.3 | negsub 7632 negsubd 7701 negsubi 7662 |
| [Apostol] p. 18 | Theorem I.4 | negneg 7634 negnegd 7686 negnegi 7654 |
| [Apostol] p. 18 | Theorem I.5 | subdi 7765 subdid 7794 subdii 7787 subdir 7766 subdird 7795 subdiri 7788 |
| [Apostol] p. 18 | Theorem I.6 | mul01 7769 mul01d 7773 mul01i 7771 mul02 7767 mul02d 7772 mul02i 7770 |
| [Apostol] p. 18 | Theorem I.9 | divrecapd 8156 |
| [Apostol] p. 18 | Theorem I.10 | recrecapi 8108 |
| [Apostol] p. 18 | Theorem I.12 | mul2neg 7778 mul2negd 7793 mul2negi 7786 mulneg1 7775 mulneg1d 7791 mulneg1i 7784 |
| [Apostol] p. 18 | Theorem I.15 | divdivdivap 8077 |
| [Apostol] p. 20 | Axiom 7 | rpaddcl 9051 rpaddcld 9083 rpmulcl 9052 rpmulcld 9084 |
| [Apostol] p. 20 | Axiom 9 | 0nrp 9061 |
| [Apostol] p. 20 | Theorem I.17 | lttri 7491 |
| [Apostol] p. 20 | Theorem I.18 | ltadd1d 7914 ltadd1dd 7932 ltadd1i 7879 |
| [Apostol] p. 20 | Theorem I.19 | ltmul1 7968 ltmul1a 7967 ltmul1i 8274 ltmul1ii 8282 ltmul2 8210 ltmul2d 9110 ltmul2dd 9124 ltmul2i 8277 |
| [Apostol] p. 20 | Theorem I.21 | 0lt1 7512 |
| [Apostol] p. 20 | Theorem I.23 | lt0neg1 7848 lt0neg1d 7892 ltneg 7842 ltnegd 7899 ltnegi 7870 |
| [Apostol] p. 20 | Theorem I.25 | lt2add 7825 lt2addd 7943 lt2addi 7887 |
| [Apostol] p. 20 | Definition of positive numbers | df-rp 9029 |
| [Apostol] p. 21 | Exercise 4 | recgt0 8204 recgt0d 8288 recgt0i 8260 recgt0ii 8261 |
| [Apostol] p. 22 | Definition of integers | df-z 8646 |
| [Apostol] p. 22 | Definition of rationals | df-q 8999 |
| [Apostol] p. 24 | Theorem I.26 | supeuti 6595 |
| [Apostol] p. 26 | Theorem I.29 | arch 8561 |
| [Apostol] p. 28 | Exercise 2 | btwnz 8760 |
| [Apostol] p. 28 | Exercise 3 | nnrecl 8562 |
| [Apostol] p. 28 | Exercise 6 | qbtwnre 9556 |
| [Apostol] p. 28 | Exercise 10(a) | zeneo 10650 zneo 8742 |
| [Apostol] p. 29 | Theorem I.35 | resqrtth 10290 sqrtthi 10378 |
| [Apostol] p. 34 | Theorem I.36 (principle of mathematical induction) | peano5nni 8318 |
| [Apostol] p. 363 | Remark | absgt0api 10405 |
| [Apostol] p. 363 | Example | abssubd 10452 abssubi 10409 |
| [ApostolNT] p. 14 | Definition | df-dvds 10576 |
| [ApostolNT] p. 14 | Theorem 1.1(a) | iddvds 10588 |
| [ApostolNT] p. 14 | Theorem 1.1(b) | dvdstr 10612 |
| [ApostolNT] p. 14 | Theorem 1.1(c) | dvds2ln 10608 |
| [ApostolNT] p. 14 | Theorem 1.1(d) | dvdscmul 10602 |
| [ApostolNT] p. 14 | Theorem 1.1(e) | dvdscmulr 10604 |
| [ApostolNT] p. 14 | Theorem 1.1(f) | 1dvds 10589 |
| [ApostolNT] p. 14 | Theorem 1.1(g) | dvds0 10590 |
| [ApostolNT] p. 14 | Theorem 1.1(h) | 0dvds 10595 |
| [ApostolNT] p. 14 | Theorem 1.1(i) | dvdsleabs 10625 |
| [ApostolNT] p. 14 | Theorem 1.1(j) | dvdsabseq 10627 |
| [ApostolNT] p. 14 | Theorem 1.1(k) | divconjdvds 10629 |
| [ApostolNT] p. 15 | Definition | dfgcd2 10782 |
| [ApostolNT] p. 16 | Definition | isprm2 10878 |
| [ApostolNT] p. 16 | Theorem 1.5 | coprmdvds 10853 |
| [ApostolNT] p. 16 | Theorem 1.4(a) | gcdcom 10744 |
| [ApostolNT] p. 16 | Theorem 1.4(b) | gcdass 10783 |
| [ApostolNT] p. 16 | Theorem 1.4(c) | absmulgcd 10785 |
| [ApostolNT] p. 16 | Theorem 1.4(d)1 | gcd1 10757 |
| [ApostolNT] p. 16 | Theorem 1.4(d)2 | gcdid0 10750 |
| [ApostolNT] p. 17 | Theorem 1.8 | coprm 10902 |
| [ApostolNT] p. 17 | Theorem 1.9 | euclemma 10904 |
| [ApostolNT] p. 19 | Theorem 1.14 | divalg 10703 |
| [ApostolNT] p. 20 | Theorem 1.15 | eucialg 10820 |
| [ApostolNT] p. 25 | Definition | df-phi 10966 |
| [ApostolNT] p. 28 | Theorem 2.5(a) | phiprmpw 10977 |
| [ApostolNT] p. 28 | Theorem 2.5(c) | phimul 10981 |
| [ApostolNT] p. 104 | Definition | congr 10861 |
| [ApostolNT] p. 106 | Remark | dvdsval3 10579 |
| [ApostolNT] p. 106 | Definition | moddvds 10584 |
| [ApostolNT] p. 107 | Example 2 | mod2eq0even 10657 |
| [ApostolNT] p. 107 | Example 3 | mod2eq1n2dvds 10658 |
| [ApostolNT] p. 107 | Example 4 | zmod1congr 9636 |
| [ApostolNT] p. 107 | Theorem 5.2(b) | modqmul12d 9673 |
| [ApostolNT] p. 108 | Theorem 5.3 | modmulconst 10607 |
| [ApostolNT] p. 109 | Theorem 5.4 | cncongr1 10864 |
| [ApostolNT] p. 109 | Theorem 5.4 "Cancellation law" | cncongr 10866 |
| [Bauer] p. 482 | Section 1.2 | pm2.01 579 pm2.65 618 |
| [Bauer] p. 483 | Theorem 1.3 | acexmid 5589 onsucelsucexmidlem 4307 |
| [Bauer], p. 483 | Definition | n0rf 3278 |
| [Bauer], p. 485 | Theorem 2.1 | ssfiexmid 6521 |
| [BauerTaylor], p. 32 | Lemma 6.16 | prarloclem 6962 |
| [BauerTaylor], p. 50 | Lemma 11.4 | subhalfnqq 6875 |
| [BauerTaylor], p. 52 | Proposition 11.15 | prarloc 6964 |
| [BauerTaylor], p. 53 | Lemma 11.16 | addclpr 6998 addlocpr 6997 |
| [BauerTaylor], p. 55 | Proposition 12.7 | appdivnq 7024 |
| [BauerTaylor], p. 56 | Lemma 12.8 | prmuloc 7027 |
| [BauerTaylor], p. 56 | Lemma 12.9 | mullocpr 7032 |
| [BellMachover] p. 36 | Lemma 10.3 | idALT 20 |
| [BellMachover] p. 97 | Definition 10.1 | df-eu 1946 |
| [BellMachover] p. 460 | Notation | df-mo 1947 |
| [BellMachover] p. 460 | Definition | mo3 1997 mo3h 1996 |
| [BellMachover] p. 462 | Theorem 1.1 | bm1.1 2068 |
| [BellMachover] p. 463 | Theorem 1.3ii | bm1.3ii 3925 |
| [BellMachover] p. 466 | Axiom Pow | axpow3 3977 |
| [BellMachover] p. 466 | Axiom Union | axun2 4225 |
| [BellMachover] p. 469 | Theorem 2.2(i) | ordirr 4320 |
| [BellMachover] p. 469 | Theorem 2.2(iii) | onelon 4174 |
| [BellMachover] p. 469 | Theorem 2.2(vii) | ordn2lp 4323 |
| [BellMachover] p. 471 | Problem 2.5(ii) | bm2.5ii 4275 |
| [BellMachover] p. 471 | Definition of Lim | df-ilim 4159 |
| [BellMachover] p. 472 | Axiom Inf | zfinf2 4366 |
| [BellMachover] p. 473 | Theorem 2.8 | limom 4390 |
| [Bobzien] p. 116 | Statement T3 | stoic3 1361 |
| [Bobzien] p. 117 | Statement T2 | stoic2a 1359 |
| [Bobzien] p. 117 | Statement T4 | stoic4a 1362 |
| [BourbakiEns] p. | Proposition 8 | fcof1 5501 fcofo 5502 |
| [BourbakiTop1] p. | Remark | xnegmnf 9185 xnegpnf 9184 |
| [BourbakiTop1] p. | Remark | rexneg 9186 |
| [ChoquetDD] p. 2 | Definition of mapping | df-mpt 3867 |
| [Crosilla] p. | Axiom 1 | ax-ext 2065 |
| [Crosilla] p. | Axiom 2 | ax-pr 3999 |
| [Crosilla] p. | Axiom 3 | ax-un 4223 |
| [Crosilla] p. | Axiom 4 | ax-nul 3930 |
| [Crosilla] p. | Axiom 5 | ax-iinf 4365 |
| [Crosilla] p. | Axiom 6 | ru 2825 |
| [Crosilla] p. | Axiom 8 | ax-pow 3974 |
| [Crosilla] p. | Axiom 9 | ax-setind 4315 |
| [Crosilla], p. | Axiom 6 | ax-sep 3922 |
| [Crosilla], p. | Axiom 7 | ax-coll 3919 |
| [Crosilla], p. | Axiom 7' | repizf 3920 |
| [Crosilla], p. | Theorem is stated | ordtriexmid 4300 |
| [Crosilla], p. | Axiom of choice implies instances | acexmid 5589 |
| [Crosilla], p. | Definition of ordinal | df-iord 4156 |
| [Crosilla], p. | Theorem "Foundation implies instances of EM" | regexmid 4313 |
| [Eisenberg] p. 67 | Definition 5.3 | df-dif 2986 |
| [Eisenberg] p. 82 | Definition 6.3 | df-iom 4368 |
| [Eisenberg] p. 125 | Definition 8.21 | df-map 6336 |
| [Enderton] p. 18 | Axiom of Empty Set | axnul 3929 |
| [Enderton] p. 19 | Definition | df-tp 3430 |
| [Enderton] p. 26 | Exercise 5 | unissb 3657 |
| [Enderton] p. 26 | Exercise 10 | pwel 4008 |
| [Enderton] p. 28 | Exercise 7(b) | pwunim 4076 |
| [Enderton] p. 30 | Theorem "Distributive laws" | iinin1m 3773 iinin2m 3772 iunin1 3768 iunin2 3767 |
| [Enderton] p. 31 | Theorem "De Morgan's laws" | iindif2m 3771 iundif2ss 3769 |
| [Enderton] p. 33 | Exercise 23 | iinuniss 3784 |
| [Enderton] p. 33 | Exercise 25 | iununir 3785 |
| [Enderton] p. 33 | Exercise 24(a) | iinpw 3789 |
| [Enderton] p. 33 | Exercise 24(b) | iunpw 4264 iunpwss 3790 |
| [Enderton] p. 38 | Exercise 6(a) | unipw 4007 |
| [Enderton] p. 38 | Exercise 6(b) | pwuni 3990 |
| [Enderton] p. 41 | Lemma 3D | opeluu 4235 rnex 4657 rnexg 4655 |
| [Enderton] p. 41 | Exercise 8 | dmuni 4603 rnuni 4796 |
| [Enderton] p. 42 | Definition of a function | dffun7 4994 dffun8 4995 |
| [Enderton] p. 43 | Definition of function value | funfvdm2 5312 |
| [Enderton] p. 43 | Definition of single-rooted | funcnv 5027 |
| [Enderton] p. 44 | Definition (d) | dfima2 4730 dfima3 4731 |
| [Enderton] p. 47 | Theorem 3H | fvco2 5317 |
| [Enderton] p. 50 | Theorem 3K(a) | imauni 5479 |
| [Enderton] p. 52 | Definition | df-map 6336 |
| [Enderton] p. 53 | Exercise 21 | coass 4902 |
| [Enderton] p. 53 | Exercise 27 | dmco 4892 |
| [Enderton] p. 53 | Exercise 14(a) | funin 5037 |
| [Enderton] p. 53 | Exercise 22(a) | imass2 4762 |
| [Enderton] p. 56 | Theorem 3M | erref 6241 |
| [Enderton] p. 57 | Lemma 3N | erthi 6267 |
| [Enderton] p. 57 | Definition | df-ec 6223 |
| [Enderton] p. 58 | Definition | df-qs 6227 |
| [Enderton] p. 60 | Theorem 3Q | th3q 6326 th3qcor 6325 th3qlem1 6323 th3qlem2 6324 |
| [Enderton] p. 61 | Exercise 35 | df-ec 6223 |
| [Enderton] p. 65 | Exercise 56(a) | dmun 4600 |
| [Enderton] p. 68 | Definition of successor | df-suc 4161 |
| [Enderton] p. 71 | Definition | df-tr 3902 dftr4 3906 |
| [Enderton] p. 72 | Theorem 4E | unisuc 4203 unisucg 4204 |
| [Enderton] p. 73 | Exercise 6 | unisuc 4203 unisucg 4204 |
| [Enderton] p. 73 | Exercise 5(a) | truni 3915 |
| [Enderton] p. 73 | Exercise 5(b) | trint 3916 |
| [Enderton] p. 79 | Theorem 4I(A1) | nna0 6166 |
| [Enderton] p. 79 | Theorem 4I(A2) | nnasuc 6168 onasuc 6158 |
| [Enderton] p. 79 | Definition of operation value | df-ov 5593 |
| [Enderton] p. 80 | Theorem 4J(A1) | nnm0 6167 |
| [Enderton] p. 80 | Theorem 4J(A2) | nnmsuc 6169 onmsuc 6165 |
| [Enderton] p. 81 | Theorem 4K(1) | nnaass 6177 |
| [Enderton] p. 81 | Theorem 4K(2) | nna0r 6170 nnacom 6176 |
| [Enderton] p. 81 | Theorem 4K(3) | nndi 6178 |
| [Enderton] p. 81 | Theorem 4K(4) | nnmass 6179 |
| [Enderton] p. 81 | Theorem 4K(5) | nnmcom 6181 |
| [Enderton] p. 82 | Exercise 16 | nnm0r 6171 nnmsucr 6180 |
| [Enderton] p. 88 | Exercise 23 | nnaordex 6215 |
| [Enderton] p. 129 | Definition | df-en 6387 |
| [Enderton] p. 133 | Exercise 1 | xpomen 10987 |
| [Enderton] p. 134 | Theorem (Pigeonhole Principle) | phpm 6510 |
| [Enderton] p. 136 | Corollary 6E | nneneq 6502 |
| [Enderton] p. 139 | Theorem 6H(c) | mapen 6491 |
| [Enderton] p. 144 | Corollary 6K | undif2ss 3340 |
| [Enderton] p. 145 | Figure 38 | ffoss 5232 |
| [Enderton] p. 145 | Definition | df-dom 6388 |
| [Enderton] p. 146 | Example 1 | domen 6397 domeng 6398 |
| [Enderton] p. 146 | Example 3 | nndomo 6509 |
| [Enderton] p. 149 | Theorem 6L(c) | xpdom1 6480 xpdom1g 6478 xpdom2g 6477 |
| [Enderton] p. 168 | Definition | df-po 4086 |
| [Enderton] p. 192 | Theorem 7M(a) | oneli 4218 |
| [Enderton] p. 192 | Theorem 7M(b) | ontr1 4179 |
| [Enderton] p. 192 | Theorem 7M(c) | onirri 4321 |
| [Enderton] p. 193 | Corollary 7N(b) | 0elon 4182 |
| [Enderton] p. 193 | Corollary 7N(c) | onsuci 4295 |
| [Enderton] p. 193 | Corollary 7N(d) | ssonunii 4268 |
| [Enderton] p. 194 | Remark | onprc 4330 |
| [Enderton] p. 194 | Exercise 16 | suc11 4336 |
| [Enderton] p. 197 | Definition | df-card 6710 |
| [Enderton] p. 200 | Exercise 25 | tfis 4360 |
| [Enderton] p. 206 | Theorem 7X(b) | en2lp 4332 |
| [Enderton] p. 207 | Exercise 34 | opthreg 4334 |
| [Enderton] p. 208 | Exercise 35 | suc11g 4335 |
| [Geuvers], p. 6 | Lemma 2.13 | mulap0r 7991 |
| [Geuvers], p. 6 | Lemma 2.15 | mulap0 8020 |
| [Geuvers], p. 9 | Lemma 2.35 | msqge0 7992 |
| [Geuvers], p. 9 | Definition 3.1(2) | ax-arch 7366 |
| [Geuvers], p. 10 | Lemma 3.9 | maxcom 10462 |
| [Geuvers], p. 10 | Lemma 3.10 | maxle1 10470 maxle2 10471 |
| [Geuvers], p. 10 | Lemma 3.11 | maxleast 10472 |
| [Geuvers], p. 10 | Lemma 3.12 | maxleb 10475 |
| [Geuvers], p. 11 | Definition 3.13 | dfabsmax 10476 |
| [Geuvers], p. 17 | Definition 6.1 | df-ap 7958 |
| [Gleason] p. 117 | Proposition 9-2.1 | df-enq 6808 enqer 6819 |
| [Gleason] p. 117 | Proposition 9-2.2 | df-1nqqs 6812 df-nqqs 6809 |
| [Gleason] p. 117 | Proposition 9-2.3 | df-plpq 6805 df-plqqs 6810 |
| [Gleason] p. 119 | Proposition 9-2.4 | df-mpq 6806 df-mqqs 6811 |
| [Gleason] p. 119 | Proposition 9-2.5 | df-rq 6813 |
| [Gleason] p. 119 | Proposition 9-2.6 | ltexnqq 6869 |
| [Gleason] p. 120 | Proposition 9-2.6(i) | halfnq 6872 ltbtwnnq 6877 ltbtwnnqq 6876 |
| [Gleason] p. 120 | Proposition 9-2.6(ii) | ltanqg 6861 |
| [Gleason] p. 120 | Proposition 9-2.6(iii) | ltmnqg 6862 |
| [Gleason] p. 123 | Proposition 9-3.5 | addclpr 6998 |
| [Gleason] p. 123 | Proposition 9-3.5(i) | addassprg 7040 |
| [Gleason] p. 123 | Proposition 9-3.5(ii) | addcomprg 7039 |
| [Gleason] p. 123 | Proposition 9-3.5(iii) | ltaddpr 7058 |
| [Gleason] p. 123 | Proposition 9-3.5(iv) | ltexpri 7074 |
| [Gleason] p. 123 | Proposition 9-3.5(v) | ltaprg 7080 ltaprlem 7079 |
| [Gleason] p. 123 | Proposition 9-3.5(vi) | addcanprg 7077 |
| [Gleason] p. 124 | Proposition 9-3.7 | mulclpr 7033 |
| [Gleason] p. 124 | Theorem 9-3.7(iv) | 1idpr 7053 |
| [Gleason] p. 124 | Proposition 9-3.7(i) | mulassprg 7042 |
| [Gleason] p. 124 | Proposition 9-3.7(ii) | mulcomprg 7041 |
| [Gleason] p. 124 | Proposition 9-3.7(iii) | distrprg 7049 |
| [Gleason] p. 124 | Proposition 9-3.7(v) | recexpr 7099 |
| [Gleason] p. 126 | Proposition 9-4.1 | df-enr 7174 enrer 7183 |
| [Gleason] p. 126 | Proposition 9-4.2 | df-0r 7179 df-1r 7180 df-nr 7175 |
| [Gleason] p. 126 | Proposition 9-4.3 | df-mr 7177 df-plr 7176 negexsr 7220 recexsrlem 7222 |
| [Gleason] p. 127 | Proposition 9-4.4 | df-ltr 7178 |
| [Gleason] p. 130 | Proposition 10-1.3 | creui 8313 creur 8312 cru 7978 |
| [Gleason] p. 130 | Definition 10-1.1(v) | ax-cnre 7358 axcnre 7318 |
| [Gleason] p. 132 | Definition 10-3.1 | crim 10118 crimd 10237 crimi 10197 crre 10117 crred 10236 crrei 10196 |
| [Gleason] p. 132 | Definition 10-3.2 | remim 10120 remimd 10202 |
| [Gleason] p. 133 | Definition 10.36 | absval2 10316 absval2d 10444 absval2i 10403 |
| [Gleason] p. 133 | Proposition 10-3.4(a) | cjadd 10144 cjaddd 10225 cjaddi 10192 |
| [Gleason] p. 133 | Proposition 10-3.4(c) | cjmul 10145 cjmuld 10226 cjmuli 10193 |
| [Gleason] p. 133 | Proposition 10-3.4(e) | cjcj 10143 cjcjd 10203 cjcji 10175 |
| [Gleason] p. 133 | Proposition 10-3.4(f) | cjre 10142 cjreb 10126 cjrebd 10206 cjrebi 10178 cjred 10231 rere 10125 rereb 10123 rerebd 10205 rerebi 10177 rered 10229 |
| [Gleason] p. 133 | Proposition 10-3.4(h) | addcj 10151 addcjd 10217 addcji 10187 |
| [Gleason] p. 133 | Proposition 10-3.7(a) | absval 10260 |
| [Gleason] p. 133 | Proposition 10-3.7(b) | abscj 10311 abscjd 10449 abscji 10407 |
| [Gleason] p. 133 | Proposition 10-3.7(c) | abs00 10323 abs00d 10445 abs00i 10404 absne0d 10446 |
| [Gleason] p. 133 | Proposition 10-3.7(d) | releabs 10355 releabsd 10450 releabsi 10408 |
| [Gleason] p. 133 | Proposition 10-3.7(f) | absmul 10328 absmuld 10453 absmuli 10410 |
| [Gleason] p. 133 | Proposition 10-3.7(g) | sqabsadd 10314 sqabsaddi 10411 |
| [Gleason] p. 133 | Proposition 10-3.7(h) | abstri 10363 abstrid 10455 abstrii 10414 |
| [Gleason] p. 134 | Definition 10-4.1 | 0exp0e1 9796 df-iexp 9791 exp0 9795 expp1 9798 expp1d 9921 |
| [Gleason] p. 135 | Proposition 10-4.2(a) | expadd 9833 expaddd 9922 |
| [Gleason] p. 135 | Proposition 10-4.2(b) | expmul 9836 expmuld 9923 |
| [Gleason] p. 135 | Proposition 10-4.2(c) | mulexp 9830 mulexpd 9935 |
| [Gleason] p. 140 | Exercise 1 | znnen 10990 |
| [Gleason] p. 141 | Definition 11-2.1 | fzval 9320 |
| [Gleason] p. 168 | Proposition 12-2.1(a) | climadd 10537 |
| [Gleason] p. 168 | Proposition 12-2.1(b) | climsub 10539 |
| [Gleason] p. 168 | Proposition 12-2.1(c) | climmul 10538 |
| [Gleason] p. 171 | Corollary 12-2.2 | climmulc2 10542 |
| [Gleason] p. 172 | Corollary 12-2.5 | climrecl 10535 |
| [Gleason] p. 172 | Proposition 12-2.4(c) | climabs 10531 climcj 10532 climim 10534 climre 10533 |
| [Gleason] p. 173 | Definition 12-3.1 | df-ltxr 7429 df-xr 7428 ltxr 9140 |
| [Gleason] p. 180 | Theorem 12-5.3 | climcau 10557 |
| [Gleason] p. 217 | Lemma 13-4.1 | btwnzge0 9595 |
| [Gleason] p. 243 | Proposition 14-4.16 | addcn2 10522 mulcn2 10524 subcn2 10523 |
| [Gleason] p. 295 | Remark | bcval3 9993 bcval4 9994 |
| [Gleason] p. 295 | Equation 2 | bcpasc 10008 |
| [Gleason] p. 295 | Definition of binomial coefficient | bcval 9991 df-bc 9990 |
| [Gleason] p. 296 | Remark | bcn0 9997 bcnn 9999 |
| [Hamilton] p. 31 | Example 2.7(a) | idALT 20 |
| [Hamilton] p. 73 | Rule 1 | ax-mp 7 |
| [Hamilton] p. 74 | Rule 2 | ax-gen 1379 |
| [Heyting] p. 127 | Axiom #1 | ax1hfs 11228 |
| [Hitchcock] p. 5 | Rule A3 | mptnan 1355 |
| [Hitchcock] p. 5 | Rule A4 | mptxor 1356 |
| [Hitchcock] p. 5 | Rule A5 | mtpxor 1358 |
| [HoTT], p. | Theorem 7.2.6 | nndceq 6191 |
| [HoTT], p. | Section 11.2.1 | df-iltp 6931 df-imp 6930 df-iplp 6929 df-reap 7951 |
| [HoTT], p. | Theorem 11.2.12 | cauappcvgpr 7123 |
| [HoTT], p. | Corollary 11.4.3 | conventions 10991 |
| [HoTT], p. | Corollary 11.2.13 | axcaucvg 7337 caucvgpr 7143 caucvgprpr 7173 caucvgsr 7249 |
| [HoTT], p. | Definition 11.2.1 | df-inp 6927 |
| [HoTT], p. | Proposition 11.2.3 | df-iso 4087 ltpopr 7056 ltsopr 7057 |
| [HoTT], p. | Definition 11.2.7(v) | apsym 7982 reapcotr 7974 reapirr 7953 |
| [HoTT], p. | Definition 11.2.7(vi) | 0lt1 7512 gt0add 7949 leadd1 7810 lelttr 7475 lemul1a 8212 lenlt 7463 ltadd1 7809 ltletr 7476 ltmul1 7968 reaplt 7964 |
| [Jech] p. 4 | Definition of class | cv 1284 cvjust 2078 |
| [Jech] p. 78 | Note | opthprc 4446 |
| [KalishMontague] p. 81 | Note 1 | ax-i9 1464 |
| [Kreyszig] p. 12 | Equation 5 | muleqadd 8034 |
| [Kunen] p. 10 | Axiom 0 | a9e 1627 |
| [Kunen] p. 12 | Axiom 6 | zfrep6 3921 |
| [Kunen] p. 24 | Definition 10.24 | mapval 6346 mapvalg 6344 |
| [Kunen] p. 31 | Definition 10.24 | mapex 6340 |
| [KuratowskiMostowski] p. 109 | Section. Eq. 14 | iuniin 3714 |
| [Levy] p. 338 | Axiom | df-clab 2070 df-clel 2079 df-cleq 2076 |
| [Lopez-Astorga] p. 12 | Rule 1 | mptnan 1355 |
| [Lopez-Astorga] p. 12 | Rule 2 | mptxor 1356 |
| [Lopez-Astorga] p. 12 | Rule 3 | mtpxor 1358 |
| [Margaris] p. 40 | Rule C | exlimiv 1530 |
| [Margaris] p. 49 | Axiom A1 | ax-1 5 |
| [Margaris] p. 49 | Axiom A2 | ax-2 6 |
| [Margaris] p. 49 | Axiom A3 | condc 783 |
| [Margaris] p. 49 | Definition | dfbi2 380 dfordc 825 exalim 1432 |
| [Margaris] p. 51 | Theorem 1 | idALT 20 |
| [Margaris] p. 56 | Theorem 3 | syld 44 |
| [Margaris] p. 60 | Theorem 8 | mth8 612 |
| [Margaris] p. 89 | Theorem 19.2 | 19.2 1570 r19.2m 3350 |
| [Margaris] p. 89 | Theorem 19.3 | 19.3 1487 19.3h 1486 rr19.3v 2743 |
| [Margaris] p. 89 | Theorem 19.5 | alcom 1408 |
| [Margaris] p. 89 | Theorem 19.6 | alexdc 1551 alexim 1577 |
| [Margaris] p. 89 | Theorem 19.7 | alnex 1429 |
| [Margaris] p. 89 | Theorem 19.8 | 19.8a 1523 spsbe 1765 |
| [Margaris] p. 89 | Theorem 19.9 | 19.9 1576 19.9h 1575 19.9v 1794 exlimd 1529 |
| [Margaris] p. 89 | Theorem 19.11 | excom 1595 excomim 1594 |
| [Margaris] p. 89 | Theorem 19.12 | 19.12 1596 r19.12 2472 |
| [Margaris] p. 90 | Theorem 19.14 | exnalim 1578 |
| [Margaris] p. 90 | Theorem 19.15 | albi 1398 ralbi 2495 |
| [Margaris] p. 90 | Theorem 19.16 | 19.16 1488 |
| [Margaris] p. 90 | Theorem 19.17 | 19.17 1489 |
| [Margaris] p. 90 | Theorem 19.18 | exbi 1536 rexbi 2496 |
| [Margaris] p. 90 | Theorem 19.19 | 19.19 1597 |
| [Margaris] p. 90 | Theorem 19.20 | alim 1387 alimd 1455 alimdh 1397 alimdv 1802 ralimdaa 2434 ralimdv 2436 ralimdva 2435 sbcimdv 2890 |
| [Margaris] p. 90 | Theorem 19.21 | 19.21-2 1598 19.21 1516 19.21bi 1491 19.21h 1490 19.21ht 1514 19.21t 1515 19.21v 1796 alrimd 1542 alrimdd 1541 alrimdh 1409 alrimdv 1799 alrimi 1456 alrimih 1399 alrimiv 1797 alrimivv 1798 r19.21 2443 r19.21be 2458 r19.21bi 2455 r19.21t 2442 r19.21v 2444 ralrimd 2445 ralrimdv 2446 ralrimdva 2447 ralrimdvv 2451 ralrimdvva 2452 ralrimi 2438 ralrimiv 2439 ralrimiva 2440 ralrimivv 2448 ralrimivva 2449 ralrimivvva 2450 ralrimivw 2441 rexlimi 2476 |
| [Margaris] p. 90 | Theorem 19.22 | 2alimdv 1804 2eximdv 1805 exim 1531 eximd 1544 eximdh 1543 eximdv 1803 rexim 2461 reximdai 2465 reximddv 2470 reximddv2 2471 reximdv 2468 reximdv2 2466 reximdva 2469 reximdvai 2467 reximi2 2463 |
| [Margaris] p. 90 | Theorem 19.23 | 19.23 1609 19.23bi 1524 19.23h 1428 19.23ht 1427 19.23t 1608 19.23v 1806 19.23vv 1807 exlimd2 1527 exlimdh 1528 exlimdv 1742 exlimdvv 1820 exlimi 1526 exlimih 1525 exlimiv 1530 exlimivv 1819 r19.23 2474 r19.23v 2475 rexlimd 2480 rexlimdv 2482 rexlimdv3a 2485 rexlimdva 2483 rexlimdvaa 2484 rexlimdvv 2489 rexlimdvva 2490 rexlimdvw 2486 rexlimiv 2477 rexlimiva 2478 rexlimivv 2488 |
| [Margaris] p. 90 | Theorem 19.24 | i19.24 1571 |
| [Margaris] p. 90 | Theorem 19.25 | 19.25 1558 |
| [Margaris] p. 90 | Theorem 19.26 | 19.26-2 1412 19.26-3an 1413 19.26 1411 r19.26-2 2492 r19.26-3 2493 r19.26 2491 r19.26m 2494 |
| [Margaris] p. 90 | Theorem 19.27 | 19.27 1494 19.27h 1493 19.27v 1822 r19.27av 2498 r19.27m 3358 r19.27mv 3359 |
| [Margaris] p. 90 | Theorem 19.28 | 19.28 1496 19.28h 1495 19.28v 1823 r19.28av 2499 r19.28m 3352 r19.28mv 3355 rr19.28v 2744 |
| [Margaris] p. 90 | Theorem 19.29 | 19.29 1552 19.29r 1553 19.29r2 1554 19.29x 1555 r19.29 2500 r19.29d2r 2505 r19.29r 2501 |
| [Margaris] p. 90 | Theorem 19.30 | 19.30dc 1559 |
| [Margaris] p. 90 | Theorem 19.31 | 19.31r 1612 |
| [Margaris] p. 90 | Theorem 19.32 | 19.32dc 1610 19.32r 1611 r19.32r 2507 r19.32vdc 2509 r19.32vr 2508 |
| [Margaris] p. 90 | Theorem 19.33 | 19.33 1414 19.33b2 1561 19.33bdc 1562 |
| [Margaris] p. 90 | Theorem 19.34 | 19.34 1615 |
| [Margaris] p. 90 | Theorem 19.35 | 19.35-1 1556 19.35i 1557 |
| [Margaris] p. 90 | Theorem 19.36 | 19.36-1 1604 19.36aiv 1824 19.36i 1603 r19.36av 2511 |
| [Margaris] p. 90 | Theorem 19.37 | 19.37-1 1605 19.37aiv 1606 r19.37 2512 r19.37av 2513 |
| [Margaris] p. 90 | Theorem 19.38 | 19.38 1607 |
| [Margaris] p. 90 | Theorem 19.39 | i19.39 1572 |
| [Margaris] p. 90 | Theorem 19.40 | 19.40-2 1564 19.40 1563 r19.40 2514 |
| [Margaris] p. 90 | Theorem 19.41 | 19.41 1617 19.41h 1616 19.41v 1825 19.41vv 1826 19.41vvv 1827 19.41vvvv 1828 r19.41 2515 r19.41v 2516 |
| [Margaris] p. 90 | Theorem 19.42 | 19.42 1619 19.42h 1618 19.42v 1829 19.42vv 1831 19.42vvv 1832 19.42vvvv 1833 r19.42v 2517 |
| [Margaris] p. 90 | Theorem 19.43 | 19.43 1560 r19.43 2518 |
| [Margaris] p. 90 | Theorem 19.44 | 19.44 1613 r19.44av 2519 r19.44mv 3357 |
| [Margaris] p. 90 | Theorem 19.45 | 19.45 1614 r19.45av 2520 r19.45mv 3356 |
| [Margaris] p. 110 | Exercise 2(b) | eu1 1968 |
| [Megill] p. 444 | Axiom C5 | ax-17 1460 |
| [Megill] p. 445 | Lemma L12 | alequcom 1449 ax-10 1437 |
| [Megill] p. 446 | Lemma L17 | equtrr 1638 |
| [Megill] p. 446 | Lemma L19 | hbnae 1651 |
| [Megill] p. 447 | Remark 9.1 | df-sb 1688 sbid 1699 |
| [Megill] p. 448 | Scheme C5' | ax-4 1441 |
| [Megill] p. 448 | Scheme C6' | ax-7 1378 |
| [Megill] p. 448 | Scheme C8' | ax-8 1436 |
| [Megill] p. 448 | Scheme C9' | ax-i12 1439 |
| [Megill] p. 448 | Scheme C11' | ax-10o 1646 |
| [Megill] p. 448 | Scheme C12' | ax-13 1445 |
| [Megill] p. 448 | Scheme C13' | ax-14 1446 |
| [Megill] p. 448 | Scheme C15' | ax-11o 1746 |
| [Megill] p. 448 | Scheme C16' | ax-16 1737 |
| [Megill] p. 448 | Theorem 9.4 | dral1 1660 dral2 1661 drex1 1721 drex2 1662 drsb1 1722 drsb2 1764 |
| [Megill] p. 449 | Theorem 9.7 | sbcom2 1906 sbequ 1763 sbid2v 1915 |
| [Megill] p. 450 | Example in Appendix | hba1 1474 |
| [Mendelson] p. 36 | Lemma 1.8 | idALT 20 |
| [Mendelson] p. 69 | Axiom 4 | rspsbc 2907 rspsbca 2908 stdpc4 1700 |
| [Mendelson] p. 69 | Axiom 5 | ra5 2913 stdpc5 1517 |
| [Mendelson] p. 81 | Rule C | exlimiv 1530 |
| [Mendelson] p. 95 | Axiom 6 | stdpc6 1632 |
| [Mendelson] p. 95 | Axiom 7 | stdpc7 1695 |
| [Mendelson] p. 231 | Exercise 4.10(k) | inv1 3301 |
| [Mendelson] p. 231 | Exercise 4.10(l) | unv 3302 |
| [Mendelson] p. 231 | Exercise 4.10(n) | inssun 3222 |
| [Mendelson] p. 231 | Exercise 4.10(o) | df-nul 3270 |
| [Mendelson] p. 231 | Exercise 4.10(q) | inssddif 3223 |
| [Mendelson] p. 231 | Exercise 4.10(s) | ddifnel 3115 |
| [Mendelson] p. 231 | Definition of union | unssin 3221 |
| [Mendelson] p. 235 | Exercise 4.12(c) | univ 4260 |
| [Mendelson] p. 235 | Exercise 4.12(d) | pwv 3626 |
| [Mendelson] p. 235 | Exercise 4.12(j) | pwin 4072 |
| [Mendelson] p. 235 | Exercise 4.12(k) | pwunss 4073 |
| [Mendelson] p. 235 | Exercise 4.12(l) | pwssunim 4074 |
| [Mendelson] p. 235 | Exercise 4.12(n) | uniin 3647 |
| [Mendelson] p. 235 | Exercise 4.12(p) | reli 4522 |
| [Mendelson] p. 235 | Exercise 4.12(t) | relssdmrn 4904 |
| [Mendelson] p. 246 | Definition of successor | df-suc 4161 |
| [Mendelson] p. 254 | Proposition 4.22(b) | xpen 6490 |
| [Mendelson] p. 254 | Proposition 4.22(c) | xpsnen 6466 xpsneng 6467 |
| [Mendelson] p. 254 | Proposition 4.22(d) | xpcomen 6472 xpcomeng 6473 |
| [Mendelson] p. 254 | Proposition 4.22(e) | xpassen 6475 |
| [Mendelson] p. 255 | Exercise 4.39 | endisj 6469 |
| [Mendelson] p. 255 | Exercise 4.41 | mapprc 6338 |
| [Mendelson] p. 255 | Exercise 4.43 | mapsnen 6457 |
| [Mendelson] p. 255 | Exercise 4.47 | xpmapen 6495 |
| [Mendelson] p. 255 | Exercise 4.42(a) | map0e 6372 |
| [Mendelson] p. 255 | Exercise 4.42(b) | map1 6458 |
| [Mendelson] p. 266 | Proposition 4.34(a) | oa1suc 6159 |
| [Monk1] p. 26 | Theorem 2.8(vii) | ssin 3206 |
| [Monk1] p. 33 | Theorem 3.2(i) | ssrel 4483 |
| [Monk1] p. 33 | Theorem 3.2(ii) | eqrel 4484 |
| [Monk1] p. 34 | Definition 3.3 | df-opab 3866 |
| [Monk1] p. 36 | Theorem 3.7(i) | coi1 4899 coi2 4900 |
| [Monk1] p. 36 | Theorem 3.8(v) | dm0 4607 rn0 4646 |
| [Monk1] p. 36 | Theorem 3.7(ii) | cnvi 4789 |
| [Monk1] p. 37 | Theorem 3.13(i) | relxp 4504 |
| [Monk1] p. 37 | Theorem 3.13(x) | dmxpm 4613 rnxpm 4813 |
| [Monk1] p. 37 | Theorem 3.13(ii) | 0xp 4475 xp0 4804 |
| [Monk1] p. 38 | Theorem 3.16(ii) | ima0 4745 |
| [Monk1] p. 38 | Theorem 3.16(viii) | imai 4742 |
| [Monk1] p. 39 | Theorem 3.17 | imaex 4741 imaexg 4740 |
| [Monk1] p. 39 | Theorem 3.16(xi) | imassrn 4739 |
| [Monk1] p. 41 | Theorem 4.3(i) | fnopfv 5373 funfvop 5355 |
| [Monk1] p. 42 | Theorem 4.3(ii) | funopfvb 5292 |
| [Monk1] p. 42 | Theorem 4.4(iii) | fvelima 5300 |
| [Monk1] p. 43 | Theorem 4.6 | funun 5010 |
| [Monk1] p. 43 | Theorem 4.8(iv) | dff13 5486 dff13f 5488 |
| [Monk1] p. 46 | Theorem 4.15(v) | funex 5459 funrnex 5819 |
| [Monk1] p. 50 | Definition 5.4 | fniunfv 5480 |
| [Monk1] p. 52 | Theorem 5.12(ii) | op2ndb 4867 |
| [Monk1] p. 52 | Theorem 5.11(viii) | ssint 3678 |
| [Monk1] p. 52 | Definition 5.13 (i) | 1stval2 5860 df-1st 5845 |
| [Monk1] p. 52 | Definition 5.13 (ii) | 2ndval2 5861 df-2nd 5846 |
| [Monk2] p. 105 | Axiom C4 | ax-5 1377 |
| [Monk2] p. 105 | Axiom C7 | ax-8 1436 |
| [Monk2] p. 105 | Axiom C8 | ax-11 1438 ax-11o 1746 |
| [Monk2] p. 105 | Axiom (C8) | ax11v 1750 |
| [Monk2] p. 109 | Lemma 12 | ax-7 1378 |
| [Monk2] p. 109 | Lemma 15 | equvin 1786 equvini 1683 eqvinop 4033 |
| [Monk2] p. 113 | Axiom C5-1 | ax-17 1460 |
| [Monk2] p. 113 | Axiom C5-2 | ax6b 1582 |
| [Monk2] p. 113 | Axiom C5-3 | ax-7 1378 |
| [Monk2] p. 114 | Lemma 22 | hba1 1474 |
| [Monk2] p. 114 | Lemma 23 | hbia1 1485 nfia1 1513 |
| [Monk2] p. 114 | Lemma 24 | hba2 1484 nfa2 1512 |
| [Moschovakis] p. 2 | Chapter 2 | df-stab 774 dftest 856 |
| [Pierik], p. 8 | Section 2.2.1 | dfrex2fin 6545 |
| [Pierik], p. 10 | Section 2.3 | dfdif3 3094 |
| [Pierik], p. 14 | Definition 3.1 | df-omni 6695 exmidomniim 6701 finomni 6700 |
| [Pierik], p. 15 | Section 3.1 | df-nninf 8630 |
| [PradicBrown2021], p. 2 | Remark | exmidpw 6550 |
| [PradicBrown2021], p. 2 | Proposition 1.1 | exmidfodomrlemim 6729 |
| [PradicBrown2021], p. 2 | Proposition 1.2 | exmidfodomrlemr 6730 exmidfodomrlemrALT 6731 |
| [PradicBrown2021], p. 4 | Lemma 3.2 | fodjuomni 6708 |
| [Quine] p. 16 | Definition 2.1 | df-clab 2070 rabid 2535 |
| [Quine] p. 17 | Definition 2.1'' | dfsb7 1910 |
| [Quine] p. 18 | Definition 2.7 | df-cleq 2076 |
| [Quine] p. 19 | Definition 2.9 | df-v 2614 |
| [Quine] p. 34 | Theorem 5.1 | abeq2 2191 |
| [Quine] p. 35 | Theorem 5.2 | abid2 2203 abid2f 2247 |
| [Quine] p. 40 | Theorem 6.1 | sb5 1810 |
| [Quine] p. 40 | Theorem 6.2 | sb56 1808 sb6 1809 |
| [Quine] p. 41 | Theorem 6.3 | df-clel 2079 |
| [Quine] p. 41 | Theorem 6.4 | eqid 2083 |
| [Quine] p. 41 | Theorem 6.5 | eqcom 2085 |
| [Quine] p. 42 | Theorem 6.6 | df-sbc 2827 |
| [Quine] p. 42 | Theorem 6.7 | dfsbcq 2828 dfsbcq2 2829 |
| [Quine] p. 43 | Theorem 6.8 | vex 2615 |
| [Quine] p. 43 | Theorem 6.9 | isset 2616 |
| [Quine] p. 44 | Theorem 7.3 | spcgf 2691 spcgv 2696 spcimgf 2689 |
| [Quine] p. 44 | Theorem 6.11 | spsbc 2837 spsbcd 2838 |
| [Quine] p. 44 | Theorem 6.12 | elex 2621 |
| [Quine] p. 44 | Theorem 6.13 | elab 2748 elabg 2749 elabgf 2746 |
| [Quine] p. 44 | Theorem 6.14 | noel 3273 |
| [Quine] p. 48 | Theorem 7.2 | snprc 3481 |
| [Quine] p. 48 | Definition 7.1 | df-pr 3429 df-sn 3428 |
| [Quine] p. 49 | Theorem 7.4 | snss 3540 snssg 3547 |
| [Quine] p. 49 | Theorem 7.5 | prss 3567 prssg 3568 |
| [Quine] p. 49 | Theorem 7.6 | prid1 3522 prid1g 3520 prid2 3523 prid2g 3521 snid 3449 snidg 3447 |
| [Quine] p. 51 | Theorem 7.12 | snexg 3982 snexprc 3984 |
| [Quine] p. 51 | Theorem 7.13 | prexg 4001 |
| [Quine] p. 53 | Theorem 8.2 | unisn 3643 unisng 3644 |
| [Quine] p. 53 | Theorem 8.3 | uniun 3646 |
| [Quine] p. 54 | Theorem 8.6 | elssuni 3655 |
| [Quine] p. 54 | Theorem 8.7 | uni0 3654 |
| [Quine] p. 56 | Theorem 8.17 | uniabio 4943 |
| [Quine] p. 56 | Definition 8.18 | dfiota2 4934 |
| [Quine] p. 57 | Theorem 8.19 | iotaval 4944 |
| [Quine] p. 57 | Theorem 8.22 | iotanul 4948 |
| [Quine] p. 58 | Theorem 8.23 | euiotaex 4949 |
| [Quine] p. 58 | Definition 9.1 | df-op 3431 |
| [Quine] p. 61 | Theorem 9.5 | opabid 4047 opelopab 4061 opelopaba 4056 opelopabaf 4063 opelopabf 4064 opelopabg 4058 opelopabga 4053 oprabid 5615 |
| [Quine] p. 64 | Definition 9.11 | df-xp 4406 |
| [Quine] p. 64 | Definition 9.12 | df-cnv 4408 |
| [Quine] p. 64 | Definition 9.15 | df-id 4083 |
| [Quine] p. 65 | Theorem 10.3 | fun0 5024 |
| [Quine] p. 65 | Theorem 10.4 | funi 4998 |
| [Quine] p. 65 | Theorem 10.5 | funsn 5014 funsng 5012 |
| [Quine] p. 65 | Definition 10.1 | df-fun 4970 |
| [Quine] p. 65 | Definition 10.2 | args 4755 dffv4g 5249 |
| [Quine] p. 68 | Definition 10.11 | df-fv 4976 fv2 5247 |
| [Quine] p. 124 | Theorem 17.3 | nn0opth2 9966 nn0opth2d 9965 nn0opthd 9964 |
| [Quine] p. 284 | Axiom 39(vi) | funimaex 5051 funimaexg 5050 |
| [Sanford] p. 39 | Rule 3 | mtpxor 1358 |
| [Sanford] p. 39 | Rule 4 | mptxor 1356 |
| [Sanford] p. 40 | Rule 1 | mptnan 1355 |
| [Schechter] p. 51 | Definition of antisymmetry | intasym 4770 |
| [Schechter] p. 51 | Definition of irreflexivity | intirr 4772 |
| [Schechter] p. 51 | Definition of symmetry | cnvsym 4769 |
| [Schechter] p. 51 | Definition of transitivity | cotr 4767 |
| [Stoll] p. 13 | Definition of symmetric difference | symdif1 3247 |
| [Stoll] p. 16 | Exercise 4.4 | 0dif 3336 dif0 3335 |
| [Stoll] p. 16 | Exercise 4.8 | difdifdirss 3348 |
| [Stoll] p. 19 | Theorem 5.2(13) | undm 3240 |
| [Stoll] p. 19 | Theorem 5.2(13') | indmss 3241 |
| [Stoll] p. 20 | Remark | invdif 3224 |
| [Stoll] p. 25 | Definition of ordered triple | df-ot 3432 |
| [Stoll] p. 43 | Definition | uniiun 3757 |
| [Stoll] p. 44 | Definition | intiin 3758 |
| [Stoll] p. 45 | Definition | df-iin 3707 |
| [Stoll] p. 45 | Definition indexed union | df-iun 3706 |
| [Stoll] p. 176 | Theorem 3.4(27) | imandc 820 |
| [Stoll] p. 262 | Example 4.1 | symdif1 3247 |
| [Suppes] p. 22 | Theorem 2 | eq0 3284 |
| [Suppes] p. 22 | Theorem 4 | eqss 3025 eqssd 3027 eqssi 3026 |
| [Suppes] p. 23 | Theorem 5 | ss0 3305 ss0b 3304 |
| [Suppes] p. 23 | Theorem 6 | sstr 3018 |
| [Suppes] p. 25 | Theorem 12 | elin 3167 elun 3125 |
| [Suppes] p. 26 | Theorem 15 | inidm 3193 |
| [Suppes] p. 26 | Theorem 16 | in0 3300 |
| [Suppes] p. 27 | Theorem 23 | unidm 3127 |
| [Suppes] p. 27 | Theorem 24 | un0 3299 |
| [Suppes] p. 27 | Theorem 25 | ssun1 3147 |
| [Suppes] p. 27 | Theorem 26 | ssequn1 3154 |
| [Suppes] p. 27 | Theorem 27 | unss 3158 |
| [Suppes] p. 27 | Theorem 28 | indir 3231 |
| [Suppes] p. 27 | Theorem 29 | undir 3232 |
| [Suppes] p. 28 | Theorem 32 | difid 3333 difidALT 3334 |
| [Suppes] p. 29 | Theorem 33 | difin 3219 |
| [Suppes] p. 29 | Theorem 34 | indif 3225 |
| [Suppes] p. 29 | Theorem 35 | undif1ss 3339 |
| [Suppes] p. 29 | Theorem 36 | difun2 3343 |
| [Suppes] p. 29 | Theorem 37 | difin0 3338 |
| [Suppes] p. 29 | Theorem 38 | disjdif 3337 |
| [Suppes] p. 29 | Theorem 39 | difundi 3234 |
| [Suppes] p. 29 | Theorem 40 | difindiss 3236 |
| [Suppes] p. 30 | Theorem 41 | nalset 3934 |
| [Suppes] p. 39 | Theorem 61 | uniss 3648 |
| [Suppes] p. 39 | Theorem 65 | uniop 4045 |
| [Suppes] p. 41 | Theorem 70 | intsn 3697 |
| [Suppes] p. 42 | Theorem 71 | intpr 3694 intprg 3695 |
| [Suppes] p. 42 | Theorem 73 | op1stb 4262 op1stbg 4263 |
| [Suppes] p. 42 | Theorem 78 | intun 3693 |
| [Suppes] p. 44 | Definition 15(a) | dfiun2 3738 dfiun2g 3736 |
| [Suppes] p. 44 | Definition 15(b) | dfiin2 3739 |
| [Suppes] p. 47 | Theorem 86 | elpw 3412 elpw2 3958 elpw2g 3957 elpwg 3414 |
| [Suppes] p. 47 | Theorem 87 | pwid 3420 |
| [Suppes] p. 47 | Theorem 89 | pw0 3558 |
| [Suppes] p. 48 | Theorem 90 | pwpw0ss 3622 |
| [Suppes] p. 52 | Theorem 101 | xpss12 4502 |
| [Suppes] p. 52 | Theorem 102 | xpindi 4528 xpindir 4529 |
| [Suppes] p. 52 | Theorem 103 | xpundi 4451 xpundir 4452 |
| [Suppes] p. 54 | Theorem 105 | elirrv 4326 |
| [Suppes] p. 58 | Theorem 2 | relss 4482 |
| [Suppes] p. 59 | Theorem 4 | eldm 4590 eldm2 4591 eldm2g 4589 eldmg 4588 |
| [Suppes] p. 59 | Definition 3 | df-dm 4410 |
| [Suppes] p. 60 | Theorem 6 | dmin 4601 |
| [Suppes] p. 60 | Theorem 8 | rnun 4793 |
| [Suppes] p. 60 | Theorem 9 | rnin 4794 |
| [Suppes] p. 60 | Definition 4 | dfrn2 4581 |
| [Suppes] p. 61 | Theorem 11 | brcnv 4576 brcnvg 4574 |
| [Suppes] p. 62 | Equation 5 | elcnv 4570 elcnv2 4571 |
| [Suppes] p. 62 | Theorem 12 | relcnv 4764 |
| [Suppes] p. 62 | Theorem 15 | cnvin 4792 |
| [Suppes] p. 62 | Theorem 16 | cnvun 4790 |
| [Suppes] p. 63 | Theorem 20 | co02 4897 |
| [Suppes] p. 63 | Theorem 21 | dmcoss 4659 |
| [Suppes] p. 63 | Definition 7 | df-co 4409 |
| [Suppes] p. 64 | Theorem 26 | cnvco 4578 |
| [Suppes] p. 64 | Theorem 27 | coass 4902 |
| [Suppes] p. 65 | Theorem 31 | resundi 4683 |
| [Suppes] p. 65 | Theorem 34 | elima 4733 elima2 4734 elima3 4735 elimag 4732 |
| [Suppes] p. 65 | Theorem 35 | imaundi 4797 |
| [Suppes] p. 66 | Theorem 40 | dminss 4799 |
| [Suppes] p. 66 | Theorem 41 | imainss 4800 |
| [Suppes] p. 67 | Exercise 11 | cnvxp 4803 |
| [Suppes] p. 81 | Definition 34 | dfec2 6224 |
| [Suppes] p. 82 | Theorem 72 | elec 6260 elecg 6259 |
| [Suppes] p. 82 | Theorem 73 | erth 6265 erth2 6266 |
| [Suppes] p. 89 | Theorem 96 | map0b 6373 |
| [Suppes] p. 89 | Theorem 97 | map0 6375 map0g 6374 |
| [Suppes] p. 89 | Theorem 98 | mapsn 6376 |
| [Suppes] p. 89 | Theorem 99 | mapss 6377 |
| [Suppes] p. 92 | Theorem 1 | enref 6411 enrefg 6410 |
| [Suppes] p. 92 | Theorem 2 | ensym 6427 ensymb 6426 ensymi 6428 |
| [Suppes] p. 92 | Theorem 3 | entr 6430 |
| [Suppes] p. 92 | Theorem 4 | unen 6462 |
| [Suppes] p. 94 | Theorem 15 | endom 6409 |
| [Suppes] p. 94 | Theorem 16 | ssdomg 6424 |
| [Suppes] p. 94 | Theorem 17 | domtr 6431 |
| [Suppes] p. 98 | Exercise 4 | fundmen 6452 fundmeng 6453 |
| [Suppes] p. 98 | Exercise 6 | xpdom3m 6479 |
| [Suppes] p. 130 | Definition 3 | df-tr 3902 |
| [Suppes] p. 132 | Theorem 9 | ssonuni 4267 |
| [Suppes] p. 134 | Definition 6 | df-suc 4161 |
| [Suppes] p. 136 | Theorem Schema 22 | findes 4380 finds 4377 finds1 4379 finds2 4378 |
| [Suppes] p. 162 | Definition 5 | df-ltnqqs 6814 df-ltpq 6807 |
| [Suppes] p. 228 | Theorem Schema 61 | onintss 4180 |
| [TakeutiZaring] p. 8 | Axiom 1 | ax-ext 2065 |
| [TakeutiZaring] p. 13 | Definition 4.5 | df-cleq 2076 |
| [TakeutiZaring] p. 13 | Proposition 4.6 | df-clel 2079 |
| [TakeutiZaring] p. 13 | Proposition 4.9 | cvjust 2078 |
| [TakeutiZaring] p. 13 | Proposition 4.7(3) | eqtr 2100 |
| [TakeutiZaring] p. 14 | Definition 4.16 | df-oprab 5594 |
| [TakeutiZaring] p. 14 | Proposition 4.14 | ru 2825 |
| [TakeutiZaring] p. 15 | Exercise 1 | elpr 3443 elpr2 3444 elprg 3442 |
| [TakeutiZaring] p. 15 | Exercise 2 | elsn 3438 elsn2 3452 elsn2g 3451 elsng 3437 velsn 3439 |
| [TakeutiZaring] p. 15 | Exercise 3 | elop 4021 |
| [TakeutiZaring] p. 15 | Exercise 4 | sneq 3433 sneqr 3578 |
| [TakeutiZaring] p. 15 | Definition 5.1 | dfpr2 3441 dfsn2 3436 |
| [TakeutiZaring] p. 16 | Axiom 3 | uniex 4227 |
| [TakeutiZaring] p. 16 | Exercise 6 | opth 4027 |
| [TakeutiZaring] p. 16 | Exercise 8 | rext 4005 |
| [TakeutiZaring] p. 16 | Corollary 5.8 | unex 4229 unexg 4231 |
| [TakeutiZaring] p. 16 | Definition 5.3 | dftp2 3465 |
| [TakeutiZaring] p. 16 | Definition 5.5 | df-uni 3628 |
| [TakeutiZaring] p. 16 | Definition 5.6 | df-in 2990 df-un 2988 |
| [TakeutiZaring] p. 16 | Proposition 5.7 | unipr 3641 uniprg 3642 |
| [TakeutiZaring] p. 17 | Axiom 4 | pwex 3979 pwexg 3980 |
| [TakeutiZaring] p. 17 | Exercise 1 | eltp 3464 |
| [TakeutiZaring] p. 17 | Exercise 5 | elsuc 4196 elsucg 4194 sstr2 3017 |
| [TakeutiZaring] p. 17 | Exercise 6 | uncom 3128 |
| [TakeutiZaring] p. 17 | Exercise 7 | incom 3176 |
| [TakeutiZaring] p. 17 | Exercise 8 | unass 3141 |
| [TakeutiZaring] p. 17 | Exercise 9 | inass 3194 |
| [TakeutiZaring] p. 17 | Exercise 10 | indi 3229 |
| [TakeutiZaring] p. 17 | Exercise 11 | undi 3230 |
| [TakeutiZaring] p. 17 | Definition 5.9 | dfss2 2999 |
| [TakeutiZaring] p. 17 | Definition 5.10 | df-pw 3408 |
| [TakeutiZaring] p. 18 | Exercise 7 | unss2 3155 |
| [TakeutiZaring] p. 18 | Exercise 9 | df-ss 2997 sseqin2 3203 |
| [TakeutiZaring] p. 18 | Exercise 10 | ssid 3029 |
| [TakeutiZaring] p. 18 | Exercise 12 | inss1 3204 inss2 3205 |
| [TakeutiZaring] p. 18 | Exercise 13 | nssr 3068 |
| [TakeutiZaring] p. 18 | Exercise 15 | unieq 3636 |
| [TakeutiZaring] p. 18 | Exercise 18 | sspwb 4006 |
| [TakeutiZaring] p. 18 | Exercise 19 | pweqb 4013 |
| [TakeutiZaring] p. 20 | Definition | df-rab 2362 |
| [TakeutiZaring] p. 20 | Corollary 5.16 | 0ex 3931 |
| [TakeutiZaring] p. 20 | Definition 5.12 | df-dif 2986 |
| [TakeutiZaring] p. 20 | Definition 5.14 | dfnul2 3271 |
| [TakeutiZaring] p. 20 | Proposition 5.15 | difid 3333 difidALT 3334 |
| [TakeutiZaring] p. 20 | Proposition 5.17(1) | n0rf 3278 |
| [TakeutiZaring] p. 21 | Theorem 5.22 | setind 4317 |
| [TakeutiZaring] p. 21 | Definition 5.20 | df-v 2614 |
| [TakeutiZaring] p. 21 | Proposition 5.21 | vprc 3935 |
| [TakeutiZaring] p. 22 | Exercise 1 | 0ss 3303 |
| [TakeutiZaring] p. 22 | Exercise 3 | ssex 3941 ssexg 3943 |
| [TakeutiZaring] p. 22 | Exercise 4 | inex1 3938 |
| [TakeutiZaring] p. 22 | Exercise 5 | ruv 4328 |
| [TakeutiZaring] p. 22 | Exercise 6 | elirr 4319 |
| [TakeutiZaring] p. 22 | Exercise 7 | ssdif0im 3329 |
| [TakeutiZaring] p. 22 | Exercise 11 | difdif 3109 |
| [TakeutiZaring] p. 22 | Exercise 13 | undif3ss 3243 |
| [TakeutiZaring] p. 22 | Exercise 14 | difss 3110 |
| [TakeutiZaring] p. 22 | Exercise 15 | sscon 3118 |
| [TakeutiZaring] p. 22 | Definition 4.15(3) | df-ral 2358 |
| [TakeutiZaring] p. 22 | Definition 4.15(4) | df-rex 2359 |
| [TakeutiZaring] p. 23 | Proposition 6.2 | xpex 4510 xpexg 4509 xpexgALT 5838 |
| [TakeutiZaring] p. 23 | Definition 6.4(1) | df-rel 4407 |
| [TakeutiZaring] p. 23 | Definition 6.4(2) | fun2cnv 5030 |
| [TakeutiZaring] p. 24 | Definition 6.4(3) | f1cnvcnv 5174 fun11 5033 |
| [TakeutiZaring] p. 24 | Definition 6.4(4) | dffun4 4979 svrelfun 5031 |
| [TakeutiZaring] p. 24 | Definition 6.5(1) | dfdm3 4580 |
| [TakeutiZaring] p. 24 | Definition 6.5(2) | dfrn3 4582 |
| [TakeutiZaring] p. 24 | Definition 6.6(1) | df-res 4412 |
| [TakeutiZaring] p. 24 | Definition 6.6(2) | df-ima 4413 |
| [TakeutiZaring] p. 24 | Definition 6.6(3) | df-co 4409 |
| [TakeutiZaring] p. 25 | Exercise 2 | cnvcnvss 4838 dfrel2 4834 |
| [TakeutiZaring] p. 25 | Exercise 3 | xpss 4503 |
| [TakeutiZaring] p. 25 | Exercise 5 | relun 4511 |
| [TakeutiZaring] p. 25 | Exercise 6 | reluni 4517 |
| [TakeutiZaring] p. 25 | Exercise 9 | inxp 4527 |
| [TakeutiZaring] p. 25 | Exercise 12 | relres 4697 |
| [TakeutiZaring] p. 25 | Exercise 13 | opelres 4675 opelresg 4677 |
| [TakeutiZaring] p. 25 | Exercise 14 | dmres 4690 |
| [TakeutiZaring] p. 25 | Exercise 15 | resss 4693 |
| [TakeutiZaring] p. 25 | Exercise 17 | resabs1 4698 |
| [TakeutiZaring] p. 25 | Exercise 18 | funres 5007 |
| [TakeutiZaring] p. 25 | Exercise 24 | relco 4882 |
| [TakeutiZaring] p. 25 | Exercise 29 | funco 5006 |
| [TakeutiZaring] p. 25 | Exercise 30 | f1co 5175 |
| [TakeutiZaring] p. 26 | Definition 6.10 | eu2 1987 |
| [TakeutiZaring] p. 26 | Definition 6.11 | df-fv 4976 fv3 5272 |
| [TakeutiZaring] p. 26 | Corollary 6.8(1) | cnvex 4922 cnvexg 4921 |
| [TakeutiZaring] p. 26 | Corollary 6.8(2) | dmex 4656 dmexg 4654 |
| [TakeutiZaring] p. 26 | Corollary 6.8(3) | rnex 4657 rnexg 4655 |
| [TakeutiZaring] p. 27 | Corollary 6.13 | funfvex 5266 |
| [TakeutiZaring] p. 27 | Theorem 6.12(1) | tz6.12-1 5275 tz6.12 5276 tz6.12c 5278 |
| [TakeutiZaring] p. 27 | Theorem 6.12(2) | tz6.12-2 5243 |
| [TakeutiZaring] p. 27 | Definition 6.15(1) | df-fn 4971 |
| [TakeutiZaring] p. 27 | Definition 6.15(3) | df-f 4972 |
| [TakeutiZaring] p. 27 | Definition 6.15(4) | df-fo 4974 wfo 4966 |
| [TakeutiZaring] p. 27 | Definition 6.15(5) | df-f1 4973 wf1 4965 |
| [TakeutiZaring] p. 27 | Definition 6.15(6) | df-f1o 4975 wf1o 4967 |
| [TakeutiZaring] p. 28 | Exercise 4 | eqfnfv 5341 eqfnfv2 5342 eqfnfv2f 5345 |
| [TakeutiZaring] p. 28 | Exercise 5 | fvco 5318 |
| [TakeutiZaring] p. 28 | Theorem 6.16(1) | fnex 5458 fnexALT 5818 |
| [TakeutiZaring] p. 28 | Proposition 6.17 | resfunexg 5457 resfunexgALT 5815 |
| [TakeutiZaring] p. 29 | Exercise 9 | funimaex 5051 funimaexg 5050 |
| [TakeutiZaring] p. 29 | Definition 6.18 | df-br 3812 |
| [TakeutiZaring] p. 30 | Definition 6.21 | eliniseg 4756 iniseg 4758 |
| [TakeutiZaring] p. 30 | Definition 6.22 | df-eprel 4079 |
| [TakeutiZaring] p. 32 | Definition 6.28 | df-isom 4977 |
| [TakeutiZaring] p. 33 | Proposition 6.30(1) | isoid 5528 |
| [TakeutiZaring] p. 33 | Proposition 6.30(2) | isocnv 5529 |
| [TakeutiZaring] p. 33 | Proposition 6.30(3) | isotr 5534 |
| [TakeutiZaring] p. 33 | Proposition 6.31(2) | isoini 5535 |
| [TakeutiZaring] p. 34 | Proposition 6.33 | f1oiso 5543 |
| [TakeutiZaring] p. 35 | Notation | wtr 3901 |
| [TakeutiZaring] p. 35 | Theorem 7.2 | tz7.2 4144 |
| [TakeutiZaring] p. 35 | Definition 7.1 | dftr3 3905 |
| [TakeutiZaring] p. 36 | Proposition 7.4 | ordwe 4353 |
| [TakeutiZaring] p. 36 | Proposition 7.6 | ordelord 4171 |
| [TakeutiZaring] p. 37 | Proposition 7.9 | ordin 4175 |
| [TakeutiZaring] p. 38 | Corollary 7.15 | ordsson 4271 |
| [TakeutiZaring] p. 38 | Definition 7.11 | df-on 4158 |
| [TakeutiZaring] p. 38 | Proposition 7.12 | ordon 4265 |
| [TakeutiZaring] p. 38 | Proposition 7.13 | onprc 4330 |
| [TakeutiZaring] p. 39 | Theorem 7.17 | tfi 4359 |
| [TakeutiZaring] p. 40 | Exercise 7 | dftr2 3903 |
| [TakeutiZaring] p. 40 | Exercise 11 | unon 4290 |
| [TakeutiZaring] p. 40 | Proposition 7.19 | ssorduni 4266 |
| [TakeutiZaring] p. 40 | Proposition 7.20 | elssuni 3655 |
| [TakeutiZaring] p. 41 | Definition 7.22 | df-suc 4161 |
| [TakeutiZaring] p. 41 | Proposition 7.23 | sssucid 4205 sucidg 4206 |
| [TakeutiZaring] p. 41 | Proposition 7.24 | suceloni 4280 |
| [TakeutiZaring] p. 42 | Exercise 1 | df-ilim 4159 |
| [TakeutiZaring] p. 42 | Exercise 8 | onsucssi 4285 ordelsuc 4284 |
| [TakeutiZaring] p. 42 | Proposition 7.30(1) | peano1 4371 |
| [TakeutiZaring] p. 42 | Proposition 7.30(2) | peano2 4372 |
| [TakeutiZaring] p. 42 | Proposition 7.30(3) | peano3 4373 |
| [TakeutiZaring] p. 43 | Axiom 7 | omex 4370 |
| [TakeutiZaring] p. 43 | Theorem 7.32 | ordom 4383 |
| [TakeutiZaring] p. 43 | Corollary 7.31 | find 4376 |
| [TakeutiZaring] p. 43 | Proposition 7.30(4) | peano4 4374 |
| [TakeutiZaring] p. 43 | Proposition 7.30(5) | peano5 4375 |
| [TakeutiZaring] p. 44 | Exercise 2 | int0 3676 |
| [TakeutiZaring] p. 44 | Exercise 3 | trintssm 3917 |
| [TakeutiZaring] p. 44 | Exercise 4 | intss1 3677 |
| [TakeutiZaring] p. 44 | Exercise 6 | onintonm 4296 |
| [TakeutiZaring] p. 44 | Definition 7.35 | df-int 3663 |
| [TakeutiZaring] p. 47 | Lemma 1 | tfrlem1 6004 |
| [TakeutiZaring] p. 47 | Theorem 7.41(1) | tfri1 6061 tfri1d 6031 |
| [TakeutiZaring] p. 47 | Theorem 7.41(2) | tfri2 6062 tfri2d 6032 |
| [TakeutiZaring] p. 47 | Theorem 7.41(3) | tfri3 6063 |
| [TakeutiZaring] p. 50 | Exercise 3 | smoiso 5998 |
| [TakeutiZaring] p. 50 | Definition 7.46 | df-smo 5982 |
| [TakeutiZaring] p. 56 | Definition 8.1 | oasuc 6156 |
| [TakeutiZaring] p. 57 | Proposition 8.2 | oacl 6152 |
| [TakeutiZaring] p. 57 | Proposition 8.3 | oa0 6149 |
| [TakeutiZaring] p. 57 | Proposition 8.16 | omcl 6153 |
| [TakeutiZaring] p. 58 | Proposition 8.4 | nnaord 6197 nnaordi 6196 |
| [TakeutiZaring] p. 59 | Proposition 8.6 | iunss2 3749 uniss2 3658 |
| [TakeutiZaring] p. 59 | Proposition 8.7 | oawordriexmid 6162 |
| [TakeutiZaring] p. 59 | Proposition 8.9 | nnacl 6172 |
| [TakeutiZaring] p. 62 | Exercise 5 | oaword1 6163 |
| [TakeutiZaring] p. 62 | Definition 8.15 | om0 6150 omsuc 6164 |
| [TakeutiZaring] p. 63 | Proposition 8.17 | nnmcl 6173 |
| [TakeutiZaring] p. 63 | Proposition 8.19 | nnmord 6205 nnmordi 6204 |
| [TakeutiZaring] p. 67 | Definition 8.30 | oei0 6151 |
| [TakeutiZaring] p. 85 | Proposition 10.6(3) | cardonle 6717 |
| [TakeutiZaring] p. 88 | Exercise 1 | en0 6441 |
| [TakeutiZaring] p. 90 | Proposition 10.20 | nneneq 6502 |
| [TakeutiZaring] p. 90 | Corollary 10.21(1) | php5 6503 |
| [TakeutiZaring] p. 91 | Definition 10.29 | df-fin 6389 isfi 6407 |
| [TakeutiZaring] p. 92 | Proposition 10.33(2) | xpdom2 6476 |
| [TakeutiZaring] p. 95 | Definition 10.42 | df-map 6336 |
| [TakeutiZaring] p. 96 | Proposition 10.45 | mapxpen 6493 |
| [Tarski] p. 67 | Axiom B5 | ax-4 1441 |
| [Tarski] p. 68 | Lemma 6 | equid 1630 |
| [Tarski] p. 69 | Lemma 7 | equcomi 1633 |
| [Tarski] p. 70 | Lemma 14 | spim 1668 spime 1671 spimeh 1669 spimh 1667 |
| [Tarski] p. 70 | Lemma 16 | ax-11 1438 ax-11o 1746 ax11i 1644 |
| [Tarski] p. 70 | Lemmas 16 and 17 | sb6 1809 |
| [Tarski] p. 77 | Axiom B6 (p. 75) of system S2 | ax-17 1460 |
| [Tarski] p. 77 | Axiom B8 (p. 75) of system S2 | ax-13 1445 ax-14 1446 |
| [WhiteheadRussell] p. 96 | Axiom *1.3 | olc 665 |
| [WhiteheadRussell] p. 96 | Axiom *1.4 | pm1.4 679 |
| [WhiteheadRussell] p. 96 | Axiom *1.2 (Taut) | pm1.2 706 |
| [WhiteheadRussell] p. 96 | Axiom *1.5 (Assoc) | pm1.5 715 |
| [WhiteheadRussell] p. 97 | Axiom *1.6 (Sum) | orim2 736 |
| [WhiteheadRussell] p. 100 | Theorem *2.01 | pm2.01 579 |
| [WhiteheadRussell] p. 100 | Theorem *2.02 | ax-1 5 |
| [WhiteheadRussell] p. 100 | Theorem *2.03 | con2 605 |
| [WhiteheadRussell] p. 100 | Theorem *2.04 | pm2.04 81 |
| [WhiteheadRussell] p. 100 | Theorem *2.05 | imim2 54 |
| [WhiteheadRussell] p. 100 | Theorem *2.06 | imim1 75 |
| [WhiteheadRussell] p. 101 | Theorem *2.1 | pm2.1dc 779 |
| [WhiteheadRussell] p. 101 | Theorem *2.06 | barbara 2041 syl 14 |
| [WhiteheadRussell] p. 101 | Theorem *2.07 | pm2.07 689 |
| [WhiteheadRussell] p. 101 | Theorem *2.08 | id 19 idALT 20 |
| [WhiteheadRussell] p. 101 | Theorem *2.11 | exmiddc 778 |
| [WhiteheadRussell] p. 101 | Theorem *2.12 | notnot 592 |
| [WhiteheadRussell] p. 101 | Theorem *2.13 | pm2.13dc 813 |
| [WhiteheadRussell] p. 102 | Theorem *2.14 | notnotrdc 785 |
| [WhiteheadRussell] p. 102 | Theorem *2.15 | con1dc 787 |
| [WhiteheadRussell] p. 103 | Theorem *2.16 | con3 604 |
| [WhiteheadRussell] p. 103 | Theorem *2.17 | condc 783 |
| [WhiteheadRussell] p. 103 | Theorem *2.18 | pm2.18dc 784 |
| [WhiteheadRussell] p. 104 | Theorem *2.2 | orc 666 |
| [WhiteheadRussell] p. 104 | Theorem *2.3 | pm2.3 725 |
| [WhiteheadRussell] p. 104 | Theorem *2.21 | pm2.21 580 |
| [WhiteheadRussell] p. 104 | Theorem *2.24 | pm2.24 584 |
| [WhiteheadRussell] p. 104 | Theorem *2.25 | pm2.25dc 826 |
| [WhiteheadRussell] p. 104 | Theorem *2.26 | pm2.26dc 847 |
| [WhiteheadRussell] p. 104 | Theorem *2.27 | pm2.27 39 |
| [WhiteheadRussell] p. 104 | Theorem *2.31 | pm2.31 718 |
| [WhiteheadRussell] p. 105 | Theorem *2.32 | pm2.32 719 |
| [WhiteheadRussell] p. 105 | Theorem *2.36 | pm2.36 751 |
| [WhiteheadRussell] p. 105 | Theorem *2.37 | pm2.37 752 |
| [WhiteheadRussell] p. 105 | Theorem *2.38 | pm2.38 750 |
| [WhiteheadRussell] p. 105 | Definition *2.33 | df-3or 921 |
| [WhiteheadRussell] p. 106 | Theorem *2.4 | pm2.4 728 |
| [WhiteheadRussell] p. 106 | Theorem *2.41 | pm2.41 726 |
| [WhiteheadRussell] p. 106 | Theorem *2.42 | pm2.42 727 |
| [WhiteheadRussell] p. 106 | Theorem *2.43 | pm2.43 52 |
| [WhiteheadRussell] p. 106 | Theorem *2.45 | pm2.45 690 |
| [WhiteheadRussell] p. 106 | Theorem *2.46 | pm2.46 691 |
| [WhiteheadRussell] p. 107 | Theorem *2.5 | pm2.5dc 797 |
| [WhiteheadRussell] p. 107 | Theorem *2.6 | pm2.6dc 793 |
| [WhiteheadRussell] p. 107 | Theorem *2.47 | pm2.47 692 |
| [WhiteheadRussell] p. 107 | Theorem *2.48 | pm2.48 693 |
| [WhiteheadRussell] p. 107 | Theorem *2.49 | pm2.49 694 |
| [WhiteheadRussell] p. 107 | Theorem *2.51 | pm2.51 614 |
| [WhiteheadRussell] p. 107 | Theorem *2.52 | pm2.52 615 |
| [WhiteheadRussell] p. 107 | Theorem *2.53 | pm2.53 674 |
| [WhiteheadRussell] p. 107 | Theorem *2.54 | pm2.54dc 824 |
| [WhiteheadRussell] p. 107 | Theorem *2.55 | orel1 677 |
| [WhiteheadRussell] p. 107 | Theorem *2.56 | orel2 678 |
| [WhiteheadRussell] p. 107 | Theorem *2.61 | pm2.61dc 796 |
| [WhiteheadRussell] p. 107 | Theorem *2.62 | pm2.62 700 |
| [WhiteheadRussell] p. 107 | Theorem *2.63 | pm2.63 747 |
| [WhiteheadRussell] p. 107 | Theorem *2.64 | pm2.64 748 |
| [WhiteheadRussell] p. 107 | Theorem *2.65 | pm2.65 618 |
| [WhiteheadRussell] p. 107 | Theorem *2.67 | pm2.67-2 667 pm2.67 695 |
| [WhiteheadRussell] p. 107 | Theorem *2.521 | pm2.521dc 798 |
| [WhiteheadRussell] p. 107 | Theorem *2.621 | pm2.621 699 |
| [WhiteheadRussell] p. 108 | Theorem *2.8 | pm2.8 757 |
| [WhiteheadRussell] p. 108 | Theorem *2.68 | pm2.68dc 827 |
| [WhiteheadRussell] p. 108 | Theorem *2.69 | looinvdc 855 |
| [WhiteheadRussell] p. 108 | Theorem *2.73 | pm2.73 753 |
| [WhiteheadRussell] p. 108 | Theorem *2.74 | pm2.74 754 |
| [WhiteheadRussell] p. 108 | Theorem *2.75 | pm2.75 756 |
| [WhiteheadRussell] p. 108 | Theorem *2.76 | pm2.76 755 |
| [WhiteheadRussell] p. 108 | Theorem *2.77 | ax-2 6 |
| [WhiteheadRussell] p. 108 | Theorem *2.81 | pm2.81 758 |
| [WhiteheadRussell] p. 108 | Theorem *2.82 | pm2.82 759 |
| [WhiteheadRussell] p. 108 | Theorem *2.83 | pm2.83 76 |
| [WhiteheadRussell] p. 108 | Theorem *2.85 | pm2.85dc 845 |
| [WhiteheadRussell] p. 108 | Theorem *2.86 | pm2.86 99 |
| [WhiteheadRussell] p. 111 | Theorem *3.1 | pm3.1 704 |
| [WhiteheadRussell] p. 111 | Theorem *3.2 | pm3.2 137 |
| [WhiteheadRussell] p. 111 | Theorem *3.11 | pm3.11dc 899 |
| [WhiteheadRussell] p. 111 | Theorem *3.12 | pm3.12dc 900 |
| [WhiteheadRussell] p. 111 | Theorem *3.13 | pm3.13dc 901 |
| [WhiteheadRussell] p. 111 | Theorem *3.14 | pm3.14 703 |
| [WhiteheadRussell] p. 111 | Theorem *3.21 | pm3.21 260 |
| [WhiteheadRussell] p. 111 | Theorem *3.22 | pm3.22 261 |
| [WhiteheadRussell] p. 111 | Theorem *3.24 | pm3.24 660 |
| [WhiteheadRussell] p. 112 | Theorem *3.35 | pm3.35 339 |
| [WhiteheadRussell] p. 112 | Theorem *3.3 (Exp) | pm3.3 257 |
| [WhiteheadRussell] p. 112 | Theorem *3.31 (Imp) | pm3.31 258 |
| [WhiteheadRussell] p. 112 | Theorem *3.26 (Simp) | simpl 107 simplimdc 791 |
| [WhiteheadRussell] p. 112 | Theorem *3.27 (Simp) | simpr 108 simprimdc 790 |
| [WhiteheadRussell] p. 112 | Theorem *3.33 (Syll) | pm3.33 337 |
| [WhiteheadRussell] p. 112 | Theorem *3.34 (Syll) | pm3.34 338 |
| [WhiteheadRussell] p. 112 | Theorem *3.37 (Transp) | pm3.37 822 |
| [WhiteheadRussell] p. 113 | Fact) | pm3.45 562 |
| [WhiteheadRussell] p. 113 | Theorem *3.4 | pm3.4 326 |
| [WhiteheadRussell] p. 113 | Theorem *3.41 | pm3.41 324 |
| [WhiteheadRussell] p. 113 | Theorem *3.42 | pm3.42 325 |
| [WhiteheadRussell] p. 113 | Theorem *3.44 | jao 705 pm3.44 668 |
| [WhiteheadRussell] p. 113 | Theorem *3.47 | prth 336 |
| [WhiteheadRussell] p. 113 | Theorem *3.43 (Comp) | pm3.43 567 |
| [WhiteheadRussell] p. 114 | Theorem *3.48 | pm3.48 732 |
| [WhiteheadRussell] p. 116 | Theorem *4.1 | con34bdc 799 |
| [WhiteheadRussell] p. 117 | Theorem *4.2 | biid 169 |
| [WhiteheadRussell] p. 117 | Theorem *4.13 | notnotbdc 800 |
| [WhiteheadRussell] p. 117 | Theorem *4.14 | pm4.14dc 821 |
| [WhiteheadRussell] p. 117 | Theorem *4.15 | pm4.15 823 |
| [WhiteheadRussell] p. 117 | Theorem *4.21 | bicom 138 |
| [WhiteheadRussell] p. 117 | Theorem *4.22 | biantr 894 bitr 456 |
| [WhiteheadRussell] p. 117 | Theorem *4.24 | pm4.24 387 |
| [WhiteheadRussell] p. 117 | Theorem *4.25 | oridm 707 pm4.25 708 |
| [WhiteheadRussell] p. 118 | Theorem *4.3 | ancom 262 |
| [WhiteheadRussell] p. 118 | Theorem *4.4 | andi 765 |
| [WhiteheadRussell] p. 118 | Theorem *4.31 | orcom 680 |
| [WhiteheadRussell] p. 118 | Theorem *4.32 | anass 393 |
| [WhiteheadRussell] p. 118 | Theorem *4.33 | orass 717 |
| [WhiteheadRussell] p. 118 | Theorem *4.36 | anbi1 454 |
| [WhiteheadRussell] p. 118 | Theorem *4.37 | orbi1 739 |
| [WhiteheadRussell] p. 118 | Theorem *4.38 | pm4.38 570 |
| [WhiteheadRussell] p. 118 | Theorem *4.39 | pm4.39 769 |
| [WhiteheadRussell] p. 118 | Definition *4.34 | df-3an 922 |
| [WhiteheadRussell] p. 119 | Theorem *4.41 | ordi 763 |
| [WhiteheadRussell] p. 119 | Theorem *4.42 | pm4.42r 913 |
| [WhiteheadRussell] p. 119 | Theorem *4.43 | pm4.43 891 |
| [WhiteheadRussell] p. 119 | Theorem *4.44 | pm4.44 729 |
| [WhiteheadRussell] p. 119 | Theorem *4.45 | orabs 761 pm4.45 731 pm4.45im 327 |
| [WhiteheadRussell] p. 119 | Theorem *10.22 | 19.26 1411 |
| [WhiteheadRussell] p. 120 | Theorem *4.5 | anordc 898 |
| [WhiteheadRussell] p. 120 | Theorem *4.6 | imordc 830 imorr 831 |
| [WhiteheadRussell] p. 120 | Theorem *4.7 | anclb 312 |
| [WhiteheadRussell] p. 120 | Theorem *4.51 | ianordc 833 |
| [WhiteheadRussell] p. 120 | Theorem *4.52 | pm4.52im 837 |
| [WhiteheadRussell] p. 120 | Theorem *4.53 | pm4.53r 838 |
| [WhiteheadRussell] p. 120 | Theorem *4.54 | pm4.54dc 839 |
| [WhiteheadRussell] p. 120 | Theorem *4.55 | pm4.55dc 880 |
| [WhiteheadRussell] p. 120 | Theorem *4.56 | ioran 702 pm4.56 840 |
| [WhiteheadRussell] p. 120 | Theorem *4.57 | orandc 881 oranim 841 |
| [WhiteheadRussell] p. 120 | Theorem *4.61 | annimim 816 |
| [WhiteheadRussell] p. 120 | Theorem *4.62 | pm4.62dc 832 |
| [WhiteheadRussell] p. 120 | Theorem *4.63 | pm4.63dc 814 |
| [WhiteheadRussell] p. 120 | Theorem *4.64 | pm4.64dc 835 |
| [WhiteheadRussell] p. 120 | Theorem *4.65 | pm4.65r 817 |
| [WhiteheadRussell] p. 120 | Theorem *4.66 | pm4.66dc 836 |
| [WhiteheadRussell] p. 120 | Theorem *4.67 | pm4.67dc 815 |
| [WhiteheadRussell] p. 120 | Theorem *4.71 | pm4.71 381 pm4.71d 385 pm4.71i 383 pm4.71r 382 pm4.71rd 386 pm4.71ri 384 |
| [WhiteheadRussell] p. 121 | Theorem *4.72 | pm4.72 770 |
| [WhiteheadRussell] p. 121 | Theorem *4.73 | iba 294 |
| [WhiteheadRussell] p. 121 | Theorem *4.74 | biorf 696 |
| [WhiteheadRussell] p. 121 | Theorem *4.76 | jcab 568 pm4.76 569 |
| [WhiteheadRussell] p. 121 | Theorem *4.77 | jaob 664 pm4.77 746 |
| [WhiteheadRussell] p. 121 | Theorem *4.78 | pm4.78i 842 |
| [WhiteheadRussell] p. 121 | Theorem *4.79 | pm4.79dc 843 |
| [WhiteheadRussell] p. 122 | Theorem *4.8 | pm4.8 656 |
| [WhiteheadRussell] p. 122 | Theorem *4.81 | pm4.81dc 848 |
| [WhiteheadRussell] p. 122 | Theorem *4.82 | pm4.82 892 |
| [WhiteheadRussell] p. 122 | Theorem *4.83 | pm4.83dc 893 |
| [WhiteheadRussell] p. 122 | Theorem *4.84 | imbi1 234 |
| [WhiteheadRussell] p. 122 | Theorem *4.85 | imbi2 235 |
| [WhiteheadRussell] p. 122 | Theorem *4.86 | bibi1 238 |
| [WhiteheadRussell] p. 122 | Theorem *4.87 | bi2.04 246 impexp 259 pm4.87 524 |
| [WhiteheadRussell] p. 123 | Theorem *5.1 | pm5.1 566 |
| [WhiteheadRussell] p. 123 | Theorem *5.11 | pm5.11dc 849 |
| [WhiteheadRussell] p. 123 | Theorem *5.12 | pm5.12dc 850 |
| [WhiteheadRussell] p. 123 | Theorem *5.13 | pm5.13dc 852 |
| [WhiteheadRussell] p. 123 | Theorem *5.14 | pm5.14dc 851 |
| [WhiteheadRussell] p. 124 | Theorem *5.15 | pm5.15dc 1321 |
| [WhiteheadRussell] p. 124 | Theorem *5.16 | pm5.16 771 |
| [WhiteheadRussell] p. 124 | Theorem *5.17 | pm5.17dc 844 |
| [WhiteheadRussell] p. 124 | Theorem *5.18 | nbbndc 1326 pm5.18dc 811 |
| [WhiteheadRussell] p. 124 | Theorem *5.19 | pm5.19 655 |
| [WhiteheadRussell] p. 124 | Theorem *5.21 | pm5.21 644 |
| [WhiteheadRussell] p. 124 | Theorem *5.22 | xordc 1324 |
| [WhiteheadRussell] p. 124 | Theorem *5.23 | dfbi3dc 1329 |
| [WhiteheadRussell] p. 124 | Theorem *5.24 | pm5.24dc 1330 |
| [WhiteheadRussell] p. 124 | Theorem *5.25 | dfor2dc 828 |
| [WhiteheadRussell] p. 125 | Theorem *5.3 | pm5.3 459 |
| [WhiteheadRussell] p. 125 | Theorem *5.4 | pm5.4 247 |
| [WhiteheadRussell] p. 125 | Theorem *5.5 | pm5.5 240 |
| [WhiteheadRussell] p. 125 | Theorem *5.6 | pm5.6dc 869 pm5.6r 870 |
| [WhiteheadRussell] p. 125 | Theorem *5.7 | pm5.7dc 896 |
| [WhiteheadRussell] p. 125 | Theorem *5.31 | pm5.31 340 |
| [WhiteheadRussell] p. 125 | Theorem *5.32 | pm5.32 441 |
| [WhiteheadRussell] p. 125 | Theorem *5.33 | pm5.33 574 |
| [WhiteheadRussell] p. 125 | Theorem *5.35 | pm5.35 860 |
| [WhiteheadRussell] p. 125 | Theorem *5.36 | pm5.36 575 |
| [WhiteheadRussell] p. 125 | Theorem *5.41 | imdi 248 pm5.41 249 |
| [WhiteheadRussell] p. 125 | Theorem *5.42 | pm5.42 313 |
| [WhiteheadRussell] p. 125 | Theorem *5.44 | pm5.44 868 |
| [WhiteheadRussell] p. 125 | Theorem *5.53 | pm5.53 749 |
| [WhiteheadRussell] p. 125 | Theorem *5.54 | pm5.54dc 861 |
| [WhiteheadRussell] p. 125 | Theorem *5.55 | pm5.55dc 853 |
| [WhiteheadRussell] p. 125 | Theorem *5.61 | pm5.61 741 |
| [WhiteheadRussell] p. 125 | Theorem *5.62 | pm5.62dc 887 |
| [WhiteheadRussell] p. 125 | Theorem *5.63 | pm5.63dc 888 |
| [WhiteheadRussell] p. 125 | Theorem *5.71 | pm5.71dc 903 |
| [WhiteheadRussell] p. 125 | Theorem *5.501 | pm5.501 242 |
| [WhiteheadRussell] p. 126 | Theorem *5.74 | pm5.74 177 |
| [WhiteheadRussell] p. 126 | Theorem *5.75 | pm5.75 904 |
| [WhiteheadRussell] p. 150 | Theorem *10.3 | alsyl 1567 |
| [WhiteheadRussell] p. 160 | Theorem *11.21 | alrot3 1415 |
| [WhiteheadRussell] p. 163 | Theorem *11.42 | 19.40-2 1564 |
| [WhiteheadRussell] p. 164 | Theorem *11.53 | pm11.53 1818 |
| [WhiteheadRussell] p. 175 | Definition *14.02 | df-eu 1946 |
| [WhiteheadRussell] p. 178 | Theorem *13.18 | pm13.18 2330 |
| [WhiteheadRussell] p. 178 | Theorem *13.181 | pm13.181 2331 |
| [WhiteheadRussell] p. 178 | Theorem *13.183 | pm13.183 2742 |
| [WhiteheadRussell] p. 185 | Theorem *14.121 | sbeqalb 2881 |
| [WhiteheadRussell] p. 190 | Theorem *14.22 | iota4 4951 |
| [WhiteheadRussell] p. 191 | Theorem *14.23 | iota4an 4952 |
| [WhiteheadRussell] p. 192 | Theorem *14.26 | eupick 2022 eupickbi 2025 |
| [WhiteheadRussell] p. 235 | Definition *30.01 | df-fv 4976 |
| [WhiteheadRussell] p. 360 | Theorem *54.43 | pm54.43 6720 |
| This page was last updated on 14-Aug-2016.
Copyright terms: Public domain |
W3C HTML validation [external] |