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 9139
[Apostol] p. 18Theorem I.1addcan 7147  addcan2d 7152  addcan2i 7150  addcand 7151  addcani 7149
[Apostol] p. 18Theorem I.2negeu 7158
[Apostol] p. 18Theorem I.3negsub 7214  negsubd 7283  negsubi 7244
[Apostol] p. 18Theorem I.4negneg 7216  negnegd 7268  negnegi 7236
[Apostol] p. 18Theorem I.5subdi 7337  subdid 7366  subdii 7359  subdir 7338  subdird 7367  subdiri 7360
[Apostol] p. 18Theorem I.6mul01 7341  mul01d 7345  mul01i 7343  mul02 7339  mul02d 7344  mul02i 7342
[Apostol] p. 18Theorem I.9divrecapd 7720
[Apostol] p. 18Theorem I.10recrecapi 7672
[Apostol] p. 18Theorem I.12mul2neg 7350  mul2negd 7365  mul2negi 7358  mulneg1 7347  mulneg1d 7363  mulneg1i 7356
[Apostol] p. 18Theorem I.15divdivdivap 7641
[Apostol] p. 20Axiom 7rpaddcl 8553  rpaddcld 8585  rpmulcl 8554  rpmulcld 8586
[Apostol] p. 20Axiom 90nrp 8563
[Apostol] p. 20Theorem I.17lttri 7078
[Apostol] p. 20Theorem I.18ltadd1d 7483  ltadd1dd 7501  ltadd1i 7448
[Apostol] p. 20Theorem I.19ltmul1 7535  ltmul1a 7534  ltmul1i 7838  ltmul1ii 7846  ltmul2 7774  ltmul2d 8608  ltmul2dd 8622  ltmul2i 7841
[Apostol] p. 20Theorem I.210lt1 7097
[Apostol] p. 20Theorem I.23lt0neg1 7417  lt0neg1d 7461  ltneg 7411  ltnegd 7468  ltnegi 7439
[Apostol] p. 20Theorem I.25lt2add 7394  lt2addd 7512  lt2addi 7456
[Apostol] p. 20Definition of positive numbersdf-rp 8531
[Apostol] p. 21Exercise 4recgt0 7768  recgt0d 7852  recgt0i 7824  recgt0ii 7825
[Apostol] p. 22Definition of integersdf-z 8194
[Apostol] p. 22Definition of rationalsdf-q 8503
[Apostol] p. 26Theorem I.29arch 8126
[Apostol] p. 28Exercise 2btwnz 8305
[Apostol] p. 28Exercise 3nnrecl 8127
[Apostol] p. 28Exercise 10(a)zneo 8287
[Apostol] p. 29Theorem I.35resqrtth 9483  sqrtthi 9569
[Apostol] p. 34Theorem I.36 (principle of mathematical induction)peano5nni 7869
[Apostol] p. 363Remarkabsgt0api 9596
[Apostol] p. 363Exampleabssubd 9643  abssubi 9600
[Bauer] p. 482Section 1.2pm2.01 546  pm2.65 585
[Bauer] p. 483Theorem 1.3acexmid 5474  onsucelsucexmidlem 4226
[Bauer], p. 483Definitionn0rf 3230
[Bauer], p. 485Theorem 2.1ssfiexmid 6299
[BauerTaylor], p. 32Lemma 6.16prarloclem 6556
[BauerTaylor], p. 50Lemma 11.4subhalfnqq 6469
[BauerTaylor], p. 52Proposition 11.15prarloc 6558
[BauerTaylor], p. 53Lemma 11.16addclpr 6592  addlocpr 6591
[BauerTaylor], p. 55Proposition 12.7appdivnq 6618
[BauerTaylor], p. 56Lemma 12.8prmuloc 6621
[BauerTaylor], p. 56Lemma 12.9mullocpr 6626
[BellMachover] p. 36Lemma 10.3idALT 20
[BellMachover] p. 97Definition 10.1df-eu 1903
[BellMachover] p. 460Notationdf-mo 1904
[BellMachover] p. 460Definitionmo3 1954  mo3h 1953
[BellMachover] p. 462Theorem 1.1bm1.1 2025
[BellMachover] p. 463Theorem 1.3iibm1.3ii 3875
[BellMachover] p. 466Axiom Powaxpow3 3927
[BellMachover] p. 466Axiom Unionaxun2 4144
[BellMachover] p. 469Theorem 2.2(i)ordirr 4237
[BellMachover] p. 469Theorem 2.2(iii)onelon 4093
[BellMachover] p. 469Theorem 2.2(vii)ordn2lp 4239
[BellMachover] p. 471Problem 2.5(ii)bm2.5ii 4194
[BellMachover] p. 471Definition of Limdf-ilim 4078
[BellMachover] p. 472Axiom Infzfinf2 4275
[BellMachover] p. 473Theorem 2.8limom 4299
[Bobzien] p. 116Statement T3stoic3 1320
[Bobzien] p. 117Statement T2stoic2a 1318
[Bobzien] p. 117Statement T4stoic4a 1321
[BourbakiEns] p. Proposition 8fcof1 5386  fcofo 5387
[BourbakiTop1] p. Remarkxnegmnf 8685  xnegpnf 8684
[BourbakiTop1] p. Remark rexneg 8686
[ChoquetDD] p. 2Definition of mappingdf-mpt 3817
[Crosilla] p. Axiom 1ax-ext 2022
[Crosilla] p. Axiom 2ax-pr 3941
[Crosilla] p. Axiom 3ax-un 4142
[Crosilla] p. Axiom 4ax-nul 3880
[Crosilla] p. Axiom 5ax-iinf 4274
[Crosilla] p. Axiom 6ru 2760
[Crosilla] p. Axiom 8ax-pow 3924
[Crosilla] p. Axiom 9ax-setind 4232
[Crosilla], p. Axiom 6ax-sep 3872
[Crosilla], p. Axiom 7ax-coll 3869
[Crosilla], p. Axiom 7'repizf 3870
[Crosilla], p. Theorem is statedordtriexmid 4219
[Crosilla], p. Axiom of choice implies instancesacexmid 5474
[Crosilla], p. Definition of ordinaldf-iord 4075
[Crosilla], p. Theorem "Foundation implies instances of EM"regexmid 4231
[Eisenberg] p. 67Definition 5.3df-dif 2917
[Eisenberg] p. 82Definition 6.3df-iom 4277
[Enderton] p. 18Axiom of Empty Setaxnul 3879
[Enderton] p. 19Definitiondf-tp 3380
[Enderton] p. 26Exercise 5unissb 3607
[Enderton] p. 26Exercise 10pwel 3951
[Enderton] p. 28Exercise 7(b)pwunim 4020
[Enderton] p. 30Theorem "Distributive laws"iinin1m 3723  iinin2m 3722  iunin1 3718  iunin2 3717
[Enderton] p. 31Theorem "De Morgan's laws"iindif2m 3721  iundif2ss 3719
[Enderton] p. 33Exercise 23iinuniss 3734
[Enderton] p. 33Exercise 25iununir 3735
[Enderton] p. 33Exercise 24(a)iinpw 3739
[Enderton] p. 33Exercise 24(b)iunpw 4183  iunpwss 3740
[Enderton] p. 38Exercise 6(a)unipw 3950
[Enderton] p. 38Exercise 6(b)pwuni 3940
[Enderton] p. 41Lemma 3Dopeluu 4154  rnex 4562  rnexg 4560
[Enderton] p. 41Exercise 8dmuni 4508  rnuni 4698
[Enderton] p. 42Definition of a functiondffun7 4891  dffun8 4892
[Enderton] p. 43Definition of function valuefunfvdm2 5200
[Enderton] p. 43Definition of single-rootedfuncnv 4923
[Enderton] p. 44Definition (d)dfima2 4633  dfima3 4634
[Enderton] p. 47Theorem 3Hfvco2 5205
[Enderton] p. 50Theorem 3K(a)imauni 5363
[Enderton] p. 53Exercise 21coass 4802
[Enderton] p. 53Exercise 27dmco 4792
[Enderton] p. 53Exercise 14(a)funin 4933
[Enderton] p. 53Exercise 22(a)imass2 4664
[Enderton] p. 56Theorem 3Merref 6089
[Enderton] p. 57Lemma 3Nerthi 6115
[Enderton] p. 57Definitiondf-ec 6071
[Enderton] p. 58Definitiondf-qs 6075
[Enderton] p. 60Theorem 3Qth3q 6174  th3qcor 6173  th3qlem1 6171  th3qlem2 6172
[Enderton] p. 61Exercise 35df-ec 6071
[Enderton] p. 65Exercise 56(a)dmun 4505
[Enderton] p. 68Definition of successordf-suc 4080
[Enderton] p. 71Definitiondf-tr 3852  dftr4 3856
[Enderton] p. 72Theorem 4Eunisuc 4122  unisucg 4123
[Enderton] p. 73Exercise 6unisuc 4122  unisucg 4123
[Enderton] p. 73Exercise 5(a)truni 3865
[Enderton] p. 73Exercise 5(b)trint 3866
[Enderton] p. 79Theorem 4I(A1)nna0 6016
[Enderton] p. 79Theorem 4I(A2)nnasuc 6018  onasuc 6009
[Enderton] p. 79Definition of operation valuedf-ov 5478
[Enderton] p. 80Theorem 4J(A1)nnm0 6017
[Enderton] p. 80Theorem 4J(A2)nnmsuc 6019  onmsuc 6015
[Enderton] p. 81Theorem 4K(1)nnaass 6027
[Enderton] p. 81Theorem 4K(2)nna0r 6020  nnacom 6026
[Enderton] p. 81Theorem 4K(3)nndi 6028
[Enderton] p. 81Theorem 4K(4)nnmass 6029
[Enderton] p. 81Theorem 4K(5)nnmcom 6031
[Enderton] p. 82Exercise 16nnm0r 6021  nnmsucr 6030
[Enderton] p. 88Exercise 23nnaordex 6063
[Enderton] p. 129Definitiondf-en 6185
[Enderton] p. 134Theorem (Pigeonhole Principle)phpm 6290
[Enderton] p. 136Corollary 6Enneneq 6283
[Enderton] p. 144Corollary 6Kundif2ss 3296
[Enderton] p. 145Figure 38ffoss 5121
[Enderton] p. 145Definitiondf-dom 6186
[Enderton] p. 146Example 1domen 6195  domeng 6196
[Enderton] p. 146Example 3nndomo 6289
[Enderton] p. 149Theorem 6L(c)xpdom1 6272  xpdom1g 6270  xpdom2g 6269
[Enderton] p. 168Definitiondf-po 4030
[Enderton] p. 192Theorem 7M(a)oneli 4137
[Enderton] p. 192Theorem 7M(b)ontr1 4098
[Enderton] p. 193Corollary 7N(b)0elon 4101
[Enderton] p. 193Corollary 7N(c)onsuci 4214
[Enderton] p. 193Corollary 7N(d)ssonunii 4187
[Enderton] p. 194Remarkonprc 4246
[Enderton] p. 194Exercise 16suc11 4252
[Enderton] p. 197Definitiondf-card 6317
[Enderton] p. 200Exercise 25tfis 4269
[Enderton] p. 206Theorem 7X(b)en2lp 4248
[Enderton] p. 207Exercise 34opthreg 4250
[Enderton] p. 208Exercise 35suc11g 4251
[Geuvers], p. 6Lemma 2.13mulap0r 7558
[Geuvers], p. 6Lemma 2.15mulap0 7587
[Geuvers], p. 9Lemma 2.35msqge0 7559
[Geuvers], p. 9Definition 3.1(2)ax-arch 6960
[Geuvers], p. 17Definition 6.1df-ap 7525
[Gleason] p. 117Proposition 9-2.1df-enq 6402  enqer 6413
[Gleason] p. 117Proposition 9-2.2df-1nqqs 6406  df-nqqs 6403
[Gleason] p. 117Proposition 9-2.3df-plpq 6399  df-plqqs 6404
[Gleason] p. 119Proposition 9-2.4df-mpq 6400  df-mqqs 6405
[Gleason] p. 119Proposition 9-2.5df-rq 6407
[Gleason] p. 119Proposition 9-2.6ltexnqq 6463
[Gleason] p. 120Proposition 9-2.6(i)halfnq 6466  ltbtwnnq 6471  ltbtwnnqq 6470
[Gleason] p. 120Proposition 9-2.6(ii)ltanqg 6455
[Gleason] p. 120Proposition 9-2.6(iii)ltmnqg 6456
[Gleason] p. 123Proposition 9-3.5addclpr 6592
[Gleason] p. 123Proposition 9-3.5(i)addassprg 6634
[Gleason] p. 123Proposition 9-3.5(ii)addcomprg 6633
[Gleason] p. 123Proposition 9-3.5(iii)ltaddpr 6652
[Gleason] p. 123Proposition 9-3.5(iv)ltexpri 6668
[Gleason] p. 123Proposition 9-3.5(v)ltaprg 6674  ltaprlem 6673
[Gleason] p. 123Proposition 9-3.5(vi)addcanprg 6671
[Gleason] p. 124Proposition 9-3.7mulclpr 6627
[Gleason] p. 124Theorem 9-3.7(iv)1idpr 6647
[Gleason] p. 124Proposition 9-3.7(i)mulassprg 6636
[Gleason] p. 124Proposition 9-3.7(ii)mulcomprg 6635
[Gleason] p. 124Proposition 9-3.7(iii)distrprg 6643
[Gleason] p. 124Proposition 9-3.7(v)recexpr 6693
[Gleason] p. 126Proposition 9-4.1df-enr 6768  enrer 6777
[Gleason] p. 126Proposition 9-4.2df-0r 6773  df-1r 6774  df-nr 6769
[Gleason] p. 126Proposition 9-4.3df-mr 6771  df-plr 6770  negexsr 6814  recexsrlem 6816
[Gleason] p. 127Proposition 9-4.4df-ltr 6772
[Gleason] p. 130Proposition 10-1.3creui 7864  creur 7863  cru 7545
[Gleason] p. 130Definition 10-1.1(v)ax-cnre 6952  axcnre 6912
[Gleason] p. 132Definition 10-3.1crim 9312  crimd 9431  crimi 9391  crre 9311  crred 9430  crrei 9390
[Gleason] p. 132Definition 10-3.2remim 9314  remimd 9396
[Gleason] p. 133Definition 10.36absval2 9509  absval2d 9635  absval2i 9594
[Gleason] p. 133Proposition 10-3.4(a)cjadd 9338  cjaddd 9419  cjaddi 9386
[Gleason] p. 133Proposition 10-3.4(c)cjmul 9339  cjmuld 9420  cjmuli 9387
[Gleason] p. 133Proposition 10-3.4(e)cjcj 9337  cjcjd 9397  cjcji 9369
[Gleason] p. 133Proposition 10-3.4(f)cjre 9336  cjreb 9320  cjrebd 9400  cjrebi 9372  cjred 9425  rere 9319  rereb 9317  rerebd 9399  rerebi 9371  rered 9423
[Gleason] p. 133Proposition 10-3.4(h)addcj 9345  addcjd 9411  addcji 9381
[Gleason] p. 133Proposition 10-3.7(a)absval 9453
[Gleason] p. 133Proposition 10-3.7(b)abscj 9504  abscjd 9640  abscji 9598
[Gleason] p. 133Proposition 10-3.7(c)abs00 9516  abs00d 9636  abs00i 9595  absne0d 9637
[Gleason] p. 133Proposition 10-3.7(d)releabs 9546  releabsd 9641  releabsi 9599
[Gleason] p. 133Proposition 10-3.7(f)absmul 9521  absmuld 9644  absmuli 9601
[Gleason] p. 133Proposition 10-3.7(g)sqabsadd 9507  sqabsaddi 9602
[Gleason] p. 133Proposition 10-3.7(h)abstri 9554  abstrid 9646  abstrii 9605
[Gleason] p. 134Definition 10-4.10exp0e1 9114  df-iexp 9109  exp0 9113  expp1 9116  expp1d 9236
[Gleason] p. 135Proposition 10-4.2(a)expadd 9151  expaddd 9237
[Gleason] p. 135Proposition 10-4.2(b)expmul 9154  expmuld 9238
[Gleason] p. 135Proposition 10-4.2(c)mulexp 9148  mulexpd 9250
[Gleason] p. 141Definition 11-2.1fzval 8819
[Gleason] p. 168Proposition 12-2.1(a)climadd 9699
[Gleason] p. 168Proposition 12-2.1(b)climsub 9701
[Gleason] p. 168Proposition 12-2.1(c)climmul 9700
[Gleason] p. 171Corollary 12-2.2climmulc2 9704
[Gleason] p. 172Corollary 12-2.5climrecl 9697
[Gleason] p. 172Proposition 12-2.4(c)climabs 9693  climcj 9694  climim 9696  climre 9695
[Gleason] p. 173Definition 12-3.1df-ltxr 7021  df-xr 7020  ltxr 8638
[Gleason] p. 180Theorem 12-5.3climcau 9719
[Gleason] p. 243Proposition 14-4.16addcn2 9684  mulcn2 9686  subcn2 9685
[Hamilton] p. 31Example 2.7(a)idALT 20
[Hamilton] p. 73Rule 1ax-mp 7
[Hamilton] p. 74Rule 2ax-gen 1338
[Heyting] p. 127Axiom #1ax1hfs 9747
[Hitchcock] p. 5Rule A3mptnan 1314
[Hitchcock] p. 5Rule A4mptxor 1315
[Hitchcock] p. 5Rule A5mtpxor 1317
[HoTT], p. Theorem 7.2.6nndceq 6040
[HoTT], p. Section 11.2.1df-iltp 6525  df-imp 6524  df-iplp 6523  df-reap 7518
[HoTT], p. Theorem 11.2.12cauappcvgpr 6717
[HoTT], p. Corollary 11.4.3conventions 9745
[HoTT], p. Corollary 11.2.13axcaucvg 6931  caucvgpr 6737  caucvgprpr 6767  caucvgsr 6843
[HoTT], p. Definition 11.2.1df-inp 6521
[HoTT], p. Proposition 11.2.3df-iso 4031  ltpopr 6650  ltsopr 6651
[HoTT], p. Definition 11.2.7(v)apsym 7549  reapcotr 7541  reapirr 7520
[HoTT], p. Definition 11.2.7(vi)0lt1 7097  gt0add 7516  leadd1 7379  lelttr 7062  lemul1a 7776  lenlt 7050  ltadd1 7378  ltletr 7063  ltmul1 7535  reaplt 7531
[Jech] p. 4Definition of classcv 1242  cvjust 2035
[Jech] p. 78Noteopthprc 4354
[KalishMontague] p. 81Note 1ax-i9 1423
[Kreyszig] p. 12Equation 5muleqadd 7601
[Kunen] p. 10Axiom 0a9e 1586
[Kunen] p. 12Axiom 6zfrep6 3871
[KuratowskiMostowski] p. 109Section. Eq. 14iuniin 3664
[Levy] p. 338Axiomdf-clab 2027  df-clel 2036  df-cleq 2033
[Lopez-Astorga] p. 12Rule 1mptnan 1314
[Lopez-Astorga] p. 12Rule 2mptxor 1315
[Lopez-Astorga] p. 12Rule 3mtpxor 1317
[Margaris] p. 40Rule Cexlimiv 1489
[Margaris] p. 49Axiom A1ax-1 5
[Margaris] p. 49Axiom A2ax-2 6
[Margaris] p. 49Axiom A3condc 749
[Margaris] p. 49Definitiondfbi2 368  dfordc 791  exalim 1391
[Margaris] p. 51Theorem 1idALT 20
[Margaris] p. 56Theorem 3syld 40
[Margaris] p. 60Theorem 8mth8 579
[Margaris] p. 89Theorem 19.219.2 1529  r19.2m 3306
[Margaris] p. 89Theorem 19.319.3 1446  19.3h 1445  rr19.3v 2679
[Margaris] p. 89Theorem 19.5alcom 1367
[Margaris] p. 89Theorem 19.6alexdc 1510  alexim 1536
[Margaris] p. 89Theorem 19.7alnex 1388
[Margaris] p. 89Theorem 19.819.8a 1482  spsbe 1723
[Margaris] p. 89Theorem 19.919.9 1535  19.9h 1534  19.9v 1751  exlimd 1488
[Margaris] p. 89Theorem 19.11excom 1554  excomim 1553
[Margaris] p. 89Theorem 19.1219.12 1555  r19.12 2419
[Margaris] p. 90Theorem 19.14exnalim 1537
[Margaris] p. 90Theorem 19.15albi 1357  ralbi 2442
[Margaris] p. 90Theorem 19.1619.16 1447
[Margaris] p. 90Theorem 19.1719.17 1448
[Margaris] p. 90Theorem 19.18exbi 1495  rexbi 2443
[Margaris] p. 90Theorem 19.1919.19 1556
[Margaris] p. 90Theorem 19.20alim 1346  alimd 1414  alimdh 1356  alimdv 1759  ralimdaa 2383  ralimdv 2385  ralimdva 2384  sbcimdv 2820
[Margaris] p. 90Theorem 19.2119.21-2 1557  19.21 1475  19.21bi 1450  19.21h 1449  19.21ht 1473  19.21t 1474  19.21v 1753  alrimd 1501  alrimdd 1500  alrimdh 1368  alrimdv 1756  alrimi 1415  alrimih 1358  alrimiv 1754  alrimivv 1755  r19.21 2392  r19.21be 2407  r19.21bi 2404  r19.21t 2391  r19.21v 2393  ralrimd 2394  ralrimdv 2395  ralrimdva 2396  ralrimdvv 2400  ralrimdvva 2401  ralrimi 2387  ralrimiv 2388  ralrimiva 2389  ralrimivv 2397  ralrimivva 2398  ralrimivvva 2399  ralrimivw 2390  rexlimi 2423
[Margaris] p. 90Theorem 19.222alimdv 1761  2eximdv 1762  exim 1490  eximd 1503  eximdh 1502  eximdv 1760  rexim 2410  reximdai 2414  reximdv 2417  reximdv2 2415  reximdva 2418  reximdvai 2416  reximi2 2412
[Margaris] p. 90Theorem 19.2319.23 1568  19.23bi 1483  19.23h 1387  19.23ht 1386  19.23t 1567  19.23v 1763  19.23vv 1764  exlimd2 1486  exlimdh 1487  exlimdv 1700  exlimdvv 1777  exlimi 1485  exlimih 1484  exlimiv 1489  exlimivv 1776  r19.23 2421  r19.23v 2422  rexlimd 2427  rexlimdv 2429  rexlimdv3a 2432  rexlimdva 2430  rexlimdvaa 2431  rexlimdvv 2436  rexlimdvva 2437  rexlimdvw 2433  rexlimiv 2424  rexlimiva 2425  rexlimivv 2435
[Margaris] p. 90Theorem 19.24i19.24 1530
[Margaris] p. 90Theorem 19.2519.25 1517
[Margaris] p. 90Theorem 19.2619.26-2 1371  19.26-3an 1372  19.26 1370  r19.26-2 2439  r19.26-3 2440  r19.26 2438  r19.26m 2441
[Margaris] p. 90Theorem 19.2719.27 1453  19.27h 1452  19.27v 1779  r19.27av 2445  r19.27m 3313  r19.27mv 3314
[Margaris] p. 90Theorem 19.2819.28 1455  19.28h 1454  19.28v 1780  r19.28av 2446  r19.28m 3308  r19.28mv 3311  rr19.28v 2680
[Margaris] p. 90Theorem 19.2919.29 1511  19.29r 1512  19.29r2 1513  19.29x 1514  r19.29 2447  r19.29d2r 2452  r19.29r 2448
[Margaris] p. 90Theorem 19.3019.30dc 1518
[Margaris] p. 90Theorem 19.3119.31r 1571
[Margaris] p. 90Theorem 19.3219.32dc 1569  19.32r 1570  r19.32r 2454  r19.32vdc 2456  r19.32vr 2455
[Margaris] p. 90Theorem 19.3319.33 1373  19.33b2 1520  19.33bdc 1521
[Margaris] p. 90Theorem 19.3419.34 1574
[Margaris] p. 90Theorem 19.3519.35-1 1515  19.35i 1516
[Margaris] p. 90Theorem 19.3619.36-1 1563  19.36aiv 1781  19.36i 1562  r19.36av 2458
[Margaris] p. 90Theorem 19.3719.37-1 1564  19.37aiv 1565  r19.37 2459  r19.37av 2460
[Margaris] p. 90Theorem 19.3819.38 1566
[Margaris] p. 90Theorem 19.39i19.39 1531
[Margaris] p. 90Theorem 19.4019.40-2 1523  19.40 1522  r19.40 2461
[Margaris] p. 90Theorem 19.4119.41 1576  19.41h 1575  19.41v 1782  19.41vv 1783  19.41vvv 1784  19.41vvvv 1785  r19.41 2462  r19.41v 2463
[Margaris] p. 90Theorem 19.4219.42 1578  19.42h 1577  19.42v 1786  19.42vv 1788  19.42vvv 1789  19.42vvvv 1790  r19.42v 2464
[Margaris] p. 90Theorem 19.4319.43 1519  r19.43 2465
[Margaris] p. 90Theorem 19.4419.44 1572  r19.44av 2466
[Margaris] p. 90Theorem 19.4519.45 1573  r19.45av 2467  r19.45mv 3312
[Margaris] p. 110Exercise 2(b)eu1 1925
[Megill] p. 444Axiom C5ax-17 1419
[Megill] p. 445Lemma L12alequcom 1408  ax-10 1396
[Megill] p. 446Lemma L17equtrr 1596
[Megill] p. 446Lemma L19hbnae 1609
[Megill] p. 447Remark 9.1df-sb 1646  sbid 1657
[Megill] p. 448Scheme C5'ax-4 1400
[Megill] p. 448Scheme C6'ax-7 1337
[Megill] p. 448Scheme C8'ax-8 1395
[Megill] p. 448Scheme C9'ax-i12 1398
[Megill] p. 448Scheme C11'ax-10o 1604
[Megill] p. 448Scheme C12'ax-13 1404
[Megill] p. 448Scheme C13'ax-14 1405
[Megill] p. 448Scheme C15'ax-11o 1704
[Megill] p. 448Scheme C16'ax-16 1695
[Megill] p. 448Theorem 9.4dral1 1618  dral2 1619  drex1 1679  drex2 1620  drsb1 1680  drsb2 1722
[Megill] p. 449Theorem 9.7sbcom2 1863  sbequ 1721  sbid2v 1872
[Megill] p. 450Example in Appendixhba1 1433
[Mendelson] p. 36Lemma 1.8idALT 20
[Mendelson] p. 69Axiom 4rspsbc 2837  rspsbca 2838  stdpc4 1658
[Mendelson] p. 69Axiom 5ra5 2843  stdpc5 1476
[Mendelson] p. 81Rule Cexlimiv 1489
[Mendelson] p. 95Axiom 6stdpc6 1591
[Mendelson] p. 95Axiom 7stdpc7 1653
[Mendelson] p. 231Exercise 4.10(k)inv1 3250
[Mendelson] p. 231Exercise 4.10(l)unv 3251
[Mendelson] p. 231Exercise 4.10(n)inssun 3174
[Mendelson] p. 231Exercise 4.10(o)df-nul 3222
[Mendelson] p. 231Exercise 4.10(q)inssddif 3175
[Mendelson] p. 231Exercise 4.10(s)ddifnel 3072
[Mendelson] p. 231Definition of unionunssin 3173
[Mendelson] p. 235Exercise 4.12(c)univ 4179
[Mendelson] p. 235Exercise 4.12(d)pwv 3576
[Mendelson] p. 235Exercise 4.12(j)pwin 4016
[Mendelson] p. 235Exercise 4.12(k)pwunss 4017
[Mendelson] p. 235Exercise 4.12(l)pwssunim 4018
[Mendelson] p. 235Exercise 4.12(n)uniin 3597
[Mendelson] p. 235Exercise 4.12(p)reli 4428
[Mendelson] p. 235Exercise 4.12(t)relssdmrn 4804
[Mendelson] p. 246Definition of successordf-suc 4080
[Mendelson] p. 254Proposition 4.22(c)xpsnen 6258  xpsneng 6259
[Mendelson] p. 254Proposition 4.22(d)xpcomen 6264  xpcomeng 6265
[Mendelson] p. 254Proposition 4.22(e)xpassen 6267
[Mendelson] p. 255Exercise 4.39endisj 6261
[Mendelson] p. 266Proposition 4.34(a)oa1suc 6010
[Monk1] p. 26Theorem 2.8(vii)ssin 3156
[Monk1] p. 33Theorem 3.2(i)ssrel 4391
[Monk1] p. 33Theorem 3.2(ii)eqrel 4392
[Monk1] p. 34Definition 3.3df-opab 3816
[Monk1] p. 36Theorem 3.7(i)coi1 4799  coi2 4800
[Monk1] p. 36Theorem 3.8(v)dm0 4512  rn0 4551
[Monk1] p. 36Theorem 3.7(ii)cnvi 4691
[Monk1] p. 37Theorem 3.13(i)relxp 4410
[Monk1] p. 37Theorem 3.13(x)dmxpm 4518  rnxpm 4715
[Monk1] p. 37Theorem 3.13(ii)0xp 4383  xp0 4706
[Monk1] p. 38Theorem 3.16(ii)ima0 4647
[Monk1] p. 38Theorem 3.16(viii)imai 4644
[Monk1] p. 39Theorem 3.17imaexg 4643
[Monk1] p. 39Theorem 3.16(xi)imassrn 4642
[Monk1] p. 41Theorem 4.3(i)fnopfv 5260  funfvop 5242
[Monk1] p. 42Theorem 4.3(ii)funopfvb 5180
[Monk1] p. 42Theorem 4.4(iii)fvelima 5188
[Monk1] p. 43Theorem 4.6funun 4907
[Monk1] p. 43Theorem 4.8(iv)dff13 5370  dff13f 5372
[Monk1] p. 46Theorem 4.15(v)funex 5347  funrnex 5704
[Monk1] p. 50Definition 5.4fniunfv 5364
[Monk1] p. 52Theorem 5.12(ii)op2ndb 4767
[Monk1] p. 52Theorem 5.11(viii)ssint 3628
[Monk1] p. 52Definition 5.13 (i)1stval2 5745  df-1st 5730
[Monk1] p. 52Definition 5.13 (ii)2ndval2 5746  df-2nd 5731
[Monk2] p. 105Axiom C4ax-5 1336
[Monk2] p. 105Axiom C7ax-8 1395
[Monk2] p. 105Axiom C8ax-11 1397  ax-11o 1704
[Monk2] p. 105Axiom (C8)ax11v 1708
[Monk2] p. 109Lemma 12ax-7 1337
[Monk2] p. 109Lemma 15equvin 1743  equvini 1641  eqvinop 3977
[Monk2] p. 113Axiom C5-1ax-17 1419
[Monk2] p. 113Axiom C5-2ax6b 1541
[Monk2] p. 113Axiom C5-3ax-7 1337
[Monk2] p. 114Lemma 22hba1 1433
[Monk2] p. 114Lemma 23hbia1 1444  nfia1 1472
[Monk2] p. 114Lemma 24hba2 1443  nfa2 1471
[Moschovakis] p. 2Chapter 2 df-stab 740  dftest 822
[Quine] p. 16Definition 2.1df-clab 2027  rabid 2482
[Quine] p. 17Definition 2.1''dfsb7 1867
[Quine] p. 18Definition 2.7df-cleq 2033
[Quine] p. 19Definition 2.9df-v 2556
[Quine] p. 34Theorem 5.1abeq2 2146
[Quine] p. 35Theorem 5.2abid2 2158  abid2f 2202
[Quine] p. 40Theorem 6.1sb5 1767
[Quine] p. 40Theorem 6.2sb56 1765  sb6 1766
[Quine] p. 41Theorem 6.3df-clel 2036
[Quine] p. 41Theorem 6.4eqid 2040
[Quine] p. 41Theorem 6.5eqcom 2042
[Quine] p. 42Theorem 6.6df-sbc 2762
[Quine] p. 42Theorem 6.7dfsbcq 2763  dfsbcq2 2764
[Quine] p. 43Theorem 6.8vex 2557
[Quine] p. 43Theorem 6.9isset 2558
[Quine] p. 44Theorem 7.3spcgf 2632  spcgv 2637  spcimgf 2630
[Quine] p. 44Theorem 6.11spsbc 2772  spsbcd 2773
[Quine] p. 44Theorem 6.12elex 2563
[Quine] p. 44Theorem 6.13elab 2684  elabg 2685  elabgf 2682
[Quine] p. 44Theorem 6.14noel 3225
[Quine] p. 48Theorem 7.2snprc 3432
[Quine] p. 48Definition 7.1df-pr 3379  df-sn 3378
[Quine] p. 49Theorem 7.4snss 3491  snssg 3497
[Quine] p. 49Theorem 7.5prss 3517  prssg 3518
[Quine] p. 49Theorem 7.6prid1 3473  prid1g 3471  prid2 3474  prid2g 3472  snid 3399  snidg 3397
[Quine] p. 51Theorem 7.12snexg 3933  snexprc 3935
[Quine] p. 51Theorem 7.13prexg 3944
[Quine] p. 53Theorem 8.2unisn 3593  unisng 3594
[Quine] p. 53Theorem 8.3uniun 3596
[Quine] p. 54Theorem 8.6elssuni 3605
[Quine] p. 54Theorem 8.7uni0 3604
[Quine] p. 56Theorem 8.17uniabio 4840
[Quine] p. 56Definition 8.18dfiota2 4831
[Quine] p. 57Theorem 8.19iotaval 4841
[Quine] p. 57Theorem 8.22iotanul 4845
[Quine] p. 58Theorem 8.23euiotaex 4846
[Quine] p. 58Definition 9.1df-op 3381
[Quine] p. 61Theorem 9.5opabid 3991  opelopab 4005  opelopaba 4000  opelopabaf 4007  opelopabf 4008  opelopabg 4002  opelopabga 3997  oprabid 5500
[Quine] p. 64Definition 9.11df-xp 4314
[Quine] p. 64Definition 9.12df-cnv 4316
[Quine] p. 64Definition 9.15df-id 4027
[Quine] p. 65Theorem 10.3fun0 4920
[Quine] p. 65Theorem 10.4funi 4895
[Quine] p. 65Theorem 10.5funsn 4911  funsng 4909
[Quine] p. 65Definition 10.1df-fun 4867
[Quine] p. 65Definition 10.2args 4657  dffv4g 5138
[Quine] p. 68Definition 10.11df-fv 4873  fv2 5136
[Quine] p. 284Axiom 39(vi)funimaex 4947  funimaexg 4946
[Sanford] p. 39Rule 3mtpxor 1317
[Sanford] p. 39Rule 4mptxor 1315
[Sanford] p. 40Rule 1mptnan 1314
[Schechter] p. 51Definition of antisymmetryintasym 4672
[Schechter] p. 51Definition of irreflexivityintirr 4674
[Schechter] p. 51Definition of symmetrycnvsym 4671
[Schechter] p. 51Definition of transitivitycotr 4669
[Stoll] p. 13Definition of symmetric differencesymdif1 3199
[Stoll] p. 16Exercise 4.40dif 3292  dif0 3291
[Stoll] p. 16Exercise 4.8difdifdirss 3304
[Stoll] p. 19Theorem 5.2(13)undm 3192
[Stoll] p. 19Theorem 5.2(13')indmss 3193
[Stoll] p. 20Remarkinvdif 3176
[Stoll] p. 25Definition of ordered tripledf-ot 3382
[Stoll] p. 43Definitionuniiun 3707
[Stoll] p. 44Definitionintiin 3708
[Stoll] p. 45Definitiondf-iin 3657
[Stoll] p. 45Definition indexed uniondf-iun 3656
[Stoll] p. 176Theorem 3.4(27)imandc 786
[Stoll] p. 262Example 4.1symdif1 3199
[Suppes] p. 22Theorem 2eq0 3236
[Suppes] p. 22Theorem 4eqss 2957  eqssd 2959  eqssi 2958
[Suppes] p. 23Theorem 5ss0 3254  ss0b 3253
[Suppes] p. 23Theorem 6sstr 2950
[Suppes] p. 23Theorem 7pssirr 3041
[Suppes] p. 23Theorem 8pssn2lp 3042
[Suppes] p. 23Theorem 9psstr 3046
[Suppes] p. 23Theorem 10pssss 3036
[Suppes] p. 25Theorem 12elin 3123  elun 3081
[Suppes] p. 26Theorem 15inidm 3143
[Suppes] p. 26Theorem 16in0 3249
[Suppes] p. 27Theorem 23unidm 3083
[Suppes] p. 27Theorem 24un0 3248
[Suppes] p. 27Theorem 25ssun1 3103
[Suppes] p. 27Theorem 26ssequn1 3110
[Suppes] p. 27Theorem 27unss 3114
[Suppes] p. 27Theorem 28indir 3183
[Suppes] p. 27Theorem 29undir 3184
[Suppes] p. 28Theorem 32difid 3289  difidALT 3290
[Suppes] p. 29Theorem 33difin 3171
[Suppes] p. 29Theorem 34indif 3177
[Suppes] p. 29Theorem 35undif1ss 3295
[Suppes] p. 29Theorem 36difun2 3299
[Suppes] p. 29Theorem 37difin0 3294
[Suppes] p. 29Theorem 38disjdif 3293
[Suppes] p. 29Theorem 39difundi 3186
[Suppes] p. 29Theorem 40difindiss 3188
[Suppes] p. 30Theorem 41nalset 3884
[Suppes] p. 39Theorem 61uniss 3598
[Suppes] p. 39Theorem 65uniop 3989
[Suppes] p. 41Theorem 70intsn 3647
[Suppes] p. 42Theorem 71intpr 3644  intprg 3645
[Suppes] p. 42Theorem 73op1stb 4181  op1stbg 4182
[Suppes] p. 42Theorem 78intun 3643
[Suppes] p. 44Definition 15(a)dfiun2 3688  dfiun2g 3686
[Suppes] p. 44Definition 15(b)dfiin2 3689
[Suppes] p. 47Theorem 86elpw 3362  elpw2 3908  elpw2g 3907  elpwg 3364
[Suppes] p. 47Theorem 87pwid 3370
[Suppes] p. 47Theorem 89pw0 3508
[Suppes] p. 48Theorem 90pwpw0ss 3572
[Suppes] p. 52Theorem 101xpss12 4408
[Suppes] p. 52Theorem 102xpindi 4434  xpindir 4435
[Suppes] p. 52Theorem 103xpundi 4359  xpundir 4360
[Suppes] p. 54Theorem 105elirrv 4242
[Suppes] p. 58Theorem 2relss 4390
[Suppes] p. 59Theorem 4eldm 4495  eldm2 4496  eldm2g 4494  eldmg 4493
[Suppes] p. 59Definition 3df-dm 4318
[Suppes] p. 60Theorem 6dmin 4506
[Suppes] p. 60Theorem 8rnun 4695
[Suppes] p. 60Theorem 9rnin 4696
[Suppes] p. 60Definition 4dfrn2 4486
[Suppes] p. 61Theorem 11brcnv 4481  brcnvg 4479
[Suppes] p. 62Equation 5elcnv 4475  elcnv2 4476
[Suppes] p. 62Theorem 12relcnv 4666
[Suppes] p. 62Theorem 15cnvin 4694
[Suppes] p. 62Theorem 16cnvun 4692
[Suppes] p. 63Theorem 20co02 4797
[Suppes] p. 63Theorem 21dmcoss 4564
[Suppes] p. 63Definition 7df-co 4317
[Suppes] p. 64Theorem 26cnvco 4483
[Suppes] p. 64Theorem 27coass 4802
[Suppes] p. 65Theorem 31resundi 4588
[Suppes] p. 65Theorem 34elima 4636  elima2 4637  elima3 4638  elimag 4635
[Suppes] p. 65Theorem 35imaundi 4699
[Suppes] p. 66Theorem 40dminss 4701
[Suppes] p. 66Theorem 41imainss 4702
[Suppes] p. 67Exercise 11cnvxp 4705
[Suppes] p. 81Definition 34dfec2 6072
[Suppes] p. 82Theorem 72elec 6108  elecg 6107
[Suppes] p. 82Theorem 73erth 6113  erth2 6114
[Suppes] p. 92Theorem 1enref 6208  enrefg 6207
[Suppes] p. 92Theorem 2ensym 6224  ensymb 6223  ensymi 6225
[Suppes] p. 92Theorem 3entr 6227
[Suppes] p. 92Theorem 4unen 6256
[Suppes] p. 94Theorem 15endom 6206
[Suppes] p. 94Theorem 16ssdomg 6221
[Suppes] p. 94Theorem 17domtr 6228
[Suppes] p. 98Exercise 4fundmen 6249  fundmeng 6250
[Suppes] p. 98Exercise 6xpdom3m 6271
[Suppes] p. 130Definition 3df-tr 3852
[Suppes] p. 132Theorem 9ssonuni 4186
[Suppes] p. 134Definition 6df-suc 4080
[Suppes] p. 136Theorem Schema 22findes 4289  finds 4286  finds1 4288  finds2 4287
[Suppes] p. 162Definition 5df-ltnqqs 6408  df-ltpq 6401
[Suppes] p. 228Theorem Schema 61onintss 4099
[TakeutiZaring] p. 8Axiom 1ax-ext 2022
[TakeutiZaring] p. 13Definition 4.5df-cleq 2033
[TakeutiZaring] p. 13Proposition 4.6df-clel 2036
[TakeutiZaring] p. 13Proposition 4.9cvjust 2035
[TakeutiZaring] p. 13Proposition 4.7(3)eqtr 2057
[TakeutiZaring] p. 14Definition 4.16df-oprab 5479
[TakeutiZaring] p. 14Proposition 4.14ru 2760
[TakeutiZaring] p. 15Exercise 1elpr 3393  elpr2 3394  elprg 3392
[TakeutiZaring] p. 15Exercise 2elsn 3388  elsn2 3402  elsn2g 3401  elsng 3387  velsn 3389
[TakeutiZaring] p. 15Exercise 3elop 3965
[TakeutiZaring] p. 15Exercise 4sneq 3383  sneqr 3528
[TakeutiZaring] p. 15Definition 5.1dfpr2 3391  dfsn2 3386
[TakeutiZaring] p. 16Axiom 3uniex 4146
[TakeutiZaring] p. 16Exercise 6opth 3971
[TakeutiZaring] p. 16Exercise 8rext 3948
[TakeutiZaring] p. 16Corollary 5.8unex 4148  unexg 4150
[TakeutiZaring] p. 16Definition 5.3dftp2 3416
[TakeutiZaring] p. 16Definition 5.5df-uni 3578
[TakeutiZaring] p. 16Definition 5.6df-in 2921  df-un 2919
[TakeutiZaring] p. 16Proposition 5.7unipr 3591  uniprg 3592
[TakeutiZaring] p. 17Axiom 4pwex 3929  pwexg 3930
[TakeutiZaring] p. 17Exercise 1eltp 3415
[TakeutiZaring] p. 17Exercise 5elsuc 4115  elsucg 4113  sstr2 2949
[TakeutiZaring] p. 17Exercise 6uncom 3084
[TakeutiZaring] p. 17Exercise 7incom 3126
[TakeutiZaring] p. 17Exercise 8unass 3097
[TakeutiZaring] p. 17Exercise 9inass 3144
[TakeutiZaring] p. 17Exercise 10indi 3181
[TakeutiZaring] p. 17Exercise 11undi 3182
[TakeutiZaring] p. 17Definition 5.9df-pss 2930  dfss2 2931
[TakeutiZaring] p. 17Definition 5.10df-pw 3358
[TakeutiZaring] p. 18Exercise 7unss2 3111
[TakeutiZaring] p. 18Exercise 9df-ss 2928  sseqin2 3153
[TakeutiZaring] p. 18Exercise 10ssid 2961
[TakeutiZaring] p. 18Exercise 12inss1 3154  inss2 3155
[TakeutiZaring] p. 18Exercise 13nssr 3000
[TakeutiZaring] p. 18Exercise 15unieq 3586
[TakeutiZaring] p. 18Exercise 18sspwb 3949
[TakeutiZaring] p. 18Exercise 19pweqb 3956
[TakeutiZaring] p. 20Definitiondf-rab 2312
[TakeutiZaring] p. 20Corollary 5.160ex 3881
[TakeutiZaring] p. 20Definition 5.12df-dif 2917
[TakeutiZaring] p. 20Definition 5.14dfnul2 3223
[TakeutiZaring] p. 20Proposition 5.15difid 3289  difidALT 3290
[TakeutiZaring] p. 20Proposition 5.17(1)n0rf 3230
[TakeutiZaring] p. 21Theorem 5.22setind 4234
[TakeutiZaring] p. 21Definition 5.20df-v 2556
[TakeutiZaring] p. 21Proposition 5.21vprc 3885
[TakeutiZaring] p. 22Exercise 10ss 3252
[TakeutiZaring] p. 22Exercise 3ssex 3891  ssexg 3893
[TakeutiZaring] p. 22Exercise 4inex1 3888
[TakeutiZaring] p. 22Exercise 5ruv 4244
[TakeutiZaring] p. 22Exercise 6elirr 4236
[TakeutiZaring] p. 22Exercise 7ssdif0im 3283
[TakeutiZaring] p. 22Exercise 11difdif 3066
[TakeutiZaring] p. 22Exercise 13undif3ss 3195
[TakeutiZaring] p. 22Exercise 14difss 3067
[TakeutiZaring] p. 22Exercise 15sscon 3074
[TakeutiZaring] p. 22Definition 4.15(3)df-ral 2308
[TakeutiZaring] p. 22Definition 4.15(4)df-rex 2309
[TakeutiZaring] p. 23Proposition 6.2xpex 4416  xpexg 4415  xpexgALT 5723
[TakeutiZaring] p. 23Definition 6.4(1)df-rel 4315
[TakeutiZaring] p. 23Definition 6.4(2)fun2cnv 4926
[TakeutiZaring] p. 24Definition 6.4(3)f1cnvcnv 5063  fun11 4929
[TakeutiZaring] p. 24Definition 6.4(4)dffun4 4876  svrelfun 4927
[TakeutiZaring] p. 24Definition 6.5(1)dfdm3 4485
[TakeutiZaring] p. 24Definition 6.5(2)dfrn3 4487
[TakeutiZaring] p. 24Definition 6.6(1)df-res 4320
[TakeutiZaring] p. 24Definition 6.6(2)df-ima 4321
[TakeutiZaring] p. 24Definition 6.6(3)df-co 4317
[TakeutiZaring] p. 25Exercise 2cnvcnvss 4738  dfrel2 4734
[TakeutiZaring] p. 25Exercise 3xpss 4409
[TakeutiZaring] p. 25Exercise 5relun 4417
[TakeutiZaring] p. 25Exercise 6reluni 4423
[TakeutiZaring] p. 25Exercise 9inxp 4433
[TakeutiZaring] p. 25Exercise 12relres 4602
[TakeutiZaring] p. 25Exercise 13opelres 4580  opelresg 4582
[TakeutiZaring] p. 25Exercise 14dmres 4595
[TakeutiZaring] p. 25Exercise 15resss 4598
[TakeutiZaring] p. 25Exercise 17resabs1 4603
[TakeutiZaring] p. 25Exercise 18funres 4904
[TakeutiZaring] p. 25Exercise 24relco 4782
[TakeutiZaring] p. 25Exercise 29funco 4903
[TakeutiZaring] p. 25Exercise 30f1co 5064
[TakeutiZaring] p. 26Definition 6.10eu2 1944
[TakeutiZaring] p. 26Definition 6.11df-fv 4873  fv3 5160
[TakeutiZaring] p. 26Corollary 6.8(1)cnvex 4819  cnvexg 4818
[TakeutiZaring] p. 26Corollary 6.8(2)dmex 4561  dmexg 4559
[TakeutiZaring] p. 26Corollary 6.8(3)rnex 4562  rnexg 4560
[TakeutiZaring] p. 27Corollary 6.13funfvex 5155
[TakeutiZaring] p. 27Theorem 6.12(1)tz6.12-1 5163  tz6.12 5164  tz6.12c 5166
[TakeutiZaring] p. 27Theorem 6.12(2)tz6.12-2 5132
[TakeutiZaring] p. 27Definition 6.15(1)df-fn 4868
[TakeutiZaring] p. 27Definition 6.15(3)df-f 4869
[TakeutiZaring] p. 27Definition 6.15(4)df-fo 4871  wfo 4863
[TakeutiZaring] p. 27Definition 6.15(5)df-f1 4870  wf1 4862
[TakeutiZaring] p. 27Definition 6.15(6)df-f1o 4872  wf1o 4864
[TakeutiZaring] p. 28Exercise 4eqfnfv 5228  eqfnfv2 5229  eqfnfv2f 5232
[TakeutiZaring] p. 28Exercise 5fvco 5206
[TakeutiZaring] p. 28Theorem 6.16(1)fnex 5346  fnexALT 5703
[TakeutiZaring] p. 28Proposition 6.17resfunexg 5345  resfunexgALT 5700
[TakeutiZaring] p. 29Exercise 9funimaex 4947  funimaexg 4946
[TakeutiZaring] p. 29Definition 6.18df-br 3762
[TakeutiZaring] p. 30Definition 6.21eliniseg 4658  iniseg 4660
[TakeutiZaring] p. 30Definition 6.22df-eprel 4023
[TakeutiZaring] p. 32Definition 6.28df-isom 4874
[TakeutiZaring] p. 33Proposition 6.30(1)isoid 5413
[TakeutiZaring] p. 33Proposition 6.30(2)isocnv 5414
[TakeutiZaring] p. 33Proposition 6.30(3)isotr 5419
[TakeutiZaring] p. 33Proposition 6.31(2)isoini 5420
[TakeutiZaring] p. 34Proposition 6.33f1oiso 5428
[TakeutiZaring] p. 35Notationwtr 3851
[TakeutiZaring] p. 35Definition 7.1dftr3 3855
[TakeutiZaring] p. 36Proposition 7.6ordelord 4090
[TakeutiZaring] p. 37Proposition 7.9ordin 4094
[TakeutiZaring] p. 38Corollary 7.15ordsson 4190
[TakeutiZaring] p. 38Definition 7.11df-on 4077
[TakeutiZaring] p. 38Proposition 7.12ordon 4184
[TakeutiZaring] p. 38Proposition 7.13onprc 4246
[TakeutiZaring] p. 39Theorem 7.17tfi 4268
[TakeutiZaring] p. 40Exercise 7dftr2 3853
[TakeutiZaring] p. 40Exercise 11unon 4209
[TakeutiZaring] p. 40Proposition 7.19ssorduni 4185
[TakeutiZaring] p. 40Proposition 7.20elssuni 3605
[TakeutiZaring] p. 41Definition 7.22df-suc 4080
[TakeutiZaring] p. 41Proposition 7.23sssucid 4124  sucidg 4125
[TakeutiZaring] p. 41Proposition 7.24suceloni 4199
[TakeutiZaring] p. 42Exercise 1df-ilim 4078
[TakeutiZaring] p. 42Exercise 8onsucssi 4204  ordelsuc 4203
[TakeutiZaring] p. 42Proposition 7.30(1)peano1 4280
[TakeutiZaring] p. 42Proposition 7.30(2)peano2 4281
[TakeutiZaring] p. 42Proposition 7.30(3)peano3 4282
[TakeutiZaring] p. 43Axiom 7omex 4279
[TakeutiZaring] p. 43Theorem 7.32ordom 4292
[TakeutiZaring] p. 43Corollary 7.31find 4285
[TakeutiZaring] p. 43Proposition 7.30(4)peano4 4283
[TakeutiZaring] p. 43Proposition 7.30(5)peano5 4284
[TakeutiZaring] p. 44Exercise 2int0 3626  trint0m 3868
[TakeutiZaring] p. 44Exercise 4intss1 3627
[TakeutiZaring] p. 44Exercise 6onintonm 4215
[TakeutiZaring] p. 44Definition 7.35df-int 3613
[TakeutiZaring] p. 47Lemma 1tfrlem1 5886
[TakeutiZaring] p. 47Theorem 7.41(1)tfri1 5914  tfri1d 5912
[TakeutiZaring] p. 47Theorem 7.41(2)tfri2 5915  tfri2d 5913
[TakeutiZaring] p. 47Theorem 7.41(3)tfri3 5916
[TakeutiZaring] p. 50Exercise 3smoiso 5880
[TakeutiZaring] p. 50Definition 7.46df-smo 5864
[TakeutiZaring] p. 56Definition 8.1oasuc 6007
[TakeutiZaring] p. 57Proposition 8.2oacl 6003
[TakeutiZaring] p. 57Proposition 8.3oa0 6000
[TakeutiZaring] p. 57Proposition 8.16omcl 6004
[TakeutiZaring] p. 58Proposition 8.4nnaord 6045  nnaordi 6044
[TakeutiZaring] p. 59Proposition 8.6iunss2 3699  uniss2 3608
[TakeutiZaring] p. 59Proposition 8.9nnacl 6022
[TakeutiZaring] p. 62Exercise 5oaword1 6013
[TakeutiZaring] p. 62Definition 8.15om0 6001  omsuc 6014
[TakeutiZaring] p. 63Proposition 8.17nnmcl 6023
[TakeutiZaring] p. 63Proposition 8.19nnmord 6053  nnmordi 6052
[TakeutiZaring] p. 67Definition 8.30oei0 6002
[TakeutiZaring] p. 85Proposition 10.6(3)cardonle 6324
[TakeutiZaring] p. 88Exercise 1en0 6238
[TakeutiZaring] p. 90Proposition 10.20nneneq 6283
[TakeutiZaring] p. 90Corollary 10.21(1)php5 6284
[TakeutiZaring] p. 91Definition 10.29df-fin 6187  isfi 6204
[TakeutiZaring] p. 92Proposition 10.33(2)xpdom2 6268
[Tarski] p. 67Axiom B5ax-4 1400
[Tarski] p. 68Lemma 6equid 1589
[Tarski] p. 69Lemma 7equcomi 1592
[Tarski] p. 70Lemma 14spim 1626  spime 1629  spimeh 1627  spimh 1625
[Tarski] p. 70Lemma 16ax-11 1397  ax-11o 1704  ax11i 1602
[Tarski] p. 70Lemmas 16 and 17sb6 1766
[Tarski] p. 77Axiom B6 (p. 75) of system S2ax-17 1419
[Tarski] p. 77Axiom B8 (p. 75) of system S2ax-13 1404  ax-14 1405
[WhiteheadRussell] p. 96Axiom *1.3olc 632
[WhiteheadRussell] p. 96Axiom *1.4pm1.4 646
[WhiteheadRussell] p. 96Axiom *1.2 (Taut)pm1.2 673
[WhiteheadRussell] p. 96Axiom *1.5 (Assoc)pm1.5 682
[WhiteheadRussell] p. 97Axiom *1.6 (Sum)orim2 703
[WhiteheadRussell] p. 100Theorem *2.01pm2.01 546
[WhiteheadRussell] p. 100Theorem *2.02ax-1 5
[WhiteheadRussell] p. 100Theorem *2.03con2 572
[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 745
[WhiteheadRussell] p. 101Theorem *2.06barbara 1998  syl 14
[WhiteheadRussell] p. 101Theorem *2.07pm2.07 656
[WhiteheadRussell] p. 101Theorem *2.08id 19  idALT 20
[WhiteheadRussell] p. 101Theorem *2.11exmiddc 744
[WhiteheadRussell] p. 101Theorem *2.12notnot 559
[WhiteheadRussell] p. 101Theorem *2.13pm2.13dc 779
[WhiteheadRussell] p. 102Theorem *2.14notnotrdc 751
[WhiteheadRussell] p. 102Theorem *2.15con1dc 753
[WhiteheadRussell] p. 103Theorem *2.16con3 571
[WhiteheadRussell] p. 103Theorem *2.17condc 749
[WhiteheadRussell] p. 103Theorem *2.18pm2.18dc 750
[WhiteheadRussell] p. 104Theorem *2.2orc 633
[WhiteheadRussell] p. 104Theorem *2.3pm2.3 692
[WhiteheadRussell] p. 104Theorem *2.21pm2.21 547
[WhiteheadRussell] p. 104Theorem *2.24pm2.24 551
[WhiteheadRussell] p. 104Theorem *2.25pm2.25dc 792
[WhiteheadRussell] p. 104Theorem *2.26pm2.26dc 813
[WhiteheadRussell] p. 104Theorem *2.27pm2.27 35
[WhiteheadRussell] p. 104Theorem *2.31pm2.31 685
[WhiteheadRussell] p. 105Theorem *2.32pm2.32 686
[WhiteheadRussell] p. 105Theorem *2.36pm2.36 717
[WhiteheadRussell] p. 105Theorem *2.37pm2.37 718
[WhiteheadRussell] p. 105Theorem *2.38pm2.38 716
[WhiteheadRussell] p. 105Definition *2.33df-3or 886
[WhiteheadRussell] p. 106Theorem *2.4pm2.4 695
[WhiteheadRussell] p. 106Theorem *2.41pm2.41 693
[WhiteheadRussell] p. 106Theorem *2.42pm2.42 694
[WhiteheadRussell] p. 106Theorem *2.43pm2.43 47
[WhiteheadRussell] p. 106Theorem *2.45pm2.45 657
[WhiteheadRussell] p. 106Theorem *2.46pm2.46 658
[WhiteheadRussell] p. 107Theorem *2.5pm2.5dc 763
[WhiteheadRussell] p. 107Theorem *2.6pm2.6dc 759
[WhiteheadRussell] p. 107Theorem *2.47pm2.47 659
[WhiteheadRussell] p. 107Theorem *2.48pm2.48 660
[WhiteheadRussell] p. 107Theorem *2.49pm2.49 661
[WhiteheadRussell] p. 107Theorem *2.51pm2.51 581
[WhiteheadRussell] p. 107Theorem *2.52pm2.52 582
[WhiteheadRussell] p. 107Theorem *2.53pm2.53 641
[WhiteheadRussell] p. 107Theorem *2.54pm2.54dc 790
[WhiteheadRussell] p. 107Theorem *2.55orel1 644
[WhiteheadRussell] p. 107Theorem *2.56orel2 645
[WhiteheadRussell] p. 107Theorem *2.61pm2.61dc 762
[WhiteheadRussell] p. 107Theorem *2.62pm2.62 667
[WhiteheadRussell] p. 107Theorem *2.63pm2.63 713
[WhiteheadRussell] p. 107Theorem *2.64pm2.64 714
[WhiteheadRussell] p. 107Theorem *2.65pm2.65 585
[WhiteheadRussell] p. 107Theorem *2.67pm2.67-2 634  pm2.67 662
[WhiteheadRussell] p. 107Theorem *2.521pm2.521dc 764
[WhiteheadRussell] p. 107Theorem *2.621pm2.621 666
[WhiteheadRussell] p. 108Theorem *2.8pm2.8 723
[WhiteheadRussell] p. 108Theorem *2.68pm2.68dc 793
[WhiteheadRussell] p. 108Theorem *2.69looinvdc 821
[WhiteheadRussell] p. 108Theorem *2.73pm2.73 719
[WhiteheadRussell] p. 108Theorem *2.74pm2.74 720
[WhiteheadRussell] p. 108Theorem *2.75pm2.75 722
[WhiteheadRussell] p. 108Theorem *2.76pm2.76 721
[WhiteheadRussell] p. 108Theorem *2.77ax-2 6
[WhiteheadRussell] p. 108Theorem *2.81pm2.81 724
[WhiteheadRussell] p. 108Theorem *2.82pm2.82 725
[WhiteheadRussell] p. 108Theorem *2.83pm2.83 71
[WhiteheadRussell] p. 108Theorem *2.85pm2.85dc 811
[WhiteheadRussell] p. 108Theorem *2.86pm2.86 94
[WhiteheadRussell] p. 111Theorem *3.1pm3.1 671
[WhiteheadRussell] p. 111Theorem *3.2pm3.2 126
[WhiteheadRussell] p. 111Theorem *3.11pm3.11dc 864
[WhiteheadRussell] p. 111Theorem *3.12pm3.12dc 865
[WhiteheadRussell] p. 111Theorem *3.13pm3.13dc 866
[WhiteheadRussell] p. 111Theorem *3.14pm3.14 670
[WhiteheadRussell] p. 111Theorem *3.21pm3.21 251
[WhiteheadRussell] p. 111Theorem *3.22pm3.22 252
[WhiteheadRussell] p. 111Theorem *3.24pm3.24 627
[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 757
[WhiteheadRussell] p. 112Theorem *3.27 (Simp)simpr 103  simprimdc 756
[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 788
[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 672  pm3.44 635
[WhiteheadRussell] p. 113Theorem *3.47prth 326
[WhiteheadRussell] p. 113Theorem *3.43 (Comp)pm3.43 534
[WhiteheadRussell] p. 114Theorem *3.48pm3.48 699
[WhiteheadRussell] p. 116Theorem *4.1con34bdc 765
[WhiteheadRussell] p. 117Theorem *4.2biid 160
[WhiteheadRussell] p. 117Theorem *4.13notnotbdc 766
[WhiteheadRussell] p. 117Theorem *4.14pm4.14dc 787
[WhiteheadRussell] p. 117Theorem *4.15pm4.15 789
[WhiteheadRussell] p. 117Theorem *4.21bicom 128
[WhiteheadRussell] p. 117Theorem *4.22biantr 859  bitr 441
[WhiteheadRussell] p. 117Theorem *4.24pm4.24 375
[WhiteheadRussell] p. 117Theorem *4.25oridm 674  pm4.25 675
[WhiteheadRussell] p. 118Theorem *4.3ancom 253
[WhiteheadRussell] p. 118Theorem *4.4andi 731
[WhiteheadRussell] p. 118Theorem *4.31orcom 647
[WhiteheadRussell] p. 118Theorem *4.32anass 381
[WhiteheadRussell] p. 118Theorem *4.33orass 684
[WhiteheadRussell] p. 118Theorem *4.36anbi1 439
[WhiteheadRussell] p. 118Theorem *4.37orbi1 706
[WhiteheadRussell] p. 118Theorem *4.38pm4.38 537
[WhiteheadRussell] p. 118Theorem *4.39pm4.39 735
[WhiteheadRussell] p. 118Definition *4.34df-3an 887
[WhiteheadRussell] p. 119Theorem *4.41ordi 729
[WhiteheadRussell] p. 119Theorem *4.42pm4.42r 878
[WhiteheadRussell] p. 119Theorem *4.43pm4.43 856
[WhiteheadRussell] p. 119Theorem *4.44pm4.44 696
[WhiteheadRussell] p. 119Theorem *4.45orabs 727  pm4.45 698  pm4.45im 317
[WhiteheadRussell] p. 119Theorem *10.2219.26 1370
[WhiteheadRussell] p. 120Theorem *4.5anordc 863
[WhiteheadRussell] p. 120Theorem *4.6imordc 796  imorr 797
[WhiteheadRussell] p. 120Theorem *4.7anclb 302
[WhiteheadRussell] p. 120Theorem *4.51ianordc 799
[WhiteheadRussell] p. 120Theorem *4.52pm4.52im 803
[WhiteheadRussell] p. 120Theorem *4.53pm4.53r 804
[WhiteheadRussell] p. 120Theorem *4.54pm4.54dc 805
[WhiteheadRussell] p. 120Theorem *4.55pm4.55dc 846
[WhiteheadRussell] p. 120Theorem *4.56ioran 669  pm4.56 806
[WhiteheadRussell] p. 120Theorem *4.57oranim 807
[WhiteheadRussell] p. 120Theorem *4.61annimim 782
[WhiteheadRussell] p. 120Theorem *4.62pm4.62dc 798
[WhiteheadRussell] p. 120Theorem *4.63pm4.63dc 780
[WhiteheadRussell] p. 120Theorem *4.64pm4.64dc 801
[WhiteheadRussell] p. 120Theorem *4.65pm4.65r 783
[WhiteheadRussell] p. 120Theorem *4.66pm4.66dc 802
[WhiteheadRussell] p. 120Theorem *4.67pm4.67dc 781
[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 736
[WhiteheadRussell] p. 121Theorem *4.73iba 284
[WhiteheadRussell] p. 121Theorem *4.74biorf 663
[WhiteheadRussell] p. 121Theorem *4.76jcab 535  pm4.76 536
[WhiteheadRussell] p. 121Theorem *4.77jaob 631  pm4.77 712
[WhiteheadRussell] p. 121Theorem *4.78pm4.78i 808
[WhiteheadRussell] p. 121Theorem *4.79pm4.79dc 809
[WhiteheadRussell] p. 122Theorem *4.8pm4.8 623
[WhiteheadRussell] p. 122Theorem *4.81pm4.81dc 814
[WhiteheadRussell] p. 122Theorem *4.82pm4.82 857
[WhiteheadRussell] p. 122Theorem *4.83pm4.83dc 858
[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 815
[WhiteheadRussell] p. 123Theorem *5.12pm5.12dc 816
[WhiteheadRussell] p. 123Theorem *5.13pm5.13dc 818
[WhiteheadRussell] p. 123Theorem *5.14pm5.14dc 817
[WhiteheadRussell] p. 124Theorem *5.15pm5.15dc 1280
[WhiteheadRussell] p. 124Theorem *5.16pm5.16 737
[WhiteheadRussell] p. 124Theorem *5.17pm5.17dc 810
[WhiteheadRussell] p. 124Theorem *5.18nbbndc 1285  pm5.18dc 777
[WhiteheadRussell] p. 124Theorem *5.19pm5.19 622
[WhiteheadRussell] p. 124Theorem *5.21pm5.21 611
[WhiteheadRussell] p. 124Theorem *5.22xordc 1283
[WhiteheadRussell] p. 124Theorem *5.23dfbi3dc 1288
[WhiteheadRussell] p. 124Theorem *5.24pm5.24dc 1289
[WhiteheadRussell] p. 124Theorem *5.25dfor2dc 794
[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 835  pm5.6r 836
[WhiteheadRussell] p. 125Theorem *5.7pm5.7dc 861
[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 826
[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 834
[WhiteheadRussell] p. 125Theorem *5.53pm5.53 715
[WhiteheadRussell] p. 125Theorem *5.54pm5.54dc 827
[WhiteheadRussell] p. 125Theorem *5.55pm5.55dc 819
[WhiteheadRussell] p. 125Theorem *5.61pm5.61 708
[WhiteheadRussell] p. 125Theorem *5.62pm5.62dc 852
[WhiteheadRussell] p. 125Theorem *5.63pm5.63dc 853
[WhiteheadRussell] p. 125Theorem *5.71pm5.71dc 868
[WhiteheadRussell] p. 125Theorem *5.501pm5.501 233
[WhiteheadRussell] p. 126Theorem *5.74pm5.74 168
[WhiteheadRussell] p. 126Theorem *5.75pm5.75 869
[WhiteheadRussell] p. 150Theorem *10.3alsyl 1526
[WhiteheadRussell] p. 160Theorem *11.21alrot3 1374
[WhiteheadRussell] p. 163Theorem *11.4219.40-2 1523
[WhiteheadRussell] p. 164Theorem *11.53pm11.53 1775
[WhiteheadRussell] p. 175Definition *14.02df-eu 1903
[WhiteheadRussell] p. 178Theorem *13.18pm13.18 2283
[WhiteheadRussell] p. 178Theorem *13.181pm13.181 2284
[WhiteheadRussell] p. 178Theorem *13.183pm13.183 2678
[WhiteheadRussell] p. 185Theorem *14.121sbeqalb 2812
[WhiteheadRussell] p. 190Theorem *14.22iota4 4848
[WhiteheadRussell] p. 191Theorem *14.23iota4an 4849
[WhiteheadRussell] p. 192Theorem *14.26eupick 1979  eupickbi 1982
[WhiteheadRussell] p. 235Definition *30.01df-fv 4873

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