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 6873  fidcenum 6745
[AczelRathjen], p. 72Proposition 8.1.11fidcenum 6745
[AczelRathjen], p. 73Lemma 8.1.14enumct 6873
[AczelRathjen], p. 74Lemma 8.1.16xpfi 6720
[AczelRathjen], p. 74Remark 8.1.17unfiexmid 6708
[AczelRathjen], p. 75Corollary 8.1.23znnen 11638
[AczelRathjen], p. 80Corollary 8.2.4df-ihash 10299
[AczelRathjen], p. 183Chapter 20ax-setind 4381
[Apostol] p. 18Theorem I.1addcan 7759  addcan2d 7764  addcan2i 7762  addcand 7763  addcani 7761
[Apostol] p. 18Theorem I.2negeu 7770
[Apostol] p. 18Theorem I.3negsub 7827  negsubd 7896  negsubi 7857
[Apostol] p. 18Theorem I.4negneg 7829  negnegd 7881  negnegi 7849
[Apostol] p. 18Theorem I.5subdi 7960  subdid 7989  subdii 7982  subdir 7961  subdird 7990  subdiri 7983
[Apostol] p. 18Theorem I.6mul01 7964  mul01d 7968  mul01i 7966  mul02 7962  mul02d 7967  mul02i 7965
[Apostol] p. 18Theorem I.9divrecapd 8357
[Apostol] p. 18Theorem I.10recrecapi 8308
[Apostol] p. 18Theorem I.12mul2neg 7973  mul2negd 7988  mul2negi 7981  mulneg1 7970  mulneg1d 7986  mulneg1i 7979
[Apostol] p. 18Theorem I.15divdivdivap 8277
[Apostol] p. 20Axiom 7rpaddcl 9256  rpaddcld 9288  rpmulcl 9257  rpmulcld 9289
[Apostol] p. 20Axiom 90nrp 9266
[Apostol] p. 20Theorem I.17lttri 7686
[Apostol] p. 20Theorem I.18ltadd1d 8112  ltadd1dd 8130  ltadd1i 8077
[Apostol] p. 20Theorem I.19ltmul1 8166  ltmul1a 8165  ltmul1i 8478  ltmul1ii 8486  ltmul2 8414  ltmul2d 9315  ltmul2dd 9329  ltmul2i 8481
[Apostol] p. 20Theorem I.210lt1 7707
[Apostol] p. 20Theorem I.23lt0neg1 8043  lt0neg1d 8090  ltneg 8037  ltnegd 8097  ltnegi 8068
[Apostol] p. 20Theorem I.25lt2add 8020  lt2addd 8141  lt2addi 8085
[Apostol] p. 20Definition of positive numbersdf-rp 9234
[Apostol] p. 21Exercise 4recgt0 8408  recgt0d 8492  recgt0i 8464  recgt0ii 8465
[Apostol] p. 22Definition of integersdf-z 8849
[Apostol] p. 22Definition of rationalsdf-q 9204
[Apostol] p. 24Theorem I.26supeuti 6769
[Apostol] p. 26Theorem I.29arch 8768
[Apostol] p. 28Exercise 2btwnz 8964
[Apostol] p. 28Exercise 3nnrecl 8769
[Apostol] p. 28Exercise 6qbtwnre 9817
[Apostol] p. 28Exercise 10(a)zeneo 11298  zneo 8946
[Apostol] p. 29Theorem I.35resqrtth 10579  sqrtthi 10667
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 8523
[Apostol] p. 363Remarkabsgt0api 10694
[Apostol] p. 363Exampleabssubd 10741  abssubi 10698
[ApostolNT] p. 14Definitiondf-dvds 11224
[ApostolNT] p. 14Theorem 1.1(a)iddvds 11236
[ApostolNT] p. 14Theorem 1.1(b)dvdstr 11260
[ApostolNT] p. 14Theorem 1.1(c)dvds2ln 11256
[ApostolNT] p. 14Theorem 1.1(d)dvdscmul 11250
[ApostolNT] p. 14Theorem 1.1(e)dvdscmulr 11252
[ApostolNT] p. 14Theorem 1.1(f)1dvds 11237
[ApostolNT] p. 14Theorem 1.1(g)dvds0 11238
[ApostolNT] p. 14Theorem 1.1(h)0dvds 11243
[ApostolNT] p. 14Theorem 1.1(i)dvdsleabs 11273
[ApostolNT] p. 14Theorem 1.1(j)dvdsabseq 11275
[ApostolNT] p. 14Theorem 1.1(k)divconjdvds 11277
[ApostolNT] p. 15Definitiondfgcd2 11430
[ApostolNT] p. 16Definitionisprm2 11526
[ApostolNT] p. 16Theorem 1.5coprmdvds 11501
[ApostolNT] p. 16Theorem 1.4(a)gcdcom 11392
[ApostolNT] p. 16Theorem 1.4(b)gcdass 11431
[ApostolNT] p. 16Theorem 1.4(c)absmulgcd 11433
[ApostolNT] p. 16Theorem 1.4(d)1gcd1 11405
[ApostolNT] p. 16Theorem 1.4(d)2gcdid0 11398
[ApostolNT] p. 17Theorem 1.8coprm 11550
[ApostolNT] p. 17Theorem 1.9euclemma 11552
[ApostolNT] p. 19Theorem 1.14divalg 11351
[ApostolNT] p. 20Theorem 1.15eucalg 11468
[ApostolNT] p. 25Definitiondf-phi 11614
[ApostolNT] p. 28Theorem 2.5(a)phiprmpw 11625
[ApostolNT] p. 28Theorem 2.5(c)phimul 11629
[ApostolNT] p. 104Definitioncongr 11509
[ApostolNT] p. 106Remarkdvdsval3 11227
[ApostolNT] p. 106Definitionmoddvds 11232
[ApostolNT] p. 107Example 2mod2eq0even 11305
[ApostolNT] p. 107Example 3mod2eq1n2dvds 11306
[ApostolNT] p. 107Example 4zmod1congr 9897
[ApostolNT] p. 107Theorem 5.2(b)modqmul12d 9934
[ApostolNT] p. 108Theorem 5.3modmulconst 11255
[ApostolNT] p. 109Theorem 5.4cncongr1 11512
[ApostolNT] p. 109Theorem 5.4 "Cancellation law"cncongr 11514
[Bauer] p. 482Section 1.2pm2.01 584  pm2.65 623
[Bauer] p. 483Theorem 1.3acexmid 5689  onsucelsucexmidlem 4373
[Bauer], p. 483Definitionn0rf 3314
[Bauer], p. 485Theorem 2.1ssfiexmid 6672
[BauerSwan], p. 14Remark0ct 6869  ctm 6871
[BauerSwan], p. 14Table" is defined as ` ` per enumct 6873
[BauerTaylor], p. 32Lemma 6.16prarloclem 7157
[BauerTaylor], p. 50Lemma 11.4subhalfnqq 7070
[BauerTaylor], p. 52Proposition 11.15prarloc 7159
[BauerTaylor], p. 53Lemma 11.16addclpr 7193  addlocpr 7192
[BauerTaylor], p. 55Proposition 12.7appdivnq 7219
[BauerTaylor], p. 56Lemma 12.8prmuloc 7222
[BauerTaylor], p. 56Lemma 12.9mullocpr 7227
[BellMachover] p. 36Lemma 10.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 1958
[BellMachover] p. 460Notationdf-mo 1959
[BellMachover] p. 460Definitionmo3 2009  mo3h 2008
[BellMachover] p. 462Theorem 1.1bm1.1 2080
[BellMachover] p. 463Theorem 1.3iibm1.3ii 3981
[BellMachover] p. 466Axiom Powaxpow3 4033
[BellMachover] p. 466Axiom Unionaxun2 4286
[BellMachover] p. 469Theorem 2.2(i)ordirr 4386
[BellMachover] p. 469Theorem 2.2(iii)onelon 4235
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4389
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4341
[BellMachover] p. 471Definition of Limdf-ilim 4220
[BellMachover] p. 472Axiom Infzfinf2 4432
[BellMachover] p. 473Theorem 2.8limom 4456
[Bobzien] p. 116Statement T3stoic3 1372
[Bobzien] p. 117Statement T2stoic2a 1370
[Bobzien] p. 117Statement T4stoic4a 1373
[BourbakiEns] p. Proposition 8fcof1 5600  fcofo 5601
[BourbakiTop1] p. Remarkxnegmnf 9395  xnegpnf 9394
[BourbakiTop1] p. Remark rexneg 9396
[BourbakiTop1] p. Property V_issnei2 12009
[BourbakiTop1] p. Property V_iiinnei 12015
[BourbakiTop1] p. Property V_ivneissex 12017
[BourbakiTop1] p. Proposition 1neipsm 12006  neiss 12002
[BourbakiTop1] p. Proposition 2cnptopco 12073
[BourbakiTop1] p. Property V_iiielnei 12004
[BourbakiTop1] p. Definition is due to Bourbaki (Def. 1df-top 11849
[ChoquetDD] p. 2Definition of mappingdf-mpt 3923
[Crosilla] p. Axiom 1ax-ext 2077
[Crosilla] p. Axiom 2ax-pr 4060
[Crosilla] p. Axiom 3ax-un 4284
[Crosilla] p. Axiom 4ax-nul 3986
[Crosilla] p. Axiom 5ax-iinf 4431
[Crosilla] p. Axiom 6ru 2853
[Crosilla] p. Axiom 8ax-pow 4030
[Crosilla] p. Axiom 9ax-setind 4381
[Crosilla], p. Axiom 6ax-sep 3978
[Crosilla], p. Axiom 7ax-coll 3975
[Crosilla], p. Axiom 7'repizf 3976
[Crosilla], p. Theorem is statedordtriexmid 4366
[Crosilla], p. Axiom of choice implies instancesacexmid 5689
[Crosilla], p. Definition of ordinaldf-iord 4217
[Crosilla], p. Theorem "Foundation implies instances of EM"regexmid 4379
[Eisenberg] p. 67Definition 5.3df-dif 3015
[Eisenberg] p. 82Definition 6.3df-iom 4434
[Eisenberg] p. 125Definition 8.21df-map 6447
[Enderton] p. 18Axiom of Empty Setaxnul 3985
[Enderton] p. 19Definitiondf-tp 3474
[Enderton] p. 26Exercise 5unissb 3705
[Enderton] p. 26Exercise 10pwel 4069
[Enderton] p. 28Exercise 7(b)pwunim 4137
[Enderton] p. 30Theorem "Distributive laws"iinin1m 3821  iinin2m 3820  iunin1 3816  iunin2 3815
[Enderton] p. 31Theorem "De Morgan's laws"iindif2m 3819  iundif2ss 3817
[Enderton] p. 33Exercise 23iinuniss 3833
[Enderton] p. 33Exercise 25iununir 3834
[Enderton] p. 33Exercise 24(a)iinpw 3841
[Enderton] p. 33Exercise 24(b)iunpw 4330  iunpwss 3842
[Enderton] p. 38Exercise 6(a)unipw 4068
[Enderton] p. 38Exercise 6(b)pwuni 4048
[Enderton] p. 41Lemma 3Dopeluu 4300  rnex 4732  rnexg 4730
[Enderton] p. 41Exercise 8dmuni 4677  rnuni 4876
[Enderton] p. 42Definition of a functiondffun7 5076  dffun8 5077
[Enderton] p. 43Definition of function valuefunfvdm2 5403
[Enderton] p. 43Definition of single-rootedfuncnv 5109
[Enderton] p. 44Definition (d)dfima2 4809  dfima3 4810
[Enderton] p. 47Theorem 3Hfvco2 5408
[Enderton] p. 50Theorem 3K(a)imauni 5578
[Enderton] p. 52Definitiondf-map 6447
[Enderton] p. 53Exercise 21coass 4983
[Enderton] p. 53Exercise 27dmco 4973
[Enderton] p. 53Exercise 14(a)funin 5119
[Enderton] p. 53Exercise 22(a)imass2 4841
[Enderton] p. 54Remarkixpf 6517  ixpssmap 6529
[Enderton] p. 54Definition of infinite Cartesian productdf-ixp 6496
[Enderton] p. 56Theorem 3Merref 6352
[Enderton] p. 57Lemma 3Nerthi 6378
[Enderton] p. 57Definitiondf-ec 6334
[Enderton] p. 58Definitiondf-qs 6338
[Enderton] p. 60Theorem 3Qth3q 6437  th3qcor 6436  th3qlem1 6434  th3qlem2 6435
[Enderton] p. 61Exercise 35df-ec 6334
[Enderton] p. 65Exercise 56(a)dmun 4674
[Enderton] p. 68Definition of successordf-suc 4222
[Enderton] p. 71Definitiondf-tr 3959  dftr4 3963
[Enderton] p. 72Theorem 4Eunisuc 4264  unisucg 4265
[Enderton] p. 73Exercise 6unisuc 4264  unisucg 4265
[Enderton] p. 73Exercise 5(a)truni 3972
[Enderton] p. 73Exercise 5(b)trint 3973
[Enderton] p. 79Theorem 4I(A1)nna0 6275
[Enderton] p. 79Theorem 4I(A2)nnasuc 6277  onasuc 6267
[Enderton] p. 79Definition of operation valuedf-ov 5693
[Enderton] p. 80Theorem 4J(A1)nnm0 6276
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6278  onmsuc 6274
[Enderton] p. 81Theorem 4K(1)nnaass 6286
[Enderton] p. 81Theorem 4K(2)nna0r 6279  nnacom 6285
[Enderton] p. 81Theorem 4K(3)nndi 6287
[Enderton] p. 81Theorem 4K(4)nnmass 6288
[Enderton] p. 81Theorem 4K(5)nnmcom 6290
[Enderton] p. 82Exercise 16nnm0r 6280  nnmsucr 6289
[Enderton] p. 88Exercise 23nnaordex 6326
[Enderton] p. 129Definitiondf-en 6538
[Enderton] p. 133Exercise 1xpomen 11635
[Enderton] p. 134Theorem (Pigeonhole Principle)phpm 6661
[Enderton] p. 136Corollary 6Enneneq 6653
[Enderton] p. 139Theorem 6H(c)mapen 6642
[Enderton] p. 144Corollary 6Kundif2ss 3377
[Enderton] p. 145Figure 38ffoss 5320
[Enderton] p. 145Definitiondf-dom 6539
[Enderton] p. 146Example 1domen 6548  domeng 6549
[Enderton] p. 146Example 3nndomo 6660
[Enderton] p. 149Theorem 6L(c)xpdom1 6631  xpdom1g 6629  xpdom2g 6628
[Enderton] p. 168Definitiondf-po 4147
[Enderton] p. 192Theorem 7M(a)oneli 4279
[Enderton] p. 192Theorem 7M(b)ontr1 4240
[Enderton] p. 192Theorem 7M(c)onirri 4387
[Enderton] p. 193Corollary 7N(b)0elon 4243
[Enderton] p. 193Corollary 7N(c)onsuci 4361
[Enderton] p. 193Corollary 7N(d)ssonunii 4334
[Enderton] p. 194Remarkonprc 4396
[Enderton] p. 194Exercise 16suc11 4402
[Enderton] p. 197Definitiondf-card 6905
[Enderton] p. 200Exercise 25tfis 4426
[Enderton] p. 206Theorem 7X(b)en2lp 4398
[Enderton] p. 207Exercise 34opthreg 4400
[Enderton] p. 208Exercise 35suc11g 4401
[Geuvers], p. 1Remarkexpap0 10100
[Geuvers], p. 6Lemma 2.13mulap0r 8189
[Geuvers], p. 6Lemma 2.15mulap0 8220
[Geuvers], p. 9Lemma 2.35msqge0 8190
[Geuvers], p. 9Definition 3.1(2)ax-arch 7561
[Geuvers], p. 10Lemma 3.9maxcom 10751
[Geuvers], p. 10Lemma 3.10maxle1 10759  maxle2 10760
[Geuvers], p. 10Lemma 3.11maxleast 10761
[Geuvers], p. 10Lemma 3.12maxleb 10764
[Geuvers], p. 11Definition 3.13dfabsmax 10765
[Geuvers], p. 17Definition 6.1df-ap 8156
[Gleason] p. 117Proposition 9-2.1df-enq 7003  enqer 7014
[Gleason] p. 117Proposition 9-2.2df-1nqqs 7007  df-nqqs 7004
[Gleason] p. 117Proposition 9-2.3df-plpq 7000  df-plqqs 7005
[Gleason] p. 119Proposition 9-2.4df-mpq 7001  df-mqqs 7006
[Gleason] p. 119Proposition 9-2.5df-rq 7008
[Gleason] p. 119Proposition 9-2.6ltexnqq 7064
[Gleason] p. 120Proposition 9-2.6(i)halfnq 7067  ltbtwnnq 7072  ltbtwnnqq 7071
[Gleason] p. 120Proposition 9-2.6(ii)ltanqg 7056
[Gleason] p. 120Proposition 9-2.6(iii)ltmnqg 7057
[Gleason] p. 123Proposition 9-3.5addclpr 7193
[Gleason] p. 123Proposition 9-3.5(i)addassprg 7235
[Gleason] p. 123Proposition 9-3.5(ii)addcomprg 7234
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 7253
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 7269
[Gleason] p. 123Proposition 9-3.5(v)ltaprg 7275  ltaprlem 7274
[Gleason] p. 123Proposition 9-3.5(vi)addcanprg 7272
[Gleason] p. 124Proposition 9-3.7mulclpr 7228
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 7248
[Gleason] p. 124Proposition 9-3.7(i)mulassprg 7237
[Gleason] p. 124Proposition 9-3.7(ii)mulcomprg 7236
[Gleason] p. 124Proposition 9-3.7(iii)distrprg 7244
[Gleason] p. 124Proposition 9-3.7(v)recexpr 7294
[Gleason] p. 126Proposition 9-4.1df-enr 7369  enrer 7378
[Gleason] p. 126Proposition 9-4.2df-0r 7374  df-1r 7375  df-nr 7370
[Gleason] p. 126Proposition 9-4.3df-mr 7372  df-plr 7371  negexsr 7415  recexsrlem 7417
[Gleason] p. 127Proposition 9-4.4df-ltr 7373
[Gleason] p. 130Proposition 10-1.3creui 8518  creur 8517  cru 8176
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 7553  axcnre 7513
[Gleason] p. 132Definition 10-3.1crim 10407  crimd 10526  crimi 10486  crre 10406  crred 10525  crrei 10485
[Gleason] p. 132Definition 10-3.2remim 10409  remimd 10491
[Gleason] p. 133Definition 10.36absval2 10605  absval2d 10733  absval2i 10692
[Gleason] p. 133Proposition 10-3.4(a)cjadd 10433  cjaddd 10514  cjaddi 10481
[Gleason] p. 133Proposition 10-3.4(c)cjmul 10434  cjmuld 10515  cjmuli 10482
[Gleason] p. 133Proposition 10-3.4(e)cjcj 10432  cjcjd 10492  cjcji 10464
[Gleason] p. 133Proposition 10-3.4(f)cjre 10431  cjreb 10415  cjrebd 10495  cjrebi 10467  cjred 10520  rere 10414  rereb 10412  rerebd 10494  rerebi 10466  rered 10518
[Gleason] p. 133Proposition 10-3.4(h)addcj 10440  addcjd 10506  addcji 10476
[Gleason] p. 133Proposition 10-3.7(a)absval 10549
[Gleason] p. 133Proposition 10-3.7(b)abscj 10600  abscjd 10738  abscji 10696
[Gleason] p. 133Proposition 10-3.7(c)abs00 10612  abs00d 10734  abs00i 10693  absne0d 10735
[Gleason] p. 133Proposition 10-3.7(d)releabs 10644  releabsd 10739  releabsi 10697
[Gleason] p. 133Proposition 10-3.7(f)absmul 10617  absmuld 10742  absmuli 10699
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 10603  sqabsaddi 10700
[Gleason] p. 133Proposition 10-3.7(h)abstri 10652  abstrid 10744  abstrii 10703
[Gleason] p. 134Definition 10-4.10exp0e1 10075  df-exp 10070  exp0 10074  expp1 10077  expp1d 10202
[Gleason] p. 135Proposition 10-4.2(a)expadd 10112  expaddd 10203
[Gleason] p. 135Proposition 10-4.2(b)expmul 10115  expmuld 10204
[Gleason] p. 135Proposition 10-4.2(c)mulexp 10109  mulexpd 10216
[Gleason] p. 141Definition 11-2.1fzval 9575
[Gleason] p. 168Proposition 12-2.1(a)climadd 10869
[Gleason] p. 168Proposition 12-2.1(b)climsub 10871
[Gleason] p. 168Proposition 12-2.1(c)climmul 10870
[Gleason] p. 171Corollary 12-2.2climmulc2 10874
[Gleason] p. 172Corollary 12-2.5climrecl 10867
[Gleason] p. 172Proposition 12-2.4(c)climabs 10863  climcj 10864  climim 10866  climre 10865
[Gleason] p. 173Definition 12-3.1df-ltxr 7624  df-xr 7623  ltxr 9345
[Gleason] p. 180Theorem 12-5.3climcau 10890
[Gleason] p. 217Lemma 13-4.1btwnzge0 9856
[Gleason] p. 223Definition 14-1.1df-met 11842
[Gleason] p. 223Definition 14-1.1(a)met0 12150  xmet0 12149
[Gleason] p. 223Definition 14-1.1(c)metsym 12157
[Gleason] p. 223Definition 14-1.1(d)mettri 12159  mstri 12259  xmettri 12158  xmstri 12258
[Gleason] p. 240Proposition 14-4.2metcnp3 12293
[Gleason] p. 243Proposition 14-4.16addcn2 10853  mulcn2 10855  subcn2 10854
[Gleason] p. 295Remarkbcval3 10274  bcval4 10275
[Gleason] p. 295Equation 2bcpasc 10289
[Gleason] p. 295Definition of binomial coefficientbcval 10272  df-bc 10271
[Gleason] p. 296Remarkbcn0 10278  bcnn 10280
[Gleason] p. 296Theorem 15-2.8binom 11027
[Gleason] p. 308Equation 2ef0 11111
[Gleason] p. 308Equation 3efcj 11112
[Gleason] p. 309Corollary 15-4.3efne0 11117
[Gleason] p. 309Corollary 15-4.4efexp 11121
[Gleason] p. 310Equation 14sinadd 11176
[Gleason] p. 310Equation 15cosadd 11177
[Gleason] p. 311Equation 17sincossq 11188
[Gleason] p. 311Equation 18cosbnd 11193  sinbnd 11192
[Gleason] p. 311Definition of ` `df-pi 11092
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 7
[Hamilton] p. 74Rule 2ax-gen 1390
[Heyting] p. 127Axiom #1ax1hfs 12623
[Hitchcock] p. 5Rule A3mptnan 1366
[Hitchcock] p. 5Rule A4mptxor 1367
[Hitchcock] p. 5Rule A5mtpxor 1369
[HoTT], p. Theorem 7.2.6nndceq 6300
[HoTT], p. Exercise 11.11mulap0bd 8223
[HoTT], p. Section 11.2.1df-iltp 7126  df-imp 7125  df-iplp 7124  df-reap 8149
[HoTT], p. Theorem 11.2.12cauappcvgpr 7318
[HoTT], p. Corollary 11.4.3conventions 12356
[HoTT], p. Corollary 11.2.13axcaucvg 7532  caucvgpr 7338  caucvgprpr 7368  caucvgsr 7444
[HoTT], p. Definition 11.2.1df-inp 7122
[HoTT], p. Proposition 11.2.3df-iso 4148  ltpopr 7251  ltsopr 7252
[HoTT], p. Definition 11.2.7(v)apsym 8180  reapcotr 8172  reapirr 8151
[HoTT], p. Definition 11.2.7(vi)0lt1 7707  gt0add 8147  leadd1 8005  lelttr 7670  lemul1a 8416  lenlt 7658  ltadd1 8004  ltletr 7671  ltmul1 8166  reaplt 8162
[Jech] p. 4Definition of classcv 1295  cvjust 2090
[Jech] p. 78Noteopthprc 4518
[KalishMontague] p. 81Note 1ax-i9 1475
[Kreyszig] p. 3Property M1metcl 12139  xmetcl 12138
[Kreyszig] p. 4Property M2meteq0 12146
[Kreyszig] p. 12Equation 5muleqadd 8234
[Kreyszig] p. 18Definition 1.3-2mopnval 12228
[Kreyszig] p. 19Remarkmopntopon 12229
[Kreyszig] p. 19Theorem T1mopn0 12274  mopnm 12234
[Kreyszig] p. 19Theorem T2unimopn 12272
[Kreyszig] p. 19Definition of neighborhoodneibl 12277
[Kreyszig] p. 20Definition 1.3-3metcnp2 12295
[Kreyszig] p. 25Definition 1.4-1lmbr 12064
[Kunen] p. 10Axiom 0a9e 1638
[Kunen] p. 12Axiom 6zfrep6 3977
[Kunen] p. 24Definition 10.24mapval 6457  mapvalg 6455
[Kunen] p. 31Definition 10.24mapex 6451
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3762
[Levy] p. 338Axiomdf-clab 2082  df-clel 2091  df-cleq 2088
[Lopez-Astorga] p. 12Rule 1mptnan 1366
[Lopez-Astorga] p. 12Rule 2mptxor 1367
[Lopez-Astorga] p. 12Rule 3mtpxor 1369
[Margaris] p. 40Rule Cexlimiv 1541
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3condc 790
[Margaris] p. 49Definitiondfbi2 381  dfordc 832  exalim 1443
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 45
[Margaris] p. 60Theorem 8mth8 617
[Margaris] p. 89Theorem 19.219.2 1581  r19.2m 3388
[Margaris] p. 89Theorem 19.319.3 1498  19.3h 1497  rr19.3v 2769
[Margaris] p. 89Theorem 19.5alcom 1419
[Margaris] p. 89Theorem 19.6alexdc 1562  alexim 1588
[Margaris] p. 89Theorem 19.7alnex 1440
[Margaris] p. 89Theorem 19.819.8a 1534  spsbe 1777
[Margaris] p. 89Theorem 19.919.9 1587  19.9h 1586  19.9v 1806  exlimd 1540
[Margaris] p. 89Theorem 19.11excom 1606  excomim 1605
[Margaris] p. 89Theorem 19.1219.12 1607  r19.12 2491
[Margaris] p. 90Theorem 19.14exnalim 1589
[Margaris] p. 90Theorem 19.15albi 1409  ralbi 2515
[Margaris] p. 90Theorem 19.1619.16 1499
[Margaris] p. 90Theorem 19.1719.17 1500
[Margaris] p. 90Theorem 19.18exbi 1547  rexbi 2516
[Margaris] p. 90Theorem 19.1919.19 1608
[Margaris] p. 90Theorem 19.20alim 1398  alimd 1466  alimdh 1408  alimdv 1814  ralimdaa 2452  ralimdv 2454  ralimdva 2453  sbcimdv 2918
[Margaris] p. 90Theorem 19.2119.21-2 1609  19.21 1527  19.21bi 1502  19.21h 1501  19.21ht 1525  19.21t 1526  19.21v 1808  alrimd 1553  alrimdd 1552  alrimdh 1420  alrimdv 1811  alrimi 1467  alrimih 1410  alrimiv 1809  alrimivv 1810  r19.21 2461  r19.21be 2476  r19.21bi 2473  r19.21t 2460  r19.21v 2462  ralrimd 2463  ralrimdv 2464  ralrimdva 2465  ralrimdvv 2469  ralrimdvva 2470  ralrimi 2456  ralrimiv 2457  ralrimiva 2458  ralrimivv 2466  ralrimivva 2467  ralrimivvva 2468  ralrimivw 2459  rexlimi 2495
[Margaris] p. 90Theorem 19.222alimdv 1816  2eximdv 1817  exim 1542  eximd 1555  eximdh 1554  eximdv 1815  rexim 2479  reximdai 2483  reximddv 2488  reximddv2 2490  reximdv 2486  reximdv2 2484  reximdva 2487  reximdvai 2485  reximi2 2481
[Margaris] p. 90Theorem 19.2319.23 1620  19.23bi 1535  19.23h 1439  19.23ht 1438  19.23t 1619  19.23v 1818  19.23vv 1819  exlimd2 1538  exlimdh 1539  exlimdv 1754  exlimdvv 1832  exlimi 1537  exlimih 1536  exlimiv 1541  exlimivv 1831  r19.23 2493  r19.23v 2494  rexlimd 2499  rexlimdv 2501  rexlimdv3a 2504  rexlimdva 2502  rexlimdva2 2505  rexlimdvaa 2503  rexlimdvv 2509  rexlimdvva 2510  rexlimdvw 2506  rexlimiv 2496  rexlimiva 2497  rexlimivv 2508
[Margaris] p. 90Theorem 19.24i19.24 1582
[Margaris] p. 90Theorem 19.2519.25 1569
[Margaris] p. 90Theorem 19.2619.26-2 1423  19.26-3an 1424  19.26 1422  r19.26-2 2512  r19.26-3 2513  r19.26 2511  r19.26m 2514
[Margaris] p. 90Theorem 19.2719.27 1505  19.27h 1504  19.27v 1834  r19.27av 2518  r19.27m 3397  r19.27mv 3398
[Margaris] p. 90Theorem 19.2819.28 1507  19.28h 1506  19.28v 1835  r19.28av 2519  r19.28m 3391  r19.28mv 3394  rr19.28v 2770
[Margaris] p. 90Theorem 19.2919.29 1563  19.29r 1564  19.29r2 1565  19.29x 1566  r19.29 2520  r19.29d2r 2526  r19.29r 2521
[Margaris] p. 90Theorem 19.3019.30dc 1570
[Margaris] p. 90Theorem 19.3119.31r 1623
[Margaris] p. 90Theorem 19.3219.32dc 1621  19.32r 1622  r19.32r 2528  r19.32vdc 2530  r19.32vr 2529
[Margaris] p. 90Theorem 19.3319.33 1425  19.33b2 1572  19.33bdc 1573
[Margaris] p. 90Theorem 19.3419.34 1626
[Margaris] p. 90Theorem 19.3519.35-1 1567  19.35i 1568
[Margaris] p. 90Theorem 19.3619.36-1 1615  19.36aiv 1836  19.36i 1614  r19.36av 2532
[Margaris] p. 90Theorem 19.3719.37-1 1616  19.37aiv 1617  r19.37 2533  r19.37av 2534
[Margaris] p. 90Theorem 19.3819.38 1618
[Margaris] p. 90Theorem 19.39i19.39 1583
[Margaris] p. 90Theorem 19.4019.40-2 1575  19.40 1574  r19.40 2535
[Margaris] p. 90Theorem 19.4119.41 1628  19.41h 1627  19.41v 1837  19.41vv 1838  19.41vvv 1839  19.41vvvv 1840  r19.41 2536  r19.41v 2537
[Margaris] p. 90Theorem 19.4219.42 1630  19.42h 1629  19.42v 1841  19.42vv 1843  19.42vvv 1844  19.42vvvv 1845  r19.42v 2538
[Margaris] p. 90Theorem 19.4319.43 1571  r19.43 2539
[Margaris] p. 90Theorem 19.4419.44 1624  r19.44av 2540  r19.44mv 3396
[Margaris] p. 90Theorem 19.4519.45 1625  r19.45av 2541  r19.45mv 3395
[Margaris] p. 110Exercise 2(b)eu1 1980
[Megill] p. 444Axiom C5ax-17 1471
[Megill] p. 445Lemma L12alequcom 1460  ax-10 1448
[Megill] p. 446Lemma L17equtrr 1650
[Megill] p. 446Lemma L19hbnae 1663
[Megill] p. 447Remark 9.1df-sb 1700  sbid 1711
[Megill] p. 448Scheme C5'ax-4 1452
[Megill] p. 448Scheme C6'ax-7 1389
[Megill] p. 448Scheme C8'ax-8 1447
[Megill] p. 448Scheme C9'ax-i12 1450
[Megill] p. 448Scheme C11'ax-10o 1658
[Megill] p. 448Scheme C12'ax-13 1456
[Megill] p. 448Scheme C13'ax-14 1457
[Megill] p. 448Scheme C15'ax-11o 1758
[Megill] p. 448Scheme C16'ax-16 1749
[Megill] p. 448Theorem 9.4dral1 1672  dral2 1673  drex1 1733  drex2 1674  drsb1 1734  drsb2 1776
[Megill] p. 449Theorem 9.7sbcom2 1918  sbequ 1775  sbid2v 1927
[Megill] p. 450Example in Appendixhba1 1485
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 2935  rspsbca 2936  stdpc4 1712
[Mendelson] p. 69Axiom 5ra5 2941  stdpc5 1528
[Mendelson] p. 81Rule Cexlimiv 1541
[Mendelson] p. 95Axiom 6stdpc6 1643
[Mendelson] p. 95Axiom 7stdpc7 1707
[Mendelson] p. 231Exercise 4.10(k)inv1 3338
[Mendelson] p. 231Exercise 4.10(l)unv 3339
[Mendelson] p. 231Exercise 4.10(n)inssun 3255
[Mendelson] p. 231Exercise 4.10(o)df-nul 3303
[Mendelson] p. 231Exercise 4.10(q)inssddif 3256
[Mendelson] p. 231Exercise 4.10(s)ddifnel 3146
[Mendelson] p. 231Definition of unionunssin 3254
[Mendelson] p. 235Exercise 4.12(c)univ 4326
[Mendelson] p. 235Exercise 4.12(d)pwv 3674
[Mendelson] p. 235Exercise 4.12(j)pwin 4133
[Mendelson] p. 235Exercise 4.12(k)pwunss 4134
[Mendelson] p. 235Exercise 4.12(l)pwssunim 4135
[Mendelson] p. 235Exercise 4.12(n)uniin 3695
[Mendelson] p. 235Exercise 4.12(p)reli 4596
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 4985
[Mendelson] p. 246Definition of successordf-suc 4222
[Mendelson] p. 254Proposition 4.22(b)xpen 6641
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6617  xpsneng 6618
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6623  xpcomeng 6624
[Mendelson] p. 254Proposition 4.22(e)xpassen 6626
[Mendelson] p. 255Exercise 4.39endisj 6620
[Mendelson] p. 255Exercise 4.41mapprc 6449
[Mendelson] p. 255Exercise 4.43mapsnen 6608
[Mendelson] p. 255Exercise 4.47xpmapen 6646
[Mendelson] p. 255Exercise 4.42(a)map0e 6483
[Mendelson] p. 255Exercise 4.42(b)map1 6609
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6268
[Monk1] p. 26Theorem 2.8(vii)ssin 3237
[Monk1] p. 33Theorem 3.2(i)ssrel 4555
[Monk1] p. 33Theorem 3.2(ii)eqrel 4556
[Monk1] p. 34Definition 3.3df-opab 3922
[Monk1] p. 36Theorem 3.7(i)coi1 4980  coi2 4981
[Monk1] p. 36Theorem 3.8(v)dm0 4681  rn0 4721
[Monk1] p. 36Theorem 3.7(ii)cnvi 4869
[Monk1] p. 37Theorem 3.13(i)relxp 4576
[Monk1] p. 37Theorem 3.13(x)dmxpm 4687  rnxpm 4894
[Monk1] p. 37Theorem 3.13(ii)0xp 4547  xp0 4884
[Monk1] p. 38Theorem 3.16(ii)ima0 4824
[Monk1] p. 38Theorem 3.16(viii)imai 4821
[Monk1] p. 39Theorem 3.17imaex 4820  imaexg 4819
[Monk1] p. 39Theorem 3.16(xi)imassrn 4818
[Monk1] p. 41Theorem 4.3(i)fnopfv 5468  funfvop 5450
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5383
[Monk1] p. 42Theorem 4.4(iii)fvelima 5391
[Monk1] p. 43Theorem 4.6funun 5092
[Monk1] p. 43Theorem 4.8(iv)dff13 5585  dff13f 5587
[Monk1] p. 46Theorem 4.15(v)funex 5559  funrnex 5923
[Monk1] p. 50Definition 5.4fniunfv 5579
[Monk1] p. 52Theorem 5.12(ii)op2ndb 4948
[Monk1] p. 52Theorem 5.11(viii)ssint 3726
[Monk1] p. 52Definition 5.13 (i)1stval2 5964  df-1st 5949
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5965  df-2nd 5950
[Monk2] p. 105Axiom C4ax-5 1388
[Monk2] p. 105Axiom C7ax-8 1447
[Monk2] p. 105Axiom C8ax-11 1449  ax-11o 1758
[Monk2] p. 105Axiom (C8)ax11v 1762
[Monk2] p. 109Lemma 12ax-7 1389
[Monk2] p. 109Lemma 15equvin 1798  equvini 1695  eqvinop 4094
[Monk2] p. 113Axiom C5-1ax-17 1471
[Monk2] p. 113Axiom C5-2ax6b 1593
[Monk2] p. 113Axiom C5-3ax-7 1389
[Monk2] p. 114Lemma 22hba1 1485
[Monk2] p. 114Lemma 23hbia1 1496  nfia1 1524
[Monk2] p. 114Lemma 24hba2 1495  nfa2 1523
[Moschovakis] p. 2Chapter 2 df-stab 779  dftest 863
[Munkres] p. 77Example 2distop 11937
[Munkres] p. 78Definition of basisdf-bases 11893  isbasis3g 11896
[Munkres] p. 78Definition of a topology generated by a basisdf-topgen 11825  tgval2 11903
[Munkres] p. 79Remarktgcl 11916
[Munkres] p. 80Lemma 2.1tgval3 11910
[Munkres] p. 80Lemma 2.2tgss2 11931  tgss3 11930
[Munkres] p. 81Lemma 2.3basgen 11932  basgen2 11933
[Munkres] p. 89Definition of subspace topologyresttop 12022
[Munkres] p. 93Theorem 6.1(1)0cld 11964  topcld 11961
[Munkres] p. 93Theorem 6.1(3)uncld 11965
[Munkres] p. 94Definition of closureclsval 11963
[Munkres] p. 94Definition of interiorntrval 11962
[Munkres] p. 102Definition of continuous functiondf-cn 12040  iscn 12048  iscn2 12051
[Munkres] p. 107Theorem 7.2(g)cncnp 12081  cncnp2m 12082  cncnpi 12079  df-cnp 12041  iscnp 12050
[Munkres] p. 127Theorem 10.1metcn 12296
[Pierik], p. 8Section 2.2.1dfrex2fin 6699
[Pierik], p. 9Definition 2.5df-markov 6896
[Pierik], p. 10Section 2.3dfdif3 3125
[Pierik], p. 14Definition 3.1df-omni 6877  exmidomniim 6884  finomni 6883
[Pierik], p. 15Section 3.1df-nninf 6878
[PradicBrown2022], p. 1Theorem 1exmidsbthr 12618
[PradicBrown2022], p. 2Remarkexmidpw 6704
[PradicBrown2022], p. 2Proposition 1.1exmidfodomrlemim 6924
[PradicBrown2022], p. 2Proposition 1.2exmidfodomrlemr 6925  exmidfodomrlemrALT 6926
[PradicBrown2022], p. 4Lemma 3.2fodjuomni 6892
[PradicBrown2022], p. 5Lemma 3.4peano3nninf 12602  peano4nninf 12601
[PradicBrown2022], p. 5Lemma 3.5nninfall 12605
[PradicBrown2022], p. 5Theorem 3.6nninfsel 12614
[PradicBrown2022], p. 5Corollary 3.7nninfomni 12616
[PradicBrown2022], p. 5Definition 3.3nnsf 12600
[Quine] p. 16Definition 2.1df-clab 2082  rabid 2556
[Quine] p. 17Definition 2.1''dfsb7 1922
[Quine] p. 18Definition 2.7df-cleq 2088
[Quine] p. 19Definition 2.9df-v 2635
[Quine] p. 34Theorem 5.1abeq2 2203
[Quine] p. 35Theorem 5.2abid2 2215  abid2f 2260
[Quine] p. 40Theorem 6.1sb5 1822
[Quine] p. 40Theorem 6.2sb56 1820  sb6 1821
[Quine] p. 41Theorem 6.3df-clel 2091
[Quine] p. 41Theorem 6.4eqid 2095
[Quine] p. 41Theorem 6.5eqcom 2097
[Quine] p. 42Theorem 6.6df-sbc 2855
[Quine] p. 42Theorem 6.7dfsbcq 2856  dfsbcq2 2857
[Quine] p. 43Theorem 6.8vex 2636
[Quine] p. 43Theorem 6.9isset 2639
[Quine] p. 44Theorem 7.3spcgf 2715  spcgv 2720  spcimgf 2713
[Quine] p. 44Theorem 6.11spsbc 2865  spsbcd 2866
[Quine] p. 44Theorem 6.12elex 2644
[Quine] p. 44Theorem 6.13elab 2774  elabg 2775  elabgf 2772
[Quine] p. 44Theorem 6.14noel 3306
[Quine] p. 48Theorem 7.2snprc 3527
[Quine] p. 48Definition 7.1df-pr 3473  df-sn 3472
[Quine] p. 49Theorem 7.4snss 3588  snssg 3595
[Quine] p. 49Theorem 7.5prss 3615  prssg 3616
[Quine] p. 49Theorem 7.6prid1 3568  prid1g 3566  prid2 3569  prid2g 3567  snid 3495  snidg 3493
[Quine] p. 51Theorem 7.12snexg 4040  snexprc 4042
[Quine] p. 51Theorem 7.13prexg 4062
[Quine] p. 53Theorem 8.2unisn 3691  unisng 3692
[Quine] p. 53Theorem 8.3uniun 3694
[Quine] p. 54Theorem 8.6elssuni 3703
[Quine] p. 54Theorem 8.7uni0 3702
[Quine] p. 56Theorem 8.17uniabio 5024
[Quine] p. 56Definition 8.18dfiota2 5015
[Quine] p. 57Theorem 8.19iotaval 5025
[Quine] p. 57Theorem 8.22iotanul 5029
[Quine] p. 58Theorem 8.23euiotaex 5030
[Quine] p. 58Definition 9.1df-op 3475
[Quine] p. 61Theorem 9.5opabid 4108  opelopab 4122  opelopaba 4117  opelopabaf 4124  opelopabf 4125  opelopabg 4119  opelopabga 4114  oprabid 5719
[Quine] p. 64Definition 9.11df-xp 4473
[Quine] p. 64Definition 9.12df-cnv 4475
[Quine] p. 64Definition 9.15df-id 4144
[Quine] p. 65Theorem 10.3fun0 5106
[Quine] p. 65Theorem 10.4funi 5080
[Quine] p. 65Theorem 10.5funsn 5096  funsng 5094
[Quine] p. 65Definition 10.1df-fun 5051
[Quine] p. 65Definition 10.2args 4834  dffv4g 5337
[Quine] p. 68Definition 10.11df-fv 5057  fv2 5335
[Quine] p. 124Theorem 17.3nn0opth2 10247  nn0opth2d 10246  nn0opthd 10245
[Quine] p. 284Axiom 39(vi)funimaex 5133  funimaexg 5132
[Rudin] p. 164Equation 27efcan 11115
[Rudin] p. 164Equation 30efzval 11122
[Rudin] p. 167Equation 48absefi 11207
[Sanford] p. 39Rule 3mtpxor 1369
[Sanford] p. 39Rule 4mptxor 1367
[Sanford] p. 40Rule 1mptnan 1366
[Schechter] p. 51Definition of antisymmetryintasym 4849
[Schechter] p. 51Definition of irreflexivityintirr 4851
[Schechter] p. 51Definition of symmetrycnvsym 4848
[Schechter] p. 51Definition of transitivitycotr 4846
[Schechter] p. 428Definition 15.35bastop1 11935
[Stoll] p. 13Definition of symmetric differencesymdif1 3280
[Stoll] p. 16Exercise 4.40dif 3373  dif0 3372
[Stoll] p. 16Exercise 4.8difdifdirss 3386
[Stoll] p. 19Theorem 5.2(13)undm 3273
[Stoll] p. 19Theorem 5.2(13')indmss 3274
[Stoll] p. 20Remarkinvdif 3257
[Stoll] p. 25Definition of ordered tripledf-ot 3476
[Stoll] p. 43Definitionuniiun 3805
[Stoll] p. 44Definitionintiin 3806
[Stoll] p. 45Definitiondf-iin 3755
[Stoll] p. 45Definition indexed uniondf-iun 3754
[Stoll] p. 176Theorem 3.4(27)imandc 827  imanst 782
[Stoll] p. 262Example 4.1symdif1 3280
[Suppes] p. 22Theorem 2eq0 3320
[Suppes] p. 22Theorem 4eqss 3054  eqssd 3056  eqssi 3055
[Suppes] p. 23Theorem 5ss0 3342  ss0b 3341
[Suppes] p. 23Theorem 6sstr 3047
[Suppes] p. 25Theorem 12elin 3198  elun 3156
[Suppes] p. 26Theorem 15inidm 3224
[Suppes] p. 26Theorem 16in0 3336
[Suppes] p. 27Theorem 23unidm 3158
[Suppes] p. 27Theorem 24un0 3335
[Suppes] p. 27Theorem 25ssun1 3178
[Suppes] p. 27Theorem 26ssequn1 3185
[Suppes] p. 27Theorem 27unss 3189
[Suppes] p. 27Theorem 28indir 3264
[Suppes] p. 27Theorem 29undir 3265
[Suppes] p. 28Theorem 32difid 3370  difidALT 3371
[Suppes] p. 29Theorem 33difin 3252
[Suppes] p. 29Theorem 34indif 3258
[Suppes] p. 29Theorem 35undif1ss 3376
[Suppes] p. 29Theorem 36difun2 3381
[Suppes] p. 29Theorem 37difin0 3375
[Suppes] p. 29Theorem 38disjdif 3374
[Suppes] p. 29Theorem 39difundi 3267
[Suppes] p. 29Theorem 40difindiss 3269
[Suppes] p. 30Theorem 41nalset 3990
[Suppes] p. 39Theorem 61uniss 3696
[Suppes] p. 39Theorem 65uniop 4106
[Suppes] p. 41Theorem 70intsn 3745
[Suppes] p. 42Theorem 71intpr 3742  intprg 3743
[Suppes] p. 42Theorem 73op1stb 4328  op1stbg 4329
[Suppes] p. 42Theorem 78intun 3741
[Suppes] p. 44Definition 15(a)dfiun2 3786  dfiun2g 3784
[Suppes] p. 44Definition 15(b)dfiin2 3787
[Suppes] p. 47Theorem 86elpw 3455  elpw2 4014  elpw2g 4013  elpwg 3457
[Suppes] p. 47Theorem 87pwid 3464
[Suppes] p. 47Theorem 89pw0 3606
[Suppes] p. 48Theorem 90pwpw0ss 3670
[Suppes] p. 52Theorem 101xpss12 4574
[Suppes] p. 52Theorem 102xpindi 4602  xpindir 4603
[Suppes] p. 52Theorem 103xpundi 4523  xpundir 4524
[Suppes] p. 54Theorem 105elirrv 4392
[Suppes] p. 58Theorem 2relss 4554
[Suppes] p. 59Theorem 4eldm 4664  eldm2 4665  eldm2g 4663  eldmg 4662
[Suppes] p. 59Definition 3df-dm 4477
[Suppes] p. 60Theorem 6dmin 4675
[Suppes] p. 60Theorem 8rnun 4873
[Suppes] p. 60Theorem 9rnin 4874
[Suppes] p. 60Definition 4dfrn2 4655
[Suppes] p. 61Theorem 11brcnv 4650  brcnvg 4648
[Suppes] p. 62Equation 5elcnv 4644  elcnv2 4645
[Suppes] p. 62Theorem 12relcnv 4843
[Suppes] p. 62Theorem 15cnvin 4872
[Suppes] p. 62Theorem 16cnvun 4870
[Suppes] p. 63Theorem 20co02 4978
[Suppes] p. 63Theorem 21dmcoss 4734
[Suppes] p. 63Definition 7df-co 4476
[Suppes] p. 64Theorem 26cnvco 4652
[Suppes] p. 64Theorem 27coass 4983
[Suppes] p. 65Theorem 31resundi 4758
[Suppes] p. 65Theorem 34elima 4812  elima2 4813  elima3 4814  elimag 4811
[Suppes] p. 65Theorem 35imaundi 4877
[Suppes] p. 66Theorem 40dminss 4879
[Suppes] p. 66Theorem 41imainss 4880
[Suppes] p. 67Exercise 11cnvxp 4883
[Suppes] p. 81Definition 34dfec2 6335
[Suppes] p. 82Theorem 72elec 6371  elecg 6370
[Suppes] p. 82Theorem 73erth 6376  erth2 6377
[Suppes] p. 89Theorem 96map0b 6484
[Suppes] p. 89Theorem 97map0 6486  map0g 6485
[Suppes] p. 89Theorem 98mapsn 6487
[Suppes] p. 89Theorem 99mapss 6488
[Suppes] p. 92Theorem 1enref 6562  enrefg 6561
[Suppes] p. 92Theorem 2ensym 6578  ensymb 6577  ensymi 6579
[Suppes] p. 92Theorem 3entr 6581
[Suppes] p. 92Theorem 4unen 6613
[Suppes] p. 94Theorem 15endom 6560
[Suppes] p. 94Theorem 16ssdomg 6575
[Suppes] p. 94Theorem 17domtr 6582
[Suppes] p. 95Theorem 18isbth 6756
[Suppes] p. 98Exercise 4fundmen 6603  fundmeng 6604
[Suppes] p. 98Exercise 6xpdom3m 6630
[Suppes] p. 130Definition 3df-tr 3959
[Suppes] p. 132Theorem 9ssonuni 4333
[Suppes] p. 134Definition 6df-suc 4222
[Suppes] p. 136Theorem Schema 22findes 4446  finds 4443  finds1 4445  finds2 4444
[Suppes] p. 162Definition 5df-ltnqqs 7009  df-ltpq 7002
[Suppes] p. 228Theorem Schema 61onintss 4241
[TakeutiZaring] p. 8Axiom 1ax-ext 2077
[TakeutiZaring] p. 13Definition 4.5df-cleq 2088
[TakeutiZaring] p. 13Proposition 4.6df-clel 2091
[TakeutiZaring] p. 13Proposition 4.9cvjust 2090
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2112
[TakeutiZaring] p. 14Definition 4.16df-oprab 5694
[TakeutiZaring] p. 14Proposition 4.14ru 2853
[TakeutiZaring] p. 15Exercise 1elpr 3487  elpr2 3488  elprg 3486
[TakeutiZaring] p. 15Exercise 2elsn 3482  elsn2 3498  elsn2g 3497  elsng 3481  velsn 3483
[TakeutiZaring] p. 15Exercise 3elop 4082
[TakeutiZaring] p. 15Exercise 4sneq 3477  sneqr 3626
[TakeutiZaring] p. 15Definition 5.1dfpr2 3485  dfsn2 3480
[TakeutiZaring] p. 16Axiom 3uniex 4288
[TakeutiZaring] p. 16Exercise 6opth 4088
[TakeutiZaring] p. 16Exercise 8rext 4066
[TakeutiZaring] p. 16Corollary 5.8unex 4291  unexg 4293
[TakeutiZaring] p. 16Definition 5.3dftp2 3511
[TakeutiZaring] p. 16Definition 5.5df-uni 3676
[TakeutiZaring] p. 16Definition 5.6df-in 3019  df-un 3017
[TakeutiZaring] p. 16Proposition 5.7unipr 3689  uniprg 3690
[TakeutiZaring] p. 17Axiom 4vpwex 4035
[TakeutiZaring] p. 17Exercise 1eltp 3510
[TakeutiZaring] p. 17Exercise 5elsuc 4257  elsucg 4255  sstr2 3046
[TakeutiZaring] p. 17Exercise 6uncom 3159
[TakeutiZaring] p. 17Exercise 7incom 3207
[TakeutiZaring] p. 17Exercise 8unass 3172
[TakeutiZaring] p. 17Exercise 9inass 3225
[TakeutiZaring] p. 17Exercise 10indi 3262
[TakeutiZaring] p. 17Exercise 11undi 3263
[TakeutiZaring] p. 17Definition 5.9dfss2 3028
[TakeutiZaring] p. 17Definition 5.10df-pw 3451
[TakeutiZaring] p. 18Exercise 7unss2 3186
[TakeutiZaring] p. 18Exercise 9df-ss 3026  sseqin2 3234
[TakeutiZaring] p. 18Exercise 10ssid 3059
[TakeutiZaring] p. 18Exercise 12inss1 3235  inss2 3236
[TakeutiZaring] p. 18Exercise 13nssr 3099
[TakeutiZaring] p. 18Exercise 15unieq 3684
[TakeutiZaring] p. 18Exercise 18sspwb 4067
[TakeutiZaring] p. 18Exercise 19pweqb 4074
[TakeutiZaring] p. 20Definitiondf-rab 2379
[TakeutiZaring] p. 20Corollary 5.160ex 3987
[TakeutiZaring] p. 20Definition 5.12df-dif 3015
[TakeutiZaring] p. 20Definition 5.14dfnul2 3304
[TakeutiZaring] p. 20Proposition 5.15difid 3370  difidALT 3371
[TakeutiZaring] p. 20Proposition 5.17(1)n0rf 3314
[TakeutiZaring] p. 21Theorem 5.22setind 4383
[TakeutiZaring] p. 21Definition 5.20df-v 2635
[TakeutiZaring] p. 21Proposition 5.21vprc 3992
[TakeutiZaring] p. 22Exercise 10ss 3340
[TakeutiZaring] p. 22Exercise 3ssex 3997  ssexg 3999
[TakeutiZaring] p. 22Exercise 4inex1 3994
[TakeutiZaring] p. 22Exercise 5ruv 4394
[TakeutiZaring] p. 22Exercise 6elirr 4385
[TakeutiZaring] p. 22Exercise 7ssdif0im 3366
[TakeutiZaring] p. 22Exercise 11difdif 3140
[TakeutiZaring] p. 22Exercise 13undif3ss 3276
[TakeutiZaring] p. 22Exercise 14difss 3141
[TakeutiZaring] p. 22Exercise 15sscon 3149
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2375
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2376
[TakeutiZaring] p. 23Proposition 6.2xpex 4582  xpexg 4581  xpexgALT 5942
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4474
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 5112
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5262  fun11 5115
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 5060  svrelfun 5113
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4654
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4656
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4479
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4480
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4476
[TakeutiZaring] p. 25Exercise 2cnvcnvss 4919  dfrel2 4915
[TakeutiZaring] p. 25Exercise 3xpss 4575
[TakeutiZaring] p. 25Exercise 5relun 4584
[TakeutiZaring] p. 25Exercise 6reluni 4590
[TakeutiZaring] p. 25Exercise 9inxp 4601
[TakeutiZaring] p. 25Exercise 12relres 4773
[TakeutiZaring] p. 25Exercise 13opelres 4750  opelresg 4752
[TakeutiZaring] p. 25Exercise 14dmres 4766
[TakeutiZaring] p. 25Exercise 15resss 4769
[TakeutiZaring] p. 25Exercise 17resabs1 4774
[TakeutiZaring] p. 25Exercise 18funres 5089
[TakeutiZaring] p. 25Exercise 24relco 4963
[TakeutiZaring] p. 25Exercise 29funco 5088
[TakeutiZaring] p. 25Exercise 30f1co 5263
[TakeutiZaring] p. 26Definition 6.10eu2 1999
[TakeutiZaring] p. 26Definition 6.11df-fv 5057  fv3 5363
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 5003  cnvexg 5002
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4731  dmexg 4729
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4732  rnexg 4730
[TakeutiZaring] p. 27Corollary 6.13funfvex 5357
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5366  tz6.12 5367  tz6.12c 5369
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5331
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 5052
[TakeutiZaring] p. 27Definition 6.15(3)df-f 5053
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 5055  wfo 5047
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 5054  wf1 5046
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 5056  wf1o 5048
[TakeutiZaring] p. 28Exercise 4eqfnfv 5436  eqfnfv2 5437  eqfnfv2f 5440
[TakeutiZaring] p. 28Exercise 5fvco 5409
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5558  fnexALT 5922
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5557  resfunexgALT 5919
[TakeutiZaring] p. 29Exercise 9funimaex 5133  funimaexg 5132
[TakeutiZaring] p. 29Definition 6.18df-br 3868
[TakeutiZaring] p. 30Definition 6.21eliniseg 4835  iniseg 4837
[TakeutiZaring] p. 30Definition 6.22df-eprel 4140
[TakeutiZaring] p. 32Definition 6.28df-isom 5058
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5627
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5628
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5633
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5635
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5643
[TakeutiZaring] p. 35Notationwtr 3958
[TakeutiZaring] p. 35Theorem 7.2tz7.2 4205
[TakeutiZaring] p. 35Definition 7.1dftr3 3962
[TakeutiZaring] p. 36Proposition 7.4ordwe 4419
[TakeutiZaring] p. 36Proposition 7.6ordelord 4232
[TakeutiZaring] p. 37Proposition 7.9ordin 4236
[TakeutiZaring] p. 38Corollary 7.15ordsson 4337
[TakeutiZaring] p. 38Definition 7.11df-on 4219
[TakeutiZaring] p. 38Proposition 7.12ordon 4331
[TakeutiZaring] p. 38Proposition 7.13onprc 4396
[TakeutiZaring] p. 39Theorem 7.17tfi 4425
[TakeutiZaring] p. 40Exercise 7dftr2 3960
[TakeutiZaring] p. 40Exercise 11unon 4356
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4332
[TakeutiZaring] p. 40Proposition 7.20elssuni 3703
[TakeutiZaring] p. 41Definition 7.22df-suc 4222
[TakeutiZaring] p. 41Proposition 7.23sssucid 4266  sucidg 4267
[TakeutiZaring] p. 41Proposition 7.24suceloni 4346
[TakeutiZaring] p. 42Exercise 1df-ilim 4220
[TakeutiZaring] p. 42Exercise 8onsucssi 4351  ordelsuc 4350
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4437
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4438
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4439
[TakeutiZaring] p. 43Axiom 7omex 4436
[TakeutiZaring] p. 43Theorem 7.32ordom 4449
[TakeutiZaring] p. 43Corollary 7.31find 4442
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4440
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4441
[TakeutiZaring] p. 44Exercise 2int0 3724
[TakeutiZaring] p. 44Exercise 3trintssm 3974
[TakeutiZaring] p. 44Exercise 4intss1 3725
[TakeutiZaring] p. 44Exercise 6onintonm 4362
[TakeutiZaring] p. 44Definition 7.35df-int 3711
[TakeutiZaring] p. 47Lemma 1tfrlem1 6111
[TakeutiZaring] p. 47Theorem 7.41(1)tfri1 6168  tfri1d 6138
[TakeutiZaring] p. 47Theorem 7.41(2)tfri2 6169  tfri2d 6139
[TakeutiZaring] p. 47Theorem 7.41(3)tfri3 6170
[TakeutiZaring] p. 50Exercise 3smoiso 6105
[TakeutiZaring] p. 50Definition 7.46df-smo 6089
[TakeutiZaring] p. 56Definition 8.1oasuc 6265
[TakeutiZaring] p. 57Proposition 8.2oacl 6261
[TakeutiZaring] p. 57Proposition 8.3oa0 6258
[TakeutiZaring] p. 57Proposition 8.16omcl 6262
[TakeutiZaring] p. 58Proposition 8.4nnaord 6308  nnaordi 6307
[TakeutiZaring] p. 59Proposition 8.6iunss2 3797  uniss2 3706
[TakeutiZaring] p. 59Proposition 8.7oawordriexmid 6271
[TakeutiZaring] p. 59Proposition 8.9nnacl 6281
[TakeutiZaring] p. 62Exercise 5oaword1 6272
[TakeutiZaring] p. 62Definition 8.15om0 6259  omsuc 6273
[TakeutiZaring] p. 63Proposition 8.17nnmcl 6282
[TakeutiZaring] p. 63Proposition 8.19nnmord 6316  nnmordi 6315
[TakeutiZaring] p. 67Definition 8.30oei0 6260
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 6912
[TakeutiZaring] p. 88Exercise 1en0 6592
[TakeutiZaring] p. 90Proposition 10.20nneneq 6653
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6654
[TakeutiZaring] p. 91Definition 10.29df-fin 6540  isfi 6558
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6627
[TakeutiZaring] p. 95Definition 10.42df-map 6447
[TakeutiZaring] p. 96Proposition 10.45mapxpen 6644
[Tarski] p. 67Axiom B5ax-4 1452
[Tarski] p. 68Lemma 6equid 1641
[Tarski] p. 69Lemma 7equcomi 1644
[Tarski] p. 70Lemma 14spim 1680  spime 1683  spimeh 1681  spimh 1679
[Tarski] p. 70Lemma 16ax-11 1449  ax-11o 1758  ax11i 1656
[Tarski] p. 70Lemmas 16 and 17sb6 1821
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1471
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1456  ax-14 1457
[WhiteheadRussell] p. 96Axiom *1.3olc 670
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 684
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 711
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 720
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 741
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 584
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 610
[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 786
[WhiteheadRussell] p. 101Theorem *2.06barbara 2053  syl 14
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 694
[WhiteheadRussell] p. 101Theorem *2.08id 19  idALT 20
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 785
[WhiteheadRussell] p. 101Theorem *2.12notnot 597
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 820
[WhiteheadRussell] p. 102Theorem *2.14notnotrdc 792
[WhiteheadRussell] p. 102Theorem *2.15con1dc 794
[WhiteheadRussell] p. 103Theorem *2.16con3 609
[WhiteheadRussell] p. 103Theorem *2.17condc 790
[WhiteheadRussell] p. 103Theorem *2.18pm2.18dc 791
[WhiteheadRussell] p. 104Theorem *2.2orc 671
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 730
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 585
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 589
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 833
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 854
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 40
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 723
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 724
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 756
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 757
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 755
[WhiteheadRussell] p. 105Definition *2.33df-3or 928
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 733
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 731
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 732
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 53
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 695
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 696
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 804
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 800
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 697
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 698
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 699
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 619
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 620
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 679
[WhiteheadRussell] p. 107Theorem *2.54pm2.54dc 831
[WhiteheadRussell] p. 107Theorem *2.55orel1 682
[WhiteheadRussell] p. 107Theorem *2.56orel2 683
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 803
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 705
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 752
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 753
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 623
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 672  pm2.67 700
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 805
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 704
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 762
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 834
[WhiteheadRussell] p. 108Theorem *2.69looinvdc 862
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 758
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 759
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 761
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 760
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 763
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 764
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 77
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 852
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 100
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 709
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 138
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 906
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 907
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 908
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 708
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 261
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 262
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 665
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 340
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 258
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 259
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 108  simplimdc 798
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 109  simprimdc 797
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 338
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 339
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37 829
[WhiteheadRussell] p. 113Fact)pm3.45 565
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 327
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 325
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 326
[WhiteheadRussell] p. 113Theorem *3.44jao 710  pm3.44 673
[WhiteheadRussell] p. 113Theorem *3.47prth 337
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 570
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 737
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 806
[WhiteheadRussell] p. 117Theorem *4.2biid 170
[WhiteheadRussell] p. 117Theorem *4.13notnotbdc 807
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 828
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 830
[WhiteheadRussell] p. 117Theorem *4.21bicom 139
[WhiteheadRussell] p. 117Theorem *4.22biantr 901  bitr 457
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 388
[WhiteheadRussell] p. 117Theorem *4.25oridm 712  pm4.25 713
[WhiteheadRussell] p. 118Theorem *4.3ancom 263
[WhiteheadRussell] p. 118Theorem *4.4andi 770
[WhiteheadRussell] p. 118Theorem *4.31orcom 685
[WhiteheadRussell] p. 118Theorem *4.32anass 394
[WhiteheadRussell] p. 118Theorem *4.33orass 722
[WhiteheadRussell] p. 118Theorem *4.36anbi1 455
[WhiteheadRussell] p. 118Theorem *4.37orbi1 744
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 573
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 774
[WhiteheadRussell] p. 118Definition *4.34df-3an 929
[WhiteheadRussell] p. 119Theorem *4.41ordi 768
[WhiteheadRussell] p. 119Theorem *4.42pm4.42r 920
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 898
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 734
[WhiteheadRussell] p. 119Theorem *4.45orabs 766  pm4.45 736  pm4.45im 328
[WhiteheadRussell] p. 119Theorem *10.2219.26 1422
[WhiteheadRussell] p. 120Theorem *4.5anordc 905
[WhiteheadRussell] p. 120Theorem *4.6imordc 837  imorr 838
[WhiteheadRussell] p. 120Theorem *4.7anclb 313
[WhiteheadRussell] p. 120Theorem *4.51ianordc 840
[WhiteheadRussell] p. 120Theorem *4.52pm4.52im 844
[WhiteheadRussell] p. 120Theorem *4.53pm4.53r 845
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 846
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 887
[WhiteheadRussell] p. 120Theorem *4.56ioran 707  pm4.56 847
[WhiteheadRussell] p. 120Theorem *4.57orandc 888  oranim 848
[WhiteheadRussell] p. 120Theorem *4.61annimim 823
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 839
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 821
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 842
[WhiteheadRussell] p. 120Theorem *4.65pm4.65r 824
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 843
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 822
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 382  pm4.71d 386  pm4.71i 384  pm4.71r 383  pm4.71rd 387  pm4.71ri 385
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 775
[WhiteheadRussell] p. 121Theorem *4.73iba 295
[WhiteheadRussell] p. 121Theorem *4.74biorf 701
[WhiteheadRussell] p. 121Theorem *4.76jcab 571  pm4.76 572
[WhiteheadRussell] p. 121Theorem *4.77jaob 669  pm4.77 751
[WhiteheadRussell] p. 121Theorem *4.78pm4.78i 849
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 850
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 661
[WhiteheadRussell] p. 122Theorem *4.81pm4.81dc 855
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 899
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 900
[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 260  pm4.87 525
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 569
[WhiteheadRussell] p. 123Theorem *5.11pm5.11dc 856
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 857
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 859
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 858
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1332
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 776
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 851
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1337  pm5.18dc 818
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 660
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 649
[WhiteheadRussell] p. 124Theorem *5.22xordc 1335
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1340
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1341
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 835
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 460
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 248
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 241
[WhiteheadRussell] p. 125Theorem *5.6pm5.6dc 876  pm5.6r 877
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 903
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 341
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 442
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 577
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 867
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 578
[WhiteheadRussell] p. 125Theorem *5.41imdi 249  pm5.41 250
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 314
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 875
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 754
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 868
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 860
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 746
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 894
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 895
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 910
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 243
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 178
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 911
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1578
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1426
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1575
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1830
[WhiteheadRussell] p. 175Definition *14.02df-eu 1958
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2343
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2344
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2768
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2909
[WhiteheadRussell] p. 190Theorem *14.22iota4 5032
[WhiteheadRussell] p. 191Theorem *14.23iota4an 5033
[WhiteheadRussell] p. 192Theorem *14.26eupick 2034  eupickbi 2037
[WhiteheadRussell] p. 235Definition *30.01df-fv 5057
[WhiteheadRussell] p. 360Theorem *54.43pm54.43 6915

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