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 7108  fidcenum 6949
[AczelRathjen], p. 72Proposition 8.1.11fidcenum 6949
[AczelRathjen], p. 73Lemma 8.1.14enumct 7108
[AczelRathjen], p. 73Corollary 8.1.13ennnfone 12409
[AczelRathjen], p. 74Lemma 8.1.16xpfi 6923
[AczelRathjen], p. 74Remark 8.1.17unfiexmid 6911
[AczelRathjen], p. 74Theorem 8.1.19ctiunct 12424
[AczelRathjen], p. 75Corollary 8.1.20unct 12426
[AczelRathjen], p. 75Corollary 8.1.23qnnen 12415  znnen 12382
[AczelRathjen], p. 77Lemma 8.1.27omctfn 12427
[AczelRathjen], p. 78Theorem 8.1.28omiunct 12428
[AczelRathjen], p. 80Corollary 8.2.4df-ihash 10740
[AczelRathjen], p. 183Chapter 20ax-setind 4533
[Apostol] p. 18Theorem I.1addcan 8127  addcan2d 8132  addcan2i 8130  addcand 8131  addcani 8129
[Apostol] p. 18Theorem I.2negeu 8138
[Apostol] p. 18Theorem I.3negsub 8195  negsubd 8264  negsubi 8225
[Apostol] p. 18Theorem I.4negneg 8197  negnegd 8249  negnegi 8217
[Apostol] p. 18Theorem I.5subdi 8332  subdid 8361  subdii 8354  subdir 8333  subdird 8362  subdiri 8355
[Apostol] p. 18Theorem I.6mul01 8336  mul01d 8340  mul01i 8338  mul02 8334  mul02d 8339  mul02i 8337
[Apostol] p. 18Theorem I.9divrecapd 8739
[Apostol] p. 18Theorem I.10recrecapi 8690
[Apostol] p. 18Theorem I.12mul2neg 8345  mul2negd 8360  mul2negi 8353  mulneg1 8342  mulneg1d 8358  mulneg1i 8351
[Apostol] p. 18Theorem I.15divdivdivap 8659
[Apostol] p. 20Axiom 7rpaddcl 9664  rpaddcld 9699  rpmulcl 9665  rpmulcld 9700
[Apostol] p. 20Axiom 90nrp 9676
[Apostol] p. 20Theorem I.17lttri 8052
[Apostol] p. 20Theorem I.18ltadd1d 8485  ltadd1dd 8503  ltadd1i 8449
[Apostol] p. 20Theorem I.19ltmul1 8539  ltmul1a 8538  ltmul1i 8866  ltmul1ii 8874  ltmul2 8802  ltmul2d 9726  ltmul2dd 9740  ltmul2i 8869
[Apostol] p. 20Theorem I.210lt1 8074
[Apostol] p. 20Theorem I.23lt0neg1 8415  lt0neg1d 8462  ltneg 8409  ltnegd 8470  ltnegi 8440
[Apostol] p. 20Theorem I.25lt2add 8392  lt2addd 8514  lt2addi 8457
[Apostol] p. 20Definition of positive numbersdf-rp 9641
[Apostol] p. 21Exercise 4recgt0 8796  recgt0d 8880  recgt0i 8852  recgt0ii 8853
[Apostol] p. 22Definition of integersdf-z 9243
[Apostol] p. 22Definition of rationalsdf-q 9609
[Apostol] p. 24Theorem I.26supeuti 6987
[Apostol] p. 26Theorem I.29arch 9162
[Apostol] p. 28Exercise 2btwnz 9361
[Apostol] p. 28Exercise 3nnrecl 9163
[Apostol] p. 28Exercise 6qbtwnre 10243
[Apostol] p. 28Exercise 10(a)zeneo 11859  zneo 9343
[Apostol] p. 29Theorem I.35resqrtth 11024  sqrtthi 11112
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 8911
[Apostol] p. 34Theorem I.37 (well-ordering principle)nnwodc 12020
[Apostol] p. 363Remarkabsgt0api 11139
[Apostol] p. 363Exampleabssubd 11186  abssubi 11143
[ApostolNT] p. 14Definitiondf-dvds 11779
[ApostolNT] p. 14Theorem 1.1(a)iddvds 11795
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 11819
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 11815
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 11809
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 11811
[ApostolNT] p. 14Theorem 1.1(f)1dvds 11796
[ApostolNT] p. 14Theorem 1.1(g)dvds0 11797
[ApostolNT] p. 14Theorem 1.1(h)0dvds 11802
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 11834
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 11836
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 11838
[ApostolNT] p. 15Definitiondfgcd2 11998
[ApostolNT] p. 16Definitionisprm2 12100
[ApostolNT] p. 16Theorem 1.5coprmdvds 12075
[ApostolNT] p. 16Theorem 1.7prminf 12439
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 11957
[ApostolNT] p. 16Theorem 1.4(b)gcdass 11999
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 12001
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 11971
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 11964
[ApostolNT] p. 17Theorem 1.8coprm 12127
[ApostolNT] p. 17Theorem 1.9euclemma 12129
[ApostolNT] p. 17Theorem 1.101arith2 12349
[ApostolNT] p. 19Theorem 1.14divalg 11912
[ApostolNT] p. 20Theorem 1.15eucalg 12042
[ApostolNT] p. 25Definitiondf-phi 12194
[ApostolNT] p. 26Theorem 2.2phisum 12223
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 12205
[ApostolNT] p. 28Theorem 2.5(c)phimul 12209
[ApostolNT] p. 104Definitioncongr 12083
[ApostolNT] p. 106Remarkdvdsval3 11782
[ApostolNT] p. 106Definitionmoddvds 11790
[ApostolNT] p. 107Example 2mod2eq0even 11866
[ApostolNT] p. 107Example 3mod2eq1n2dvds 11867
[ApostolNT] p. 107Example 4zmod1congr 10327
[ApostolNT] p. 107Theorem 5.2(b)modqmul12d 10364
[ApostolNT] p. 107Theorem 5.2(c)modqexp 10632
[ApostolNT] p. 108Theorem 5.3modmulconst 11814
[ApostolNT] p. 109Theorem 5.4cncongr1 12086
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 12088
[ApostolNT] p. 113Theorem 5.17eulerth 12216
[ApostolNT] p. 113Theorem 5.18vfermltl 12234
[ApostolNT] p. 114Theorem 5.19fermltl 12217
[ApostolNT] p. 179Definitiondf-lgs 14066  lgsprme0 14110
[ApostolNT] p. 180Example 11lgs 14111
[ApostolNT] p. 180Theorem 9.2lgsvalmod 14087
[ApostolNT] p. 180Theorem 9.3lgsdirprm 14102
[ApostolNT] p. 188Definitiondf-lgs 14066  lgs1 14112
[ApostolNT] p. 188Theorem 9.9(a)lgsdir 14103
[ApostolNT] p. 188Theorem 9.9(b)lgsdi 14105
[ApostolNT] p. 188Theorem 9.9(c)lgsmodeq 14113
[ApostolNT] p. 188Theorem 9.9(d)lgsmulsqcoprm 14114
[Bauer] p. 482Section 1.2pm2.01 616  pm2.65 659
[Bauer] p. 483Theorem 1.3acexmid 5868  onsucelsucexmidlem 4525
[Bauer], p. 481Section 1.1pwtrufal 14403
[Bauer], p. 483Definitionn0rf 3435
[Bauer], p. 483Theorem 1.22irrexpq 14061  2irrexpqap 14063
[Bauer], p. 485Theorem 2.1ssfiexmid 6870
[Bauer], p. 494Theorem 5.5ivthinc 13788
[BauerHanson], p. 27Proposition 5.2cnstab 8592
[BauerSwan], p. 14Remark0ct 7100  ctm 7102
[BauerSwan], p. 14Proposition 2.6subctctexmid 14406
[BauerSwan], p. 14Table" is defined as ` ` per enumct 7108
[BauerTaylor], p. 32Lemma 6.16prarloclem 7491
[BauerTaylor], p. 50Lemma 11.4subhalfnqq 7404
[BauerTaylor], p. 52Proposition 11.15prarloc 7493
[BauerTaylor], p. 53Lemma 11.16addclpr 7527  addlocpr 7526
[BauerTaylor], p. 55Proposition 12.7appdivnq 7553
[BauerTaylor], p. 56Lemma 12.8prmuloc 7556
[BauerTaylor], p. 56Lemma 12.9mullocpr 7561
[BellMachover] p. 36Lemma 10.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 2029
[BellMachover] p. 460Notationdf-mo 2030
[BellMachover] p. 460Definitionmo3 2080  mo3h 2079
[BellMachover] p. 462Theorem 1.1bm1.1 2162
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4121
[BellMachover] p. 466Axiom Powaxpow3 4174
[BellMachover] p. 466Axiom Unionaxun2 4432
[BellMachover] p. 469Theorem 2.2(i)ordirr 4538
[BellMachover] p. 469Theorem 2.2(iii)onelon 4381
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4541
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4492
[BellMachover] p. 471Definition of Limdf-ilim 4366
[BellMachover] p. 472Axiom Infzfinf2 4585
[BellMachover] p. 473Theorem 2.8limom 4610
[Bobzien] p. 116Statement T3stoic3 1431
[Bobzien] p. 117Statement T2stoic2a 1429
[Bobzien] p. 117Statement T4stoic4a 1432
[Bobzien] p. 117Conclusion the contradictorystoic1a 1427
[BourbakiAlg1] p. 1Definition 1df-mgm 12667
[BourbakiAlg1] p. 4Definition 5df-sgrp 12700
[BourbakiAlg1] p. 12Definition 2df-mnd 12710
[BourbakiAlg1] p. 92Definition 1df-ring 13007
[BourbakiEns] p. Proposition 8fcof1 5778  fcofo 5779
[BourbakiTop1] p. Remarkxnegmnf 9816  xnegpnf 9815
[BourbakiTop1] p. Remark rexneg 9817
[BourbakiTop1] p. Propositionishmeo 13471
[BourbakiTop1] p. Property V_issnei2 13324
[BourbakiTop1] p. Property V_iiinnei 13330
[BourbakiTop1] p. Property V_ivneissex 13332
[BourbakiTop1] p. Proposition 1neipsm 13321  neiss 13317
[BourbakiTop1] p. Proposition 2cnptopco 13389
[BourbakiTop1] p. Proposition 4imasnopn 13466
[BourbakiTop1] p. Property V_iiielnei 13319
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 13163
[Bruck] p. 1Section I.1df-mgm 12667
[Bruck] p. 23Section II.1df-sgrp 12700
[Bruck] p. 28Theorem 3.2dfgrp3m 12858
[ChoquetDD] p. 2Definition of mappingdf-mpt 4063
[Cohen] p. 301Remarkrelogoprlem 13956
[Cohen] p. 301Property 2relogmul 13957  relogmuld 13972
[Cohen] p. 301Property 3relogdiv 13958  relogdivd 13973
[Cohen] p. 301Property 4relogexp 13960
[Cohen] p. 301Property 1alog1 13954
[Cohen] p. 301Property 1bloge 13955
[Cohen4] p. 348Observationrelogbcxpbap 14050
[Cohen4] p. 352Definitionrpelogb 14034
[Cohen4] p. 361Property 2rprelogbmul 14040
[Cohen4] p. 361Property 3logbrec 14045  rprelogbdiv 14042
[Cohen4] p. 361Property 4rplogbreexp 14038
[Cohen4] p. 361Property 6relogbexpap 14043
[Cohen4] p. 361Property 1(a)rplogbid1 14032
[Cohen4] p. 361Property 1(b)rplogb1 14033
[Cohen4] p. 367Propertyrplogbchbase 14035
[Cohen4] p. 377Property 2logblt 14047
[Crosilla] p. Axiom 1ax-ext 2159
[Crosilla] p. Axiom 2ax-pr 4206
[Crosilla] p. Axiom 3ax-un 4430
[Crosilla] p. Axiom 4ax-nul 4126
[Crosilla] p. Axiom 5ax-iinf 4584
[Crosilla] p. Axiom 6ru 2961
[Crosilla] p. Axiom 8ax-pow 4171
[Crosilla] p. Axiom 9ax-setind 4533
[Crosilla], p. Axiom 6ax-sep 4118
[Crosilla], p. Axiom 7ax-coll 4115
[Crosilla], p. Axiom 7'repizf 4116
[Crosilla], p. Theorem is statedordtriexmid 4517
[Crosilla], p. Axiom of choice implies instancesacexmid 5868
[Crosilla], p. Definition of ordinaldf-iord 4363
[Crosilla], p. Theorem "Foundation implies instances of EM"regexmid 4531
[Eisenberg] p. 67Definition 5.3df-dif 3131
[Eisenberg] p. 82Definition 6.3df-iom 4587
[Eisenberg] p. 125Definition 8.21df-map 6644
[Enderton] p. 18Axiom of Empty Setaxnul 4125
[Enderton] p. 19Definitiondf-tp 3599
[Enderton] p. 26Exercise 5unissb 3837
[Enderton] p. 26Exercise 10pwel 4215
[Enderton] p. 28Exercise 7(b)pwunim 4283
[Enderton] p. 30Theorem "Distributive laws"iinin1m 3953  iinin2m 3952  iunin1 3948  iunin2 3947
[Enderton] p. 31Theorem "De Morgan's laws"iindif2m 3951  iundif2ss 3949
[Enderton] p. 33Exercise 23iinuniss 3966
[Enderton] p. 33Exercise 25iununir 3967
[Enderton] p. 33Exercise 24(a)iinpw 3974
[Enderton] p. 33Exercise 24(b)iunpw 4477  iunpwss 3975
[Enderton] p. 38Exercise 6(a)unipw 4214
[Enderton] p. 38Exercise 6(b)pwuni 4189
[Enderton] p. 41Lemma 3Dopeluu 4447  rnex 4890  rnexg 4888
[Enderton] p. 41Exercise 8dmuni 4833  rnuni 5036
[Enderton] p. 42Definition of a functiondffun7 5239  dffun8 5240
[Enderton] p. 43Definition of function valuefunfvdm2 5576
[Enderton] p. 43Definition of single-rootedfuncnv 5273
[Enderton] p. 44Definition (d)dfima2 4968  dfima3 4969
[Enderton] p. 47Theorem 3Hfvco2 5581
[Enderton] p. 49Axiom of Choice (first form)df-ac 7199
[Enderton] p. 50Theorem 3K(a)imauni 5756
[Enderton] p. 52Definitiondf-map 6644
[Enderton] p. 53Exercise 21coass 5143
[Enderton] p. 53Exercise 27dmco 5133
[Enderton] p. 53Exercise 14(a)funin 5283
[Enderton] p. 53Exercise 22(a)imass2 5000
[Enderton] p. 54Remarkixpf 6714  ixpssmap 6726
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6693
[Enderton] p. 56Theorem 3Merref 6549
[Enderton] p. 57Lemma 3Nerthi 6575
[Enderton] p. 57Definitiondf-ec 6531
[Enderton] p. 58Definitiondf-qs 6535
[Enderton] p. 60Theorem 3Qth3q 6634  th3qcor 6633  th3qlem1 6631  th3qlem2 6632
[Enderton] p. 61Exercise 35df-ec 6531
[Enderton] p. 65Exercise 56(a)dmun 4830
[Enderton] p. 68Definition of successordf-suc 4368
[Enderton] p. 71Definitiondf-tr 4099  dftr4 4103
[Enderton] p. 72Theorem 4Eunisuc 4410  unisucg 4411
[Enderton] p. 73Exercise 6unisuc 4410  unisucg 4411
[Enderton] p. 73Exercise 5(a)truni 4112
[Enderton] p. 73Exercise 5(b)trint 4113
[Enderton] p. 79Theorem 4I(A1)nna0 6469
[Enderton] p. 79Theorem 4I(A2)nnasuc 6471  onasuc 6461
[Enderton] p. 79Definition of operation valuedf-ov 5872
[Enderton] p. 80Theorem 4J(A1)nnm0 6470
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6472  onmsuc 6468
[Enderton] p. 81Theorem 4K(1)nnaass 6480
[Enderton] p. 81Theorem 4K(2)nna0r 6473  nnacom 6479
[Enderton] p. 81Theorem 4K(3)nndi 6481
[Enderton] p. 81Theorem 4K(4)nnmass 6482
[Enderton] p. 81Theorem 4K(5)nnmcom 6484
[Enderton] p. 82Exercise 16nnm0r 6474  nnmsucr 6483
[Enderton] p. 88Exercise 23nnaordex 6523
[Enderton] p. 129Definitiondf-en 6735
[Enderton] p. 132Theorem 6B(b)canth 5823
[Enderton] p. 133Exercise 1xpomen 12379
[Enderton] p. 134Theorem (Pigeonhole Principle)phpm 6859
[Enderton] p. 136Corollary 6Enneneq 6851
[Enderton] p. 139Theorem 6H(c)mapen 6840
[Enderton] p. 142Theorem 6I(3)xpdjuen 7211
[Enderton] p. 143Theorem 6Jdju0en 7207  dju1en 7206
[Enderton] p. 144Corollary 6Kundif2ss 3498
[Enderton] p. 145Figure 38ffoss 5489
[Enderton] p. 145Definitiondf-dom 6736
[Enderton] p. 146Example 1domen 6745  domeng 6746
[Enderton] p. 146Example 3nndomo 6858
[Enderton] p. 149Theorem 6L(c)xpdom1 6829  xpdom1g 6827  xpdom2g 6826
[Enderton] p. 168Definitiondf-po 4293
[Enderton] p. 192Theorem 7M(a)oneli 4425
[Enderton] p. 192Theorem 7M(b)ontr1 4386
[Enderton] p. 192Theorem 7M(c)onirri 4539
[Enderton] p. 193Corollary 7N(b)0elon 4389
[Enderton] p. 193Corollary 7N(c)onsuci 4512
[Enderton] p. 193Corollary 7N(d)ssonunii 4485
[Enderton] p. 194Remarkonprc 4548
[Enderton] p. 194Exercise 16suc11 4554
[Enderton] p. 197Definitiondf-card 7173
[Enderton] p. 200Exercise 25tfis 4579
[Enderton] p. 206Theorem 7X(b)en2lp 4550
[Enderton] p. 207Exercise 34opthreg 4552
[Enderton] p. 208Exercise 35suc11g 4553
[Geuvers], p. 1Remarkexpap0 10536
[Geuvers], p. 6Lemma 2.13mulap0r 8562
[Geuvers], p. 6Lemma 2.15mulap0 8600
[Geuvers], p. 9Lemma 2.35msqge0 8563
[Geuvers], p. 9Definition 3.1(2)ax-arch 7921
[Geuvers], p. 10Lemma 3.9maxcom 11196
[Geuvers], p. 10Lemma 3.10maxle1 11204  maxle2 11205
[Geuvers], p. 10Lemma 3.11maxleast 11206
[Geuvers], p. 10Lemma 3.12maxleb 11209
[Geuvers], p. 11Definition 3.13dfabsmax 11210
[Geuvers], p. 17Definition 6.1df-ap 8529
[Gleason] p. 117Proposition 9-2.1df-enq 7337  enqer 7348
[Gleason] p. 117Proposition 9-2.2df-1nqqs 7341  df-nqqs 7338
[Gleason] p. 117Proposition 9-2.3df-plpq 7334  df-plqqs 7339
[Gleason] p. 119Proposition 9-2.4df-mpq 7335  df-mqqs 7340
[Gleason] p. 119Proposition 9-2.5df-rq 7342
[Gleason] p. 119Proposition 9-2.6ltexnqq 7398
[Gleason] p. 120Proposition 9-2.6(i)halfnq 7401  ltbtwnnq 7406  ltbtwnnqq 7405
[Gleason] p. 120Proposition 9-2.6(ii)ltanqg 7390
[Gleason] p. 120Proposition 9-2.6(iii)ltmnqg 7391
[Gleason] p. 123Proposition 9-3.5addclpr 7527
[Gleason] p. 123Proposition 9-3.5(i)addassprg 7569
[Gleason] p. 123Proposition 9-3.5(ii)addcomprg 7568
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 7587
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 7603
[Gleason] p. 123Proposition 9-3.5(v)ltaprg 7609  ltaprlem 7608
[Gleason] p. 123Proposition 9-3.5(vi)addcanprg 7606
[Gleason] p. 124Proposition 9-3.7mulclpr 7562
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 7582
[Gleason] p. 124Proposition 9-3.7(i)mulassprg 7571
[Gleason] p. 124Proposition 9-3.7(ii)mulcomprg 7570
[Gleason] p. 124Proposition 9-3.7(iii)distrprg 7578
[Gleason] p. 124Proposition 9-3.7(v)recexpr 7628
[Gleason] p. 126Proposition 9-4.1df-enr 7716  enrer 7725
[Gleason] p. 126Proposition 9-4.2df-0r 7721  df-1r 7722  df-nr 7717
[Gleason] p. 126Proposition 9-4.3df-mr 7719  df-plr 7718  negexsr 7762  recexsrlem 7764
[Gleason] p. 127Proposition 9-4.4df-ltr 7720
[Gleason] p. 130Proposition 10-1.3creui 8906  creur 8905  cru 8549
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 7913  axcnre 7871
[Gleason] p. 132Definition 10-3.1crim 10851  crimd 10970  crimi 10930  crre 10850  crred 10969  crrei 10929
[Gleason] p. 132Definition 10-3.2remim 10853  remimd 10935
[Gleason] p. 133Definition 10.36absval2 11050  absval2d 11178  absval2i 11137
[Gleason] p. 133Proposition 10-3.4(a)cjadd 10877  cjaddd 10958  cjaddi 10925
[Gleason] p. 133Proposition 10-3.4(c)cjmul 10878  cjmuld 10959  cjmuli 10926
[Gleason] p. 133Proposition 10-3.4(e)cjcj 10876  cjcjd 10936  cjcji 10908
[Gleason] p. 133Proposition 10-3.4(f)cjre 10875  cjreb 10859  cjrebd 10939  cjrebi 10911  cjred 10964  rere 10858  rereb 10856  rerebd 10938  rerebi 10910  rered 10962
[Gleason] p. 133Proposition 10-3.4(h)addcj 10884  addcjd 10950  addcji 10920
[Gleason] p. 133Proposition 10-3.7(a)absval 10994
[Gleason] p. 133Proposition 10-3.7(b)abscj 11045  abscjd 11183  abscji 11141
[Gleason] p. 133Proposition 10-3.7(c)abs00 11057  abs00d 11179  abs00i 11138  absne0d 11180
[Gleason] p. 133Proposition 10-3.7(d)releabs 11089  releabsd 11184  releabsi 11142
[Gleason] p. 133Proposition 10-3.7(f)absmul 11062  absmuld 11187  absmuli 11144
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 11048  sqabsaddi 11145
[Gleason] p. 133Proposition 10-3.7(h)abstri 11097  abstrid 11189  abstrii 11148
[Gleason] p. 134Definition 10-4.1df-exp 10506  exp0 10510  expp1 10513  expp1d 10640
[Gleason] p. 135Proposition 10-4.2(a)expadd 10548  expaddd 10641
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 14000  cxpmuld 14023  expmul 10551  expmuld 10642
[Gleason] p. 135Proposition 10-4.2(c)mulexp 10545  mulexpd 10654  rpmulcxp 13997
[Gleason] p. 141Definition 11-2.1fzval 9997
[Gleason] p. 168Proposition 12-2.1(a)climadd 11318
[Gleason] p. 168Proposition 12-2.1(b)climsub 11320
[Gleason] p. 168Proposition 12-2.1(c)climmul 11319
[Gleason] p. 171Corollary 12-2.2climmulc2 11323
[Gleason] p. 172Corollary 12-2.5climrecl 11316
[Gleason] p. 172Proposition 12-2.4(c)climabs 11312  climcj 11313  climim 11315  climre 11314
[Gleason] p. 173Definition 12-3.1df-ltxr 7987  df-xr 7986  ltxr 9762
[Gleason] p. 180Theorem 12-5.3climcau 11339
[Gleason] p. 217Lemma 13-4.1btwnzge0 10286
[Gleason] p. 223Definition 14-1.1df-met 13156
[Gleason] p. 223Definition 14-1.1(a)met0 13531  xmet0 13530
[Gleason] p. 223Definition 14-1.1(c)metsym 13538
[Gleason] p. 223Definition 14-1.1(d)mettri 13540  mstri 13640  xmettri 13539  xmstri 13639
[Gleason] p. 230Proposition 14-2.6txlm 13446
[Gleason] p. 240Proposition 14-4.2metcnp3 13678
[Gleason] p. 243Proposition 14-4.16addcn2 11302  addcncntop 13719  mulcn2 11304  mulcncntop 13721  subcn2 11303  subcncntop 13720
[Gleason] p. 295Remarkbcval3 10715  bcval4 10716
[Gleason] p. 295Equation 2bcpasc 10730
[Gleason] p. 295Definition of binomial coefficientbcval 10713  df-bc 10712
[Gleason] p. 296Remarkbcn0 10719  bcnn 10721
[Gleason] p. 296Theorem 15-2.8binom 11476
[Gleason] p. 308Equation 2ef0 11664
[Gleason] p. 308Equation 3efcj 11665
[Gleason] p. 309Corollary 15-4.3efne0 11670
[Gleason] p. 309Corollary 15-4.4efexp 11674
[Gleason] p. 310Equation 14sinadd 11728
[Gleason] p. 310Equation 15cosadd 11729
[Gleason] p. 311Equation 17sincossq 11740
[Gleason] p. 311Equation 18cosbnd 11745  sinbnd 11744
[Gleason] p. 311Definition of ` `df-pi 11645
[Golan] p. 1Remarksrgisid 12995
[Golan] p. 1Definitiondf-srg 12973
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1449
[Herstein] p. 55Lemma 2.2.1(a)grpideu 12778  mndideu 12719
[Herstein] p. 55Lemma 2.2.1(b)grpinveu 12801
[Herstein] p. 55Lemma 2.2.1(c)grpinvinv 12826
[Herstein] p. 55Lemma 2.2.1(d)grpinvadd 12837
[Herstein] p. 57Exercise 1dfgrp3me 12859
[Heyting] p. 127Axiom #1ax1hfs 14475
[Hitchcock] p. 5Rule A3mptnan 1423
[Hitchcock] p. 5Rule A4mptxor 1424
[Hitchcock] p. 5Rule A5mtpxor 1426
[HoTT], p. Lemma 10.4.1exmidontriim 7218
[HoTT], p. Theorem 7.2.6nndceq 6494
[HoTT], p. Exercise 11.10neapmkv 14471
[HoTT], p. Exercise 11.11mulap0bd 8603
[HoTT], p. Section 11.2.1df-iltp 7460  df-imp 7459  df-iplp 7458  df-reap 8522
[HoTT], p. Theorem 11.2.4recapb 8617  rerecapb 8789
[HoTT], p. Theorem 11.2.12cauappcvgpr 7652
[HoTT], p. Corollary 11.4.3conventions 14129
[HoTT], p. Exercise 11.6(i)dcapnconst 14464  dceqnconst 14463
[HoTT], p. Corollary 11.2.13axcaucvg 7890  caucvgpr 7672  caucvgprpr 7702  caucvgsr 7792
[HoTT], p. Definition 11.2.1df-inp 7456
[HoTT], p. Exercise 11.6(ii)nconstwlpo 14469
[HoTT], p. Proposition 11.2.3df-iso 4294  ltpopr 7585  ltsopr 7586
[HoTT], p. Definition 11.2.7(v)apsym 8553  reapcotr 8545  reapirr 8524
[HoTT], p. Definition 11.2.7(vi)0lt1 8074  gt0add 8520  leadd1 8377  lelttr 8036  lemul1a 8804  lenlt 8023  ltadd1 8376  ltletr 8037  ltmul1 8539  reaplt 8535
[Jech] p. 4Definition of classcv 1352  cvjust 2172
[Jech] p. 78Noteopthprc 4674
[KalishMontague] p. 81Note 1ax-i9 1530
[Kreyszig] p. 3Property M1metcl 13520  xmetcl 13519
[Kreyszig] p. 4Property M2meteq0 13527
[Kreyszig] p. 12Equation 5muleqadd 8614
[Kreyszig] p. 18Definition 1.3-2mopnval 13609
[Kreyszig] p. 19Remarkmopntopon 13610
[Kreyszig] p. 19Theorem T1mopn0 13655  mopnm 13615
[Kreyszig] p. 19Theorem T2unimopn 13653
[Kreyszig] p. 19Definition of neighborhoodneibl 13658
[Kreyszig] p. 20Definition 1.3-3metcnp2 13680
[Kreyszig] p. 25Definition 1.4-1lmbr 13380
[Kunen] p. 10Axiom 0a9e 1696
[Kunen] p. 12Axiom 6zfrep6 4117
[Kunen] p. 24Definition 10.24mapval 6654  mapvalg 6652
[Kunen] p. 31Definition 10.24mapex 6648
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3894
[Lang] p. 3Statementlidrideqd 12692  mndbn0 12724
[Lang] p. 3Definitiondf-mnd 12710
[Lang] p. 7Definitiondfgrp2e 12793
[Levy] p. 338Axiomdf-clab 2164  df-clel 2173  df-cleq 2170
[Lopez-Astorga] p. 12Rule 1mptnan 1423
[Lopez-Astorga] p. 12Rule 2mptxor 1424
[Lopez-Astorga] p. 12Rule 3mtpxor 1426
[Margaris] p. 40Rule Cexlimiv 1598
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3condc 853
[Margaris] p. 49Definitiondfbi2 388  dfordc 892  exalim 1502
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 45
[Margaris] p. 60Theorem 8jcn 651
[Margaris] p. 89Theorem 19.219.2 1638  r19.2m 3509
[Margaris] p. 89Theorem 19.319.3 1554  19.3h 1553  rr19.3v 2876
[Margaris] p. 89Theorem 19.5alcom 1478
[Margaris] p. 89Theorem 19.6alexdc 1619  alexim 1645
[Margaris] p. 89Theorem 19.7alnex 1499
[Margaris] p. 89Theorem 19.819.8a 1590  spsbe 1842
[Margaris] p. 89Theorem 19.919.9 1644  19.9h 1643  19.9v 1871  exlimd 1597
[Margaris] p. 89Theorem 19.11excom 1664  excomim 1663
[Margaris] p. 89Theorem 19.1219.12 1665  r19.12 2583
[Margaris] p. 90Theorem 19.14exnalim 1646
[Margaris] p. 90Theorem 19.15albi 1468  ralbi 2609
[Margaris] p. 90Theorem 19.1619.16 1555
[Margaris] p. 90Theorem 19.1719.17 1556
[Margaris] p. 90Theorem 19.18exbi 1604  rexbi 2610
[Margaris] p. 90Theorem 19.1919.19 1666
[Margaris] p. 90Theorem 19.20alim 1457  alimd 1521  alimdh 1467  alimdv 1879  ralimdaa 2543  ralimdv 2545  ralimdva 2544  ralimdvva 2546  sbcimdv 3028
[Margaris] p. 90Theorem 19.2119.21-2 1667  19.21 1583  19.21bi 1558  19.21h 1557  19.21ht 1581  19.21t 1582  19.21v 1873  alrimd 1610  alrimdd 1609  alrimdh 1479  alrimdv 1876  alrimi 1522  alrimih 1469  alrimiv 1874  alrimivv 1875  r19.21 2553  r19.21be 2568  r19.21bi 2565  r19.21t 2552  r19.21v 2554  ralrimd 2555  ralrimdv 2556  ralrimdva 2557  ralrimdvv 2561  ralrimdvva 2562  ralrimi 2548  ralrimiv 2549  ralrimiva 2550  ralrimivv 2558  ralrimivva 2559  ralrimivvva 2560  ralrimivw 2551  rexlimi 2587
[Margaris] p. 90Theorem 19.222alimdv 1881  2eximdv 1882  exim 1599  eximd 1612  eximdh 1611  eximdv 1880  rexim 2571  reximdai 2575  reximddv 2580  reximddv2 2582  reximdv 2578  reximdv2 2576  reximdva 2579  reximdvai 2577  reximi2 2573
[Margaris] p. 90Theorem 19.2319.23 1678  19.23bi 1592  19.23h 1498  19.23ht 1497  19.23t 1677  19.23v 1883  19.23vv 1884  exlimd2 1595  exlimdh 1596  exlimdv 1819  exlimdvv 1897  exlimi 1594  exlimih 1593  exlimiv 1598  exlimivv 1896  r19.23 2585  r19.23v 2586  rexlimd 2591  rexlimdv 2593  rexlimdv3a 2596  rexlimdva 2594  rexlimdva2 2597  rexlimdvaa 2595  rexlimdvv 2601  rexlimdvva 2602  rexlimdvw 2598  rexlimiv 2588  rexlimiva 2589  rexlimivv 2600
[Margaris] p. 90Theorem 19.24i19.24 1639
[Margaris] p. 90Theorem 19.2519.25 1626
[Margaris] p. 90Theorem 19.2619.26-2 1482  19.26-3an 1483  19.26 1481  r19.26-2 2606  r19.26-3 2607  r19.26 2603  r19.26m 2608
[Margaris] p. 90Theorem 19.2719.27 1561  19.27h 1560  19.27v 1899  r19.27av 2612  r19.27m 3518  r19.27mv 3519
[Margaris] p. 90Theorem 19.2819.28 1563  19.28h 1562  19.28v 1900  r19.28av 2613  r19.28m 3512  r19.28mv 3515  rr19.28v 2877
[Margaris] p. 90Theorem 19.2919.29 1620  19.29r 1621  19.29r2 1622  19.29x 1623  r19.29 2614  r19.29d2r 2621  r19.29r 2615
[Margaris] p. 90Theorem 19.3019.30dc 1627
[Margaris] p. 90Theorem 19.3119.31r 1681
[Margaris] p. 90Theorem 19.3219.32dc 1679  19.32r 1680  r19.32r 2623  r19.32vdc 2626  r19.32vr 2625
[Margaris] p. 90Theorem 19.3319.33 1484  19.33b2 1629  19.33bdc 1630
[Margaris] p. 90Theorem 19.3419.34 1684
[Margaris] p. 90Theorem 19.3519.35-1 1624  19.35i 1625
[Margaris] p. 90Theorem 19.3619.36-1 1673  19.36aiv 1901  19.36i 1672  r19.36av 2628
[Margaris] p. 90Theorem 19.3719.37-1 1674  19.37aiv 1675  r19.37 2629  r19.37av 2630
[Margaris] p. 90Theorem 19.3819.38 1676
[Margaris] p. 90Theorem 19.39i19.39 1640
[Margaris] p. 90Theorem 19.4019.40-2 1632  19.40 1631  r19.40 2631
[Margaris] p. 90Theorem 19.4119.41 1686  19.41h 1685  19.41v 1902  19.41vv 1903  19.41vvv 1904  19.41vvvv 1905  r19.41 2632  r19.41v 2633
[Margaris] p. 90Theorem 19.4219.42 1688  19.42h 1687  19.42v 1906  19.42vv 1911  19.42vvv 1912  19.42vvvv 1913  r19.42v 2634
[Margaris] p. 90Theorem 19.4319.43 1628  r19.43 2635
[Margaris] p. 90Theorem 19.4419.44 1682  r19.44av 2636  r19.44mv 3517
[Margaris] p. 90Theorem 19.4519.45 1683  r19.45av 2637  r19.45mv 3516
[Margaris] p. 110Exercise 2(b)eu1 2051
[Megill] p. 444Axiom C5ax-17 1526
[Megill] p. 445Lemma L12alequcom 1515  ax-10 1505
[Megill] p. 446Lemma L17equtrr 1710
[Megill] p. 446Lemma L19hbnae 1721
[Megill] p. 447Remark 9.1df-sb 1763  sbid 1774
[Megill] p. 448Scheme C5'ax-4 1510
[Megill] p. 448Scheme C6'ax-7 1448
[Megill] p. 448Scheme C8'ax-8 1504
[Megill] p. 448Scheme C9'ax-i12 1507
[Megill] p. 448Scheme C11'ax-10o 1716
[Megill] p. 448Scheme C12'ax-13 2150
[Megill] p. 448Scheme C13'ax-14 2151
[Megill] p. 448Scheme C15'ax-11o 1823
[Megill] p. 448Scheme C16'ax-16 1814
[Megill] p. 448Theorem 9.4dral1 1730  dral2 1731  drex1 1798  drex2 1732  drsb1 1799  drsb2 1841
[Megill] p. 449Theorem 9.7sbcom2 1987  sbequ 1840  sbid2v 1996
[Megill] p. 450Example in Appendixhba1 1540
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 3045  rspsbca 3046  stdpc4 1775
[Mendelson] p. 69Axiom 5ra5 3051  stdpc5 1584
[Mendelson] p. 81Rule Cexlimiv 1598
[Mendelson] p. 95Axiom 6stdpc6 1703
[Mendelson] p. 95Axiom 7stdpc7 1770
[Mendelson] p. 231Exercise 4.10(k)inv1 3459
[Mendelson] p. 231Exercise 4.10(l)unv 3460
[Mendelson] p. 231Exercise 4.10(n)inssun 3375
[Mendelson] p. 231Exercise 4.10(o)df-nul 3423
[Mendelson] p. 231Exercise 4.10(q)inssddif 3376
[Mendelson] p. 231Exercise 4.10(s)ddifnel 3266
[Mendelson] p. 231Definition of unionunssin 3374
[Mendelson] p. 235Exercise 4.12(c)univ 4473
[Mendelson] p. 235Exercise 4.12(d)pwv 3806
[Mendelson] p. 235Exercise 4.12(j)pwin 4279
[Mendelson] p. 235Exercise 4.12(k)pwunss 4280
[Mendelson] p. 235Exercise 4.12(l)pwssunim 4281
[Mendelson] p. 235Exercise 4.12(n)uniin 3827
[Mendelson] p. 235Exercise 4.12(p)reli 4752
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5145
[Mendelson] p. 246Definition of successordf-suc 4368
[Mendelson] p. 254Proposition 4.22(b)xpen 6839
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6815  xpsneng 6816
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6821  xpcomeng 6822
[Mendelson] p. 254Proposition 4.22(e)xpassen 6824
[Mendelson] p. 255Exercise 4.39endisj 6818
[Mendelson] p. 255Exercise 4.41mapprc 6646
[Mendelson] p. 255Exercise 4.43mapsnen 6805
[Mendelson] p. 255Exercise 4.47xpmapen 6844
[Mendelson] p. 255Exercise 4.42(a)map0e 6680
[Mendelson] p. 255Exercise 4.42(b)map1 6806
[Mendelson] p. 258Exercise 4.56(c)djuassen 7210  djucomen 7209
[Mendelson] p. 258Exercise 4.56(g)xp2dju 7208
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6462
[Monk1] p. 26Theorem 2.8(vii)ssin 3357
[Monk1] p. 33Theorem 3.2(i)ssrel 4711
[Monk1] p. 33Theorem 3.2(ii)eqrel 4712
[Monk1] p. 34Definition 3.3df-opab 4062
[Monk1] p. 36Theorem 3.7(i)coi1 5140  coi2 5141
[Monk1] p. 36Theorem 3.8(v)dm0 4837  rn0 4879
[Monk1] p. 36Theorem 3.7(ii)cnvi 5029
[Monk1] p. 37Theorem 3.13(i)relxp 4732
[Monk1] p. 37Theorem 3.13(x)dmxpm 4843  rnxpm 5054
[Monk1] p. 37Theorem 3.13(ii)0xp 4703  xp0 5044
[Monk1] p. 38Theorem 3.16(ii)ima0 4983
[Monk1] p. 38Theorem 3.16(viii)imai 4980
[Monk1] p. 39Theorem 3.17imaex 4979  imaexg 4978
[Monk1] p. 39Theorem 3.16(xi)imassrn 4977
[Monk1] p. 41Theorem 4.3(i)fnopfv 5642  funfvop 5624
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5555
[Monk1] p. 42Theorem 4.4(iii)fvelima 5563
[Monk1] p. 43Theorem 4.6funun 5256
[Monk1] p. 43Theorem 4.8(iv)dff13 5763  dff13f 5765
[Monk1] p. 46Theorem 4.15(v)funex 5735  funrnex 6109
[Monk1] p. 50Definition 5.4fniunfv 5757
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5108
[Monk1] p. 52Theorem 5.11(viii)ssint 3858
[Monk1] p. 52Definition 5.13 (i)1stval2 6150  df-1st 6135
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6151  df-2nd 6136
[Monk2] p. 105Axiom C4ax-5 1447
[Monk2] p. 105Axiom C7ax-8 1504
[Monk2] p. 105Axiom C8ax-11 1506  ax-11o 1823
[Monk2] p. 105Axiom (C8)ax11v 1827
[Monk2] p. 109Lemma 12ax-7 1448
[Monk2] p. 109Lemma 15equvin 1863  equvini 1758  eqvinop 4240
[Monk2] p. 113Axiom C5-1ax-17 1526
[Monk2] p. 113Axiom C5-2ax6b 1651
[Monk2] p. 113Axiom C5-3ax-7 1448
[Monk2] p. 114Lemma 22hba1 1540
[Monk2] p. 114Lemma 23hbia1 1552  nfia1 1580
[Monk2] p. 114Lemma 24hba2 1551  nfa2 1579
[Moschovakis] p. 2Chapter 2 df-stab 831  dftest 14476
[Munkres] p. 77Example 2distop 13252
[Munkres] p. 78Definition of basisdf-bases 13208  isbasis3g 13211
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 12657  tgval2 13218
[Munkres] p. 79Remarktgcl 13231
[Munkres] p. 80Lemma 2.1tgval3 13225
[Munkres] p. 80Lemma 2.2tgss2 13246  tgss3 13245
[Munkres] p. 81Lemma 2.3basgen 13247  basgen2 13248
[Munkres] p. 89Definition of subspace topologyresttop 13337
[Munkres] p. 93Theorem 6.1(1)0cld 13279  topcld 13276
[Munkres] p. 93Theorem 6.1(3)uncld 13280
[Munkres] p. 94Definition of closureclsval 13278
[Munkres] p. 94Definition of interiorntrval 13277
[Munkres] p. 102Definition of continuous functiondf-cn 13355  iscn 13364  iscn2 13367
[Munkres] p. 107Theorem 7.2(g)cncnp 13397  cncnp2m 13398  cncnpi 13395  df-cnp 13356  iscnp 13366
[Munkres] p. 127Theorem 10.1metcn 13681
[Pierik], p. 8Section 2.2.1dfrex2fin 6897
[Pierik], p. 9Definition 2.4df-womni 7156
[Pierik], p. 9Definition 2.5df-markov 7144  omniwomnimkv 7159
[Pierik], p. 10Section 2.3dfdif3 3245
[Pierik], p. 14Definition 3.1df-omni 7127  exmidomniim 7133  finomni 7132
[Pierik], p. 15Section 3.1df-nninf 7113
[PradicBrown2022], p. 1Theorem 1exmidsbthr 14427
[PradicBrown2022], p. 2Remarkexmidpw 6902
[PradicBrown2022], p. 2Proposition 1.1exmidfodomrlemim 7194
[PradicBrown2022], p. 2Proposition 1.2exmidfodomrlemr 7195  exmidfodomrlemrALT 7196
[PradicBrown2022], p. 4Lemma 3.2fodjuomni 7141
[PradicBrown2022], p. 5Lemma 3.4peano3nninf 14412  peano4nninf 14411
[PradicBrown2022], p. 5Lemma 3.5nninfall 14414
[PradicBrown2022], p. 5Theorem 3.6nninfsel 14422
[PradicBrown2022], p. 5Corollary 3.7nninfomni 14424
[PradicBrown2022], p. 5Definition 3.3nnsf 14410
[Quine] p. 16Definition 2.1df-clab 2164  rabid 2652
[Quine] p. 17Definition 2.1''dfsb7 1991
[Quine] p. 18Definition 2.7df-cleq 2170
[Quine] p. 19Definition 2.9df-v 2739
[Quine] p. 34Theorem 5.1abeq2 2286
[Quine] p. 35Theorem 5.2abid2 2298  abid2f 2345
[Quine] p. 40Theorem 6.1sb5 1887
[Quine] p. 40Theorem 6.2sb56 1885  sb6 1886
[Quine] p. 41Theorem 6.3df-clel 2173
[Quine] p. 41Theorem 6.4eqid 2177
[Quine] p. 41Theorem 6.5eqcom 2179
[Quine] p. 42Theorem 6.6df-sbc 2963
[Quine] p. 42Theorem 6.7dfsbcq 2964  dfsbcq2 2965
[Quine] p. 43Theorem 6.8vex 2740
[Quine] p. 43Theorem 6.9isset 2743
[Quine] p. 44Theorem 7.3spcgf 2819  spcgv 2824  spcimgf 2817
[Quine] p. 44Theorem 6.11spsbc 2974  spsbcd 2975
[Quine] p. 44Theorem 6.12elex 2748
[Quine] p. 44Theorem 6.13elab 2881  elabg 2883  elabgf 2879
[Quine] p. 44Theorem 6.14noel 3426
[Quine] p. 48Theorem 7.2snprc 3656
[Quine] p. 48Definition 7.1df-pr 3598  df-sn 3597
[Quine] p. 49Theorem 7.4snss 3726  snssg 3725
[Quine] p. 49Theorem 7.5prss 3747  prssg 3748
[Quine] p. 49Theorem 7.6prid1 3697  prid1g 3695  prid2 3698  prid2g 3696  snid 3622  snidg 3620
[Quine] p. 51Theorem 7.12snexg 4181  snexprc 4183
[Quine] p. 51Theorem 7.13prexg 4208
[Quine] p. 53Theorem 8.2unisn 3823  unisng 3824
[Quine] p. 53Theorem 8.3uniun 3826
[Quine] p. 54Theorem 8.6elssuni 3835
[Quine] p. 54Theorem 8.7uni0 3834
[Quine] p. 56Theorem 8.17uniabio 5184
[Quine] p. 56Definition 8.18dfiota2 5175
[Quine] p. 57Theorem 8.19iotaval 5185
[Quine] p. 57Theorem 8.22iotanul 5189
[Quine] p. 58Theorem 8.23euiotaex 5190
[Quine] p. 58Definition 9.1df-op 3600
[Quine] p. 61Theorem 9.5opabid 4254  opelopab 4268  opelopaba 4263  opelopabaf 4270  opelopabf 4271  opelopabg 4265  opelopabga 4260  oprabid 5901
[Quine] p. 64Definition 9.11df-xp 4629
[Quine] p. 64Definition 9.12df-cnv 4631
[Quine] p. 64Definition 9.15df-id 4290
[Quine] p. 65Theorem 10.3fun0 5270
[Quine] p. 65Theorem 10.4funi 5244
[Quine] p. 65Theorem 10.5funsn 5260  funsng 5258
[Quine] p. 65Definition 10.1df-fun 5214
[Quine] p. 65Definition 10.2args 4993  dffv4g 5508
[Quine] p. 68Definition 10.11df-fv 5220  fv2 5506
[Quine] p. 124Theorem 17.3nn0opth2 10688  nn0opth2d 10687  nn0opthd 10686
[Quine] p. 284Axiom 39(vi)funimaex 5297  funimaexg 5296
[Roman] p. 19Part Preliminariesdf-ring 13007
[Rudin] p. 164Equation 27efcan 11668
[Rudin] p. 164Equation 30efzval 11675
[Rudin] p. 167Equation 48absefi 11760
[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 5009
[Schechter] p. 51Definition of irreflexivityintirr 5011
[Schechter] p. 51Definition of symmetrycnvsym 5008
[Schechter] p. 51Definition of transitivitycotr 5006
[Schechter] p. 187Definition of "ring with unit"isring 13009
[Schechter] p. 428Definition 15.35bastop1 13250
[Stoll] p. 13Definition of symmetric differencesymdif1 3400
[Stoll] p. 16Exercise 4.40dif 3494  dif0 3493
[Stoll] p. 16Exercise 4.8difdifdirss 3507
[Stoll] p. 19Theorem 5.2(13)undm 3393
[Stoll] p. 19Theorem 5.2(13')indmss 3394
[Stoll] p. 20Remarkinvdif 3377
[Stoll] p. 25Definition of ordered tripledf-ot 3601
[Stoll] p. 43Definitionuniiun 3937
[Stoll] p. 44Definitionintiin 3938
[Stoll] p. 45Definitiondf-iin 3887
[Stoll] p. 45Definition indexed uniondf-iun 3886
[Stoll] p. 176Theorem 3.4(27)imandc 889  imanst 888
[Stoll] p. 262Example 4.1symdif1 3400
[Suppes] p. 22Theorem 2eq0 3441
[Suppes] p. 22Theorem 4eqss 3170  eqssd 3172  eqssi 3171
[Suppes] p. 23Theorem 5ss0 3463  ss0b 3462
[Suppes] p. 23Theorem 6sstr 3163
[Suppes] p. 25Theorem 12elin 3318  elun 3276
[Suppes] p. 26Theorem 15inidm 3344
[Suppes] p. 26Theorem 16in0 3457
[Suppes] p. 27Theorem 23unidm 3278
[Suppes] p. 27Theorem 24un0 3456
[Suppes] p. 27Theorem 25ssun1 3298
[Suppes] p. 27Theorem 26ssequn1 3305
[Suppes] p. 27Theorem 27unss 3309
[Suppes] p. 27Theorem 28indir 3384
[Suppes] p. 27Theorem 29undir 3385
[Suppes] p. 28Theorem 32difid 3491  difidALT 3492
[Suppes] p. 29Theorem 33difin 3372
[Suppes] p. 29Theorem 34indif 3378
[Suppes] p. 29Theorem 35undif1ss 3497
[Suppes] p. 29Theorem 36difun2 3502
[Suppes] p. 29Theorem 37difin0 3496
[Suppes] p. 29Theorem 38disjdif 3495
[Suppes] p. 29Theorem 39difundi 3387
[Suppes] p. 29Theorem 40difindiss 3389
[Suppes] p. 30Theorem 41nalset 4130
[Suppes] p. 39Theorem 61uniss 3828
[Suppes] p. 39Theorem 65uniop 4252
[Suppes] p. 41Theorem 70intsn 3877
[Suppes] p. 42Theorem 71intpr 3874  intprg 3875
[Suppes] p. 42Theorem 73op1stb 4475  op1stbg 4476
[Suppes] p. 42Theorem 78intun 3873
[Suppes] p. 44Definition 15(a)dfiun2 3918  dfiun2g 3916
[Suppes] p. 44Definition 15(b)dfiin2 3919
[Suppes] p. 47Theorem 86elpw 3580  elpw2 4154  elpw2g 4153  elpwg 3582
[Suppes] p. 47Theorem 87pwid 3589
[Suppes] p. 47Theorem 89pw0 3738
[Suppes] p. 48Theorem 90pwpw0ss 3802
[Suppes] p. 52Theorem 101xpss12 4730
[Suppes] p. 52Theorem 102xpindi 4758  xpindir 4759
[Suppes] p. 52Theorem 103xpundi 4679  xpundir 4680
[Suppes] p. 54Theorem 105elirrv 4544
[Suppes] p. 58Theorem 2relss 4710
[Suppes] p. 59Theorem 4eldm 4820  eldm2 4821  eldm2g 4819  eldmg 4818
[Suppes] p. 59Definition 3df-dm 4633
[Suppes] p. 60Theorem 6dmin 4831
[Suppes] p. 60Theorem 8rnun 5033
[Suppes] p. 60Theorem 9rnin 5034
[Suppes] p. 60Definition 4dfrn2 4811
[Suppes] p. 61Theorem 11brcnv 4806  brcnvg 4804
[Suppes] p. 62Equation 5elcnv 4800  elcnv2 4801
[Suppes] p. 62Theorem 12relcnv 5002
[Suppes] p. 62Theorem 15cnvin 5032
[Suppes] p. 62Theorem 16cnvun 5030
[Suppes] p. 63Theorem 20co02 5138
[Suppes] p. 63Theorem 21dmcoss 4892
[Suppes] p. 63Definition 7df-co 4632
[Suppes] p. 64Theorem 26cnvco 4808
[Suppes] p. 64Theorem 27coass 5143
[Suppes] p. 65Theorem 31resundi 4916
[Suppes] p. 65Theorem 34elima 4971  elima2 4972  elima3 4973  elimag 4970
[Suppes] p. 65Theorem 35imaundi 5037
[Suppes] p. 66Theorem 40dminss 5039
[Suppes] p. 66Theorem 41imainss 5040
[Suppes] p. 67Exercise 11cnvxp 5043
[Suppes] p. 81Definition 34dfec2 6532
[Suppes] p. 82Theorem 72elec 6568  elecg 6567
[Suppes] p. 82Theorem 73erth 6573  erth2 6574
[Suppes] p. 89Theorem 96map0b 6681
[Suppes] p. 89Theorem 97map0 6683  map0g 6682
[Suppes] p. 89Theorem 98mapsn 6684
[Suppes] p. 89Theorem 99mapss 6685
[Suppes] p. 92Theorem 1enref 6759  enrefg 6758
[Suppes] p. 92Theorem 2ensym 6775  ensymb 6774  ensymi 6776
[Suppes] p. 92Theorem 3entr 6778
[Suppes] p. 92Theorem 4unen 6810
[Suppes] p. 94Theorem 15endom 6757
[Suppes] p. 94Theorem 16ssdomg 6772
[Suppes] p. 94Theorem 17domtr 6779
[Suppes] p. 95Theorem 18isbth 6960
[Suppes] p. 98Exercise 4fundmen 6800  fundmeng 6801
[Suppes] p. 98Exercise 6xpdom3m 6828
[Suppes] p. 130Definition 3df-tr 4099
[Suppes] p. 132Theorem 9ssonuni 4484
[Suppes] p. 134Definition 6df-suc 4368
[Suppes] p. 136Theorem Schema 22findes 4599  finds 4596  finds1 4598  finds2 4597
[Suppes] p. 162Definition 5df-ltnqqs 7343  df-ltpq 7336
[Suppes] p. 228Theorem Schema 61onintss 4387
[TakeutiZaring] p. 8Axiom 1ax-ext 2159
[TakeutiZaring] p. 13Definition 4.5df-cleq 2170
[TakeutiZaring] p. 13Proposition 4.6df-clel 2173
[TakeutiZaring] p. 13Proposition 4.9cvjust 2172
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2195
[TakeutiZaring] p. 14Definition 4.16df-oprab 5873
[TakeutiZaring] p. 14Proposition 4.14ru 2961
[TakeutiZaring] p. 15Exercise 1elpr 3612  elpr2 3613  elprg 3611
[TakeutiZaring] p. 15Exercise 2elsn 3607  elsn2 3625  elsn2g 3624  elsng 3606  velsn 3608
[TakeutiZaring] p. 15Exercise 3elop 4228
[TakeutiZaring] p. 15Exercise 4sneq 3602  sneqr 3758
[TakeutiZaring] p. 15Definition 5.1dfpr2 3610  dfsn2 3605
[TakeutiZaring] p. 16Axiom 3uniex 4434
[TakeutiZaring] p. 16Exercise 6opth 4234
[TakeutiZaring] p. 16Exercise 8rext 4212
[TakeutiZaring] p. 16Corollary 5.8unex 4438  unexg 4440
[TakeutiZaring] p. 16Definition 5.3dftp2 3640
[TakeutiZaring] p. 16Definition 5.5df-uni 3808
[TakeutiZaring] p. 16Definition 5.6df-in 3135  df-un 3133
[TakeutiZaring] p. 16Proposition 5.7unipr 3821  uniprg 3822
[TakeutiZaring] p. 17Axiom 4vpwex 4176
[TakeutiZaring] p. 17Exercise 1eltp 3639
[TakeutiZaring] p. 17Exercise 5elsuc 4403  elsucg 4401  sstr2 3162
[TakeutiZaring] p. 17Exercise 6uncom 3279
[TakeutiZaring] p. 17Exercise 7incom 3327
[TakeutiZaring] p. 17Exercise 8unass 3292
[TakeutiZaring] p. 17Exercise 9inass 3345
[TakeutiZaring] p. 17Exercise 10indi 3382
[TakeutiZaring] p. 17Exercise 11undi 3383
[TakeutiZaring] p. 17Definition 5.9dfss2 3144
[TakeutiZaring] p. 17Definition 5.10df-pw 3576
[TakeutiZaring] p. 18Exercise 7unss2 3306
[TakeutiZaring] p. 18Exercise 9df-ss 3142  sseqin2 3354
[TakeutiZaring] p. 18Exercise 10ssid 3175
[TakeutiZaring] p. 18Exercise 12inss1 3355  inss2 3356
[TakeutiZaring] p. 18Exercise 13nssr 3215
[TakeutiZaring] p. 18Exercise 15unieq 3816
[TakeutiZaring] p. 18Exercise 18sspwb 4213
[TakeutiZaring] p. 18Exercise 19pweqb 4220
[TakeutiZaring] p. 20Definitiondf-rab 2464
[TakeutiZaring] p. 20Corollary 5.160ex 4127
[TakeutiZaring] p. 20Definition 5.12df-dif 3131
[TakeutiZaring] p. 20Definition 5.14dfnul2 3424
[TakeutiZaring] p. 20Proposition 5.15difid 3491  difidALT 3492
[TakeutiZaring] p. 20Proposition 5.17(1)n0rf 3435
[TakeutiZaring] p. 21Theorem 5.22setind 4535
[TakeutiZaring] p. 21Definition 5.20df-v 2739
[TakeutiZaring] p. 21Proposition 5.21vprc 4132
[TakeutiZaring] p. 22Exercise 10ss 3461
[TakeutiZaring] p. 22Exercise 3ssex 4137  ssexg 4139
[TakeutiZaring] p. 22Exercise 4inex1 4134
[TakeutiZaring] p. 22Exercise 5ruv 4546
[TakeutiZaring] p. 22Exercise 6elirr 4537
[TakeutiZaring] p. 22Exercise 7ssdif0im 3487
[TakeutiZaring] p. 22Exercise 11difdif 3260
[TakeutiZaring] p. 22Exercise 13undif3ss 3396
[TakeutiZaring] p. 22Exercise 14difss 3261
[TakeutiZaring] p. 22Exercise 15sscon 3269
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2460
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2461
[TakeutiZaring] p. 23Proposition 6.2xpex 4738  xpexg 4737  xpexgALT 6128
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4630
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5276
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5428  fun11 5279
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5223  svrelfun 5277
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4810
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4812
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4635
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4636
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4632
[TakeutiZaring] p. 25Exercise 2cnvcnvss 5079  dfrel2 5075
[TakeutiZaring] p. 25Exercise 3xpss 4731
[TakeutiZaring] p. 25Exercise 5relun 4740
[TakeutiZaring] p. 25Exercise 6reluni 4746
[TakeutiZaring] p. 25Exercise 9inxp 4757
[TakeutiZaring] p. 25Exercise 12relres 4931
[TakeutiZaring] p. 25Exercise 13opelres 4908  opelresg 4910
[TakeutiZaring] p. 25Exercise 14dmres 4924
[TakeutiZaring] p. 25Exercise 15resss 4927
[TakeutiZaring] p. 25Exercise 17resabs1 4932
[TakeutiZaring] p. 25Exercise 18funres 5253
[TakeutiZaring] p. 25Exercise 24relco 5123
[TakeutiZaring] p. 25Exercise 29funco 5252
[TakeutiZaring] p. 25Exercise 30f1co 5429
[TakeutiZaring] p. 26Definition 6.10eu2 2070
[TakeutiZaring] p. 26Definition 6.11df-fv 5220  fv3 5534
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5163  cnvexg 5162
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4889  dmexg 4887
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4890  rnexg 4888
[TakeutiZaring] p. 27Corollary 6.13funfvex 5528
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5538  tz6.12 5539  tz6.12c 5541
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5502
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5215
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5216
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5218  wfo 5210
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5217  wf1 5209
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5219  wf1o 5211
[TakeutiZaring] p. 28Exercise 4eqfnfv 5609  eqfnfv2 5610  eqfnfv2f 5613
[TakeutiZaring] p. 28Exercise 5fvco 5582
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5734  fnexALT 6106
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5733  resfunexgALT 6103
[TakeutiZaring] p. 29Exercise 9funimaex 5297  funimaexg 5296
[TakeutiZaring] p. 29Definition 6.18df-br 4001
[TakeutiZaring] p. 30Definition 6.21eliniseg 4994  iniseg 4996
[TakeutiZaring] p. 30Definition 6.22df-eprel 4286
[TakeutiZaring] p. 32Definition 6.28df-isom 5221
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5805
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5806
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5811
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5813
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5821
[TakeutiZaring] p. 35Notationwtr 4098
[TakeutiZaring] p. 35Theorem 7.2tz7.2 4351
[TakeutiZaring] p. 35Definition 7.1dftr3 4102
[TakeutiZaring] p. 36Proposition 7.4ordwe 4572
[TakeutiZaring] p. 36Proposition 7.6ordelord 4378
[TakeutiZaring] p. 37Proposition 7.9ordin 4382
[TakeutiZaring] p. 38Corollary 7.15ordsson 4488
[TakeutiZaring] p. 38Definition 7.11df-on 4365
[TakeutiZaring] p. 38Proposition 7.12ordon 4482
[TakeutiZaring] p. 38Proposition 7.13onprc 4548
[TakeutiZaring] p. 39Theorem 7.17tfi 4578
[TakeutiZaring] p. 40Exercise 7dftr2 4100
[TakeutiZaring] p. 40Exercise 11unon 4507
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4483
[TakeutiZaring] p. 40Proposition 7.20elssuni 3835
[TakeutiZaring] p. 41Definition 7.22df-suc 4368
[TakeutiZaring] p. 41Proposition 7.23sssucid 4412  sucidg 4413
[TakeutiZaring] p. 41Proposition 7.24onsuc 4497
[TakeutiZaring] p. 42Exercise 1df-ilim 4366
[TakeutiZaring] p. 42Exercise 8onsucssi 4502  ordelsuc 4501
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4590
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4591
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4592
[TakeutiZaring] p. 43Axiom 7omex 4589
[TakeutiZaring] p. 43Theorem 7.32ordom 4603
[TakeutiZaring] p. 43Corollary 7.31find 4595
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4593
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4594
[TakeutiZaring] p. 44Exercise 2int0 3856
[TakeutiZaring] p. 44Exercise 3trintssm 4114
[TakeutiZaring] p. 44Exercise 4intss1 3857
[TakeutiZaring] p. 44Exercise 6onintonm 4513
[TakeutiZaring] p. 44Definition 7.35df-int 3843
[TakeutiZaring] p. 47Lemma 1tfrlem1 6303
[TakeutiZaring] p. 47Theorem 7.41(1)tfri1 6360  tfri1d 6330
[TakeutiZaring] p. 47Theorem 7.41(2)tfri2 6361  tfri2d 6331
[TakeutiZaring] p. 47Theorem 7.41(3)tfri3 6362
[TakeutiZaring] p. 50Exercise 3smoiso 6297
[TakeutiZaring] p. 50Definition 7.46df-smo 6281
[TakeutiZaring] p. 56Definition 8.1oasuc 6459
[TakeutiZaring] p. 57Proposition 8.2oacl 6455
[TakeutiZaring] p. 57Proposition 8.3oa0 6452
[TakeutiZaring] p. 57Proposition 8.16omcl 6456
[TakeutiZaring] p. 58Proposition 8.4nnaord 6504  nnaordi 6503
[TakeutiZaring] p. 59Proposition 8.6iunss2 3929  uniss2 3838
[TakeutiZaring] p. 59Proposition 8.7oawordriexmid 6465
[TakeutiZaring] p. 59Proposition 8.9nnacl 6475
[TakeutiZaring] p. 62Exercise 5oaword1 6466
[TakeutiZaring] p. 62Definition 8.15om0 6453  omsuc 6467
[TakeutiZaring] p. 63Proposition 8.17nnmcl 6476
[TakeutiZaring] p. 63Proposition 8.19nnmord 6512  nnmordi 6511
[TakeutiZaring] p. 67Definition 8.30oei0 6454
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7180
[TakeutiZaring] p. 88Exercise 1en0 6789
[TakeutiZaring] p. 90Proposition 10.20nneneq 6851
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6852
[TakeutiZaring] p. 91Definition 10.29df-fin 6737  isfi 6755
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6825
[TakeutiZaring] p. 95Definition 10.42df-map 6644
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6842
[Tarski] p. 67Axiom B5ax-4 1510
[Tarski] p. 68Lemma 6equid 1701
[Tarski] p. 69Lemma 7equcomi 1704
[Tarski] p. 70Lemma 14spim 1738  spime 1741  spimeh 1739  spimh 1737
[Tarski] p. 70Lemma 16ax-11 1506  ax-11o 1823  ax11i 1714
[Tarski] p. 70Lemmas 16 and 17sb6 1886
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1526
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 2150  ax-14 2151
[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 2124  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 1481
[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 1635
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1485
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1632
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1895
[WhiteheadRussell] p. 175Definition *14.02df-eu 2029
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2428
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2429
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2875
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 3019
[WhiteheadRussell] p. 190Theorem *14.22iota4 5192
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5193
[WhiteheadRussell] p. 192Theorem *14.26eupick 2105  eupickbi 2108
[WhiteheadRussell] p. 235Definition *30.01df-fv 5220
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7183

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