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 8939
[Apostol] p. 18Theorem I.1addcan 6988  addcan2d 6993  addcan2i 6991  addcand 6992  addcani 6990
[Apostol] p. 18Theorem I.2negeu 6999
[Apostol] p. 18Theorem I.3negsub 7055  negsubd 7124  negsubi 7085
[Apostol] p. 18Theorem I.4negneg 7057  negnegd 7109  negnegi 7077
[Apostol] p. 18Theorem I.5subdi 7178  subdid 7207  subdii 7200  subdir 7179  subdird 7208  subdiri 7201
[Apostol] p. 18Theorem I.6mul01 7182  mul01d 7186  mul01i 7184  mul02 7180  mul02d 7185  mul02i 7183
[Apostol] p. 18Theorem I.9divrecapd 7550
[Apostol] p. 18Theorem I.10recrecapi 7502
[Apostol] p. 18Theorem I.12mul2neg 7191  mul2negd 7206  mul2negi 7199  mulneg1 7188  mulneg1d 7204  mulneg1i 7197
[Apostol] p. 18Theorem I.15divdivdivap 7471
[Apostol] p. 20Axiom 7rpaddcl 8381  rpaddcld 8412  rpmulcl 8382  rpmulcld 8413
[Apostol] p. 20Axiom 90nrp 8391
[Apostol] p. 20Theorem I.17lttri 6919
[Apostol] p. 20Theorem I.18ltadd1d 7324  ltadd1dd 7342  ltadd1i 7289
[Apostol] p. 20Theorem I.19ltmul1 7376  ltmul1a 7375  ltmul1i 7667  ltmul1ii 7675  ltmul2 7603  ltmul2d 8435  ltmul2dd 8449  ltmul2i 7670
[Apostol] p. 20Theorem I.210lt1 6938
[Apostol] p. 20Theorem I.23lt0neg1 7258  lt0neg1d 7302  ltneg 7252  ltnegd 7309  ltnegi 7280
[Apostol] p. 20Theorem I.25lt2add 7235  lt2addd 7353  lt2addi 7297
[Apostol] p. 20Definition of positive numbersdf-rp 8359
[Apostol] p. 21Exercise 4recgt0 7597  recgt0d 7681  recgt0i 7653  recgt0ii 7654
[Apostol] p. 22Definition of integersdf-z 8022
[Apostol] p. 22Definition of rationalsdf-q 8331
[Apostol] p. 26Theorem I.29arch 7954
[Apostol] p. 28Exercise 2btwnz 8133
[Apostol] p. 28Exercise 3nnrecl 7955
[Apostol] p. 28Exercise 10(a)zneo 8115
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 7698
[Bauer] p. 482Section 1.2pm2.01 546  pm2.65 584
[Bauer] p. 483Theorem 1.3acexmid 5454  onsucelsucexmidlem 4214
[Bauer], p. 483Definitionn0rf 3227
[Bauer], p. 485Theorem 2.1ssfiexmid 6254
[BauerTaylor], p. 32Lemma 6.16prarloclem 6484
[BauerTaylor], p. 50Lemma 11.4subhalfnqq 6397
[BauerTaylor], p. 52Proposition 11.15prarloc 6486
[BauerTaylor], p. 53Lemma 11.16addclpr 6520  addlocpr 6519
[BauerTaylor], p. 55Proposition 12.7appdivnq 6544
[BauerTaylor], p. 56Lemma 12.8prmuloc 6547
[BauerTaylor], p. 56Lemma 12.9mullocpr 6552
[BellMachover] p. 36Lemma 10.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 1900
[BellMachover] p. 460Notationdf-mo 1901
[BellMachover] p. 460Definitionmo3 1951  mo3h 1950
[BellMachover] p. 462Theorem 1.1bm1.1 2022
[BellMachover] p. 463Theorem 1.3iibm1.3ii 3869
[BellMachover] p. 466Axiom Powaxpow3 3921
[BellMachover] p. 466Axiom Unionaxun2 4138
[BellMachover] p. 469Theorem 2.2(i)ordirr 4225
[BellMachover] p. 469Theorem 2.2(iii)onelon 4087
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4188
[BellMachover] p. 471Definition of Limdf-ilim 4072
[BellMachover] p. 472Axiom Infzfinf2 4255
[BellMachover] p. 473Theorem 2.8limom 4279
[Bobzien] p. 116Statement T3stoic3 1317
[Bobzien] p. 117Statement T2stoic2a 1315
[Bobzien] p. 117Statement T4stoic4a 1318
[BourbakiEns] p. Proposition 8fcof1 5366  fcofo 5367
[BourbakiTop1] p. Remarkxnegmnf 8512  xnegpnf 8511
[BourbakiTop1] p. Remark rexneg 8513
[ChoquetDD] p. 2Definition of mappingdf-mpt 3811
[Crosilla] p. Axiom 1ax-ext 2019
[Crosilla] p. Axiom 2ax-pr 3935
[Crosilla] p. Axiom 3ax-un 4136
[Crosilla] p. Axiom 4ax-nul 3874
[Crosilla] p. Axiom 5ax-iinf 4254
[Crosilla] p. Axiom 6ru 2757
[Crosilla] p. Axiom 8ax-pow 3918
[Crosilla] p. Axiom 9ax-setind 4220
[Crosilla], p. Axiom 6ax-sep 3866
[Crosilla], p. Axiom 7ax-coll 3863
[Crosilla], p. Axiom 7'repizf 3864
[Crosilla], p. Theorem is statedordtriexmid 4210
[Crosilla], p. Axiom of choice implies instancesacexmid 5454
[Crosilla], p. Definition of ordinaldf-iord 4069
[Crosilla], p. Theorem "Foundation implies instances of EM"regexmid 4219
[Eisenberg] p. 67Definition 5.3df-dif 2914
[Eisenberg] p. 82Definition 6.3df-iom 4257
[Enderton] p. 18Axiom of Empty Setaxnul 3873
[Enderton] p. 19Definitiondf-tp 3375
[Enderton] p. 26Exercise 5unissb 3601
[Enderton] p. 26Exercise 10pwel 3945
[Enderton] p. 28Exercise 7(b)pwunim 4014
[Enderton] p. 30Theorem "Distributive laws"iinin1m 3717  iinin2m 3716  iunin1 3712  iunin2 3711
[Enderton] p. 31Theorem "De Morgan's laws"iindif2m 3715  iundif2ss 3713
[Enderton] p. 33Exercise 23iinuniss 3728
[Enderton] p. 33Exercise 25iununir 3729
[Enderton] p. 33Exercise 24(a)iinpw 3733
[Enderton] p. 33Exercise 24(b)iunpw 4177  iunpwss 3734
[Enderton] p. 38Exercise 6(a)unipw 3944
[Enderton] p. 38Exercise 6(b)pwuni 3934
[Enderton] p. 41Lemma 3Dopeluu 4148  rnex 4542  rnexg 4540
[Enderton] p. 41Exercise 8dmuni 4488  rnuni 4678
[Enderton] p. 42Definition of a functiondffun7 4871  dffun8 4872
[Enderton] p. 43Definition of function valuefunfvdm2 5180
[Enderton] p. 43Definition of single-rootedfuncnv 4903
[Enderton] p. 44Definition (d)dfima2 4613  dfima3 4614
[Enderton] p. 47Theorem 3Hfvco2 5185
[Enderton] p. 50Theorem 3K(a)imauni 5343
[Enderton] p. 53Exercise 21coass 4782
[Enderton] p. 53Exercise 27dmco 4772
[Enderton] p. 53Exercise 14(a)funin 4913
[Enderton] p. 53Exercise 22(a)imass2 4644
[Enderton] p. 56Theorem 3Merref 6062
[Enderton] p. 57Lemma 3Nerthi 6088
[Enderton] p. 57Definitiondf-ec 6044
[Enderton] p. 58Definitiondf-qs 6048
[Enderton] p. 60Theorem 3Qth3q 6147  th3qcor 6146  th3qlem1 6144  th3qlem2 6145
[Enderton] p. 61Exercise 35df-ec 6044
[Enderton] p. 65Exercise 56(a)dmun 4485
[Enderton] p. 68Definition of successordf-suc 4074
[Enderton] p. 71Definitiondf-tr 3846  dftr4 3850
[Enderton] p. 72Theorem 4Eunisuc 4116  unisucg 4117
[Enderton] p. 73Exercise 6unisuc 4116  unisucg 4117
[Enderton] p. 73Exercise 5(a)truni 3859
[Enderton] p. 73Exercise 5(b)trint 3860
[Enderton] p. 79Theorem 4I(A1)nna0 5992
[Enderton] p. 79Theorem 4I(A2)nnasuc 5994  onasuc 5985
[Enderton] p. 79Definition of operation valuedf-ov 5458
[Enderton] p. 80Theorem 4J(A1)nnm0 5993
[Enderton] p. 80Theorem 4J(A2)nnmsuc 5995  onmsuc 5991
[Enderton] p. 81Theorem 4K(1)nnaass 6003
[Enderton] p. 81Theorem 4K(2)nna0r 5996  nnacom 6002
[Enderton] p. 81Theorem 4K(3)nndi 6004
[Enderton] p. 81Theorem 4K(4)nnmass 6005
[Enderton] p. 81Theorem 4K(5)nnmcom 6007
[Enderton] p. 82Exercise 16nnm0r 5997  nnmsucr 6006
[Enderton] p. 88Exercise 23nnaordex 6036
[Enderton] p. 129Definitiondf-en 6158
[Enderton] p. 144Corollary 6Kundif2ss 3293
[Enderton] p. 145Figure 38ffoss 5101
[Enderton] p. 145Definitiondf-dom 6159
[Enderton] p. 146Example 1domen 6168  domeng 6169
[Enderton] p. 149Theorem 6L(c)xpdom1 6245  xpdom1g 6243  xpdom2g 6242
[Enderton] p. 168Definitiondf-po 4024
[Enderton] p. 192Theorem 7M(a)oneli 4131
[Enderton] p. 192Theorem 7M(b)ontr1 4092
[Enderton] p. 193Corollary 7N(b)0elon 4095
[Enderton] p. 193Corollary 7N(c)onsuci 4207
[Enderton] p. 193Corollary 7N(d)ssonunii 4181
[Enderton] p. 194Remarkonprc 4230
[Enderton] p. 194Exercise 16suc11 4236
[Enderton] p. 200Exercise 25tfis 4249
[Enderton] p. 206Theorem 7X(b)en2lp 4232
[Enderton] p. 207Exercise 34opthreg 4234
[Enderton] p. 208Exercise 35suc11g 4235
[Geuvers], p. 6Lemma 2.13mulap0r 7399
[Geuvers], p. 6Lemma 2.15mulap0 7417
[Geuvers], p. 9Lemma 2.35msqge0 7400
[Geuvers], p. 9Definition 3.1(2)ax-arch 6802
[Geuvers], p. 17Definition 6.1df-ap 7366
[Gleason] p. 117Proposition 9-2.1df-enq 6331  enqer 6342
[Gleason] p. 117Proposition 9-2.2df-1nqqs 6335  df-nqqs 6332
[Gleason] p. 117Proposition 9-2.3df-plpq 6328  df-plqqs 6333
[Gleason] p. 119Proposition 9-2.4df-mpq 6329  df-mqqs 6334
[Gleason] p. 119Proposition 9-2.5df-rq 6336
[Gleason] p. 119Proposition 9-2.6ltexnqq 6391
[Gleason] p. 120Proposition 9-2.6(i)halfnq 6394  ltbtwnnq 6399  ltbtwnnqq 6398
[Gleason] p. 120Proposition 9-2.6(ii)ltanqg 6384
[Gleason] p. 120Proposition 9-2.6(iii)ltmnqg 6385
[Gleason] p. 123Proposition 9-3.5addclpr 6520
[Gleason] p. 123Proposition 9-3.5(i)addassprg 6555
[Gleason] p. 123Proposition 9-3.5(ii)addcomprg 6554
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 6571
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 6587
[Gleason] p. 123Proposition 9-3.5(v)ltaprg 6592  ltaprlem 6591
[Gleason] p. 123Proposition 9-3.5(vi)addcanprg 6590
[Gleason] p. 124Proposition 9-3.7mulclpr 6553
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 6568
[Gleason] p. 124Proposition 9-3.7(i)mulassprg 6557
[Gleason] p. 124Proposition 9-3.7(ii)mulcomprg 6556
[Gleason] p. 124Proposition 9-3.7(iii)distrprg 6564
[Gleason] p. 124Proposition 9-3.7(v)recexpr 6610
[Gleason] p. 126Proposition 9-4.1df-enr 6654  enrer 6663
[Gleason] p. 126Proposition 9-4.2df-0r 6659  df-1r 6660  df-nr 6655
[Gleason] p. 126Proposition 9-4.3df-mr 6657  df-plr 6656  negexsr 6700  recexsrlem 6702
[Gleason] p. 127Proposition 9-4.4df-ltr 6658
[Gleason] p. 130Proposition 10-1.3creui 7693  creur 7692  cru 7386
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 6794  axcnre 6765
[Gleason] p. 132Definition 10-3.1crim 9086  crimd 9204  crimi 9165  crre 9085  crred 9203  crrei 9164
[Gleason] p. 132Definition 10-3.2remim 9088  remimd 9170
[Gleason] p. 133Definition 10.36absval2 9221
[Gleason] p. 133Proposition 10-3.4(a)cjadd 9112  cjaddd 9192  cjaddi 9160
[Gleason] p. 133Proposition 10-3.4(c)cjmul 9113  cjmuld 9193  cjmuli 9161
[Gleason] p. 133Proposition 10-3.4(e)cjcj 9111  cjcjd 9171  cjcji 9143
[Gleason] p. 133Proposition 10-3.4(f)cjre 9110  cjreb 9094  cjrebd 9174  cjrebi 9146  cjred 9198  rere 9093  rereb 9091  rerebd 9173  rerebi 9145  rered 9196
[Gleason] p. 133Proposition 10-3.4(h)addcj 9119  addcjd 9184  addcji 9155
[Gleason] p. 133Proposition 10-3.7(a)absval 9210
[Gleason] p. 133Proposition 10-3.7(b)abscj 9220
[Gleason] p. 134Definition 10-4.10exp0e1 8914  df-iexp 8909  exp0 8913  expp1 8916  expp1d 9035
[Gleason] p. 135Proposition 10-4.2(a)expadd 8951  expaddd 9036
[Gleason] p. 135Proposition 10-4.2(b)expmul 8954  expmuld 9037
[Gleason] p. 135Proposition 10-4.2(c)mulexp 8948  mulexpd 9049
[Gleason] p. 141Definition 11-2.1fzval 8646
[Gleason] p. 173Definition 12-3.1df-ltxr 6862  df-xr 6861  ltxr 8465
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 7
[Hamilton] p. 74Rule 2ax-gen 1335
[Heyting] p. 127Axiom #1ax1hfs 9233
[Hitchcock] p. 5Rule A3mpto1 1311
[Hitchcock] p. 5Rule A4mpto2 1312
[Hitchcock] p. 5Rule A5mtp-xor 1313
[HoTT], p. Theorem 7.2.6nndceq 6015
[HoTT], p. Section 11.2.1df-iltp 6453  df-imp 6452  df-iplp 6451  df-reap 7359
[HoTT], p. Theorem 11.2.12cauappcvgpr 6634
[HoTT], p. Corollary 11.4.3conventions 9231
[HoTT], p. Corollary 11.2.13caucvgpr 6653
[HoTT], p. Definition 11.2.1df-inp 6449
[HoTT], p. Proposition 11.2.3df-iso 4025  ltpopr 6569  ltsopr 6570
[HoTT], p. Definition 11.2.7(v)apsym 7390  reapcotr 7382  reapirr 7361
[HoTT], p. Definition 11.2.7(vi)0lt1 6938  gt0add 7357  leadd1 7220  lelttr 6903  lemul1a 7605  lenlt 6891  ltadd1 7219  ltletr 6904  ltmul1 7376  reaplt 7372
[Jech] p. 4Definition of classcv 1241  cvjust 2032
[Jech] p. 78Noteopthprc 4334
[KalishMontague] p. 81Note 1ax-i9 1420
[Kreyszig] p. 12Equation 5muleqadd 7431
[Kunen] p. 10Axiom 0a9e 1583
[Kunen] p. 12Axiom 6zfrep6 3865
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3658
[Levy] p. 338Axiomdf-clab 2024  df-clel 2033  df-cleq 2030
[Lopez-Astorga] p. 12Rule 1mpto1 1311
[Lopez-Astorga] p. 12Rule 2mpto2 1312
[Lopez-Astorga] p. 12Rule 3mtp-xor 1313
[Margaris] p. 40Rule Cexlimiv 1486
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3condc 748
[Margaris] p. 49Definitiondfbi2 368  dfordc 790  exalim 1388
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 40
[Margaris] p. 60Theorem 8mth8 578
[Margaris] p. 89Theorem 19.219.2 1526  r19.2m 3303
[Margaris] p. 89Theorem 19.319.3 1443  19.3h 1442  rr19.3v 2676
[Margaris] p. 89Theorem 19.5alcom 1364
[Margaris] p. 89Theorem 19.6alexdc 1507  alexim 1533
[Margaris] p. 89Theorem 19.7alnex 1385
[Margaris] p. 89Theorem 19.819.8a 1479  spsbe 1720
[Margaris] p. 89Theorem 19.919.9 1532  19.9h 1531  19.9v 1748  exlimd 1485
[Margaris] p. 89Theorem 19.11excom 1551  excomim 1550
[Margaris] p. 89Theorem 19.1219.12 1552  r19.12 2416
[Margaris] p. 90Theorem 19.14exnalim 1534
[Margaris] p. 90Theorem 19.15albi 1354  ralbi 2439
[Margaris] p. 90Theorem 19.1619.16 1444
[Margaris] p. 90Theorem 19.1719.17 1445
[Margaris] p. 90Theorem 19.18exbi 1492  rexbi 2440
[Margaris] p. 90Theorem 19.1919.19 1553
[Margaris] p. 90Theorem 19.20alim 1343  alimd 1411  alimdh 1353  alimdv 1756  ralimdaa 2380  ralimdv 2382  ralimdva 2381  sbcimdv 2817
[Margaris] p. 90Theorem 19.2119.21-2 1554  19.21 1472  19.21bi 1447  19.21h 1446  19.21ht 1470  19.21t 1471  19.21v 1750  alrimd 1498  alrimdd 1497  alrimdh 1365  alrimdv 1753  alrimi 1412  alrimih 1355  alrimiv 1751  alrimivv 1752  r19.21 2389  r19.21be 2404  r19.21bi 2401  r19.21t 2388  r19.21v 2390  ralrimd 2391  ralrimdv 2392  ralrimdva 2393  ralrimdvv 2397  ralrimdvva 2398  ralrimi 2384  ralrimiv 2385  ralrimiva 2386  ralrimivv 2394  ralrimivva 2395  ralrimivvva 2396  ralrimivw 2387  rexlimi 2420
[Margaris] p. 90Theorem 19.222alimdv 1758  2eximdv 1759  exim 1487  eximd 1500  eximdh 1499  eximdv 1757  rexim 2407  reximdai 2411  reximdv 2414  reximdv2 2412  reximdva 2415  reximdvai 2413  reximi2 2409
[Margaris] p. 90Theorem 19.2319.23 1565  19.23bi 1480  19.23h 1384  19.23ht 1383  19.23t 1564  19.23v 1760  19.23vv 1761  exlimd2 1483  exlimdh 1484  exlimdv 1697  exlimdvv 1774  exlimi 1482  exlimih 1481  exlimiv 1486  exlimivv 1773  r19.23 2418  r19.23v 2419  rexlimd 2424  rexlimdv 2426  rexlimdv3a 2429  rexlimdva 2427  rexlimdvaa 2428  rexlimdvv 2433  rexlimdvva 2434  rexlimdvw 2430  rexlimiv 2421  rexlimiva 2422  rexlimivv 2432
[Margaris] p. 90Theorem 19.24i19.24 1527
[Margaris] p. 90Theorem 19.2519.25 1514
[Margaris] p. 90Theorem 19.2619.26-2 1368  19.26-3an 1369  19.26 1367  r19.26-2 2436  r19.26-3 2437  r19.26 2435  r19.26m 2438
[Margaris] p. 90Theorem 19.2719.27 1450  19.27h 1449  19.27v 1776  r19.27av 2442  r19.27m 3310  r19.27mv 3311
[Margaris] p. 90Theorem 19.2819.28 1452  19.28h 1451  19.28v 1777  r19.28av 2443  r19.28m 3305  r19.28mv 3308  rr19.28v 2677
[Margaris] p. 90Theorem 19.2919.29 1508  19.29r 1509  19.29r2 1510  19.29x 1511  r19.29 2444  r19.29d2r 2449  r19.29r 2445
[Margaris] p. 90Theorem 19.3019.30dc 1515
[Margaris] p. 90Theorem 19.3119.31r 1568
[Margaris] p. 90Theorem 19.3219.32dc 1566  19.32r 1567  r19.32r 2451  r19.32vdc 2453  r19.32vr 2452
[Margaris] p. 90Theorem 19.3319.33 1370  19.33b2 1517  19.33bdc 1518
[Margaris] p. 90Theorem 19.3419.34 1571
[Margaris] p. 90Theorem 19.3519.35-1 1512  19.35i 1513
[Margaris] p. 90Theorem 19.3619.36-1 1560  19.36aiv 1778  19.36i 1559  r19.36av 2455
[Margaris] p. 90Theorem 19.3719.37-1 1561  19.37aiv 1562  r19.37 2456  r19.37av 2457
[Margaris] p. 90Theorem 19.3819.38 1563
[Margaris] p. 90Theorem 19.39i19.39 1528
[Margaris] p. 90Theorem 19.4019.40-2 1520  19.40 1519  r19.40 2458
[Margaris] p. 90Theorem 19.4119.41 1573  19.41h 1572  19.41v 1779  19.41vv 1780  19.41vvv 1781  19.41vvvv 1782  r19.41 2459  r19.41v 2460
[Margaris] p. 90Theorem 19.4219.42 1575  19.42h 1574  19.42v 1783  19.42vv 1785  19.42vvv 1786  19.42vvvv 1787  r19.42v 2461
[Margaris] p. 90Theorem 19.4319.43 1516  r19.43 2462
[Margaris] p. 90Theorem 19.4419.44 1569  r19.44av 2463
[Margaris] p. 90Theorem 19.4519.45 1570  r19.45av 2464  r19.45mv 3309
[Margaris] p. 110Exercise 2(b)eu1 1922
[Megill] p. 444Axiom C5ax-17 1416
[Megill] p. 445Lemma L12alequcom 1405  ax-10 1393
[Megill] p. 446Lemma L17equtrr 1593
[Megill] p. 446Lemma L19hbnae 1606
[Megill] p. 447Remark 9.1df-sb 1643  sbid 1654
[Megill] p. 448Scheme C5'ax-4 1397
[Megill] p. 448Scheme C6'ax-7 1334
[Megill] p. 448Scheme C8'ax-8 1392
[Megill] p. 448Scheme C9'ax-i12 1395
[Megill] p. 448Scheme C11'ax-10o 1601
[Megill] p. 448Scheme C12'ax-13 1401
[Megill] p. 448Scheme C13'ax-14 1402
[Megill] p. 448Scheme C15'ax-11o 1701
[Megill] p. 448Scheme C16'ax-16 1692
[Megill] p. 448Theorem 9.4dral1 1615  dral2 1616  drex1 1676  drex2 1617  drsb1 1677  drsb2 1719
[Megill] p. 449Theorem 9.7sbcom2 1860  sbequ 1718  sbid2v 1869
[Megill] p. 450Example in Appendixhba1 1430
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 2834  rspsbca 2835  stdpc4 1655
[Mendelson] p. 69Axiom 5ra5 2840  stdpc5 1473
[Mendelson] p. 81Rule Cexlimiv 1486
[Mendelson] p. 95Axiom 6stdpc6 1588
[Mendelson] p. 95Axiom 7stdpc7 1650
[Mendelson] p. 231Exercise 4.10(k)inv1 3247
[Mendelson] p. 231Exercise 4.10(l)unv 3248
[Mendelson] p. 231Exercise 4.10(n)inssun 3171
[Mendelson] p. 231Exercise 4.10(o)df-nul 3219
[Mendelson] p. 231Exercise 4.10(q)inssddif 3172
[Mendelson] p. 231Exercise 4.10(s)ddifnel 3069
[Mendelson] p. 231Definition of unionunssin 3170
[Mendelson] p. 235Exercise 4.12(c)univ 4173
[Mendelson] p. 235Exercise 4.12(d)pwv 3570
[Mendelson] p. 235Exercise 4.12(j)pwin 4010
[Mendelson] p. 235Exercise 4.12(k)pwunss 4011
[Mendelson] p. 235Exercise 4.12(l)pwssunim 4012
[Mendelson] p. 235Exercise 4.12(n)uniin 3591
[Mendelson] p. 235Exercise 4.12(p)reli 4408
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 4784
[Mendelson] p. 246Definition of successordf-suc 4074
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6231  xpsneng 6232
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6237  xpcomeng 6238
[Mendelson] p. 254Proposition 4.22(e)xpassen 6240
[Mendelson] p. 255Exercise 4.39endisj 6234
[Mendelson] p. 266Proposition 4.34(a)oa1suc 5986
[Monk1] p. 26Theorem 2.8(vii)ssin 3153
[Monk1] p. 33Theorem 3.2(i)ssrel 4371
[Monk1] p. 33Theorem 3.2(ii)eqrel 4372
[Monk1] p. 34Definition 3.3df-opab 3810
[Monk1] p. 36Theorem 3.7(i)coi1 4779  coi2 4780
[Monk1] p. 36Theorem 3.8(v)dm0 4492  rn0 4531
[Monk1] p. 36Theorem 3.7(ii)cnvi 4671
[Monk1] p. 37Theorem 3.13(i)relxp 4390
[Monk1] p. 37Theorem 3.13(x)dmxpm 4498  rnxpm 4695
[Monk1] p. 37Theorem 3.13(ii)0xp 4363  xp0 4686
[Monk1] p. 38Theorem 3.16(ii)ima0 4627
[Monk1] p. 38Theorem 3.16(viii)imai 4624
[Monk1] p. 39Theorem 3.17imaexg 4623
[Monk1] p. 39Theorem 3.16(xi)imassrn 4622
[Monk1] p. 41Theorem 4.3(i)fnopfv 5240  funfvop 5222
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5160
[Monk1] p. 42Theorem 4.4(iii)fvelima 5168
[Monk1] p. 43Theorem 4.6funun 4887
[Monk1] p. 43Theorem 4.8(iv)dff13 5350  dff13f 5352
[Monk1] p. 46Theorem 4.15(v)funex 5327  funrnex 5683
[Monk1] p. 50Definition 5.4fniunfv 5344
[Monk1] p. 52Theorem 5.12(ii)op2ndb 4747
[Monk1] p. 52Theorem 5.11(viii)ssint 3622
[Monk1] p. 52Definition 5.13 (i)1stval2 5724  df-1st 5709
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5725  df-2nd 5710
[Monk2] p. 105Axiom C4ax-5 1333
[Monk2] p. 105Axiom C7ax-8 1392
[Monk2] p. 105Axiom C8ax-11 1394  ax-11o 1701
[Monk2] p. 105Axiom (C8)ax11v 1705
[Monk2] p. 109Lemma 12ax-7 1334
[Monk2] p. 109Lemma 15equvin 1740  equvini 1638  eqvinop 3971
[Monk2] p. 113Axiom C5-1ax-17 1416
[Monk2] p. 113Axiom C5-2ax6b 1538
[Monk2] p. 113Axiom C5-3ax-7 1334
[Monk2] p. 114Lemma 22hba1 1430
[Monk2] p. 114Lemma 23hbia1 1441  nfia1 1469
[Monk2] p. 114Lemma 24hba2 1440  nfa2 1468
[Moschovakis] p. 2Chapter 2 df-stab 739  dftest 821
[Quine] p. 16Definition 2.1df-clab 2024  rabid 2479
[Quine] p. 17Definition 2.1''dfsb7 1864
[Quine] p. 18Definition 2.7df-cleq 2030
[Quine] p. 19Definition 2.9df-v 2553
[Quine] p. 34Theorem 5.1abeq2 2143
[Quine] p. 35Theorem 5.2abid2 2155  abid2f 2199
[Quine] p. 40Theorem 6.1sb5 1764
[Quine] p. 40Theorem 6.2sb56 1762  sb6 1763
[Quine] p. 41Theorem 6.3df-clel 2033
[Quine] p. 41Theorem 6.4eqid 2037
[Quine] p. 41Theorem 6.5eqcom 2039
[Quine] p. 42Theorem 6.6df-sbc 2759
[Quine] p. 42Theorem 6.7dfsbcq 2760  dfsbcq2 2761
[Quine] p. 43Theorem 6.8vex 2554
[Quine] p. 43Theorem 6.9isset 2555
[Quine] p. 44Theorem 7.3spcgf 2629  spcgv 2634  spcimgf 2627
[Quine] p. 44Theorem 6.11spsbc 2769  spsbcd 2770
[Quine] p. 44Theorem 6.12elex 2560
[Quine] p. 44Theorem 6.13elab 2681  elabg 2682  elabgf 2679
[Quine] p. 44Theorem 6.14noel 3222
[Quine] p. 48Theorem 7.2snprc 3426
[Quine] p. 48Definition 7.1df-pr 3374  df-sn 3373
[Quine] p. 49Theorem 7.4snss 3485  snssg 3491
[Quine] p. 49Theorem 7.5prss 3511  prssg 3512
[Quine] p. 49Theorem 7.6prid1 3467  prid1g 3465  prid2 3468  prid2g 3466  snid 3394  snidg 3392
[Quine] p. 51Theorem 7.12snexg 3927  snexprc 3929
[Quine] p. 51Theorem 7.13prexg 3938
[Quine] p. 53Theorem 8.2unisn 3587  unisng 3588
[Quine] p. 53Theorem 8.3uniun 3590
[Quine] p. 54Theorem 8.6elssuni 3599
[Quine] p. 54Theorem 8.7uni0 3598
[Quine] p. 56Theorem 8.17uniabio 4820
[Quine] p. 56Definition 8.18dfiota2 4811
[Quine] p. 57Theorem 8.19iotaval 4821
[Quine] p. 57Theorem 8.22iotanul 4825
[Quine] p. 58Theorem 8.23euiotaex 4826
[Quine] p. 58Definition 9.1df-op 3376
[Quine] p. 61Theorem 9.5opabid 3985  opelopab 3999  opelopaba 3994  opelopabaf 4001  opelopabf 4002  opelopabg 3996  opelopabga 3991  oprabid 5480
[Quine] p. 64Definition 9.11df-xp 4294
[Quine] p. 64Definition 9.12df-cnv 4296
[Quine] p. 64Definition 9.15df-id 4021
[Quine] p. 65Theorem 10.3fun0 4900
[Quine] p. 65Theorem 10.4funi 4875
[Quine] p. 65Theorem 10.5funsn 4891  funsng 4889
[Quine] p. 65Definition 10.1df-fun 4847
[Quine] p. 65Definition 10.2args 4637  dffv4g 5118
[Quine] p. 68Definition 10.11df-fv 4853  fv2 5116
[Quine] p. 284Axiom 39(vi)funimaex 4927  funimaexg 4926
[Sanford] p. 39Rule 3mtp-xor 1313
[Sanford] p. 39Rule 4mpto2 1312
[Sanford] p. 40Rule 1mpto1 1311
[Schechter] p. 51Definition of antisymmetryintasym 4652
[Schechter] p. 51Definition of irreflexivityintirr 4654
[Schechter] p. 51Definition of symmetrycnvsym 4651
[Schechter] p. 51Definition of transitivitycotr 4649
[Stoll] p. 13Definition of symmetric differencesymdif1 3196
[Stoll] p. 16Exercise 4.40dif 3289  dif0 3288
[Stoll] p. 16Exercise 4.8difdifdirss 3301
[Stoll] p. 19Theorem 5.2(13)undm 3189
[Stoll] p. 19Theorem 5.2(13')indmss 3190
[Stoll] p. 20Remarkinvdif 3173
[Stoll] p. 25Definition of ordered tripledf-ot 3377
[Stoll] p. 43Definitionuniiun 3701
[Stoll] p. 44Definitionintiin 3702
[Stoll] p. 45Definitiondf-iin 3651
[Stoll] p. 45Definition indexed uniondf-iun 3650
[Stoll] p. 176Theorem 3.4(27)imandc 785
[Stoll] p. 262Example 4.1symdif1 3196
[Suppes] p. 22Theorem 2eq0 3233
[Suppes] p. 22Theorem 4eqss 2954  eqssd 2956  eqssi 2955
[Suppes] p. 23Theorem 5ss0 3251  ss0b 3250
[Suppes] p. 23Theorem 6sstr 2947
[Suppes] p. 23Theorem 7pssirr 3038
[Suppes] p. 23Theorem 8pssn2lp 3039
[Suppes] p. 23Theorem 9psstr 3043
[Suppes] p. 23Theorem 10pssss 3033
[Suppes] p. 25Theorem 12elin 3120  elun 3078
[Suppes] p. 26Theorem 15inidm 3140
[Suppes] p. 26Theorem 16in0 3246
[Suppes] p. 27Theorem 23unidm 3080
[Suppes] p. 27Theorem 24un0 3245
[Suppes] p. 27Theorem 25ssun1 3100
[Suppes] p. 27Theorem 26ssequn1 3107
[Suppes] p. 27Theorem 27unss 3111
[Suppes] p. 27Theorem 28indir 3180
[Suppes] p. 27Theorem 29undir 3181
[Suppes] p. 28Theorem 32difid 3286  difidALT 3287
[Suppes] p. 29Theorem 33difin 3168
[Suppes] p. 29Theorem 34indif 3174
[Suppes] p. 29Theorem 35undif1ss 3292
[Suppes] p. 29Theorem 36difun2 3296
[Suppes] p. 29Theorem 37difin0 3291
[Suppes] p. 29Theorem 38disjdif 3290
[Suppes] p. 29Theorem 39difundi 3183
[Suppes] p. 29Theorem 40difindiss 3185
[Suppes] p. 30Theorem 41nalset 3878
[Suppes] p. 39Theorem 61uniss 3592
[Suppes] p. 39Theorem 65uniop 3983
[Suppes] p. 41Theorem 70intsn 3641
[Suppes] p. 42Theorem 71intpr 3638  intprg 3639
[Suppes] p. 42Theorem 73op1stb 4175  op1stbg 4176
[Suppes] p. 42Theorem 78intun 3637
[Suppes] p. 44Definition 15(a)dfiun2 3682  dfiun2g 3680
[Suppes] p. 44Definition 15(b)dfiin2 3683
[Suppes] p. 47Theorem 86elpw 3357  elpw2 3902  elpw2g 3901  elpwg 3359
[Suppes] p. 47Theorem 87pwid 3365
[Suppes] p. 47Theorem 89pw0 3502
[Suppes] p. 48Theorem 90pwpw0ss 3566
[Suppes] p. 52Theorem 101xpss12 4388
[Suppes] p. 52Theorem 102xpindi 4414  xpindir 4415
[Suppes] p. 52Theorem 103xpundi 4339  xpundir 4340
[Suppes] p. 54Theorem 105elirrv 4226
[Suppes] p. 58Theorem 2relss 4370
[Suppes] p. 59Theorem 4eldm 4475  eldm2 4476  eldm2g 4474  eldmg 4473
[Suppes] p. 59Definition 3df-dm 4298
[Suppes] p. 60Theorem 6dmin 4486
[Suppes] p. 60Theorem 8rnun 4675
[Suppes] p. 60Theorem 9rnin 4676
[Suppes] p. 60Definition 4dfrn2 4466
[Suppes] p. 61Theorem 11brcnv 4461  brcnvg 4459
[Suppes] p. 62Equation 5elcnv 4455  elcnv2 4456
[Suppes] p. 62Theorem 12relcnv 4646
[Suppes] p. 62Theorem 15cnvin 4674
[Suppes] p. 62Theorem 16cnvun 4672
[Suppes] p. 63Theorem 20co02 4777
[Suppes] p. 63Theorem 21dmcoss 4544
[Suppes] p. 63Definition 7df-co 4297
[Suppes] p. 64Theorem 26cnvco 4463
[Suppes] p. 64Theorem 27coass 4782
[Suppes] p. 65Theorem 31resundi 4568
[Suppes] p. 65Theorem 34elima 4616  elima2 4617  elima3 4618  elimag 4615
[Suppes] p. 65Theorem 35imaundi 4679
[Suppes] p. 66Theorem 40dminss 4681
[Suppes] p. 66Theorem 41imainss 4682
[Suppes] p. 67Exercise 11cnvxp 4685
[Suppes] p. 81Definition 34dfec2 6045
[Suppes] p. 82Theorem 72elec 6081  elecg 6080
[Suppes] p. 82Theorem 73erth 6086  erth2 6087
[Suppes] p. 92Theorem 1enref 6181  enrefg 6180
[Suppes] p. 92Theorem 2ensym 6197  ensymb 6196  ensymi 6198
[Suppes] p. 92Theorem 3entr 6200
[Suppes] p. 92Theorem 4unen 6229
[Suppes] p. 94Theorem 15endom 6179
[Suppes] p. 94Theorem 16ssdomg 6194
[Suppes] p. 94Theorem 17domtr 6201
[Suppes] p. 98Exercise 4fundmen 6222  fundmeng 6223
[Suppes] p. 98Exercise 6xpdom3m 6244
[Suppes] p. 130Definition 3df-tr 3846
[Suppes] p. 132Theorem 9ssonuni 4180
[Suppes] p. 134Definition 6df-suc 4074
[Suppes] p. 136Theorem Schema 22findes 4269  finds 4266  finds1 4268  finds2 4267
[Suppes] p. 162Definition 5df-ltnqqs 6337  df-ltpq 6330
[Suppes] p. 228Theorem Schema 61onintss 4093
[TakeutiZaring] p. 8Axiom 1ax-ext 2019
[TakeutiZaring] p. 13Definition 4.5df-cleq 2030
[TakeutiZaring] p. 13Proposition 4.6df-clel 2033
[TakeutiZaring] p. 13Proposition 4.9cvjust 2032
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2054
[TakeutiZaring] p. 14Definition 4.16df-oprab 5459
[TakeutiZaring] p. 14Proposition 4.14ru 2757
[TakeutiZaring] p. 15Exercise 1elpr 3385  elpr2 3386  elprg 3384
[TakeutiZaring] p. 15Exercise 2elsn 3382  elsnc 3390  elsnc2 3397  elsnc2g 3396  elsncg 3389
[TakeutiZaring] p. 15Exercise 3elop 3959
[TakeutiZaring] p. 15Exercise 4sneq 3378  sneqr 3522
[TakeutiZaring] p. 15Definition 5.1dfpr2 3383  dfsn2 3381
[TakeutiZaring] p. 16Axiom 3uniex 4140
[TakeutiZaring] p. 16Exercise 6opth 3965
[TakeutiZaring] p. 16Exercise 8rext 3942
[TakeutiZaring] p. 16Corollary 5.8unex 4142  unexg 4144
[TakeutiZaring] p. 16Definition 5.3dftp2 3410
[TakeutiZaring] p. 16Definition 5.5df-uni 3572
[TakeutiZaring] p. 16Definition 5.6df-in 2918  df-un 2916
[TakeutiZaring] p. 16Proposition 5.7unipr 3585  uniprg 3586
[TakeutiZaring] p. 17Axiom 4pwex 3923  pwexg 3924
[TakeutiZaring] p. 17Exercise 1eltp 3409
[TakeutiZaring] p. 17Exercise 5elsuc 4109  elsucg 4107  sstr2 2946
[TakeutiZaring] p. 17Exercise 6uncom 3081
[TakeutiZaring] p. 17Exercise 7incom 3123
[TakeutiZaring] p. 17Exercise 8unass 3094
[TakeutiZaring] p. 17Exercise 9inass 3141
[TakeutiZaring] p. 17Exercise 10indi 3178
[TakeutiZaring] p. 17Exercise 11undi 3179
[TakeutiZaring] p. 17Definition 5.9df-pss 2927  dfss2 2928
[TakeutiZaring] p. 17Definition 5.10df-pw 3353
[TakeutiZaring] p. 18Exercise 7unss2 3108
[TakeutiZaring] p. 18Exercise 9df-ss 2925  sseqin2 3150
[TakeutiZaring] p. 18Exercise 10ssid 2958
[TakeutiZaring] p. 18Exercise 12inss1 3151  inss2 3152
[TakeutiZaring] p. 18Exercise 13nssr 2997
[TakeutiZaring] p. 18Exercise 15unieq 3580
[TakeutiZaring] p. 18Exercise 18sspwb 3943
[TakeutiZaring] p. 18Exercise 19pweqb 3950
[TakeutiZaring] p. 20Definitiondf-rab 2309
[TakeutiZaring] p. 20Corollary 5.160ex 3875
[TakeutiZaring] p. 20Definition 5.12df-dif 2914
[TakeutiZaring] p. 20Definition 5.14dfnul2 3220
[TakeutiZaring] p. 20Proposition 5.15difid 3286  difidALT 3287
[TakeutiZaring] p. 20Proposition 5.17(1)n0rf 3227
[TakeutiZaring] p. 21Theorem 5.22setind 4222
[TakeutiZaring] p. 21Definition 5.20df-v 2553
[TakeutiZaring] p. 21Proposition 5.21vprc 3879
[TakeutiZaring] p. 22Exercise 10ss 3249
[TakeutiZaring] p. 22Exercise 3ssex 3885  ssexg 3887
[TakeutiZaring] p. 22Exercise 4inex1 3882
[TakeutiZaring] p. 22Exercise 5ruv 4228
[TakeutiZaring] p. 22Exercise 6elirr 4224
[TakeutiZaring] p. 22Exercise 7ssdif0im 3280
[TakeutiZaring] p. 22Exercise 11difdif 3063
[TakeutiZaring] p. 22Exercise 13undif3ss 3192
[TakeutiZaring] p. 22Exercise 14difss 3064
[TakeutiZaring] p. 22Exercise 15sscon 3071
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2305
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2306
[TakeutiZaring] p. 23Proposition 6.2xpex 4396  xpexg 4395  xpexgALT 5702
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4295
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 4906
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5043  fun11 4909
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 4856  svrelfun 4907
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4465
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4467
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4300
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4301
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4297
[TakeutiZaring] p. 25Exercise 2cnvcnvss 4718  dfrel2 4714
[TakeutiZaring] p. 25Exercise 3xpss 4389
[TakeutiZaring] p. 25Exercise 5relun 4397
[TakeutiZaring] p. 25Exercise 6reluni 4403
[TakeutiZaring] p. 25Exercise 9inxp 4413
[TakeutiZaring] p. 25Exercise 12relres 4582
[TakeutiZaring] p. 25Exercise 13opelres 4560  opelresg 4562
[TakeutiZaring] p. 25Exercise 14dmres 4575
[TakeutiZaring] p. 25Exercise 15resss 4578
[TakeutiZaring] p. 25Exercise 17resabs1 4583
[TakeutiZaring] p. 25Exercise 18funres 4884
[TakeutiZaring] p. 25Exercise 24relco 4762
[TakeutiZaring] p. 25Exercise 29funco 4883
[TakeutiZaring] p. 25Exercise 30f1co 5044
[TakeutiZaring] p. 26Definition 6.10eu2 1941
[TakeutiZaring] p. 26Definition 6.11df-fv 4853  fv3 5140
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 4799  cnvexg 4798
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4541  dmexg 4539
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4542  rnexg 4540
[TakeutiZaring] p. 27Corollary 6.13funfvex 5135
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5143  tz6.12 5144  tz6.12c 5146
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5112
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4848
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4849
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4851  wfo 4843
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4850  wf1 4842
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4852  wf1o 4844
[TakeutiZaring] p. 28Exercise 4eqfnfv 5208  eqfnfv2 5209  eqfnfv2f 5212
[TakeutiZaring] p. 28Exercise 5fvco 5186
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5326  fnexALT 5682
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5325  resfunexgALT 5679
[TakeutiZaring] p. 29Exercise 9funimaex 4927  funimaexg 4926
[TakeutiZaring] p. 29Definition 6.18df-br 3756
[TakeutiZaring] p. 30Definition 6.21eliniseg 4638  iniseg 4640
[TakeutiZaring] p. 30Definition 6.22df-eprel 4017
[TakeutiZaring] p. 32Definition 6.28df-isom 4854
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5393
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5394
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5399
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5400
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5408
[TakeutiZaring] p. 35Notationwtr 3845
[TakeutiZaring] p. 35Definition 7.1dftr3 3849
[TakeutiZaring] p. 36Proposition 7.6ordelord 4084
[TakeutiZaring] p. 37Proposition 7.9ordin 4088
[TakeutiZaring] p. 38Corollary 7.15ordsson 4184
[TakeutiZaring] p. 38Definition 7.11df-on 4071
[TakeutiZaring] p. 38Proposition 7.12ordon 4178
[TakeutiZaring] p. 38Proposition 7.13onprc 4230
[TakeutiZaring] p. 39Theorem 7.17tfi 4248
[TakeutiZaring] p. 40Exercise 7dftr2 3847
[TakeutiZaring] p. 40Exercise 11unon 4202
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4179
[TakeutiZaring] p. 40Proposition 7.20elssuni 3599
[TakeutiZaring] p. 41Definition 7.22df-suc 4074
[TakeutiZaring] p. 41Proposition 7.23sssucid 4118  sucidg 4119
[TakeutiZaring] p. 41Proposition 7.24suceloni 4193
[TakeutiZaring] p. 42Exercise 1df-ilim 4072
[TakeutiZaring] p. 42Exercise 8ordelsuc 4197
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4260
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4261
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4262
[TakeutiZaring] p. 43Axiom 7omex 4259
[TakeutiZaring] p. 43Theorem 7.32ordom 4272
[TakeutiZaring] p. 43Corollary 7.31find 4265
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4263
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4264
[TakeutiZaring] p. 44Exercise 2int0 3620  trint0m 3862
[TakeutiZaring] p. 44Exercise 4intss1 3621
[TakeutiZaring] p. 44Definition 7.35df-int 3607
[TakeutiZaring] p. 47Lemma 1tfrlem1 5864
[TakeutiZaring] p. 47Theorem 7.41(1)tfri1 5892  tfri1d 5890
[TakeutiZaring] p. 47Theorem 7.41(2)tfri2 5893  tfri2d 5891
[TakeutiZaring] p. 47Theorem 7.41(3)tfri3 5894
[TakeutiZaring] p. 50Exercise 3smoiso 5858
[TakeutiZaring] p. 50Definition 7.46df-smo 5842
[TakeutiZaring] p. 56Definition 8.1oasuc 5983
[TakeutiZaring] p. 57Proposition 8.2oacl 5979
[TakeutiZaring] p. 57Proposition 8.3oa0 5976
[TakeutiZaring] p. 57Proposition 8.16omcl 5980
[TakeutiZaring] p. 58Proposition 8.4nnaord 6018  nnaordi 6017
[TakeutiZaring] p. 59Proposition 8.6iunss2 3693  uniss2 3602
[TakeutiZaring] p. 59Proposition 8.9nnacl 5998
[TakeutiZaring] p. 62Exercise 5oaword1 5989
[TakeutiZaring] p. 62Definition 8.15om0 5977  omsuc 5990
[TakeutiZaring] p. 63Proposition 8.17nnmcl 5999
[TakeutiZaring] p. 63Proposition 8.19nnmord 6026  nnmordi 6025
[TakeutiZaring] p. 67Definition 8.30oei0 5978
[TakeutiZaring] p. 88Exercise 1en0 6211
[TakeutiZaring] p. 91Definition 10.29df-fin 6160  isfi 6177
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6241
[Tarski] p. 67Axiom B5ax-4 1397
[Tarski] p. 68Lemma 6equid 1586
[Tarski] p. 69Lemma 7equcomi 1589
[Tarski] p. 70Lemma 14spim 1623  spime 1626  spimeh 1624  spimh 1622
[Tarski] p. 70Lemma 16ax-11 1394  ax-11o 1701  ax11i 1599
[Tarski] p. 70Lemmas 16 and 17sb6 1763
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1416
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1401  ax-14 1402
[WhiteheadRussell] p. 96Axiom *1.3olc 631
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 645
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 672
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 681
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 702
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 546
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 571
[WhiteheadRussell] p. 100Theorem *2.04pm2.04 76
[WhiteheadRussell] p. 100Theorem *2.05imim2 49
[WhiteheadRussell] p. 100Theorem *2.06imim1 70
[WhiteheadRussell] p. 101Theorem *2.1pm2.1dc 744
[WhiteheadRussell] p. 101Theorem *2.06barbara 1995  syl 14
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 655
[WhiteheadRussell] p. 101Theorem *2.08id 19  idALT 20
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 743
[WhiteheadRussell] p. 101Theorem *2.12notnot1 559
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 778
[WhiteheadRussell] p. 102Theorem *2.14notnot2dc 750
[WhiteheadRussell] p. 102Theorem *2.15con1dc 752
[WhiteheadRussell] p. 103Theorem *2.16con3 570
[WhiteheadRussell] p. 103Theorem *2.17condc 748
[WhiteheadRussell] p. 103Theorem *2.18pm2.18dc 749
[WhiteheadRussell] p. 104Theorem *2.2orc 632
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 691
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 547
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 551
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 791
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 812
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 35
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 684
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 685
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 716
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 717
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 715
[WhiteheadRussell] p. 105Definition *2.33df-3or 885
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 694
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 692
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 693
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 47
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 656
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 657
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 762
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 758
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 658
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 659
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 660
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 580
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 581
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 640
[WhiteheadRussell] p. 107Theorem *2.54pm2.54dc 789
[WhiteheadRussell] p. 107Theorem *2.55orel1 643
[WhiteheadRussell] p. 107Theorem *2.56orel2 644
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 761
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 666
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 712
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 713
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 584
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 633  pm2.67 661
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 763
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 665
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 722
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 792
[WhiteheadRussell] p. 108Theorem *2.69looinvdc 820
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 718
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 719
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 721
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 720
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 723
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 724
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 71
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 810
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 94
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 670
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 126
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 863
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 864
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 865
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 669
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 251
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 252
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 626
[WhiteheadRussell] p. 112Theorem *3.35pm3.35 329
[WhiteheadRussell] p. 112Theorem *3.3 (Exp)pm3.3 248
[WhiteheadRussell] p. 112Theorem *3.31 (Imp)pm3.31 249
[WhiteheadRussell] p. 112Theorem *3.26 (Simp)simpl 102  simplimdc 756
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 103  simprimdc 755
[WhiteheadRussell] p. 112Theorem *3.33 (Syll)pm3.33 327
[WhiteheadRussell] p. 112Theorem *3.34 (Syll)pm3.34 328
[WhiteheadRussell] p. 112Theorem *3.37 (Transp)pm3.37dc 787
[WhiteheadRussell] p. 113Fact)pm3.45 529
[WhiteheadRussell] p. 113Theorem *3.4pm3.4 316
[WhiteheadRussell] p. 113Theorem *3.41pm3.41 314
[WhiteheadRussell] p. 113Theorem *3.42pm3.42 315
[WhiteheadRussell] p. 113Theorem *3.44jao 671  pm3.44 634
[WhiteheadRussell] p. 113Theorem *3.47prth 326
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 534
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 698
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 764
[WhiteheadRussell] p. 117Theorem *4.2biid 160
[WhiteheadRussell] p. 117Theorem *4.13notnotdc 765
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 786
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 788
[WhiteheadRussell] p. 117Theorem *4.21bicom 128
[WhiteheadRussell] p. 117Theorem *4.22biantr 858  bitr 441
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 375
[WhiteheadRussell] p. 117Theorem *4.25oridm 673  pm4.25 674
[WhiteheadRussell] p. 118Theorem *4.3ancom 253
[WhiteheadRussell] p. 118Theorem *4.4andi 730
[WhiteheadRussell] p. 118Theorem *4.31orcom 646
[WhiteheadRussell] p. 118Theorem *4.32anass 381
[WhiteheadRussell] p. 118Theorem *4.33orass 683
[WhiteheadRussell] p. 118Theorem *4.36anbi1 439
[WhiteheadRussell] p. 118Theorem *4.37orbi1 705
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 537
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 734
[WhiteheadRussell] p. 118Definition *4.34df-3an 886
[WhiteheadRussell] p. 119Theorem *4.41ordi 728
[WhiteheadRussell] p. 119Theorem *4.42pm4.42r 877
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 855
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 695
[WhiteheadRussell] p. 119Theorem *4.45orabs 726  pm4.45 697  pm4.45im 317
[WhiteheadRussell] p. 119Theorem *10.2219.26 1367
[WhiteheadRussell] p. 120Theorem *4.5anordc 862
[WhiteheadRussell] p. 120Theorem *4.6imordc 795  imorr 796
[WhiteheadRussell] p. 120Theorem *4.7anclb 302
[WhiteheadRussell] p. 120Theorem *4.51ianordc 798
[WhiteheadRussell] p. 120Theorem *4.52pm4.52im 802
[WhiteheadRussell] p. 120Theorem *4.53pm4.53r 803
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 804
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 845
[WhiteheadRussell] p. 120Theorem *4.56ioran 668  pm4.56 805
[WhiteheadRussell] p. 120Theorem *4.57oranim 806
[WhiteheadRussell] p. 120Theorem *4.61annimim 781
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 797
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 779
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 800
[WhiteheadRussell] p. 120Theorem *4.65pm4.65r 782
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 801
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 780
[WhiteheadRussell] p. 120Theorem *4.71pm4.71 369  pm4.71d 373  pm4.71i 371  pm4.71r 370  pm4.71rd 374  pm4.71ri 372
[WhiteheadRussell] p. 121Theorem *4.72pm4.72 735
[WhiteheadRussell] p. 121Theorem *4.73iba 284
[WhiteheadRussell] p. 121Theorem *4.74biorf 662
[WhiteheadRussell] p. 121Theorem *4.76jcab 535  pm4.76 536
[WhiteheadRussell] p. 121Theorem *4.77jaob 630  pm4.77 711
[WhiteheadRussell] p. 121Theorem *4.78pm4.78i 807
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 808
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 622
[WhiteheadRussell] p. 122Theorem *4.81pm4.81dc 813
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 856
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 857
[WhiteheadRussell] p. 122Theorem *4.84imbi1 225
[WhiteheadRussell] p. 122Theorem *4.85imbi2 226
[WhiteheadRussell] p. 122Theorem *4.86bibi1 229
[WhiteheadRussell] p. 122Theorem *4.87bi2.04 237  impexp 250  pm4.87 493
[WhiteheadRussell] p. 123Theorem *5.1pm5.1 533
[WhiteheadRussell] p. 123Theorem *5.11pm5.11dc 814
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 815
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 817
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 816
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1277
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 736
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 809
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1282  pm5.18dc 776
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 621
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 610
[WhiteheadRussell] p. 124Theorem *5.22xordc 1280
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1285
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1286
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 793
[WhiteheadRussell] p. 125Theorem *5.3pm5.3 444
[WhiteheadRussell] p. 125Theorem *5.4pm5.4 238
[WhiteheadRussell] p. 125Theorem *5.5pm5.5 231
[WhiteheadRussell] p. 125Theorem *5.6pm5.6dc 834  pm5.6r 835
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 860
[WhiteheadRussell] p. 125Theorem *5.31pm5.31 330
[WhiteheadRussell] p. 125Theorem *5.32pm5.32 426
[WhiteheadRussell] p. 125Theorem *5.33pm5.33 541
[WhiteheadRussell] p. 125Theorem *5.35pm5.35 825
[WhiteheadRussell] p. 125Theorem *5.36pm5.36 542
[WhiteheadRussell] p. 125Theorem *5.41imdi 239  pm5.41 240
[WhiteheadRussell] p. 125Theorem *5.42pm5.42 303
[WhiteheadRussell] p. 125Theorem *5.44pm5.44 833
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 714
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 826
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 818
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 707
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 851
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 852
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 867
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 233
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 168
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 868
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1523
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1371
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1520
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1772
[WhiteheadRussell] p. 175Definition *14.02df-eu 1900
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2280
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2281
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2675
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2809
[WhiteheadRussell] p. 190Theorem *14.22iota4 4828
[WhiteheadRussell] p. 191Theorem *14.23iota4an 4829
[WhiteheadRussell] p. 192Theorem *14.26eupick 1976  eupickbi 1979
[WhiteheadRussell] p. 235Definition *30.01df-fv 4853

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