Intuitionistic Logic Explorer Home Intuitionistic Logic Explorer
Bibliographic Cross-References
 
Mirrors  >  Home  >  ILE Home  >  Bibliographic Cross-References

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the Intuitionistic Logic Explorer's axiom, definition, and theorem Descriptions. If you are studying a particular reference, this list can be handy for finding out where any corresponding Metamath theorems might be located. Keep in mind that we usually give only one reference for a theorem that may appear in several books, so it can also be useful to browse the Related Theorems around a theorem of interest.

Bibliographic Cross-Reference for the Intuitionistic Logic Explorer
Bibliographic Reference DescriptionIntuitionistic Logic Explorer Page(s)
[AczelRathjen], p. 71Definition 8.1.4enumct 7104  fidcenum 6945
[AczelRathjen], p. 72Proposition 8.1.11fidcenum 6945
[AczelRathjen], p. 73Lemma 8.1.14enumct 7104
[AczelRathjen], p. 73Corollary 8.1.13ennnfone 12391
[AczelRathjen], p. 74Lemma 8.1.16xpfi 6919
[AczelRathjen], p. 74Remark 8.1.17unfiexmid 6907
[AczelRathjen], p. 74Theorem 8.1.19ctiunct 12406
[AczelRathjen], p. 75Corollary 8.1.20unct 12408
[AczelRathjen], p. 75Corollary 8.1.23qnnen 12397  znnen 12364
[AczelRathjen], p. 77Lemma 8.1.27omctfn 12409
[AczelRathjen], p. 78Theorem 8.1.28omiunct 12410
[AczelRathjen], p. 80Corollary 8.2.4df-ihash 10722
[AczelRathjen], p. 183Chapter 20ax-setind 4530
[Apostol] p. 18Theorem I.1addcan 8111  addcan2d 8116  addcan2i 8114  addcand 8115  addcani 8113
[Apostol] p. 18Theorem I.2negeu 8122
[Apostol] p. 18Theorem I.3negsub 8179  negsubd 8248  negsubi 8209
[Apostol] p. 18Theorem I.4negneg 8181  negnegd 8233  negnegi 8201
[Apostol] p. 18Theorem I.5subdi 8316  subdid 8345  subdii 8338  subdir 8317  subdird 8346  subdiri 8339
[Apostol] p. 18Theorem I.6mul01 8320  mul01d 8324  mul01i 8322  mul02 8318  mul02d 8323  mul02i 8321
[Apostol] p. 18Theorem I.9divrecapd 8722
[Apostol] p. 18Theorem I.10recrecapi 8673
[Apostol] p. 18Theorem I.12mul2neg 8329  mul2negd 8344  mul2negi 8337  mulneg1 8326  mulneg1d 8342  mulneg1i 8335
[Apostol] p. 18Theorem I.15divdivdivap 8642
[Apostol] p. 20Axiom 7rpaddcl 9646  rpaddcld 9681  rpmulcl 9647  rpmulcld 9682
[Apostol] p. 20Axiom 90nrp 9658
[Apostol] p. 20Theorem I.17lttri 8036
[Apostol] p. 20Theorem I.18ltadd1d 8469  ltadd1dd 8487  ltadd1i 8433
[Apostol] p. 20Theorem I.19ltmul1 8523  ltmul1a 8522  ltmul1i 8848  ltmul1ii 8856  ltmul2 8784  ltmul2d 9708  ltmul2dd 9722  ltmul2i 8851
[Apostol] p. 20Theorem I.210lt1 8058
[Apostol] p. 20Theorem I.23lt0neg1 8399  lt0neg1d 8446  ltneg 8393  ltnegd 8454  ltnegi 8424
[Apostol] p. 20Theorem I.25lt2add 8376  lt2addd 8498  lt2addi 8441
[Apostol] p. 20Definition of positive numbersdf-rp 9623
[Apostol] p. 21Exercise 4recgt0 8778  recgt0d 8862  recgt0i 8834  recgt0ii 8835
[Apostol] p. 22Definition of integersdf-z 9225
[Apostol] p. 22Definition of rationalsdf-q 9591
[Apostol] p. 24Theorem I.26supeuti 6983
[Apostol] p. 26Theorem I.29arch 9144
[Apostol] p. 28Exercise 2btwnz 9343
[Apostol] p. 28Exercise 3nnrecl 9145
[Apostol] p. 28Exercise 6qbtwnre 10225
[Apostol] p. 28Exercise 10(a)zeneo 11841  zneo 9325
[Apostol] p. 29Theorem I.35resqrtth 11006  sqrtthi 11094
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 8893
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwodc 12002
[Apostol] p. 363Remarkabsgt0api 11121
[Apostol] p. 363Exampleabssubd 11168  abssubi 11125
[ApostolNT] p. 14Definitiondf-dvds 11761
[ApostolNT] p. 14Theorem 1.1(a)iddvds 11777
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 11801
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 11797
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 11791
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 11793
[ApostolNT] p. 14Theorem 1.1(f)1dvds 11778
[ApostolNT] p. 14Theorem 1.1(g)dvds0 11779
[ApostolNT] p. 14Theorem 1.1(h)0dvds 11784
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 11816
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 11818
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 11820
[ApostolNT] p. 15Definitiondfgcd2 11980
[ApostolNT] p. 16Definitionisprm2 12082
[ApostolNT] p. 16Theorem 1.5coprmdvds 12057
[ApostolNT] p. 16Theorem 1.7prminf 12421
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 11939
[ApostolNT] p. 16Theorem 1.4(b)gcdass 11981
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 11983
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 11953
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 11946
[ApostolNT] p. 17Theorem 1.8coprm 12109
[ApostolNT] p. 17Theorem 1.9euclemma 12111
[ApostolNT] p. 17Theorem 1.101arith2 12331
[ApostolNT] p. 19Theorem 1.14divalg 11894
[ApostolNT] p. 20Theorem 1.15eucalg 12024
[ApostolNT] p. 25Definitiondf-phi 12176
[ApostolNT] p. 26Theorem 2.2phisum 12205
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 12187
[ApostolNT] p. 28Theorem 2.5(c)phimul 12191
[ApostolNT] p. 104Definitioncongr 12065
[ApostolNT] p. 106Remarkdvdsval3 11764
[ApostolNT] p. 106Definitionmoddvds 11772
[ApostolNT] p. 107Example 2mod2eq0even 11848
[ApostolNT] p. 107Example 3mod2eq1n2dvds 11849
[ApostolNT] p. 107Example 4zmod1congr 10309
[ApostolNT] p. 107Theorem 5.2(b)modqmul12d 10346
[ApostolNT] p. 107Theorem 5.2(c)modqexp 10614
[ApostolNT] p. 108Theorem 5.3modmulconst 11796
[ApostolNT] p. 109Theorem 5.4cncongr1 12068
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 12070
[ApostolNT] p. 113Theorem 5.17eulerth 12198
[ApostolNT] p. 113Theorem 5.18vfermltl 12216
[ApostolNT] p. 114Theorem 5.19fermltl 12199
[ApostolNT] p. 179Definitiondf-lgs 13950  lgsprme0 13994
[ApostolNT] p. 180Example 11lgs 13995
[ApostolNT] p. 180Theorem 9.2lgsvalmod 13971
[ApostolNT] p. 180Theorem 9.3lgsdirprm 13986
[ApostolNT] p. 188Definitiondf-lgs 13950  lgs1 13996
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 13987
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 13989
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 13997
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 13998
[Bauer] p. 482Section 1.2pm2.01 616  pm2.65 659
[Bauer] p. 483Theorem 1.3acexmid 5864  onsucelsucexmidlem 4522
[Bauer], p. 481Section 1.1pwtrufal 14287
[Bauer], p. 483Definitionn0rf 3433
[Bauer], p. 483Theorem 1.22irrexpq 13945  2irrexpqap 13947
[Bauer], p. 485Theorem 2.1ssfiexmid 6866
[Bauer], p. 494Theorem 5.5ivthinc 13672
[BauerHanson], p. 27Proposition 5.2cnstab 8576
[BauerSwan], p. 14Remark0ct 7096  ctm 7098
[BauerSwan], p. 14Proposition 2.6subctctexmid 14291
[BauerSwan], p. 14Table" is defined as ` ` per enumct 7104
[BauerTaylor], p. 32Lemma 6.16prarloclem 7475
[BauerTaylor], p. 50Lemma 11.4subhalfnqq 7388
[BauerTaylor], p. 52Proposition 11.15prarloc 7477
[BauerTaylor], p. 53Lemma 11.16addclpr 7511  addlocpr 7510
[BauerTaylor], p. 55Proposition 12.7appdivnq 7537
[BauerTaylor], p. 56Lemma 12.8prmuloc 7540
[BauerTaylor], p. 56Lemma 12.9mullocpr 7545
[BellMachover] p. 36Lemma 10.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 2027
[BellMachover] p. 460Notationdf-mo 2028
[BellMachover] p. 460Definitionmo3 2078  mo3h 2077
[BellMachover] p. 462Theorem 1.1bm1.1 2160
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4119
[BellMachover] p. 466Axiom Powaxpow3 4172
[BellMachover] p. 466Axiom Unionaxun2 4429
[BellMachover] p. 469Theorem 2.2(i)ordirr 4535
[BellMachover] p. 469Theorem 2.2(iii)onelon 4378
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4538
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4489
[BellMachover] p. 471Definition of Limdf-ilim 4363
[BellMachover] p. 472Axiom Infzfinf2 4582
[BellMachover] p. 473Theorem 2.8limom 4607
[Bobzien] p. 116Statement T3stoic3 1429
[Bobzien] p. 117Statement T2stoic2a 1427
[Bobzien] p. 117Statement T4stoic4a 1430
[BourbakiAlg1] p. 1Definition 1df-mgm 12639
[BourbakiAlg1] p. 4Definition 5df-sgrp 12672
[BourbakiAlg1] p. 12Definition 2df-mnd 12682
[BourbakiAlg1] p. 92Definition 1df-ring 12974
[BourbakiEns] p. Proposition 8fcof1 5774  fcofo 5775
[BourbakiTop1] p. Remarkxnegmnf 9798  xnegpnf 9797
[BourbakiTop1] p. Remark rexneg 9799
[BourbakiTop1] p. Propositionishmeo 13355
[BourbakiTop1] p. Property V_issnei2 13208
[BourbakiTop1] p. Property V_iiinnei 13214
[BourbakiTop1] p. Property V_ivneissex 13216
[BourbakiTop1] p. Proposition 1neipsm 13205  neiss 13201
[BourbakiTop1] p. Proposition 2cnptopco 13273
[BourbakiTop1] p. Proposition 4imasnopn 13350
[BourbakiTop1] p. Property V_iiielnei 13203
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 13047
[Bruck] p. 1Section I.1df-mgm 12639
[Bruck] p. 23Section II.1df-sgrp 12672
[Bruck] p. 28Theorem 3.2dfgrp3m 12828
[ChoquetDD] p. 2Definition of mappingdf-mpt 4061
[Cohen] p. 301Remarkrelogoprlem 13840
[Cohen] p. 301Property 2relogmul 13841  relogmuld 13856
[Cohen] p. 301Property 3relogdiv 13842  relogdivd 13857
[Cohen] p. 301Property 4relogexp 13844
[Cohen] p. 301Property 1alog1 13838
[Cohen] p. 301Property 1bloge 13839
[Cohen4] p. 348Observationrelogbcxpbap 13934
[Cohen4] p. 352Definitionrpelogb 13918
[Cohen4] p. 361Property 2rprelogbmul 13924
[Cohen4] p. 361Property 3logbrec 13929  rprelogbdiv 13926
[Cohen4] p. 361Property 4rplogbreexp 13922
[Cohen4] p. 361Property 6relogbexpap 13927
[Cohen4] p. 361Property 1(a)rplogbid1 13916
[Cohen4] p. 361Property 1(b)rplogb1 13917
[Cohen4] p. 367Propertyrplogbchbase 13919
[Cohen4] p. 377Property 2logblt 13931
[Crosilla] p. Axiom 1ax-ext 2157
[Crosilla] p. Axiom 2ax-pr 4203
[Crosilla] p. Axiom 3ax-un 4427
[Crosilla] p. Axiom 4ax-nul 4124
[Crosilla] p. Axiom 5ax-iinf 4581
[Crosilla] p. Axiom 6ru 2959
[Crosilla] p. Axiom 8ax-pow 4169
[Crosilla] p. Axiom 9ax-setind 4530
[Crosilla], p. Axiom 6ax-sep 4116
[Crosilla], p. Axiom 7ax-coll 4113
[Crosilla], p. Axiom 7'repizf 4114
[Crosilla], p. Theorem is statedordtriexmid 4514
[Crosilla], p. Axiom of choice implies instancesacexmid 5864
[Crosilla], p. Definition of ordinaldf-iord 4360
[Crosilla], p. Theorem "Foundation implies instances of EM"regexmid 4528
[Eisenberg] p. 67Definition 5.3df-dif 3129
[Eisenberg] p. 82Definition 6.3df-iom 4584
[Eisenberg] p. 125Definition 8.21df-map 6640
[Enderton] p. 18Axiom of Empty Setaxnul 4123
[Enderton] p. 19Definitiondf-tp 3597
[Enderton] p. 26Exercise 5unissb 3835
[Enderton] p. 26Exercise 10pwel 4212
[Enderton] p. 28Exercise 7(b)pwunim 4280
[Enderton] p. 30Theorem "Distributive laws"iinin1m 3951  iinin2m 3950  iunin1 3946  iunin2 3945
[Enderton] p. 31Theorem "De Morgan's laws"iindif2m 3949  iundif2ss 3947
[Enderton] p. 33Exercise 23iinuniss 3964
[Enderton] p. 33Exercise 25iununir 3965
[Enderton] p. 33Exercise 24(a)iinpw 3972
[Enderton] p. 33Exercise 24(b)iunpw 4474  iunpwss 3973
[Enderton] p. 38Exercise 6(a)unipw 4211
[Enderton] p. 38Exercise 6(b)pwuni 4187
[Enderton] p. 41Lemma 3Dopeluu 4444  rnex 4887  rnexg 4885
[Enderton] p. 41Exercise 8dmuni 4830  rnuni 5032
[Enderton] p. 42Definition of a functiondffun7 5235  dffun8 5236
[Enderton] p. 43Definition of function valuefunfvdm2 5572
[Enderton] p. 43Definition of single-rootedfuncnv 5269
[Enderton] p. 44Definition (d)dfima2 4965  dfima3 4966
[Enderton] p. 47Theorem 3Hfvco2 5577
[Enderton] p. 49Axiom of Choice (first form)df-ac 7195
[Enderton] p. 50Theorem 3K(a)imauni 5752
[Enderton] p. 52Definitiondf-map 6640
[Enderton] p. 53Exercise 21coass 5139
[Enderton] p. 53Exercise 27dmco 5129
[Enderton] p. 53Exercise 14(a)funin 5279
[Enderton] p. 53Exercise 22(a)imass2 4997
[Enderton] p. 54Remarkixpf 6710  ixpssmap 6722
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6689
[Enderton] p. 56Theorem 3Merref 6545
[Enderton] p. 57Lemma 3Nerthi 6571
[Enderton] p. 57Definitiondf-ec 6527
[Enderton] p. 58Definitiondf-qs 6531
[Enderton] p. 60Theorem 3Qth3q 6630  th3qcor 6629  th3qlem1 6627  th3qlem2 6628
[Enderton] p. 61Exercise 35df-ec 6527
[Enderton] p. 65Exercise 56(a)dmun 4827
[Enderton] p. 68Definition of successordf-suc 4365
[Enderton] p. 71Definitiondf-tr 4097  dftr4 4101
[Enderton] p. 72Theorem 4Eunisuc 4407  unisucg 4408
[Enderton] p. 73Exercise 6unisuc 4407  unisucg 4408
[Enderton] p. 73Exercise 5(a)truni 4110
[Enderton] p. 73Exercise 5(b)trint 4111
[Enderton] p. 79Theorem 4I(A1)nna0 6465
[Enderton] p. 79Theorem 4I(A2)nnasuc 6467  onasuc 6457
[Enderton] p. 79Definition of operation valuedf-ov 5868
[Enderton] p. 80Theorem 4J(A1)nnm0 6466
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6468  onmsuc 6464
[Enderton] p. 81Theorem 4K(1)nnaass 6476
[Enderton] p. 81Theorem 4K(2)nna0r 6469  nnacom 6475
[Enderton] p. 81Theorem 4K(3)nndi 6477
[Enderton] p. 81Theorem 4K(4)nnmass 6478
[Enderton] p. 81Theorem 4K(5)nnmcom 6480
[Enderton] p. 82Exercise 16nnm0r 6470  nnmsucr 6479
[Enderton] p. 88Exercise 23nnaordex 6519
[Enderton] p. 129Definitiondf-en 6731
[Enderton] p. 132Theorem 6B(b)canth 5819
[Enderton] p. 133Exercise 1xpomen 12361
[Enderton] p. 134Theorem (Pigeonhole Principle)phpm 6855
[Enderton] p. 136Corollary 6Enneneq 6847
[Enderton] p. 139Theorem 6H(c)mapen 6836
[Enderton] p. 142Theorem 6I(3)xpdjuen 7207
[Enderton] p. 143Theorem 6Jdju0en 7203  dju1en 7202
[Enderton] p. 144Corollary 6Kundif2ss 3496
[Enderton] p. 145Figure 38ffoss 5485
[Enderton] p. 145Definitiondf-dom 6732
[Enderton] p. 146Example 1domen 6741  domeng 6742
[Enderton] p. 146Example 3nndomo 6854
[Enderton] p. 149Theorem 6L(c)xpdom1 6825  xpdom1g 6823  xpdom2g 6822
[Enderton] p. 168Definitiondf-po 4290
[Enderton] p. 192Theorem 7M(a)oneli 4422
[Enderton] p. 192Theorem 7M(b)ontr1 4383
[Enderton] p. 192Theorem 7M(c)onirri 4536
[Enderton] p. 193Corollary 7N(b)0elon 4386
[Enderton] p. 193Corollary 7N(c)onsuci 4509
[Enderton] p. 193Corollary 7N(d)ssonunii 4482
[Enderton] p. 194Remarkonprc 4545
[Enderton] p. 194Exercise 16suc11 4551
[Enderton] p. 197Definitiondf-card 7169
[Enderton] p. 200Exercise 25tfis 4576
[Enderton] p. 206Theorem 7X(b)en2lp 4547
[Enderton] p. 207Exercise 34opthreg 4549
[Enderton] p. 208Exercise 35suc11g 4550
[Geuvers], p. 1Remarkexpap0 10518
[Geuvers], p. 6Lemma 2.13mulap0r 8546
[Geuvers], p. 6Lemma 2.15mulap0 8584
[Geuvers], p. 9Lemma 2.35msqge0 8547
[Geuvers], p. 9Definition 3.1(2)ax-arch 7905
[Geuvers], p. 10Lemma 3.9maxcom 11178
[Geuvers], p. 10Lemma 3.10maxle1 11186  maxle2 11187
[Geuvers], p. 10Lemma 3.11maxleast 11188
[Geuvers], p. 10Lemma 3.12maxleb 11191
[Geuvers], p. 11Definition 3.13dfabsmax 11192
[Geuvers], p. 17Definition 6.1df-ap 8513
[Gleason] p. 117Proposition 9-2.1df-enq 7321  enqer 7332
[Gleason] p. 117Proposition 9-2.2df-1nqqs 7325  df-nqqs 7322
[Gleason] p. 117Proposition 9-2.3df-plpq 7318  df-plqqs 7323
[Gleason] p. 119Proposition 9-2.4df-mpq 7319  df-mqqs 7324
[Gleason] p. 119Proposition 9-2.5df-rq 7326
[Gleason] p. 119Proposition 9-2.6ltexnqq 7382
[Gleason] p. 120Proposition 9-2.6(i)halfnq 7385  ltbtwnnq 7390  ltbtwnnqq 7389
[Gleason] p. 120Proposition 9-2.6(ii)ltanqg 7374
[Gleason] p. 120Proposition 9-2.6(iii)ltmnqg 7375
[Gleason] p. 123Proposition 9-3.5addclpr 7511
[Gleason] p. 123Proposition 9-3.5(i)addassprg 7553
[Gleason] p. 123Proposition 9-3.5(ii)addcomprg 7552
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 7571
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 7587
[Gleason] p. 123Proposition 9-3.5(v)ltaprg 7593  ltaprlem 7592
[Gleason] p. 123Proposition 9-3.5(vi)addcanprg 7590
[Gleason] p. 124Proposition 9-3.7mulclpr 7546
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 7566
[Gleason] p. 124Proposition 9-3.7(i)mulassprg 7555
[Gleason] p. 124Proposition 9-3.7(ii)mulcomprg 7554
[Gleason] p. 124Proposition 9-3.7(iii)distrprg 7562
[Gleason] p. 124Proposition 9-3.7(v)recexpr 7612
[Gleason] p. 126Proposition 9-4.1df-enr 7700  enrer 7709
[Gleason] p. 126Proposition 9-4.2df-0r 7705  df-1r 7706  df-nr 7701
[Gleason] p. 126Proposition 9-4.3df-mr 7703  df-plr 7702  negexsr 7746  recexsrlem 7748
[Gleason] p. 127Proposition 9-4.4df-ltr 7704
[Gleason] p. 130Proposition 10-1.3creui 8888  creur 8887  cru 8533
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 7897  axcnre 7855
[Gleason] p. 132Definition 10-3.1crim 10833  crimd 10952  crimi 10912  crre 10832  crred 10951  crrei 10911
[Gleason] p. 132Definition 10-3.2remim 10835  remimd 10917
[Gleason] p. 133Definition 10.36absval2 11032  absval2d 11160  absval2i 11119
[Gleason] p. 133Proposition 10-3.4(a)cjadd 10859  cjaddd 10940  cjaddi 10907
[Gleason] p. 133Proposition 10-3.4(c)cjmul 10860  cjmuld 10941  cjmuli 10908
[Gleason] p. 133Proposition 10-3.4(e)cjcj 10858  cjcjd 10918  cjcji 10890
[Gleason] p. 133Proposition 10-3.4(f)cjre 10857  cjreb 10841  cjrebd 10921  cjrebi 10893  cjred 10946  rere 10840  rereb 10838  rerebd 10920  rerebi 10892  rered 10944
[Gleason] p. 133Proposition 10-3.4(h)addcj 10866  addcjd 10932  addcji 10902
[Gleason] p. 133Proposition 10-3.7(a)absval 10976
[Gleason] p. 133Proposition 10-3.7(b)abscj 11027  abscjd 11165  abscji 11123
[Gleason] p. 133Proposition 10-3.7(c)abs00 11039  abs00d 11161  abs00i 11120  absne0d 11162
[Gleason] p. 133Proposition 10-3.7(d)releabs 11071  releabsd 11166  releabsi 11124
[Gleason] p. 133Proposition 10-3.7(f)absmul 11044  absmuld 11169  absmuli 11126
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11030  sqabsaddi 11127
[Gleason] p. 133Proposition 10-3.7(h)abstri 11079  abstrid 11171  abstrii 11130
[Gleason] p. 134Definition 10-4.1df-exp 10488  exp0 10492  expp1 10495  expp1d 10622
[Gleason] p. 135Proposition 10-4.2(a)expadd 10530  expaddd 10623
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 13884  cxpmuld 13907  expmul 10533  expmuld 10624
[Gleason] p. 135Proposition 10-4.2(c)mulexp 10527  mulexpd 10636  rpmulcxp 13881
[Gleason] p. 141Definition 11-2.1fzval 9979
[Gleason] p. 168Proposition 12-2.1(a)climadd 11300
[Gleason] p. 168Proposition 12-2.1(b)climsub 11302
[Gleason] p. 168Proposition 12-2.1(c)climmul 11301
[Gleason] p. 171Corollary 12-2.2climmulc2 11305
[Gleason] p. 172Corollary 12-2.5climrecl 11298
[Gleason] p. 172Proposition 12-2.4(c)climabs 11294  climcj 11295  climim 11297  climre 11296
[Gleason] p. 173Definition 12-3.1df-ltxr 7971  df-xr 7970  ltxr 9744
[Gleason] p. 180Theorem 12-5.3climcau 11321
[Gleason] p. 217Lemma 13-4.1btwnzge0 10268
[Gleason] p. 223Definition 14-1.1df-met 13040
[Gleason] p. 223Definition 14-1.1(a)met0 13415  xmet0 13414
[Gleason] p. 223Definition 14-1.1(c)metsym 13422
[Gleason] p. 223Definition 14-1.1(d)mettri 13424  mstri 13524  xmettri 13423  xmstri 13523
[Gleason] p. 230Proposition 14-2.6txlm 13330
[Gleason] p. 240Proposition 14-4.2metcnp3 13562
[Gleason] p. 243Proposition 14-4.16addcn2 11284  addcncntop 13603  mulcn2 11286  mulcncntop 13605  subcn2 11285  subcncntop 13604
[Gleason] p. 295Remarkbcval3 10697  bcval4 10698
[Gleason] p. 295Equation 2bcpasc 10712
[Gleason] p. 295Definition of binomial coefficientbcval 10695  df-bc 10694
[Gleason] p. 296Remarkbcn0 10701  bcnn 10703
[Gleason] p. 296Theorem 15-2.8binom 11458
[Gleason] p. 308Equation 2ef0 11646
[Gleason] p. 308Equation 3efcj 11647
[Gleason] p. 309Corollary 15-4.3efne0 11652
[Gleason] p. 309Corollary 15-4.4efexp 11656
[Gleason] p. 310Equation 14sinadd 11710
[Gleason] p. 310Equation 15cosadd 11711
[Gleason] p. 311Equation 17sincossq 11722
[Gleason] p. 311Equation 18cosbnd 11727  sinbnd 11726
[Gleason] p. 311Definition of ` `df-pi 11627
[Golan] p. 1Remarksrgisid 12962
[Golan] p. 1Definitiondf-srg 12940
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1447
[Herstein] p. 55Lemma 2.2.1(a)grpideu 12748  mndideu 12691
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 12771
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 12796
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 12807
[Herstein] p. 57Exercise 1dfgrp3me 12829
[Heyting] p. 127Axiom #1ax1hfs 14360
[Hitchcock] p. 5Rule A3mptnan 1423
[Hitchcock] p. 5Rule A4mptxor 1424
[Hitchcock] p. 5Rule A5mtpxor 1426
[HoTT], p. Lemma 10.4.1exmidontriim 7214
[HoTT], p. Theorem 7.2.6nndceq 6490
[HoTT], p. Exercise 11.10neapmkv 14356
[HoTT], p. Exercise 11.11mulap0bd 8587
[HoTT], p. Section 11.2.1df-iltp 7444  df-imp 7443  df-iplp 7442  df-reap 8506
[HoTT], p. Theorem 11.2.12cauappcvgpr 7636
[HoTT], p. Corollary 11.4.3conventions 14013
[HoTT], p. Exercise 11.6(i)dcapnconst 14349  dceqnconst 14348
[HoTT], p. Corollary 11.2.13axcaucvg 7874  caucvgpr 7656  caucvgprpr 7686  caucvgsr 7776
[HoTT], p. Definition 11.2.1df-inp 7440
[HoTT], p. Exercise 11.6(ii)nconstwlpo 14354
[HoTT], p. Proposition 11.2.3df-iso 4291  ltpopr 7569  ltsopr 7570
[HoTT], p. Definition 11.2.7(v)apsym 8537  reapcotr 8529  reapirr 8508
[HoTT], p. Definition 11.2.7(vi)0lt1 8058  gt0add 8504  leadd1 8361  lelttr 8020  lemul1a 8786  lenlt 8007  ltadd1 8360  ltletr 8021  ltmul1 8523  reaplt 8519
[Jech] p. 4Definition of classcv 1352  cvjust 2170
[Jech] p. 78Noteopthprc 4671
[KalishMontague] p. 81Note 1ax-i9 1528
[Kreyszig] p. 3Property M1metcl 13404  xmetcl 13403
[Kreyszig] p. 4Property M2meteq0 13411
[Kreyszig] p. 12Equation 5muleqadd 8598
[Kreyszig] p. 18Definition 1.3-2mopnval 13493
[Kreyszig] p. 19Remarkmopntopon 13494
[Kreyszig] p. 19Theorem T1mopn0 13539  mopnm 13499
[Kreyszig] p. 19Theorem T2unimopn 13537
[Kreyszig] p. 19Definition of neighborhoodneibl 13542
[Kreyszig] p. 20Definition 1.3-3metcnp2 13564
[Kreyszig] p. 25Definition 1.4-1lmbr 13264
[Kunen] p. 10Axiom 0a9e 1694
[Kunen] p. 12Axiom 6zfrep6 4115
[Kunen] p. 24Definition 10.24mapval 6650  mapvalg 6648
[Kunen] p. 31Definition 10.24mapex 6644
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3892
[Lang] p. 3Statementlidrideqd 12664  mndbn0 12696
[Lang] p. 3Definitiondf-mnd 12682
[Lang] p. 7Definitiondfgrp2e 12763
[Levy] p. 338Axiomdf-clab 2162  df-clel 2171  df-cleq 2168
[Lopez-Astorga] p. 12Rule 1mptnan 1423
[Lopez-Astorga] p. 12Rule 2mptxor 1424
[Lopez-Astorga] p. 12Rule 3mtpxor 1426
[Margaris] p. 40Rule Cexlimiv 1596
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3condc 853
[Margaris] p. 49Definitiondfbi2 388  dfordc 892  exalim 1500
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 45
[Margaris] p. 60Theorem 8jcn 651
[Margaris] p. 89Theorem 19.219.2 1636  r19.2m 3507
[Margaris] p. 89Theorem 19.319.3 1552  19.3h 1551  rr19.3v 2874
[Margaris] p. 89Theorem 19.5alcom 1476
[Margaris] p. 89Theorem 19.6alexdc 1617  alexim 1643
[Margaris] p. 89Theorem 19.7alnex 1497
[Margaris] p. 89Theorem 19.819.8a 1588  spsbe 1840
[Margaris] p. 89Theorem 19.919.9 1642  19.9h 1641  19.9v 1869  exlimd 1595
[Margaris] p. 89Theorem 19.11excom 1662  excomim 1661
[Margaris] p. 89Theorem 19.1219.12 1663  r19.12 2581
[Margaris] p. 90Theorem 19.14exnalim 1644
[Margaris] p. 90Theorem 19.15albi 1466  ralbi 2607
[Margaris] p. 90Theorem 19.1619.16 1553
[Margaris] p. 90Theorem 19.1719.17 1554
[Margaris] p. 90Theorem 19.18exbi 1602  rexbi 2608
[Margaris] p. 90Theorem 19.1919.19 1664
[Margaris] p. 90Theorem 19.20alim 1455  alimd 1519  alimdh 1465  alimdv 1877  ralimdaa 2541  ralimdv 2543  ralimdva 2542  ralimdvva 2544  sbcimdv 3026
[Margaris] p. 90Theorem 19.2119.21-2 1665  19.21 1581  19.21bi 1556  19.21h 1555  19.21ht 1579  19.21t 1580  19.21v 1871  alrimd 1608  alrimdd 1607  alrimdh 1477  alrimdv 1874  alrimi 1520  alrimih 1467  alrimiv 1872  alrimivv 1873  r19.21 2551  r19.21be 2566  r19.21bi 2563  r19.21t 2550  r19.21v 2552  ralrimd 2553  ralrimdv 2554  ralrimdva 2555  ralrimdvv 2559  ralrimdvva 2560  ralrimi 2546  ralrimiv 2547  ralrimiva 2548  ralrimivv 2556  ralrimivva 2557  ralrimivvva 2558  ralrimivw 2549  rexlimi 2585
[Margaris] p. 90Theorem 19.222alimdv 1879  2eximdv 1880  exim 1597  eximd 1610  eximdh 1609  eximdv 1878  rexim 2569  reximdai 2573  reximddv 2578  reximddv2 2580  reximdv 2576  reximdv2 2574  reximdva 2577  reximdvai 2575  reximi2 2571
[Margaris] p. 90Theorem 19.2319.23 1676  19.23bi 1590  19.23h 1496  19.23ht 1495  19.23t 1675  19.23v 1881  19.23vv 1882  exlimd2 1593  exlimdh 1594  exlimdv 1817  exlimdvv 1895  exlimi 1592  exlimih 1591  exlimiv 1596  exlimivv 1894  r19.23 2583  r19.23v 2584  rexlimd 2589  rexlimdv 2591  rexlimdv3a 2594  rexlimdva 2592  rexlimdva2 2595  rexlimdvaa 2593  rexlimdvv 2599  rexlimdvva 2600  rexlimdvw 2596  rexlimiv 2586  rexlimiva 2587  rexlimivv 2598
[Margaris] p. 90Theorem 19.24i19.24 1637
[Margaris] p. 90Theorem 19.2519.25 1624
[Margaris] p. 90Theorem 19.2619.26-2 1480  19.26-3an 1481  19.26 1479  r19.26-2 2604  r19.26-3 2605  r19.26 2601  r19.26m 2606
[Margaris] p. 90Theorem 19.2719.27 1559  19.27h 1558  19.27v 1897  r19.27av 2610  r19.27m 3516  r19.27mv 3517
[Margaris] p. 90Theorem 19.2819.28 1561  19.28h 1560  19.28v 1898  r19.28av 2611  r19.28m 3510  r19.28mv 3513  rr19.28v 2875
[Margaris] p. 90Theorem 19.2919.29 1618  19.29r 1619  19.29r2 1620  19.29x 1621  r19.29 2612  r19.29d2r 2619  r19.29r 2613
[Margaris] p. 90Theorem 19.3019.30dc 1625
[Margaris] p. 90Theorem 19.3119.31r 1679
[Margaris] p. 90Theorem 19.3219.32dc 1677  19.32r 1678  r19.32r 2621  r19.32vdc 2624  r19.32vr 2623
[Margaris] p. 90Theorem 19.3319.33 1482  19.33b2 1627  19.33bdc 1628
[Margaris] p. 90Theorem 19.3419.34 1682
[Margaris] p. 90Theorem 19.3519.35-1 1622  19.35i 1623
[Margaris] p. 90Theorem 19.3619.36-1 1671  19.36aiv 1899  19.36i 1670  r19.36av 2626
[Margaris] p. 90Theorem 19.3719.37-1 1672  19.37aiv 1673  r19.37 2627  r19.37av 2628
[Margaris] p. 90Theorem 19.3819.38 1674
[Margaris] p. 90Theorem 19.39i19.39 1638
[Margaris] p. 90Theorem 19.4019.40-2 1630  19.40 1629  r19.40 2629
[Margaris] p. 90Theorem 19.4119.41 1684  19.41h 1683  19.41v 1900  19.41vv 1901  19.41vvv 1902  19.41vvvv 1903  r19.41 2630  r19.41v 2631
[Margaris] p. 90Theorem 19.4219.42 1686  19.42h 1685  19.42v 1904  19.42vv 1909  19.42vvv 1910  19.42vvvv 1911  r19.42v 2632
[Margaris] p. 90Theorem 19.4319.43 1626  r19.43 2633
[Margaris] p. 90Theorem 19.4419.44 1680  r19.44av 2634  r19.44mv 3515
[Margaris] p. 90Theorem 19.4519.45 1681  r19.45av 2635  r19.45mv 3514
[Margaris] p. 110Exercise 2(b)eu1 2049
[Megill] p. 444Axiom C5ax-17 1524
[Megill] p. 445Lemma L12alequcom 1513  ax-10 1503
[Megill] p. 446Lemma L17equtrr 1708
[Megill] p. 446Lemma L19hbnae 1719
[Megill] p. 447Remark 9.1df-sb 1761  sbid 1772
[Megill] p. 448Scheme C5'ax-4 1508
[Megill] p. 448Scheme C6'ax-7 1446
[Megill] p. 448Scheme C8'ax-8 1502
[Megill] p. 448Scheme C9'ax-i12 1505
[Megill] p. 448Scheme C11'ax-10o 1714
[Megill] p. 448Scheme C12'ax-13 2148
[Megill] p. 448Scheme C13'ax-14 2149
[Megill] p. 448Scheme C15'ax-11o 1821
[Megill] p. 448Scheme C16'ax-16 1812
[Megill] p. 448Theorem 9.4dral1 1728  dral2 1729  drex1 1796  drex2 1730  drsb1 1797  drsb2 1839
[Megill] p. 449Theorem 9.7sbcom2 1985  sbequ 1838  sbid2v 1994
[Megill] p. 450Example in Appendixhba1 1538
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 3043  rspsbca 3044  stdpc4 1773
[Mendelson] p. 69Axiom 5ra5 3049  stdpc5 1582
[Mendelson] p. 81Rule Cexlimiv 1596
[Mendelson] p. 95Axiom 6stdpc6 1701
[Mendelson] p. 95Axiom 7stdpc7 1768
[Mendelson] p. 231Exercise 4.10(k)inv1 3457
[Mendelson] p. 231Exercise 4.10(l)unv 3458
[Mendelson] p. 231Exercise 4.10(n)inssun 3373
[Mendelson] p. 231Exercise 4.10(o)df-nul 3421
[Mendelson] p. 231Exercise 4.10(q)inssddif 3374
[Mendelson] p. 231Exercise 4.10(s)ddifnel 3264
[Mendelson] p. 231Definition of unionunssin 3372
[Mendelson] p. 235Exercise 4.12(c)univ 4470
[Mendelson] p. 235Exercise 4.12(d)pwv 3804
[Mendelson] p. 235Exercise 4.12(j)pwin 4276
[Mendelson] p. 235Exercise 4.12(k)pwunss 4277
[Mendelson] p. 235Exercise 4.12(l)pwssunim 4278
[Mendelson] p. 235Exercise 4.12(n)uniin 3825
[Mendelson] p. 235Exercise 4.12(p)reli 4749
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5141
[Mendelson] p. 246Definition of successordf-suc 4365
[Mendelson] p. 254Proposition 4.22(b)xpen 6835
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6811  xpsneng 6812
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6817  xpcomeng 6818
[Mendelson] p. 254Proposition 4.22(e)xpassen 6820
[Mendelson] p. 255Exercise 4.39endisj 6814
[Mendelson] p. 255Exercise 4.41mapprc 6642
[Mendelson] p. 255Exercise 4.43mapsnen 6801
[Mendelson] p. 255Exercise 4.47xpmapen 6840
[Mendelson] p. 255Exercise 4.42(a)map0e 6676
[Mendelson] p. 255Exercise 4.42(b)map1 6802
[Mendelson] p. 258Exercise 4.56(c)djuassen 7206  djucomen 7205
[Mendelson] p. 258Exercise 4.56(g)xp2dju 7204
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6458
[Monk1] p. 26Theorem 2.8(vii)ssin 3355
[Monk1] p. 33Theorem 3.2(i)ssrel 4708
[Monk1] p. 33Theorem 3.2(ii)eqrel 4709
[Monk1] p. 34Definition 3.3df-opab 4060
[Monk1] p. 36Theorem 3.7(i)coi1 5136  coi2 5137
[Monk1] p. 36Theorem 3.8(v)dm0 4834  rn0 4876
[Monk1] p. 36Theorem 3.7(ii)cnvi 5025
[Monk1] p. 37Theorem 3.13(i)relxp 4729
[Monk1] p. 37Theorem 3.13(x)dmxpm 4840  rnxpm 5050
[Monk1] p. 37Theorem 3.13(ii)0xp 4700  xp0 5040
[Monk1] p. 38Theorem 3.16(ii)ima0 4980
[Monk1] p. 38Theorem 3.16(viii)imai 4977
[Monk1] p. 39Theorem 3.17imaex 4976  imaexg 4975
[Monk1] p. 39Theorem 3.16(xi)imassrn 4974
[Monk1] p. 41Theorem 4.3(i)fnopfv 5638  funfvop 5620
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5551
[Monk1] p. 42Theorem 4.4(iii)fvelima 5559
[Monk1] p. 43Theorem 4.6funun 5252
[Monk1] p. 43Theorem 4.8(iv)dff13 5759  dff13f 5761
[Monk1] p. 46Theorem 4.15(v)funex 5731  funrnex 6105
[Monk1] p. 50Definition 5.4fniunfv 5753
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5104
[Monk1] p. 52Theorem 5.11(viii)ssint 3856
[Monk1] p. 52Definition 5.13 (i)1stval2 6146  df-1st 6131
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6147  df-2nd 6132
[Monk2] p. 105Axiom C4ax-5 1445
[Monk2] p. 105Axiom C7ax-8 1502
[Monk2] p. 105Axiom C8ax-11 1504  ax-11o 1821
[Monk2] p. 105Axiom (C8)ax11v 1825
[Monk2] p. 109Lemma 12ax-7 1446
[Monk2] p. 109Lemma 15equvin 1861  equvini 1756  eqvinop 4237
[Monk2] p. 113Axiom C5-1ax-17 1524
[Monk2] p. 113Axiom C5-2ax6b 1649
[Monk2] p. 113Axiom C5-3ax-7 1446
[Monk2] p. 114Lemma 22hba1 1538
[Monk2] p. 114Lemma 23hbia1 1550  nfia1 1578
[Monk2] p. 114Lemma 24hba2 1549  nfa2 1577
[Moschovakis] p. 2Chapter 2 df-stab 831  dftest 14361
[Munkres] p. 77Example 2distop 13136
[Munkres] p. 78Definition of basisdf-bases 13092  isbasis3g 13095
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 12629  tgval2 13102
[Munkres] p. 79Remarktgcl 13115
[Munkres] p. 80Lemma 2.1tgval3 13109
[Munkres] p. 80Lemma 2.2tgss2 13130  tgss3 13129
[Munkres] p. 81Lemma 2.3basgen 13131  basgen2 13132
[Munkres] p. 89Definition of subspace topologyresttop 13221
[Munkres] p. 93Theorem 6.1(1)0cld 13163  topcld 13160
[Munkres] p. 93Theorem 6.1(3)uncld 13164
[Munkres] p. 94Definition of closureclsval 13162
[Munkres] p. 94Definition of interiorntrval 13161
[Munkres] p. 102Definition of continuous functiondf-cn 13239  iscn 13248  iscn2 13251
[Munkres] p. 107Theorem 7.2(g)cncnp 13281  cncnp2m 13282  cncnpi 13279  df-cnp 13240  iscnp 13250
[Munkres] p. 127Theorem 10.1metcn 13565
[Pierik], p. 8Section 2.2.1dfrex2fin 6893
[Pierik], p. 9Definition 2.4df-womni 7152
[Pierik], p. 9Definition 2.5df-markov 7140  omniwomnimkv 7155
[Pierik], p. 10Section 2.3dfdif3 3243
[Pierik], p. 14Definition 3.1df-omni 7123  exmidomniim 7129  finomni 7128
[Pierik], p. 15Section 3.1df-nninf 7109
[PradicBrown2022], p. 1Theorem 1exmidsbthr 14312
[PradicBrown2022], p. 2Remarkexmidpw 6898
[PradicBrown2022], p. 2Proposition 1.1exmidfodomrlemim 7190
[PradicBrown2022], p. 2Proposition 1.2exmidfodomrlemr 7191  exmidfodomrlemrALT 7192
[PradicBrown2022], p. 4Lemma 3.2fodjuomni 7137
[PradicBrown2022], p. 5Lemma 3.4peano3nninf 14297  peano4nninf 14296
[PradicBrown2022], p. 5Lemma 3.5nninfall 14299
[PradicBrown2022], p. 5Theorem 3.6nninfsel 14307
[PradicBrown2022], p. 5Corollary 3.7nninfomni 14309
[PradicBrown2022], p. 5Definition 3.3nnsf 14295
[Quine] p. 16Definition 2.1df-clab 2162  rabid 2650
[Quine] p. 17Definition 2.1''dfsb7 1989
[Quine] p. 18Definition 2.7df-cleq 2168
[Quine] p. 19Definition 2.9df-v 2737
[Quine] p. 34Theorem 5.1abeq2 2284
[Quine] p. 35Theorem 5.2abid2 2296  abid2f 2343
[Quine] p. 40Theorem 6.1sb5 1885
[Quine] p. 40Theorem 6.2sb56 1883  sb6 1884
[Quine] p. 41Theorem 6.3df-clel 2171
[Quine] p. 41Theorem 6.4eqid 2175
[Quine] p. 41Theorem 6.5eqcom 2177
[Quine] p. 42Theorem 6.6df-sbc 2961
[Quine] p. 42Theorem 6.7dfsbcq 2962  dfsbcq2 2963
[Quine] p. 43Theorem 6.8vex 2738
[Quine] p. 43Theorem 6.9isset 2741
[Quine] p. 44Theorem 7.3spcgf 2817  spcgv 2822  spcimgf 2815
[Quine] p. 44Theorem 6.11spsbc 2972  spsbcd 2973
[Quine] p. 44Theorem 6.12elex 2746
[Quine] p. 44Theorem 6.13elab 2879  elabg 2881  elabgf 2877
[Quine] p. 44Theorem 6.14noel 3424
[Quine] p. 48Theorem 7.2snprc 3654
[Quine] p. 48Definition 7.1df-pr 3596  df-sn 3595
[Quine] p. 49Theorem 7.4snss 3724  snssg 3723
[Quine] p. 49Theorem 7.5prss 3745  prssg 3746
[Quine] p. 49Theorem 7.6prid1 3695  prid1g 3693  prid2 3696  prid2g 3694  snid 3620  snidg 3618
[Quine] p. 51Theorem 7.12snexg 4179  snexprc 4181
[Quine] p. 51Theorem 7.13prexg 4205
[Quine] p. 53Theorem 8.2unisn 3821  unisng 3822
[Quine] p. 53Theorem 8.3uniun 3824
[Quine] p. 54Theorem 8.6elssuni 3833
[Quine] p. 54Theorem 8.7uni0 3832
[Quine] p. 56Theorem 8.17uniabio 5180
[Quine] p. 56Definition 8.18dfiota2 5171
[Quine] p. 57Theorem 8.19iotaval 5181
[Quine] p. 57Theorem 8.22iotanul 5185
[Quine] p. 58Theorem 8.23euiotaex 5186
[Quine] p. 58Definition 9.1df-op 3598
[Quine] p. 61Theorem 9.5opabid 4251  opelopab 4265  opelopaba 4260  opelopabaf 4267  opelopabf 4268  opelopabg 4262  opelopabga 4257  oprabid 5897
[Quine] p. 64Definition 9.11df-xp 4626
[Quine] p. 64Definition 9.12df-cnv 4628
[Quine] p. 64Definition 9.15df-id 4287
[Quine] p. 65Theorem 10.3fun0 5266
[Quine] p. 65Theorem 10.4funi 5240
[Quine] p. 65Theorem 10.5funsn 5256  funsng 5254
[Quine] p. 65Definition 10.1df-fun 5210
[Quine] p. 65Definition 10.2args 4990  dffv4g 5504
[Quine] p. 68Definition 10.11df-fv 5216  fv2 5502
[Quine] p. 124Theorem 17.3nn0opth2 10670  nn0opth2d 10669  nn0opthd 10668
[Quine] p. 284Axiom 39(vi)funimaex 5293  funimaexg 5292
[Roman] p. 19Part Preliminariesdf-ring 12974
[Rudin] p. 164Equation 27efcan 11650
[Rudin] p. 164Equation 30efzval 11657
[Rudin] p. 167Equation 48absefi 11742
[Sanford] p. 39Remarkax-mp 5
[Sanford] p. 39Rule 3mtpxor 1426
[Sanford] p. 39Rule 4mptxor 1424
[Sanford] p. 40Rule 1mptnan 1423
[Schechter] p. 51Definition of antisymmetryintasym 5005
[Schechter] p. 51Definition of irreflexivityintirr 5007
[Schechter] p. 51Definition of symmetrycnvsym 5004
[Schechter] p. 51Definition of transitivitycotr 5002
[Schechter] p. 187Definition of ring with unitisring 12976
[Schechter] p. 428Definition 15.35bastop1 13134
[Stoll] p. 13Definition of symmetric differencesymdif1 3398
[Stoll] p. 16Exercise 4.40dif 3492  dif0 3491
[Stoll] p. 16Exercise 4.8difdifdirss 3505
[Stoll] p. 19Theorem 5.2(13)undm 3391
[Stoll] p. 19Theorem 5.2(13')indmss 3392
[Stoll] p. 20Remarkinvdif 3375
[Stoll] p. 25Definition of ordered tripledf-ot 3599
[Stoll] p. 43Definitionuniiun 3935
[Stoll] p. 44Definitionintiin 3936
[Stoll] p. 45Definitiondf-iin 3885
[Stoll] p. 45Definition indexed uniondf-iun 3884
[Stoll] p. 176Theorem 3.4(27)imandc 889  imanst 888
[Stoll] p. 262Example 4.1symdif1 3398
[Suppes] p. 22Theorem 2eq0 3439
[Suppes] p. 22Theorem 4eqss 3168  eqssd 3170  eqssi 3169
[Suppes] p. 23Theorem 5ss0 3461  ss0b 3460
[Suppes] p. 23Theorem 6sstr 3161
[Suppes] p. 25Theorem 12elin 3316  elun 3274
[Suppes] p. 26Theorem 15inidm 3342
[Suppes] p. 26Theorem 16in0 3455
[Suppes] p. 27Theorem 23unidm 3276
[Suppes] p. 27Theorem 24un0 3454
[Suppes] p. 27Theorem 25ssun1 3296
[Suppes] p. 27Theorem 26ssequn1 3303
[Suppes] p. 27Theorem 27unss 3307
[Suppes] p. 27Theorem 28indir 3382
[Suppes] p. 27Theorem 29undir 3383
[Suppes] p. 28Theorem 32difid 3489  difidALT 3490
[Suppes] p. 29Theorem 33difin 3370
[Suppes] p. 29Theorem 34indif 3376
[Suppes] p. 29Theorem 35undif1ss 3495
[Suppes] p. 29Theorem 36difun2 3500
[Suppes] p. 29Theorem 37difin0 3494
[Suppes] p. 29Theorem 38disjdif 3493
[Suppes] p. 29Theorem 39difundi 3385
[Suppes] p. 29Theorem 40difindiss 3387
[Suppes] p. 30Theorem 41nalset 4128
[Suppes] p. 39Theorem 61uniss 3826
[Suppes] p. 39Theorem 65uniop 4249
[Suppes] p. 41Theorem 70intsn 3875
[Suppes] p. 42Theorem 71intpr 3872  intprg 3873
[Suppes] p. 42Theorem 73op1stb 4472  op1stbg 4473
[Suppes] p. 42Theorem 78intun 3871
[Suppes] p. 44Definition 15(a)dfiun2 3916  dfiun2g 3914
[Suppes] p. 44Definition 15(b)dfiin2 3917
[Suppes] p. 47Theorem 86elpw 3578  elpw2 4152  elpw2g 4151  elpwg 3580
[Suppes] p. 47Theorem 87pwid 3587
[Suppes] p. 47Theorem 89pw0 3736
[Suppes] p. 48Theorem 90pwpw0ss 3800
[Suppes] p. 52Theorem 101xpss12 4727
[Suppes] p. 52Theorem 102xpindi 4755  xpindir 4756
[Suppes] p. 52Theorem 103xpundi 4676  xpundir 4677
[Suppes] p. 54Theorem 105elirrv 4541
[Suppes] p. 58Theorem 2relss 4707
[Suppes] p. 59Theorem 4eldm 4817  eldm2 4818  eldm2g 4816  eldmg 4815
[Suppes] p. 59Definition 3df-dm 4630
[Suppes] p. 60Theorem 6dmin 4828
[Suppes] p. 60Theorem 8rnun 5029
[Suppes] p. 60Theorem 9rnin 5030
[Suppes] p. 60Definition 4dfrn2 4808
[Suppes] p. 61Theorem 11brcnv 4803  brcnvg 4801
[Suppes] p. 62Equation 5elcnv 4797  elcnv2 4798
[Suppes] p. 62Theorem 12relcnv 4999
[Suppes] p. 62Theorem 15cnvin 5028
[Suppes] p. 62Theorem 16cnvun 5026
[Suppes] p. 63Theorem 20co02 5134
[Suppes] p. 63Theorem 21dmcoss 4889
[Suppes] p. 63Definition 7df-co 4629
[Suppes] p. 64Theorem 26cnvco 4805
[Suppes] p. 64Theorem 27coass 5139
[Suppes] p. 65Theorem 31resundi 4913
[Suppes] p. 65Theorem 34elima 4968  elima2 4969  elima3 4970  elimag 4967
[Suppes] p. 65Theorem 35imaundi 5033
[Suppes] p. 66Theorem 40dminss 5035
[Suppes] p. 66Theorem 41imainss 5036
[Suppes] p. 67Exercise 11cnvxp 5039
[Suppes] p. 81Definition 34dfec2 6528
[Suppes] p. 82Theorem 72elec 6564  elecg 6563
[Suppes] p. 82Theorem 73erth 6569  erth2 6570
[Suppes] p. 89Theorem 96map0b 6677
[Suppes] p. 89Theorem 97map0 6679  map0g 6678
[Suppes] p. 89Theorem 98mapsn 6680
[Suppes] p. 89Theorem 99mapss 6681
[Suppes] p. 92Theorem 1enref 6755  enrefg 6754
[Suppes] p. 92Theorem 2ensym 6771  ensymb 6770  ensymi 6772
[Suppes] p. 92Theorem 3entr 6774
[Suppes] p. 92Theorem 4unen 6806
[Suppes] p. 94Theorem 15endom 6753
[Suppes] p. 94Theorem 16ssdomg 6768
[Suppes] p. 94Theorem 17domtr 6775
[Suppes] p. 95Theorem 18isbth 6956
[Suppes] p. 98Exercise 4fundmen 6796  fundmeng 6797
[Suppes] p. 98Exercise 6xpdom3m 6824
[Suppes] p. 130Definition 3df-tr 4097
[Suppes] p. 132Theorem 9ssonuni 4481
[Suppes] p. 134Definition 6df-suc 4365
[Suppes] p. 136Theorem Schema 22findes 4596  finds 4593  finds1 4595  finds2 4594
[Suppes] p. 162Definition 5df-ltnqqs 7327  df-ltpq 7320
[Suppes] p. 228Theorem Schema 61onintss 4384
[TakeutiZaring] p. 8Axiom 1ax-ext 2157
[TakeutiZaring] p. 13Definition 4.5df-cleq 2168
[TakeutiZaring] p. 13Proposition 4.6df-clel 2171
[TakeutiZaring] p. 13Proposition 4.9cvjust 2170
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2193
[TakeutiZaring] p. 14Definition 4.16df-oprab 5869
[TakeutiZaring] p. 14Proposition 4.14ru 2959
[TakeutiZaring] p. 15Exercise 1elpr 3610  elpr2 3611  elprg 3609
[TakeutiZaring] p. 15Exercise 2elsn 3605  elsn2 3623  elsn2g 3622  elsng 3604  velsn 3606
[TakeutiZaring] p. 15Exercise 3elop 4225
[TakeutiZaring] p. 15Exercise 4sneq 3600  sneqr 3756
[TakeutiZaring] p. 15Definition 5.1dfpr2 3608  dfsn2 3603
[TakeutiZaring] p. 16Axiom 3uniex 4431
[TakeutiZaring] p. 16Exercise 6opth 4231
[TakeutiZaring] p. 16Exercise 8rext 4209
[TakeutiZaring] p. 16Corollary 5.8unex 4435  unexg 4437
[TakeutiZaring] p. 16Definition 5.3dftp2 3638
[TakeutiZaring] p. 16Definition 5.5df-uni 3806
[TakeutiZaring] p. 16Definition 5.6df-in 3133  df-un 3131
[TakeutiZaring] p. 16Proposition 5.7unipr 3819  uniprg 3820
[TakeutiZaring] p. 17Axiom 4vpwex 4174
[TakeutiZaring] p. 17Exercise 1eltp 3637
[TakeutiZaring] p. 17Exercise 5elsuc 4400  elsucg 4398  sstr2 3160
[TakeutiZaring] p. 17Exercise 6uncom 3277
[TakeutiZaring] p. 17Exercise 7incom 3325
[TakeutiZaring] p. 17Exercise 8unass 3290
[TakeutiZaring] p. 17Exercise 9inass 3343
[TakeutiZaring] p. 17Exercise 10indi 3380
[TakeutiZaring] p. 17Exercise 11undi 3381
[TakeutiZaring] p. 17Definition 5.9dfss2 3142
[TakeutiZaring] p. 17Definition 5.10df-pw 3574
[TakeutiZaring] p. 18Exercise 7unss2 3304
[TakeutiZaring] p. 18Exercise 9df-ss 3140  sseqin2 3352
[TakeutiZaring] p. 18Exercise 10ssid 3173
[TakeutiZaring] p. 18Exercise 12inss1 3353  inss2 3354
[TakeutiZaring] p. 18Exercise 13nssr 3213
[TakeutiZaring] p. 18Exercise 15unieq 3814
[TakeutiZaring] p. 18Exercise 18sspwb 4210
[TakeutiZaring] p. 18Exercise 19pweqb 4217
[TakeutiZaring] p. 20Definitiondf-rab 2462
[TakeutiZaring] p. 20Corollary 5.160ex 4125
[TakeutiZaring] p. 20Definition 5.12df-dif 3129
[TakeutiZaring] p. 20Definition 5.14dfnul2 3422
[TakeutiZaring] p. 20Proposition 5.15difid 3489  difidALT 3490
[TakeutiZaring] p. 20Proposition 5.17(1)n0rf 3433
[TakeutiZaring] p. 21Theorem 5.22setind 4532
[TakeutiZaring] p. 21Definition 5.20df-v 2737
[TakeutiZaring] p. 21Proposition 5.21vprc 4130
[TakeutiZaring] p. 22Exercise 10ss 3459
[TakeutiZaring] p. 22Exercise 3ssex 4135  ssexg 4137
[TakeutiZaring] p. 22Exercise 4inex1 4132
[TakeutiZaring] p. 22Exercise 5ruv 4543
[TakeutiZaring] p. 22Exercise 6elirr 4534
[TakeutiZaring] p. 22Exercise 7ssdif0im 3485
[TakeutiZaring] p. 22Exercise 11difdif 3258
[TakeutiZaring] p. 22Exercise 13undif3ss 3394
[TakeutiZaring] p. 22Exercise 14difss 3259
[TakeutiZaring] p. 22Exercise 15sscon 3267
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2458
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2459
[TakeutiZaring] p. 23Proposition 6.2xpex 4735  xpexg 4734  xpexgALT 6124
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4627
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5272
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5424  fun11 5275
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5219  svrelfun 5273
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4807
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4809
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4632
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4633
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4629
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5075  dfrel2 5071
[TakeutiZaring] p. 25Exercise 3xpss 4728
[TakeutiZaring] p. 25Exercise 5relun 4737
[TakeutiZaring] p. 25Exercise 6reluni 4743
[TakeutiZaring] p. 25Exercise 9inxp 4754
[TakeutiZaring] p. 25Exercise 12relres 4928
[TakeutiZaring] p. 25Exercise 13opelres 4905  opelresg 4907
[TakeutiZaring] p. 25Exercise 14dmres 4921
[TakeutiZaring] p. 25Exercise 15resss 4924
[TakeutiZaring] p. 25Exercise 17resabs1 4929
[TakeutiZaring] p. 25Exercise 18funres 5249
[TakeutiZaring] p. 25Exercise 24relco 5119
[TakeutiZaring] p. 25Exercise 29funco 5248
[TakeutiZaring] p. 25Exercise 30f1co 5425
[TakeutiZaring] p. 26Definition 6.10eu2 2068
[TakeutiZaring] p. 26Definition 6.11df-fv 5216  fv3 5530
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5159  cnvexg 5158
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4886  dmexg 4884
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4887  rnexg 4885
[TakeutiZaring] p. 27Corollary 6.13funfvex 5524
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5534  tz6.12 5535  tz6.12c 5537
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5498
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5211
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5212
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5214  wfo 5206
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5213  wf1 5205
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5215  wf1o 5207
[TakeutiZaring] p. 28Exercise 4eqfnfv 5605  eqfnfv2 5606  eqfnfv2f 5609
[TakeutiZaring] p. 28Exercise 5fvco 5578
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5730  fnexALT 6102
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5729  resfunexgALT 6099
[TakeutiZaring] p. 29Exercise 9funimaex 5293  funimaexg 5292
[TakeutiZaring] p. 29Definition 6.18df-br 3999
[TakeutiZaring] p. 30Definition 6.21eliniseg 4991  iniseg 4993
[TakeutiZaring] p. 30Definition 6.22df-eprel 4283
[TakeutiZaring] p. 32Definition 6.28df-isom 5217
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5801
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5802
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5807
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5809
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5817
[TakeutiZaring] p. 35Notationwtr 4096
[TakeutiZaring] p. 35Theorem 7.2tz7.2 4348
[TakeutiZaring] p. 35Definition 7.1dftr3 4100
[TakeutiZaring] p. 36Proposition 7.4ordwe 4569
[TakeutiZaring] p. 36Proposition 7.6ordelord 4375
[TakeutiZaring] p. 37Proposition 7.9ordin 4379
[TakeutiZaring] p. 38Corollary 7.15ordsson 4485
[TakeutiZaring] p. 38Definition 7.11df-on 4362
[TakeutiZaring] p. 38Proposition 7.12ordon 4479
[TakeutiZaring] p. 38Proposition 7.13onprc 4545
[TakeutiZaring] p. 39Theorem 7.17tfi 4575
[TakeutiZaring] p. 40Exercise 7dftr2 4098
[TakeutiZaring] p. 40Exercise 11unon 4504
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4480
[TakeutiZaring] p. 40Proposition 7.20elssuni 3833
[TakeutiZaring] p. 41Definition 7.22df-suc 4365
[TakeutiZaring] p. 41Proposition 7.23sssucid 4409  sucidg 4410
[TakeutiZaring] p. 41Proposition 7.24suceloni 4494
[TakeutiZaring] p. 42Exercise 1df-ilim 4363
[TakeutiZaring] p. 42Exercise 8onsucssi 4499  ordelsuc 4498
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4587
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4588
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4589
[TakeutiZaring] p. 43Axiom 7omex 4586
[TakeutiZaring] p. 43Theorem 7.32ordom 4600
[TakeutiZaring] p. 43Corollary 7.31find 4592
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4590
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4591
[TakeutiZaring] p. 44Exercise 2int0 3854
[TakeutiZaring] p. 44Exercise 3trintssm 4112
[TakeutiZaring] p. 44Exercise 4intss1 3855
[TakeutiZaring] p. 44Exercise 6onintonm 4510
[TakeutiZaring] p. 44Definition 7.35df-int 3841
[TakeutiZaring] p. 47Lemma 1tfrlem1 6299
[TakeutiZaring] p. 47Theorem 7.41(1)tfri1 6356  tfri1d 6326
[TakeutiZaring] p. 47Theorem 7.41(2)tfri2 6357  tfri2d 6327
[TakeutiZaring] p. 47Theorem 7.41(3)tfri3 6358
[TakeutiZaring] p. 50Exercise 3smoiso 6293
[TakeutiZaring] p. 50Definition 7.46df-smo 6277
[TakeutiZaring] p. 56Definition 8.1oasuc 6455
[TakeutiZaring] p. 57Proposition 8.2oacl 6451
[TakeutiZaring] p. 57Proposition 8.3oa0 6448
[TakeutiZaring] p. 57Proposition 8.16omcl 6452
[TakeutiZaring] p. 58Proposition 8.4nnaord 6500  nnaordi 6499
[TakeutiZaring] p. 59Proposition 8.6iunss2 3927  uniss2 3836
[TakeutiZaring] p. 59Proposition 8.7oawordriexmid 6461
[TakeutiZaring] p. 59Proposition 8.9nnacl 6471
[TakeutiZaring] p. 62Exercise 5oaword1 6462
[TakeutiZaring] p. 62Definition 8.15om0 6449  omsuc 6463
[TakeutiZaring] p. 63Proposition 8.17nnmcl 6472
[TakeutiZaring] p. 63Proposition 8.19nnmord 6508  nnmordi 6507
[TakeutiZaring] p. 67Definition 8.30oei0 6450
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7176
[TakeutiZaring] p. 88Exercise 1en0 6785
[TakeutiZaring] p. 90Proposition 10.20nneneq 6847
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6848
[TakeutiZaring] p. 91Definition 10.29df-fin 6733  isfi 6751
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6821
[TakeutiZaring] p. 95Definition 10.42df-map 6640
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6838
[Tarski] p. 67Axiom B5ax-4 1508
[Tarski] p. 68Lemma 6equid 1699
[Tarski] p. 69Lemma 7equcomi 1702
[Tarski] p. 70Lemma 14spim 1736  spime 1739  spimeh 1737  spimh 1735
[Tarski] p. 70Lemma 16ax-11 1504  ax-11o 1821  ax11i 1712
[Tarski] p. 70Lemmas 16 and 17sb6 1884
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1524
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 2148  ax-14 2149
[WhiteheadRussell] p. 96Axiom *1.3olc 711
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 727
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 756
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 765
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 789
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 616
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 643
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 82
[WhiteheadRussell] p. 100Theorem *2.05imim2 55
[WhiteheadRussell] p. 100Theorem *2.06imim1 76
[WhiteheadRussell] p. 101Theorem *2.1pm2.1dc 837
[WhiteheadRussell] p. 101Theorem *2.06barbara 2122  syl 14
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 737
[WhiteheadRussell] p. 101Theorem *2.08id 19  idALT 20
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 836
[WhiteheadRussell] p. 101Theorem *2.12notnot 629
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 885
[WhiteheadRussell] p. 102Theorem *2.14notnotrdc 843
[WhiteheadRussell] p. 102Theorem *2.15con1dc 856
[WhiteheadRussell] p. 103Theorem *2.16con3 642
[WhiteheadRussell] p. 103Theorem *2.17condc 853
[WhiteheadRussell] p. 103Theorem *2.18pm2.18dc 855
[WhiteheadRussell] p. 104Theorem *2.2orc 712
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 775
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 617
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 621
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 893
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 907
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 40
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 768
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 769
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 804
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 805
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 803
[WhiteheadRussell] p. 105Definition *2.33df-3or 979
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 778
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 776
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 777
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 53
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 738
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 739
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 867  pm2.5gdc 866
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 862
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 740
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 741
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 742
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 655
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 656
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 722
[WhiteheadRussell] p. 107Theorem *2.54pm2.54dc 891
[WhiteheadRussell] p. 107Theorem *2.55orel1 725
[WhiteheadRussell] p. 107Theorem *2.56orel2 726
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 865
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 748
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 800
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 801
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 659
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 713  pm2.67 743
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 869  pm2.521gdc 868
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 747
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 810
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 894
[WhiteheadRussell] p. 108Theorem *2.69looinvdc 915
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 806
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 807
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 809
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 808
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 811
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 812
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 77
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 905
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 101
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 754
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 139
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 957
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 958
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 959
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 753
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 264
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 265
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 693
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 347
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 261
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 262
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 109  simplimdc 860
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 110  simprimdc 859
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 345
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 346
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 689
[WhiteheadRussell] p. 113Fact)pm3.45 597
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 333
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 331
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 332
[WhiteheadRussell] p. 113Theorem *3.44jao 755  pm3.44 715
[WhiteheadRussell] p. 113Theorem *3.47anim12 344
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 602
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 785
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 871
[WhiteheadRussell] p. 117Theorem *4.2biid 171
[WhiteheadRussell] p. 117Theorem *4.13notnotbdc 872
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 890
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 694
[WhiteheadRussell] p. 117Theorem *4.21bicom 140
[WhiteheadRussell] p. 117Theorem *4.22biantr 952  bitr 472
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 395
[WhiteheadRussell] p. 117Theorem *4.25oridm 757  pm4.25 758
[WhiteheadRussell] p. 118Theorem *4.3ancom 266
[WhiteheadRussell] p. 118Theorem *4.4andi 818
[WhiteheadRussell] p. 118Theorem *4.31orcom 728
[WhiteheadRussell] p. 118Theorem *4.32anass 401
[WhiteheadRussell] p. 118Theorem *4.33orass 767
[WhiteheadRussell] p. 118Theorem *4.36anbi1 466
[WhiteheadRussell] p. 118Theorem *4.37orbi1 792
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 605
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 822
[WhiteheadRussell] p. 118Definition *4.34df-3an 980
[WhiteheadRussell] p. 119Theorem *4.41ordi 816
[WhiteheadRussell] p. 119Theorem *4.42pm4.42r 971
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 949
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 779
[WhiteheadRussell] p. 119Theorem *4.45orabs 814  pm4.45 784  pm4.45im 334
[WhiteheadRussell] p. 119Theorem *10.2219.26 1479
[WhiteheadRussell] p. 120Theorem *4.5anordc 956
[WhiteheadRussell] p. 120Theorem *4.6imordc 897  imorr 721
[WhiteheadRussell] p. 120Theorem *4.7anclb 319
[WhiteheadRussell] p. 120Theorem *4.51ianordc 899
[WhiteheadRussell] p. 120Theorem *4.52pm4.52im 750
[WhiteheadRussell] p. 120Theorem *4.53pm4.53r 751
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 902
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 938
[WhiteheadRussell] p. 120Theorem *4.56ioran 752  pm4.56 780
[WhiteheadRussell] p. 120Theorem *4.57orandc 939  oranim 781
[WhiteheadRussell] p. 120Theorem *4.61annimim 686
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 898
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 886
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 900
[WhiteheadRussell] p. 120Theorem *4.65pm4.65r 687
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 901
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 887
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 389  pm4.71d 393  pm4.71i 391  pm4.71r 390  pm4.71rd 394  pm4.71ri 392
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 827
[WhiteheadRussell] p. 121Theorem *4.73iba 300
[WhiteheadRussell] p. 121Theorem *4.74biorf 744
[WhiteheadRussell] p. 121Theorem *4.76jcab 603  pm4.76 604
[WhiteheadRussell] p. 121Theorem *4.77jaob 710  pm4.77 799
[WhiteheadRussell] p. 121Theorem *4.78pm4.78i 782
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 903
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 707
[WhiteheadRussell] p. 122Theorem *4.81pm4.81dc 908
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 950
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 951
[WhiteheadRussell] p. 122Theorem *4.84imbi1 236
[WhiteheadRussell] p. 122Theorem *4.85imbi2 237
[WhiteheadRussell] p. 122Theorem *4.86bibi1 240
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 248  impexp 263  pm4.87 557
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 601
[WhiteheadRussell] p. 123Theorem *5.11pm5.11dc 909
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 910
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 912
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 911
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1389
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 828
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 904
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1394  pm5.18dc 883
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 706
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 695
[WhiteheadRussell] p. 124Theorem *5.22xordc 1392
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1397
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1398
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 895
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 475
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 249
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 242
[WhiteheadRussell] p. 125Theorem *5.6pm5.6dc 926  pm5.6r 927
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 954
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 348
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 453
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 609
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 917
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 610
[WhiteheadRussell] p. 125Theorem *5.41imdi 250  pm5.41 251
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 320
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 925
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 802
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 918
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 913
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 794
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 945
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 946
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 961
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 244
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 179
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 962
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1633
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1483
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1630
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1893
[WhiteheadRussell] p. 175Definition *14.02df-eu 2027
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2426
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2427
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2873
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3017
[WhiteheadRussell] p. 190Theorem *14.22iota4 5188
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5189
[WhiteheadRussell] p. 192Theorem *14.26eupick 2103  eupickbi 2106
[WhiteheadRussell] p. 235Definition *30.01df-fv 5216
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7179

  This page was last updated on 14-Aug-2016.
Copyright terms: Public domain
W3C HTML validation [external]