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

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