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 7006  fidcenum 6850
[AczelRathjen], p. 72Proposition 8.1.11fidcenum 6850
[AczelRathjen], p. 73Lemma 8.1.14enumct 7006
[AczelRathjen], p. 73Corollary 8.1.13ennnfone 11967
[AczelRathjen], p. 74Lemma 8.1.16xpfi 6824
[AczelRathjen], p. 74Remark 8.1.17unfiexmid 6812
[AczelRathjen], p. 74Theorem 8.1.19ctiunct 11982
[AczelRathjen], p. 75Corollary 8.1.20unct 11984
[AczelRathjen], p. 75Corollary 8.1.23qnnen 11973  znnen 11940
[AczelRathjen], p. 77Lemma 8.1.27omctfn 11985
[AczelRathjen], p. 78Theorem 8.1.28omiunct 11986
[AczelRathjen], p. 80Corollary 8.2.4df-ihash 10552
[AczelRathjen], p. 183Chapter 20ax-setind 4458
[Apostol] p. 18Theorem I.1addcan 7964  addcan2d 7969  addcan2i 7967  addcand 7968  addcani 7966
[Apostol] p. 18Theorem I.2negeu 7975
[Apostol] p. 18Theorem I.3negsub 8032  negsubd 8101  negsubi 8062
[Apostol] p. 18Theorem I.4negneg 8034  negnegd 8086  negnegi 8054
[Apostol] p. 18Theorem I.5subdi 8169  subdid 8198  subdii 8191  subdir 8170  subdird 8199  subdiri 8192
[Apostol] p. 18Theorem I.6mul01 8173  mul01d 8177  mul01i 8175  mul02 8171  mul02d 8176  mul02i 8174
[Apostol] p. 18Theorem I.9divrecapd 8575
[Apostol] p. 18Theorem I.10recrecapi 8526
[Apostol] p. 18Theorem I.12mul2neg 8182  mul2negd 8197  mul2negi 8190  mulneg1 8179  mulneg1d 8195  mulneg1i 8188
[Apostol] p. 18Theorem I.15divdivdivap 8495
[Apostol] p. 20Axiom 7rpaddcl 9492  rpaddcld 9527  rpmulcl 9493  rpmulcld 9528
[Apostol] p. 20Axiom 90nrp 9504
[Apostol] p. 20Theorem I.17lttri 7890
[Apostol] p. 20Theorem I.18ltadd1d 8322  ltadd1dd 8340  ltadd1i 8286
[Apostol] p. 20Theorem I.19ltmul1 8376  ltmul1a 8375  ltmul1i 8700  ltmul1ii 8708  ltmul2 8636  ltmul2d 9554  ltmul2dd 9568  ltmul2i 8703
[Apostol] p. 20Theorem I.210lt1 7911
[Apostol] p. 20Theorem I.23lt0neg1 8252  lt0neg1d 8299  ltneg 8246  ltnegd 8307  ltnegi 8277
[Apostol] p. 20Theorem I.25lt2add 8229  lt2addd 8351  lt2addi 8294
[Apostol] p. 20Definition of positive numbersdf-rp 9469
[Apostol] p. 21Exercise 4recgt0 8630  recgt0d 8714  recgt0i 8686  recgt0ii 8687
[Apostol] p. 22Definition of integersdf-z 9077
[Apostol] p. 22Definition of rationalsdf-q 9437
[Apostol] p. 24Theorem I.26supeuti 6887
[Apostol] p. 26Theorem I.29arch 8996
[Apostol] p. 28Exercise 2btwnz 9192
[Apostol] p. 28Exercise 3nnrecl 8997
[Apostol] p. 28Exercise 6qbtwnre 10063
[Apostol] p. 28Exercise 10(a)zeneo 11597  zneo 9174
[Apostol] p. 29Theorem I.35resqrtth 10833  sqrtthi 10921
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 8745
[Apostol] p. 363Remarkabsgt0api 10948
[Apostol] p. 363Exampleabssubd 10995  abssubi 10952
[ApostolNT] p. 14Definitiondf-dvds 11523
[ApostolNT] p. 14Theorem 1.1(a)iddvds 11535
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 11559
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 11555
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 11549
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 11551
[ApostolNT] p. 14Theorem 1.1(f)1dvds 11536
[ApostolNT] p. 14Theorem 1.1(g)dvds0 11537
[ApostolNT] p. 14Theorem 1.1(h)0dvds 11542
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 11572
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 11574
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 11576
[ApostolNT] p. 15Definitiondfgcd2 11731
[ApostolNT] p. 16Definitionisprm2 11827
[ApostolNT] p. 16Theorem 1.5coprmdvds 11802
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 11691
[ApostolNT] p. 16Theorem 1.4(b)gcdass 11732
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 11734
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 11704
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 11697
[ApostolNT] p. 17Theorem 1.8coprm 11851
[ApostolNT] p. 17Theorem 1.9euclemma 11853
[ApostolNT] p. 19Theorem 1.14divalg 11650
[ApostolNT] p. 20Theorem 1.15eucalg 11769
[ApostolNT] p. 25Definitiondf-phi 11916
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 11927
[ApostolNT] p. 28Theorem 2.5(c)phimul 11931
[ApostolNT] p. 104Definitioncongr 11810
[ApostolNT] p. 106Remarkdvdsval3 11526
[ApostolNT] p. 106Definitionmoddvds 11531
[ApostolNT] p. 107Example 2mod2eq0even 11604
[ApostolNT] p. 107Example 3mod2eq1n2dvds 11605
[ApostolNT] p. 107Example 4zmod1congr 10143
[ApostolNT] p. 107Theorem 5.2(b)modqmul12d 10180
[ApostolNT] p. 108Theorem 5.3modmulconst 11554
[ApostolNT] p. 109Theorem 5.4cncongr1 11813
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 11815
[Bauer] p. 482Section 1.2pm2.01 606  pm2.65 649
[Bauer] p. 483Theorem 1.3acexmid 5779  onsucelsucexmidlem 4450
[Bauer], p. 481Section 1.1pwtrufal 13358
[Bauer], p. 483Definitionn0rf 3378
[Bauer], p. 483Theorem 1.22irrexpq 13094  2irrexpqap 13096
[Bauer], p. 485Theorem 2.1ssfiexmid 6776
[Bauer], p. 494Theorem 5.5ivthinc 12822
[BauerHanson], p. 27Proposition 5.2cnstab 8429
[BauerSwan], p. 14Remark0ct 6998  ctm 7000
[BauerSwan], p. 14Proposition 2.6subctctexmid 13362
[BauerSwan], p. 14Table" is defined as ` ` per enumct 7006
[BauerTaylor], p. 32Lemma 6.16prarloclem 7331
[BauerTaylor], p. 50Lemma 11.4subhalfnqq 7244
[BauerTaylor], p. 52Proposition 11.15prarloc 7333
[BauerTaylor], p. 53Lemma 11.16addclpr 7367  addlocpr 7366
[BauerTaylor], p. 55Proposition 12.7appdivnq 7393
[BauerTaylor], p. 56Lemma 12.8prmuloc 7396
[BauerTaylor], p. 56Lemma 12.9mullocpr 7401
[BellMachover] p. 36Lemma 10.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 2003
[BellMachover] p. 460Notationdf-mo 2004
[BellMachover] p. 460Definitionmo3 2054  mo3h 2053
[BellMachover] p. 462Theorem 1.1bm1.1 2125
[BellMachover] p. 463Theorem 1.3iibm1.3ii 4055
[BellMachover] p. 466Axiom Powaxpow3 4107
[BellMachover] p. 466Axiom Unionaxun2 4363
[BellMachover] p. 469Theorem 2.2(i)ordirr 4463
[BellMachover] p. 469Theorem 2.2(iii)onelon 4312
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4466
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4418
[BellMachover] p. 471Definition of Limdf-ilim 4297
[BellMachover] p. 472Axiom Infzfinf2 4509
[BellMachover] p. 473Theorem 2.8limom 4533
[Bobzien] p. 116Statement T3stoic3 1408
[Bobzien] p. 117Statement T2stoic2a 1406
[Bobzien] p. 117Statement T4stoic4a 1409
[BourbakiEns] p. Proposition 8fcof1 5690  fcofo 5691
[BourbakiTop1] p. Remarkxnegmnf 9640  xnegpnf 9639
[BourbakiTop1] p. Remark rexneg 9641
[BourbakiTop1] p. Propositionishmeo 12505
[BourbakiTop1] p. Property V_issnei2 12358
[BourbakiTop1] p. Property V_iiinnei 12364
[BourbakiTop1] p. Property V_ivneissex 12366
[BourbakiTop1] p. Proposition 1neipsm 12355  neiss 12351
[BourbakiTop1] p. Proposition 2cnptopco 12423
[BourbakiTop1] p. Proposition 4imasnopn 12500
[BourbakiTop1] p. Property V_iiielnei 12353
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 12197
[ChoquetDD] p. 2Definition of mappingdf-mpt 3997
[Cohen] p. 301Remarkrelogoprlem 12990
[Cohen] p. 301Property 2relogmul 12991  relogmuld 13006
[Cohen] p. 301Property 3relogdiv 12992  relogdivd 13007
[Cohen] p. 301Property 4relogexp 12994
[Cohen] p. 301Property 1alog1 12988
[Cohen] p. 301Property 1bloge 12989
[Cohen4] p. 348Observationrelogbcxpbap 13083
[Cohen4] p. 352Definitionrpelogb 13067
[Cohen4] p. 361Property 2rprelogbmul 13073
[Cohen4] p. 361Property 3logbrec 13078  rprelogbdiv 13075
[Cohen4] p. 361Property 4rplogbreexp 13071
[Cohen4] p. 361Property 6relogbexpap 13076
[Cohen4] p. 361Property 1(a)rplogbid1 13065
[Cohen4] p. 361Property 1(b)rplogb1 13066
[Cohen4] p. 367Propertyrplogbchbase 13068
[Cohen4] p. 377Property 2logblt 13080
[Crosilla] p. Axiom 1ax-ext 2122
[Crosilla] p. Axiom 2ax-pr 4137
[Crosilla] p. Axiom 3ax-un 4361
[Crosilla] p. Axiom 4ax-nul 4060
[Crosilla] p. Axiom 5ax-iinf 4508
[Crosilla] p. Axiom 6ru 2911
[Crosilla] p. Axiom 8ax-pow 4104
[Crosilla] p. Axiom 9ax-setind 4458
[Crosilla], p. Axiom 6ax-sep 4052
[Crosilla], p. Axiom 7ax-coll 4049
[Crosilla], p. Axiom 7'repizf 4050
[Crosilla], p. Theorem is statedordtriexmid 4443
[Crosilla], p. Axiom of choice implies instancesacexmid 5779
[Crosilla], p. Definition of ordinaldf-iord 4294
[Crosilla], p. Theorem "Foundation implies instances of EM"regexmid 4456
[Eisenberg] p. 67Definition 5.3df-dif 3076
[Eisenberg] p. 82Definition 6.3df-iom 4511
[Eisenberg] p. 125Definition 8.21df-map 6550
[Enderton] p. 18Axiom of Empty Setaxnul 4059
[Enderton] p. 19Definitiondf-tp 3538
[Enderton] p. 26Exercise 5unissb 3772
[Enderton] p. 26Exercise 10pwel 4146
[Enderton] p. 28Exercise 7(b)pwunim 4214
[Enderton] p. 30Theorem "Distributive laws"iinin1m 3888  iinin2m 3887  iunin1 3883  iunin2 3882
[Enderton] p. 31Theorem "De Morgan's laws"iindif2m 3886  iundif2ss 3884
[Enderton] p. 33Exercise 23iinuniss 3901
[Enderton] p. 33Exercise 25iununir 3902
[Enderton] p. 33Exercise 24(a)iinpw 3909
[Enderton] p. 33Exercise 24(b)iunpw 4407  iunpwss 3910
[Enderton] p. 38Exercise 6(a)unipw 4145
[Enderton] p. 38Exercise 6(b)pwuni 4122
[Enderton] p. 41Lemma 3Dopeluu 4377  rnex 4812  rnexg 4810
[Enderton] p. 41Exercise 8dmuni 4755  rnuni 4956
[Enderton] p. 42Definition of a functiondffun7 5156  dffun8 5157
[Enderton] p. 43Definition of function valuefunfvdm2 5491
[Enderton] p. 43Definition of single-rootedfuncnv 5190
[Enderton] p. 44Definition (d)dfima2 4889  dfima3 4890
[Enderton] p. 47Theorem 3Hfvco2 5496
[Enderton] p. 49Axiom of Choice (first form)df-ac 7077
[Enderton] p. 50Theorem 3K(a)imauni 5668
[Enderton] p. 52Definitiondf-map 6550
[Enderton] p. 53Exercise 21coass 5063
[Enderton] p. 53Exercise 27dmco 5053
[Enderton] p. 53Exercise 14(a)funin 5200
[Enderton] p. 53Exercise 22(a)imass2 4921
[Enderton] p. 54Remarkixpf 6620  ixpssmap 6632
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6599
[Enderton] p. 56Theorem 3Merref 6455
[Enderton] p. 57Lemma 3Nerthi 6481
[Enderton] p. 57Definitiondf-ec 6437
[Enderton] p. 58Definitiondf-qs 6441
[Enderton] p. 60Theorem 3Qth3q 6540  th3qcor 6539  th3qlem1 6537  th3qlem2 6538
[Enderton] p. 61Exercise 35df-ec 6437
[Enderton] p. 65Exercise 56(a)dmun 4752
[Enderton] p. 68Definition of successordf-suc 4299
[Enderton] p. 71Definitiondf-tr 4033  dftr4 4037
[Enderton] p. 72Theorem 4Eunisuc 4341  unisucg 4342
[Enderton] p. 73Exercise 6unisuc 4341  unisucg 4342
[Enderton] p. 73Exercise 5(a)truni 4046
[Enderton] p. 73Exercise 5(b)trint 4047
[Enderton] p. 79Theorem 4I(A1)nna0 6376
[Enderton] p. 79Theorem 4I(A2)nnasuc 6378  onasuc 6368
[Enderton] p. 79Definition of operation valuedf-ov 5783
[Enderton] p. 80Theorem 4J(A1)nnm0 6377
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6379  onmsuc 6375
[Enderton] p. 81Theorem 4K(1)nnaass 6387
[Enderton] p. 81Theorem 4K(2)nna0r 6380  nnacom 6386
[Enderton] p. 81Theorem 4K(3)nndi 6388
[Enderton] p. 81Theorem 4K(4)nnmass 6389
[Enderton] p. 81Theorem 4K(5)nnmcom 6391
[Enderton] p. 82Exercise 16nnm0r 6381  nnmsucr 6390
[Enderton] p. 88Exercise 23nnaordex 6429
[Enderton] p. 129Definitiondf-en 6641
[Enderton] p. 133Exercise 1xpomen 11937
[Enderton] p. 134Theorem (Pigeonhole Principle)phpm 6765
[Enderton] p. 136Corollary 6Enneneq 6757
[Enderton] p. 139Theorem 6H(c)mapen 6746
[Enderton] p. 142Theorem 6I(3)xpdjuen 7089
[Enderton] p. 143Theorem 6Jdju0en 7085  dju1en 7084
[Enderton] p. 144Corollary 6Kundif2ss 3441
[Enderton] p. 145Figure 38ffoss 5405
[Enderton] p. 145Definitiondf-dom 6642
[Enderton] p. 146Example 1domen 6651  domeng 6652
[Enderton] p. 146Example 3nndomo 6764
[Enderton] p. 149Theorem 6L(c)xpdom1 6735  xpdom1g 6733  xpdom2g 6732
[Enderton] p. 168Definitiondf-po 4224
[Enderton] p. 192Theorem 7M(a)oneli 4356
[Enderton] p. 192Theorem 7M(b)ontr1 4317
[Enderton] p. 192Theorem 7M(c)onirri 4464
[Enderton] p. 193Corollary 7N(b)0elon 4320
[Enderton] p. 193Corollary 7N(c)onsuci 4438
[Enderton] p. 193Corollary 7N(d)ssonunii 4411
[Enderton] p. 194Remarkonprc 4473
[Enderton] p. 194Exercise 16suc11 4479
[Enderton] p. 197Definitiondf-card 7051
[Enderton] p. 200Exercise 25tfis 4503
[Enderton] p. 206Theorem 7X(b)en2lp 4475
[Enderton] p. 207Exercise 34opthreg 4477
[Enderton] p. 208Exercise 35suc11g 4478
[Geuvers], p. 1Remarkexpap0 10352
[Geuvers], p. 6Lemma 2.13mulap0r 8399
[Geuvers], p. 6Lemma 2.15mulap0 8437
[Geuvers], p. 9Lemma 2.35msqge0 8400
[Geuvers], p. 9Definition 3.1(2)ax-arch 7761
[Geuvers], p. 10Lemma 3.9maxcom 11005
[Geuvers], p. 10Lemma 3.10maxle1 11013  maxle2 11014
[Geuvers], p. 10Lemma 3.11maxleast 11015
[Geuvers], p. 10Lemma 3.12maxleb 11018
[Geuvers], p. 11Definition 3.13dfabsmax 11019
[Geuvers], p. 17Definition 6.1df-ap 8366
[Gleason] p. 117Proposition 9-2.1df-enq 7177  enqer 7188
[Gleason] p. 117Proposition 9-2.2df-1nqqs 7181  df-nqqs 7178
[Gleason] p. 117Proposition 9-2.3df-plpq 7174  df-plqqs 7179
[Gleason] p. 119Proposition 9-2.4df-mpq 7175  df-mqqs 7180
[Gleason] p. 119Proposition 9-2.5df-rq 7182
[Gleason] p. 119Proposition 9-2.6ltexnqq 7238
[Gleason] p. 120Proposition 9-2.6(i)halfnq 7241  ltbtwnnq 7246  ltbtwnnqq 7245
[Gleason] p. 120Proposition 9-2.6(ii)ltanqg 7230
[Gleason] p. 120Proposition 9-2.6(iii)ltmnqg 7231
[Gleason] p. 123Proposition 9-3.5addclpr 7367
[Gleason] p. 123Proposition 9-3.5(i)addassprg 7409
[Gleason] p. 123Proposition 9-3.5(ii)addcomprg 7408
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 7427
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 7443
[Gleason] p. 123Proposition 9-3.5(v)ltaprg 7449  ltaprlem 7448
[Gleason] p. 123Proposition 9-3.5(vi)addcanprg 7446
[Gleason] p. 124Proposition 9-3.7mulclpr 7402
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 7422
[Gleason] p. 124Proposition 9-3.7(i)mulassprg 7411
[Gleason] p. 124Proposition 9-3.7(ii)mulcomprg 7410
[Gleason] p. 124Proposition 9-3.7(iii)distrprg 7418
[Gleason] p. 124Proposition 9-3.7(v)recexpr 7468
[Gleason] p. 126Proposition 9-4.1df-enr 7556  enrer 7565
[Gleason] p. 126Proposition 9-4.2df-0r 7561  df-1r 7562  df-nr 7557
[Gleason] p. 126Proposition 9-4.3df-mr 7559  df-plr 7558  negexsr 7602  recexsrlem 7604
[Gleason] p. 127Proposition 9-4.4df-ltr 7560
[Gleason] p. 130Proposition 10-1.3creui 8740  creur 8739  cru 8386
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 7753  axcnre 7711
[Gleason] p. 132Definition 10-3.1crim 10660  crimd 10779  crimi 10739  crre 10659  crred 10778  crrei 10738
[Gleason] p. 132Definition 10-3.2remim 10662  remimd 10744
[Gleason] p. 133Definition 10.36absval2 10859  absval2d 10987  absval2i 10946
[Gleason] p. 133Proposition 10-3.4(a)cjadd 10686  cjaddd 10767  cjaddi 10734
[Gleason] p. 133Proposition 10-3.4(c)cjmul 10687  cjmuld 10768  cjmuli 10735
[Gleason] p. 133Proposition 10-3.4(e)cjcj 10685  cjcjd 10745  cjcji 10717
[Gleason] p. 133Proposition 10-3.4(f)cjre 10684  cjreb 10668  cjrebd 10748  cjrebi 10720  cjred 10773  rere 10667  rereb 10665  rerebd 10747  rerebi 10719  rered 10771
[Gleason] p. 133Proposition 10-3.4(h)addcj 10693  addcjd 10759  addcji 10729
[Gleason] p. 133Proposition 10-3.7(a)absval 10803
[Gleason] p. 133Proposition 10-3.7(b)abscj 10854  abscjd 10992  abscji 10950
[Gleason] p. 133Proposition 10-3.7(c)abs00 10866  abs00d 10988  abs00i 10947  absne0d 10989
[Gleason] p. 133Proposition 10-3.7(d)releabs 10898  releabsd 10993  releabsi 10951
[Gleason] p. 133Proposition 10-3.7(f)absmul 10871  absmuld 10996  absmuli 10953
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 10857  sqabsaddi 10954
[Gleason] p. 133Proposition 10-3.7(h)abstri 10906  abstrid 10998  abstrii 10957
[Gleason] p. 134Definition 10-4.10exp0e1 10327  df-exp 10322  exp0 10326  expp1 10329  expp1d 10454
[Gleason] p. 135Proposition 10-4.2(a)expadd 10364  expaddd 10455
[Gleason] p. 135Proposition 10-4.2(b)cxpmul 13034  cxpmuld 13057  expmul 10367  expmuld 10456
[Gleason] p. 135Proposition 10-4.2(c)mulexp 10361  mulexpd 10468  rpmulcxp 13031
[Gleason] p. 141Definition 11-2.1fzval 9821
[Gleason] p. 168Proposition 12-2.1(a)climadd 11125
[Gleason] p. 168Proposition 12-2.1(b)climsub 11127
[Gleason] p. 168Proposition 12-2.1(c)climmul 11126
[Gleason] p. 171Corollary 12-2.2climmulc2 11130
[Gleason] p. 172Corollary 12-2.5climrecl 11123
[Gleason] p. 172Proposition 12-2.4(c)climabs 11119  climcj 11120  climim 11122  climre 11121
[Gleason] p. 173Definition 12-3.1df-ltxr 7827  df-xr 7826  ltxr 9590
[Gleason] p. 180Theorem 12-5.3climcau 11146
[Gleason] p. 217Lemma 13-4.1btwnzge0 10102
[Gleason] p. 223Definition 14-1.1df-met 12190
[Gleason] p. 223Definition 14-1.1(a)met0 12565  xmet0 12564
[Gleason] p. 223Definition 14-1.1(c)metsym 12572
[Gleason] p. 223Definition 14-1.1(d)mettri 12574  mstri 12674  xmettri 12573  xmstri 12673
[Gleason] p. 230Proposition 14-2.6txlm 12480
[Gleason] p. 240Proposition 14-4.2metcnp3 12712
[Gleason] p. 243Proposition 14-4.16addcn2 11109  addcncntop 12753  mulcn2 11111  mulcncntop 12755  subcn2 11110  subcncntop 12754
[Gleason] p. 295Remarkbcval3 10527  bcval4 10528
[Gleason] p. 295Equation 2bcpasc 10542
[Gleason] p. 295Definition of binomial coefficientbcval 10525  df-bc 10524
[Gleason] p. 296Remarkbcn0 10531  bcnn 10533
[Gleason] p. 296Theorem 15-2.8binom 11283
[Gleason] p. 308Equation 2ef0 11408
[Gleason] p. 308Equation 3efcj 11409
[Gleason] p. 309Corollary 15-4.3efne0 11414
[Gleason] p. 309Corollary 15-4.4efexp 11418
[Gleason] p. 310Equation 14sinadd 11472
[Gleason] p. 310Equation 15cosadd 11473
[Gleason] p. 311Equation 17sincossq 11484
[Gleason] p. 311Equation 18cosbnd 11489  sinbnd 11488
[Gleason] p. 311Definition of ` `df-pi 11389
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 5
[Hamilton] p. 74Rule 2ax-gen 1426
[Heyting] p. 127Axiom #1ax1hfs 13424
[Hitchcock] p. 5Rule A3mptnan 1402
[Hitchcock] p. 5Rule A4mptxor 1403
[Hitchcock] p. 5Rule A5mtpxor 1405
[HoTT], p. Theorem 7.2.6nndceq 6401
[HoTT], p. Exercise 11.10neapmkv 13418
[HoTT], p. Exercise 11.11mulap0bd 8440
[HoTT], p. Section 11.2.1df-iltp 7300  df-imp 7299  df-iplp 7298  df-reap 8359
[HoTT], p. Theorem 11.2.12cauappcvgpr 7492
[HoTT], p. Corollary 11.4.3conventions 13097
[HoTT], p. Exercise 11.6(i)dcapncf 13416
[HoTT], p. Corollary 11.2.13axcaucvg 7730  caucvgpr 7512  caucvgprpr 7542  caucvgsr 7632
[HoTT], p. Definition 11.2.1df-inp 7296
[HoTT], p. Proposition 11.2.3df-iso 4225  ltpopr 7425  ltsopr 7426
[HoTT], p. Definition 11.2.7(v)apsym 8390  reapcotr 8382  reapirr 8361
[HoTT], p. Definition 11.2.7(vi)0lt1 7911  gt0add 8357  leadd1 8214  lelttr 7874  lemul1a 8638  lenlt 7862  ltadd1 8213  ltletr 7875  ltmul1 8376  reaplt 8372
[Jech] p. 4Definition of classcv 1331  cvjust 2135
[Jech] p. 78Noteopthprc 4596
[KalishMontague] p. 81Note 1ax-i9 1511
[Kreyszig] p. 3Property M1metcl 12554  xmetcl 12553
[Kreyszig] p. 4Property M2meteq0 12561
[Kreyszig] p. 12Equation 5muleqadd 8451
[Kreyszig] p. 18Definition 1.3-2mopnval 12643
[Kreyszig] p. 19Remarkmopntopon 12644
[Kreyszig] p. 19Theorem T1mopn0 12689  mopnm 12649
[Kreyszig] p. 19Theorem T2unimopn 12687
[Kreyszig] p. 19Definition of neighborhoodneibl 12692
[Kreyszig] p. 20Definition 1.3-3metcnp2 12714
[Kreyszig] p. 25Definition 1.4-1lmbr 12414
[Kunen] p. 10Axiom 0a9e 1675
[Kunen] p. 12Axiom 6zfrep6 4051
[Kunen] p. 24Definition 10.24mapval 6560  mapvalg 6558
[Kunen] p. 31Definition 10.24mapex 6554
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3829
[Levy] p. 338Axiomdf-clab 2127  df-clel 2136  df-cleq 2133
[Lopez-Astorga] p. 12Rule 1mptnan 1402
[Lopez-Astorga] p. 12Rule 2mptxor 1403
[Lopez-Astorga] p. 12Rule 3mtpxor 1405
[Margaris] p. 40Rule Cexlimiv 1578
[Margaris] p. 49Axiom A1ax-1 6
[Margaris] p. 49Axiom A2ax-2 7
[Margaris] p. 49Axiom A3condc 839
[Margaris] p. 49Definitiondfbi2 386  dfordc 878  exalim 1479
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 45
[Margaris] p. 60Theorem 8jcn 641
[Margaris] p. 89Theorem 19.219.2 1618  r19.2m 3452
[Margaris] p. 89Theorem 19.319.3 1534  19.3h 1533  rr19.3v 2826
[Margaris] p. 89Theorem 19.5alcom 1455
[Margaris] p. 89Theorem 19.6alexdc 1599  alexim 1625
[Margaris] p. 89Theorem 19.7alnex 1476
[Margaris] p. 89Theorem 19.819.8a 1570  spsbe 1815
[Margaris] p. 89Theorem 19.919.9 1624  19.9h 1623  19.9v 1844  exlimd 1577
[Margaris] p. 89Theorem 19.11excom 1643  excomim 1642
[Margaris] p. 89Theorem 19.1219.12 1644  r19.12 2541
[Margaris] p. 90Theorem 19.14exnalim 1626
[Margaris] p. 90Theorem 19.15albi 1445  ralbi 2567
[Margaris] p. 90Theorem 19.1619.16 1535
[Margaris] p. 90Theorem 19.1719.17 1536
[Margaris] p. 90Theorem 19.18exbi 1584  rexbi 2568
[Margaris] p. 90Theorem 19.1919.19 1645
[Margaris] p. 90Theorem 19.20alim 1434  alimd 1502  alimdh 1444  alimdv 1852  ralimdaa 2501  ralimdv 2503  ralimdva 2502  ralimdvva 2504  sbcimdv 2977
[Margaris] p. 90Theorem 19.2119.21-2 1646  19.21 1563  19.21bi 1538  19.21h 1537  19.21ht 1561  19.21t 1562  19.21v 1846  alrimd 1590  alrimdd 1589  alrimdh 1456  alrimdv 1849  alrimi 1503  alrimih 1446  alrimiv 1847  alrimivv 1848  r19.21 2511  r19.21be 2526  r19.21bi 2523  r19.21t 2510  r19.21v 2512  ralrimd 2513  ralrimdv 2514  ralrimdva 2515  ralrimdvv 2519  ralrimdvva 2520  ralrimi 2506  ralrimiv 2507  ralrimiva 2508  ralrimivv 2516  ralrimivva 2517  ralrimivvva 2518  ralrimivw 2509  rexlimi 2545
[Margaris] p. 90Theorem 19.222alimdv 1854  2eximdv 1855  exim 1579  eximd 1592  eximdh 1591  eximdv 1853  rexim 2529  reximdai 2533  reximddv 2538  reximddv2 2540  reximdv 2536  reximdv2 2534  reximdva 2537  reximdvai 2535  reximi2 2531
[Margaris] p. 90Theorem 19.2319.23 1657  19.23bi 1572  19.23h 1475  19.23ht 1474  19.23t 1656  19.23v 1856  19.23vv 1857  exlimd2 1575  exlimdh 1576  exlimdv 1792  exlimdvv 1870  exlimi 1574  exlimih 1573  exlimiv 1578  exlimivv 1869  r19.23 2543  r19.23v 2544  rexlimd 2549  rexlimdv 2551  rexlimdv3a 2554  rexlimdva 2552  rexlimdva2 2555  rexlimdvaa 2553  rexlimdvv 2559  rexlimdvva 2560  rexlimdvw 2556  rexlimiv 2546  rexlimiva 2547  rexlimivv 2558
[Margaris] p. 90Theorem 19.24i19.24 1619
[Margaris] p. 90Theorem 19.2519.25 1606
[Margaris] p. 90Theorem 19.2619.26-2 1459  19.26-3an 1460  19.26 1458  r19.26-2 2564  r19.26-3 2565  r19.26 2561  r19.26m 2566
[Margaris] p. 90Theorem 19.2719.27 1541  19.27h 1540  19.27v 1872  r19.27av 2570  r19.27m 3461  r19.27mv 3462
[Margaris] p. 90Theorem 19.2819.28 1543  19.28h 1542  19.28v 1873  r19.28av 2571  r19.28m 3455  r19.28mv 3458  rr19.28v 2827
[Margaris] p. 90Theorem 19.2919.29 1600  19.29r 1601  19.29r2 1602  19.29x 1603  r19.29 2572  r19.29d2r 2579  r19.29r 2573
[Margaris] p. 90Theorem 19.3019.30dc 1607
[Margaris] p. 90Theorem 19.3119.31r 1660
[Margaris] p. 90Theorem 19.3219.32dc 1658  19.32r 1659  r19.32r 2581  r19.32vdc 2583  r19.32vr 2582
[Margaris] p. 90Theorem 19.3319.33 1461  19.33b2 1609  19.33bdc 1610
[Margaris] p. 90Theorem 19.3419.34 1663
[Margaris] p. 90Theorem 19.3519.35-1 1604  19.35i 1605
[Margaris] p. 90Theorem 19.3619.36-1 1652  19.36aiv 1874  19.36i 1651  r19.36av 2585
[Margaris] p. 90Theorem 19.3719.37-1 1653  19.37aiv 1654  r19.37 2586  r19.37av 2587
[Margaris] p. 90Theorem 19.3819.38 1655
[Margaris] p. 90Theorem 19.39i19.39 1620
[Margaris] p. 90Theorem 19.4019.40-2 1612  19.40 1611  r19.40 2588
[Margaris] p. 90Theorem 19.4119.41 1665  19.41h 1664  19.41v 1875  19.41vv 1876  19.41vvv 1877  19.41vvvv 1878  r19.41 2589  r19.41v 2590
[Margaris] p. 90Theorem 19.4219.42 1667  19.42h 1666  19.42v 1879  19.42vv 1884  19.42vvv 1885  19.42vvvv 1886  r19.42v 2591
[Margaris] p. 90Theorem 19.4319.43 1608  r19.43 2592
[Margaris] p. 90Theorem 19.4419.44 1661  r19.44av 2593  r19.44mv 3460
[Margaris] p. 90Theorem 19.4519.45 1662  r19.45av 2594  r19.45mv 3459
[Margaris] p. 110Exercise 2(b)eu1 2025
[Megill] p. 444Axiom C5ax-17 1507
[Megill] p. 445Lemma L12alequcom 1496  ax-10 1484
[Megill] p. 446Lemma L17equtrr 1687
[Megill] p. 446Lemma L19hbnae 1700
[Megill] p. 447Remark 9.1df-sb 1737  sbid 1748
[Megill] p. 448Scheme C5'ax-4 1488
[Megill] p. 448Scheme C6'ax-7 1425
[Megill] p. 448Scheme C8'ax-8 1483
[Megill] p. 448Scheme C9'ax-i12 1486
[Megill] p. 448Scheme C11'ax-10o 1695
[Megill] p. 448Scheme C12'ax-13 1492
[Megill] p. 448Scheme C13'ax-14 1493
[Megill] p. 448Scheme C15'ax-11o 1796
[Megill] p. 448Scheme C16'ax-16 1787
[Megill] p. 448Theorem 9.4dral1 1709  dral2 1710  drex1 1771  drex2 1711  drsb1 1772  drsb2 1814
[Megill] p. 449Theorem 9.7sbcom2 1963  sbequ 1813  sbid2v 1972
[Megill] p. 450Example in Appendixhba1 1521
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 2994  rspsbca 2995  stdpc4 1749
[Mendelson] p. 69Axiom 5ra5 3000  stdpc5 1564
[Mendelson] p. 81Rule Cexlimiv 1578
[Mendelson] p. 95Axiom 6stdpc6 1680
[Mendelson] p. 95Axiom 7stdpc7 1744
[Mendelson] p. 231Exercise 4.10(k)inv1 3402
[Mendelson] p. 231Exercise 4.10(l)unv 3403
[Mendelson] p. 231Exercise 4.10(n)inssun 3319
[Mendelson] p. 231Exercise 4.10(o)df-nul 3367
[Mendelson] p. 231Exercise 4.10(q)inssddif 3320
[Mendelson] p. 231Exercise 4.10(s)ddifnel 3210
[Mendelson] p. 231Definition of unionunssin 3318
[Mendelson] p. 235Exercise 4.12(c)univ 4403
[Mendelson] p. 235Exercise 4.12(d)pwv 3741
[Mendelson] p. 235Exercise 4.12(j)pwin 4210
[Mendelson] p. 235Exercise 4.12(k)pwunss 4211
[Mendelson] p. 235Exercise 4.12(l)pwssunim 4212
[Mendelson] p. 235Exercise 4.12(n)uniin 3762
[Mendelson] p. 235Exercise 4.12(p)reli 4674
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 5065
[Mendelson] p. 246Definition of successordf-suc 4299
[Mendelson] p. 254Proposition 4.22(b)xpen 6745
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6721  xpsneng 6722
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6727  xpcomeng 6728
[Mendelson] p. 254Proposition 4.22(e)xpassen 6730
[Mendelson] p. 255Exercise 4.39endisj 6724
[Mendelson] p. 255Exercise 4.41mapprc 6552
[Mendelson] p. 255Exercise 4.43mapsnen 6711
[Mendelson] p. 255Exercise 4.47xpmapen 6750
[Mendelson] p. 255Exercise 4.42(a)map0e 6586
[Mendelson] p. 255Exercise 4.42(b)map1 6712
[Mendelson] p. 258Exercise 4.56(c)djuassen 7088  djucomen 7087
[Mendelson] p. 258Exercise 4.56(g)xp2dju 7086
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6369
[Monk1] p. 26Theorem 2.8(vii)ssin 3301
[Monk1] p. 33Theorem 3.2(i)ssrel 4633
[Monk1] p. 33Theorem 3.2(ii)eqrel 4634
[Monk1] p. 34Definition 3.3df-opab 3996
[Monk1] p. 36Theorem 3.7(i)coi1 5060  coi2 5061
[Monk1] p. 36Theorem 3.8(v)dm0 4759  rn0 4801
[Monk1] p. 36Theorem 3.7(ii)cnvi 4949
[Monk1] p. 37Theorem 3.13(i)relxp 4654
[Monk1] p. 37Theorem 3.13(x)dmxpm 4765  rnxpm 4974
[Monk1] p. 37Theorem 3.13(ii)0xp 4625  xp0 4964
[Monk1] p. 38Theorem 3.16(ii)ima0 4904
[Monk1] p. 38Theorem 3.16(viii)imai 4901
[Monk1] p. 39Theorem 3.17imaex 4900  imaexg 4899
[Monk1] p. 39Theorem 3.16(xi)imassrn 4898
[Monk1] p. 41Theorem 4.3(i)fnopfv 5556  funfvop 5538
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5471
[Monk1] p. 42Theorem 4.4(iii)fvelima 5479
[Monk1] p. 43Theorem 4.6funun 5173
[Monk1] p. 43Theorem 4.8(iv)dff13 5675  dff13f 5677
[Monk1] p. 46Theorem 4.15(v)funex 5649  funrnex 6018
[Monk1] p. 50Definition 5.4fniunfv 5669
[Monk1] p. 52Theorem 5.12(ii)op2ndb 5028
[Monk1] p. 52Theorem 5.11(viii)ssint 3793
[Monk1] p. 52Definition 5.13 (i)1stval2 6059  df-1st 6044
[Monk1] p. 52Definition 5.13 (ii)2ndval2 6060  df-2nd 6045
[Monk2] p. 105Axiom C4ax-5 1424
[Monk2] p. 105Axiom C7ax-8 1483
[Monk2] p. 105Axiom C8ax-11 1485  ax-11o 1796
[Monk2] p. 105Axiom (C8)ax11v 1800
[Monk2] p. 109Lemma 12ax-7 1425
[Monk2] p. 109Lemma 15equvin 1836  equvini 1732  eqvinop 4171
[Monk2] p. 113Axiom C5-1ax-17 1507
[Monk2] p. 113Axiom C5-2ax6b 1630
[Monk2] p. 113Axiom C5-3ax-7 1425
[Monk2] p. 114Lemma 22hba1 1521
[Monk2] p. 114Lemma 23hbia1 1532  nfia1 1560
[Monk2] p. 114Lemma 24hba2 1531  nfa2 1559
[Moschovakis] p. 2Chapter 2 df-stab 817  dftest 13425
[Munkres] p. 77Example 2distop 12286
[Munkres] p. 78Definition of basisdf-bases 12242  isbasis3g 12245
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 12173  tgval2 12252
[Munkres] p. 79Remarktgcl 12265
[Munkres] p. 80Lemma 2.1tgval3 12259
[Munkres] p. 80Lemma 2.2tgss2 12280  tgss3 12279
[Munkres] p. 81Lemma 2.3basgen 12281  basgen2 12282
[Munkres] p. 89Definition of subspace topologyresttop 12371
[Munkres] p. 93Theorem 6.1(1)0cld 12313  topcld 12310
[Munkres] p. 93Theorem 6.1(3)uncld 12314
[Munkres] p. 94Definition of closureclsval 12312
[Munkres] p. 94Definition of interiorntrval 12311
[Munkres] p. 102Definition of continuous functiondf-cn 12389  iscn 12398  iscn2 12401
[Munkres] p. 107Theorem 7.2(g)cncnp 12431  cncnp2m 12432  cncnpi 12429  df-cnp 12390  iscnp 12400
[Munkres] p. 127Theorem 10.1metcn 12715
[Pierik], p. 8Section 2.2.1dfrex2fin 6803
[Pierik], p. 9Definition 2.4df-womni 7044
[Pierik], p. 9Definition 2.5df-markov 7032  omniwomnimkv 7047
[Pierik], p. 10Section 2.3dfdif3 3189
[Pierik], p. 14Definition 3.1df-omni 7012  exmidomniim 7019  finomni 7018
[Pierik], p. 15Section 3.1df-nninf 7013
[PradicBrown2022], p. 1Theorem 1exmidsbthr 13386
[PradicBrown2022], p. 2Remarkexmidpw 6808
[PradicBrown2022], p. 2Proposition 1.1exmidfodomrlemim 7072
[PradicBrown2022], p. 2Proposition 1.2exmidfodomrlemr 7073  exmidfodomrlemrALT 7074
[PradicBrown2022], p. 4Lemma 3.2fodjuomni 7027
[PradicBrown2022], p. 5Lemma 3.4peano3nninf 13369  peano4nninf 13368
[PradicBrown2022], p. 5Lemma 3.5nninfall 13372
[PradicBrown2022], p. 5Theorem 3.6nninfsel 13381
[PradicBrown2022], p. 5Corollary 3.7nninfomni 13383
[PradicBrown2022], p. 5Definition 3.3nnsf 13367
[Quine] p. 16Definition 2.1df-clab 2127  rabid 2609
[Quine] p. 17Definition 2.1''dfsb7 1967
[Quine] p. 18Definition 2.7df-cleq 2133
[Quine] p. 19Definition 2.9df-v 2691
[Quine] p. 34Theorem 5.1abeq2 2249
[Quine] p. 35Theorem 5.2abid2 2261  abid2f 2307
[Quine] p. 40Theorem 6.1sb5 1860
[Quine] p. 40Theorem 6.2sb56 1858  sb6 1859
[Quine] p. 41Theorem 6.3df-clel 2136
[Quine] p. 41Theorem 6.4eqid 2140
[Quine] p. 41Theorem 6.5eqcom 2142
[Quine] p. 42Theorem 6.6df-sbc 2913
[Quine] p. 42Theorem 6.7dfsbcq 2914  dfsbcq2 2915
[Quine] p. 43Theorem 6.8vex 2692
[Quine] p. 43Theorem 6.9isset 2695
[Quine] p. 44Theorem 7.3spcgf 2771  spcgv 2776  spcimgf 2769
[Quine] p. 44Theorem 6.11spsbc 2923  spsbcd 2924
[Quine] p. 44Theorem 6.12elex 2700
[Quine] p. 44Theorem 6.13elab 2831  elabg 2833  elabgf 2829
[Quine] p. 44Theorem 6.14noel 3370
[Quine] p. 48Theorem 7.2snprc 3594
[Quine] p. 48Definition 7.1df-pr 3537  df-sn 3536
[Quine] p. 49Theorem 7.4snss 3655  snssg 3662
[Quine] p. 49Theorem 7.5prss 3682  prssg 3683
[Quine] p. 49Theorem 7.6prid1 3635  prid1g 3633  prid2 3636  prid2g 3634  snid 3561  snidg 3559
[Quine] p. 51Theorem 7.12snexg 4114  snexprc 4116
[Quine] p. 51Theorem 7.13prexg 4139
[Quine] p. 53Theorem 8.2unisn 3758  unisng 3759
[Quine] p. 53Theorem 8.3uniun 3761
[Quine] p. 54Theorem 8.6elssuni 3770
[Quine] p. 54Theorem 8.7uni0 3769
[Quine] p. 56Theorem 8.17uniabio 5104
[Quine] p. 56Definition 8.18dfiota2 5095
[Quine] p. 57Theorem 8.19iotaval 5105
[Quine] p. 57Theorem 8.22iotanul 5109
[Quine] p. 58Theorem 8.23euiotaex 5110
[Quine] p. 58Definition 9.1df-op 3539
[Quine] p. 61Theorem 9.5opabid 4185  opelopab 4199  opelopaba 4194  opelopabaf 4201  opelopabf 4202  opelopabg 4196  opelopabga 4191  oprabid 5809
[Quine] p. 64Definition 9.11df-xp 4551
[Quine] p. 64Definition 9.12df-cnv 4553
[Quine] p. 64Definition 9.15df-id 4221
[Quine] p. 65Theorem 10.3fun0 5187
[Quine] p. 65Theorem 10.4funi 5161
[Quine] p. 65Theorem 10.5funsn 5177  funsng 5175
[Quine] p. 65Definition 10.1df-fun 5131
[Quine] p. 65Definition 10.2args 4914  dffv4g 5424
[Quine] p. 68Definition 10.11df-fv 5137  fv2 5422
[Quine] p. 124Theorem 17.3nn0opth2 10500  nn0opth2d 10499  nn0opthd 10498
[Quine] p. 284Axiom 39(vi)funimaex 5214  funimaexg 5213
[Rudin] p. 164Equation 27efcan 11412
[Rudin] p. 164Equation 30efzval 11419
[Rudin] p. 167Equation 48absefi 11504
[Sanford] p. 39Remarkax-mp 5
[Sanford] p. 39Rule 3mtpxor 1405
[Sanford] p. 39Rule 4mptxor 1403
[Sanford] p. 40Rule 1mptnan 1402
[Schechter] p. 51Definition of antisymmetryintasym 4929
[Schechter] p. 51Definition of irreflexivityintirr 4931
[Schechter] p. 51Definition of symmetrycnvsym 4928
[Schechter] p. 51Definition of transitivitycotr 4926
[Schechter] p. 428Definition 15.35bastop1 12284
[Stoll] p. 13Definition of symmetric differencesymdif1 3344
[Stoll] p. 16Exercise 4.40dif 3437  dif0 3436
[Stoll] p. 16Exercise 4.8difdifdirss 3450
[Stoll] p. 19Theorem 5.2(13)undm 3337
[Stoll] p. 19Theorem 5.2(13')indmss 3338
[Stoll] p. 20Remarkinvdif 3321
[Stoll] p. 25Definition of ordered tripledf-ot 3540
[Stoll] p. 43Definitionuniiun 3872
[Stoll] p. 44Definitionintiin 3873
[Stoll] p. 45Definitiondf-iin 3822
[Stoll] p. 45Definition indexed uniondf-iun 3821
[Stoll] p. 176Theorem 3.4(27)imandc 875  imanst 874
[Stoll] p. 262Example 4.1symdif1 3344
[Suppes] p. 22Theorem 2eq0 3384
[Suppes] p. 22Theorem 4eqss 3115  eqssd 3117  eqssi 3116
[Suppes] p. 23Theorem 5ss0 3406  ss0b 3405
[Suppes] p. 23Theorem 6sstr 3108
[Suppes] p. 25Theorem 12elin 3262  elun 3220
[Suppes] p. 26Theorem 15inidm 3288
[Suppes] p. 26Theorem 16in0 3400
[Suppes] p. 27Theorem 23unidm 3222
[Suppes] p. 27Theorem 24un0 3399
[Suppes] p. 27Theorem 25ssun1 3242
[Suppes] p. 27Theorem 26ssequn1 3249
[Suppes] p. 27Theorem 27unss 3253
[Suppes] p. 27Theorem 28indir 3328
[Suppes] p. 27Theorem 29undir 3329
[Suppes] p. 28Theorem 32difid 3434  difidALT 3435
[Suppes] p. 29Theorem 33difin 3316
[Suppes] p. 29Theorem 34indif 3322
[Suppes] p. 29Theorem 35undif1ss 3440
[Suppes] p. 29Theorem 36difun2 3445
[Suppes] p. 29Theorem 37difin0 3439
[Suppes] p. 29Theorem 38disjdif 3438
[Suppes] p. 29Theorem 39difundi 3331
[Suppes] p. 29Theorem 40difindiss 3333
[Suppes] p. 30Theorem 41nalset 4064
[Suppes] p. 39Theorem 61uniss 3763
[Suppes] p. 39Theorem 65uniop 4183
[Suppes] p. 41Theorem 70intsn 3812
[Suppes] p. 42Theorem 71intpr 3809  intprg 3810
[Suppes] p. 42Theorem 73op1stb 4405  op1stbg 4406
[Suppes] p. 42Theorem 78intun 3808
[Suppes] p. 44Definition 15(a)dfiun2 3853  dfiun2g 3851
[Suppes] p. 44Definition 15(b)dfiin2 3854
[Suppes] p. 47Theorem 86elpw 3519  elpw2 4088  elpw2g 4087  elpwg 3521
[Suppes] p. 47Theorem 87pwid 3528
[Suppes] p. 47Theorem 89pw0 3673
[Suppes] p. 48Theorem 90pwpw0ss 3737
[Suppes] p. 52Theorem 101xpss12 4652
[Suppes] p. 52Theorem 102xpindi 4680  xpindir 4681
[Suppes] p. 52Theorem 103xpundi 4601  xpundir 4602
[Suppes] p. 54Theorem 105elirrv 4469
[Suppes] p. 58Theorem 2relss 4632
[Suppes] p. 59Theorem 4eldm 4742  eldm2 4743  eldm2g 4741  eldmg 4740
[Suppes] p. 59Definition 3df-dm 4555
[Suppes] p. 60Theorem 6dmin 4753
[Suppes] p. 60Theorem 8rnun 4953
[Suppes] p. 60Theorem 9rnin 4954
[Suppes] p. 60Definition 4dfrn2 4733
[Suppes] p. 61Theorem 11brcnv 4728  brcnvg 4726
[Suppes] p. 62Equation 5elcnv 4722  elcnv2 4723
[Suppes] p. 62Theorem 12relcnv 4923
[Suppes] p. 62Theorem 15cnvin 4952
[Suppes] p. 62Theorem 16cnvun 4950
[Suppes] p. 63Theorem 20co02 5058
[Suppes] p. 63Theorem 21dmcoss 4814
[Suppes] p. 63Definition 7df-co 4554
[Suppes] p. 64Theorem 26cnvco 4730
[Suppes] p. 64Theorem 27coass 5063
[Suppes] p. 65Theorem 31resundi 4838
[Suppes] p. 65Theorem 34elima 4892  elima2 4893  elima3 4894  elimag 4891
[Suppes] p. 65Theorem 35imaundi 4957
[Suppes] p. 66Theorem 40dminss 4959
[Suppes] p. 66Theorem 41imainss 4960
[Suppes] p. 67Exercise 11cnvxp 4963
[Suppes] p. 81Definition 34dfec2 6438
[Suppes] p. 82Theorem 72elec 6474  elecg 6473
[Suppes] p. 82Theorem 73erth 6479  erth2 6480
[Suppes] p. 89Theorem 96map0b 6587
[Suppes] p. 89Theorem 97map0 6589  map0g 6588
[Suppes] p. 89Theorem 98mapsn 6590
[Suppes] p. 89Theorem 99mapss 6591
[Suppes] p. 92Theorem 1enref 6665  enrefg 6664
[Suppes] p. 92Theorem 2ensym 6681  ensymb 6680  ensymi 6682
[Suppes] p. 92Theorem 3entr 6684
[Suppes] p. 92Theorem 4unen 6716
[Suppes] p. 94Theorem 15endom 6663
[Suppes] p. 94Theorem 16ssdomg 6678
[Suppes] p. 94Theorem 17domtr 6685
[Suppes] p. 95Theorem 18isbth 6861
[Suppes] p. 98Exercise 4fundmen 6706  fundmeng 6707
[Suppes] p. 98Exercise 6xpdom3m 6734
[Suppes] p. 130Definition 3df-tr 4033
[Suppes] p. 132Theorem 9ssonuni 4410
[Suppes] p. 134Definition 6df-suc 4299
[Suppes] p. 136Theorem Schema 22findes 4523  finds 4520  finds1 4522  finds2 4521
[Suppes] p. 162Definition 5df-ltnqqs 7183  df-ltpq 7176
[Suppes] p. 228Theorem Schema 61onintss 4318
[TakeutiZaring] p. 8Axiom 1ax-ext 2122
[TakeutiZaring] p. 13Definition 4.5df-cleq 2133
[TakeutiZaring] p. 13Proposition 4.6df-clel 2136
[TakeutiZaring] p. 13Proposition 4.9cvjust 2135
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2158
[TakeutiZaring] p. 14Definition 4.16df-oprab 5784
[TakeutiZaring] p. 14Proposition 4.14ru 2911
[TakeutiZaring] p. 15Exercise 1elpr 3551  elpr2 3552  elprg 3550
[TakeutiZaring] p. 15Exercise 2elsn 3546  elsn2 3564  elsn2g 3563  elsng 3545  velsn 3547
[TakeutiZaring] p. 15Exercise 3elop 4159
[TakeutiZaring] p. 15Exercise 4sneq 3541  sneqr 3693
[TakeutiZaring] p. 15Definition 5.1dfpr2 3549  dfsn2 3544
[TakeutiZaring] p. 16Axiom 3uniex 4365
[TakeutiZaring] p. 16Exercise 6opth 4165
[TakeutiZaring] p. 16Exercise 8rext 4143
[TakeutiZaring] p. 16Corollary 5.8unex 4368  unexg 4370
[TakeutiZaring] p. 16Definition 5.3dftp2 3578
[TakeutiZaring] p. 16Definition 5.5df-uni 3743
[TakeutiZaring] p. 16Definition 5.6df-in 3080  df-un 3078
[TakeutiZaring] p. 16Proposition 5.7unipr 3756  uniprg 3757
[TakeutiZaring] p. 17Axiom 4vpwex 4109
[TakeutiZaring] p. 17Exercise 1eltp 3577
[TakeutiZaring] p. 17Exercise 5elsuc 4334  elsucg 4332  sstr2 3107
[TakeutiZaring] p. 17Exercise 6uncom 3223
[TakeutiZaring] p. 17Exercise 7incom 3271
[TakeutiZaring] p. 17Exercise 8unass 3236
[TakeutiZaring] p. 17Exercise 9inass 3289
[TakeutiZaring] p. 17Exercise 10indi 3326
[TakeutiZaring] p. 17Exercise 11undi 3327
[TakeutiZaring] p. 17Definition 5.9dfss2 3089
[TakeutiZaring] p. 17Definition 5.10df-pw 3515
[TakeutiZaring] p. 18Exercise 7unss2 3250
[TakeutiZaring] p. 18Exercise 9df-ss 3087  sseqin2 3298
[TakeutiZaring] p. 18Exercise 10ssid 3120
[TakeutiZaring] p. 18Exercise 12inss1 3299  inss2 3300
[TakeutiZaring] p. 18Exercise 13nssr 3160
[TakeutiZaring] p. 18Exercise 15unieq 3751
[TakeutiZaring] p. 18Exercise 18sspwb 4144
[TakeutiZaring] p. 18Exercise 19pweqb 4151
[TakeutiZaring] p. 20Definitiondf-rab 2426
[TakeutiZaring] p. 20Corollary 5.160ex 4061
[TakeutiZaring] p. 20Definition 5.12df-dif 3076
[TakeutiZaring] p. 20Definition 5.14dfnul2 3368
[TakeutiZaring] p. 20Proposition 5.15difid 3434  difidALT 3435
[TakeutiZaring] p. 20Proposition 5.17(1)n0rf 3378
[TakeutiZaring] p. 21Theorem 5.22setind 4460
[TakeutiZaring] p. 21Definition 5.20df-v 2691
[TakeutiZaring] p. 21Proposition 5.21vprc 4066
[TakeutiZaring] p. 22Exercise 10ss 3404
[TakeutiZaring] p. 22Exercise 3ssex 4071  ssexg 4073
[TakeutiZaring] p. 22Exercise 4inex1 4068
[TakeutiZaring] p. 22Exercise 5ruv 4471
[TakeutiZaring] p. 22Exercise 6elirr 4462
[TakeutiZaring] p. 22Exercise 7ssdif0im 3430
[TakeutiZaring] p. 22Exercise 11difdif 3204
[TakeutiZaring] p. 22Exercise 13undif3ss 3340
[TakeutiZaring] p. 22Exercise 14difss 3205
[TakeutiZaring] p. 22Exercise 15sscon 3213
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2422
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2423
[TakeutiZaring] p. 23Proposition 6.2xpex 4660  xpexg 4659  xpexgALT 6037
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4552
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5193
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5345  fun11 5196
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5140  svrelfun 5194
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4732
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4734
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4557
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4558
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4554
[TakeutiZaring] p. 25Exercise 2cnvcnvss 4999  dfrel2 4995
[TakeutiZaring] p. 25Exercise 3xpss 4653
[TakeutiZaring] p. 25Exercise 5relun 4662
[TakeutiZaring] p. 25Exercise 6reluni 4668
[TakeutiZaring] p. 25Exercise 9inxp 4679
[TakeutiZaring] p. 25Exercise 12relres 4853
[TakeutiZaring] p. 25Exercise 13opelres 4830  opelresg 4832
[TakeutiZaring] p. 25Exercise 14dmres 4846
[TakeutiZaring] p. 25Exercise 15resss 4849
[TakeutiZaring] p. 25Exercise 17resabs1 4854
[TakeutiZaring] p. 25Exercise 18funres 5170
[TakeutiZaring] p. 25Exercise 24relco 5043
[TakeutiZaring] p. 25Exercise 29funco 5169
[TakeutiZaring] p. 25Exercise 30f1co 5346
[TakeutiZaring] p. 26Definition 6.10eu2 2044
[TakeutiZaring] p. 26Definition 6.11df-fv 5137  fv3 5450
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5083  cnvexg 5082
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4811  dmexg 4809
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4812  rnexg 4810
[TakeutiZaring] p. 27Corollary 6.13funfvex 5444
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5454  tz6.12 5455  tz6.12c 5457
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5418
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5132
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5133
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5135  wfo 5127
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5134  wf1 5126
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5136  wf1o 5128
[TakeutiZaring] p. 28Exercise 4eqfnfv 5524  eqfnfv2 5525  eqfnfv2f 5528
[TakeutiZaring] p. 28Exercise 5fvco 5497
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5648  fnexALT 6017
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5647  resfunexgALT 6014
[TakeutiZaring] p. 29Exercise 9funimaex 5214  funimaexg 5213
[TakeutiZaring] p. 29Definition 6.18df-br 3936
[TakeutiZaring] p. 30Definition 6.21eliniseg 4915  iniseg 4917
[TakeutiZaring] p. 30Definition 6.22df-eprel 4217
[TakeutiZaring] p. 32Definition 6.28df-isom 5138
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5717
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5718
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5723
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5725
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5733
[TakeutiZaring] p. 35Notationwtr 4032
[TakeutiZaring] p. 35Theorem 7.2tz7.2 4282
[TakeutiZaring] p. 35Definition 7.1dftr3 4036
[TakeutiZaring] p. 36Proposition 7.4ordwe 4496
[TakeutiZaring] p. 36Proposition 7.6ordelord 4309
[TakeutiZaring] p. 37Proposition 7.9ordin 4313
[TakeutiZaring] p. 38Corollary 7.15ordsson 4414
[TakeutiZaring] p. 38Definition 7.11df-on 4296
[TakeutiZaring] p. 38Proposition 7.12ordon 4408
[TakeutiZaring] p. 38Proposition 7.13onprc 4473
[TakeutiZaring] p. 39Theorem 7.17tfi 4502
[TakeutiZaring] p. 40Exercise 7dftr2 4034
[TakeutiZaring] p. 40Exercise 11unon 4433
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4409
[TakeutiZaring] p. 40Proposition 7.20elssuni 3770
[TakeutiZaring] p. 41Definition 7.22df-suc 4299
[TakeutiZaring] p. 41Proposition 7.23sssucid 4343  sucidg 4344
[TakeutiZaring] p. 41Proposition 7.24suceloni 4423
[TakeutiZaring] p. 42Exercise 1df-ilim 4297
[TakeutiZaring] p. 42Exercise 8onsucssi 4428  ordelsuc 4427
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4514
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4515
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4516
[TakeutiZaring] p. 43Axiom 7omex 4513
[TakeutiZaring] p. 43Theorem 7.32ordom 4526
[TakeutiZaring] p. 43Corollary 7.31find 4519
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4517
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4518
[TakeutiZaring] p. 44Exercise 2int0 3791
[TakeutiZaring] p. 44Exercise 3trintssm 4048
[TakeutiZaring] p. 44Exercise 4intss1 3792
[TakeutiZaring] p. 44Exercise 6onintonm 4439
[TakeutiZaring] p. 44Definition 7.35df-int 3778
[TakeutiZaring] p. 47Lemma 1tfrlem1 6211
[TakeutiZaring] p. 47Theorem 7.41(1)tfri1 6268  tfri1d 6238
[TakeutiZaring] p. 47Theorem 7.41(2)tfri2 6269  tfri2d 6239
[TakeutiZaring] p. 47Theorem 7.41(3)tfri3 6270
[TakeutiZaring] p. 50Exercise 3smoiso 6205
[TakeutiZaring] p. 50Definition 7.46df-smo 6189
[TakeutiZaring] p. 56Definition 8.1oasuc 6366
[TakeutiZaring] p. 57Proposition 8.2oacl 6362
[TakeutiZaring] p. 57Proposition 8.3oa0 6359
[TakeutiZaring] p. 57Proposition 8.16omcl 6363
[TakeutiZaring] p. 58Proposition 8.4nnaord 6411  nnaordi 6410
[TakeutiZaring] p. 59Proposition 8.6iunss2 3864  uniss2 3773
[TakeutiZaring] p. 59Proposition 8.7oawordriexmid 6372
[TakeutiZaring] p. 59Proposition 8.9nnacl 6382
[TakeutiZaring] p. 62Exercise 5oaword1 6373
[TakeutiZaring] p. 62Definition 8.15om0 6360  omsuc 6374
[TakeutiZaring] p. 63Proposition 8.17nnmcl 6383
[TakeutiZaring] p. 63Proposition 8.19nnmord 6419  nnmordi 6418
[TakeutiZaring] p. 67Definition 8.30oei0 6361
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 7058
[TakeutiZaring] p. 88Exercise 1en0 6695
[TakeutiZaring] p. 90Proposition 10.20nneneq 6757
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6758
[TakeutiZaring] p. 91Definition 10.29df-fin 6643  isfi 6661
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6731
[TakeutiZaring] p. 95Definition 10.42df-map 6550
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6748
[Tarski] p. 67Axiom B5ax-4 1488
[Tarski] p. 68Lemma 6equid 1678
[Tarski] p. 69Lemma 7equcomi 1681
[Tarski] p. 70Lemma 14spim 1717  spime 1720  spimeh 1718  spimh 1716
[Tarski] p. 70Lemma 16ax-11 1485  ax-11o 1796  ax11i 1693
[Tarski] p. 70Lemmas 16 and 17sb6 1859
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1507
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1492  ax-14 1493
[WhiteheadRussell] p. 96Axiom *1.3olc 701
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 717
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 746
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 755
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 779
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 606
[WhiteheadRussell] p. 100Theorem *2.02ax-1 6
[WhiteheadRussell] p. 100Theorem *2.03con2 633
[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 823
[WhiteheadRussell] p. 101Theorem *2.06barbara 2098  syl 14
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 727
[WhiteheadRussell] p. 101Theorem *2.08id 19  idALT 20
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 822
[WhiteheadRussell] p. 101Theorem *2.12notnot 619
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 871
[WhiteheadRussell] p. 102Theorem *2.14notnotrdc 829
[WhiteheadRussell] p. 102Theorem *2.15con1dc 842
[WhiteheadRussell] p. 103Theorem *2.16con3 632
[WhiteheadRussell] p. 103Theorem *2.17condc 839
[WhiteheadRussell] p. 103Theorem *2.18pm2.18dc 841
[WhiteheadRussell] p. 104Theorem *2.2orc 702
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 765
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 607
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 611
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 879
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 893
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 40
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 758
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 759
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 794
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 795
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 793
[WhiteheadRussell] p. 105Definition *2.33df-3or 964
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 768
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 766
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 767
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 53
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 728
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 729
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 853  pm2.5gdc 852
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 848
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 730
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 731
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 732
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 645
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 646
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 712
[WhiteheadRussell] p. 107Theorem *2.54pm2.54dc 877
[WhiteheadRussell] p. 107Theorem *2.55orel1 715
[WhiteheadRussell] p. 107Theorem *2.56orel2 716
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 851
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 738
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 790
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 791
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 649
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 703  pm2.67 733
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 855  pm2.521gdc 854
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 737
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 800
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 880
[WhiteheadRussell] p. 108Theorem *2.69looinvdc 901
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 796
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 797
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 799
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 798
[WhiteheadRussell] p. 108Theorem *2.77ax-2 7
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 801
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 802
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 77
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 891
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 100
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 744
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 138
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 942
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 943
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 944
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 743
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 262
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 263
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 683
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 345
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 259
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 260
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 108  simplimdc 846
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 109  simprimdc 845
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 343
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 344
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 679
[WhiteheadRussell] p. 113Fact)pm3.45 587
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 331
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 329
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 330
[WhiteheadRussell] p. 113Theorem *3.44jao 745  pm3.44 705
[WhiteheadRussell] p. 113Theorem *3.47anim12 342
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 592
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 775
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 857
[WhiteheadRussell] p. 117Theorem *4.2biid 170
[WhiteheadRussell] p. 117Theorem *4.13notnotbdc 858
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 876
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 684
[WhiteheadRussell] p. 117Theorem *4.21bicom 139
[WhiteheadRussell] p. 117Theorem *4.22biantr 937  bitr 464
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 393
[WhiteheadRussell] p. 117Theorem *4.25oridm 747  pm4.25 748
[WhiteheadRussell] p. 118Theorem *4.3ancom 264
[WhiteheadRussell] p. 118Theorem *4.4andi 808
[WhiteheadRussell] p. 118Theorem *4.31orcom 718
[WhiteheadRussell] p. 118Theorem *4.32anass 399
[WhiteheadRussell] p. 118Theorem *4.33orass 757
[WhiteheadRussell] p. 118Theorem *4.36anbi1 462
[WhiteheadRussell] p. 118Theorem *4.37orbi1 782
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 595
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 812
[WhiteheadRussell] p. 118Definition *4.34df-3an 965
[WhiteheadRussell] p. 119Theorem *4.41ordi 806
[WhiteheadRussell] p. 119Theorem *4.42pm4.42r 956
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 934
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 769
[WhiteheadRussell] p. 119Theorem *4.45orabs 804  pm4.45 774  pm4.45im 332
[WhiteheadRussell] p. 119Theorem *10.2219.26 1458
[WhiteheadRussell] p. 120Theorem *4.5anordc 941
[WhiteheadRussell] p. 120Theorem *4.6imordc 883  imorr 711
[WhiteheadRussell] p. 120Theorem *4.7anclb 317
[WhiteheadRussell] p. 120Theorem *4.51ianordc 885
[WhiteheadRussell] p. 120Theorem *4.52pm4.52im 740
[WhiteheadRussell] p. 120Theorem *4.53pm4.53r 741
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 888
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 923
[WhiteheadRussell] p. 120Theorem *4.56ioran 742  pm4.56 770
[WhiteheadRussell] p. 120Theorem *4.57orandc 924  oranim 771
[WhiteheadRussell] p. 120Theorem *4.61annimim 676
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 884
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 872
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 886
[WhiteheadRussell] p. 120Theorem *4.65pm4.65r 677
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 887
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 873
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 387  pm4.71d 391  pm4.71i 389  pm4.71r 388  pm4.71rd 392  pm4.71ri 390
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 813
[WhiteheadRussell] p. 121Theorem *4.73iba 298
[WhiteheadRussell] p. 121Theorem *4.74biorf 734
[WhiteheadRussell] p. 121Theorem *4.76jcab 593  pm4.76 594
[WhiteheadRussell] p. 121Theorem *4.77jaob 700  pm4.77 789
[WhiteheadRussell] p. 121Theorem *4.78pm4.78i 772
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 889
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 697
[WhiteheadRussell] p. 122Theorem *4.81pm4.81dc 894
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 935
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 936
[WhiteheadRussell] p. 122Theorem *4.84imbi1 235
[WhiteheadRussell] p. 122Theorem *4.85imbi2 236
[WhiteheadRussell] p. 122Theorem *4.86bibi1 239
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 247  impexp 261  pm4.87 547
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 591
[WhiteheadRussell] p. 123Theorem *5.11pm5.11dc 895
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 896
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 898
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 897
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1368
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 814
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 890
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1373  pm5.18dc 869
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 696
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 685
[WhiteheadRussell] p. 124Theorem *5.22xordc 1371
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1376
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1377
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 881
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 467
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 248
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 241
[WhiteheadRussell] p. 125Theorem *5.6pm5.6dc 912  pm5.6r 913
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 939
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 346
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 449
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 599
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 903
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 600
[WhiteheadRussell] p. 125Theorem *5.41imdi 249  pm5.41 250
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 318
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 911
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 792
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 904
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 899
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 784
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 930
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 931
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 946
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 243
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 178
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 947
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1615
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1462
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1612
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1868
[WhiteheadRussell] p. 175Definition *14.02df-eu 2003
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2390
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2391
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2825
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2968
[WhiteheadRussell] p. 190Theorem *14.22iota4 5112
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5113
[WhiteheadRussell] p. 192Theorem *14.26eupick 2079  eupickbi 2082
[WhiteheadRussell] p. 235Definition *30.01df-fv 5137
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 7061

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