Bibliographic Cross-Reference - Intuitionistic Logic Explorer

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	Description	Intuitionistic Logic Explorer Page(s)
[AczelRathjen], p. 71	Definition 8.1.4	enumct 7282  fidcenum 7123
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7123
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7282
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12996
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7094
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 7080
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 13011
[AczelRathjen], p. 75	Corollary 8.1.20	unct 13013
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 13002  znnen 12969
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 13014
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 13015
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10998
[AczelRathjen], p. 183	Chapter 20	ax-setind 4629
[AhoHopUll] p. 318	Section 9.1	df-concat 11126  df-pfx 11205  df-substr 11178  df-word 11072  lencl 11075  wrd0 11096
[Apostol] p. 18	Theorem I.1	addcan 8326  addcan2d 8331  addcan2i 8329  addcand 8330  addcani 8328
[Apostol] p. 18	Theorem I.2	negeu 8337
[Apostol] p. 18	Theorem I.3	negsub 8394  negsubd 8463  negsubi 8424
[Apostol] p. 18	Theorem I.4	negneg 8396  negnegd 8448  negnegi 8416
[Apostol] p. 18	Theorem I.5	subdi 8531  subdid 8560  subdii 8553  subdir 8532  subdird 8561  subdiri 8554
[Apostol] p. 18	Theorem I.6	mul01 8535  mul01d 8539  mul01i 8537  mul02 8533  mul02d 8538  mul02i 8536
[Apostol] p. 18	Theorem I.9	divrecapd 8940
[Apostol] p. 18	Theorem I.10	recrecapi 8891
[Apostol] p. 18	Theorem I.12	mul2neg 8544  mul2negd 8559  mul2negi 8552  mulneg1 8541  mulneg1d 8557  mulneg1i 8550
[Apostol] p. 18	Theorem I.14	rdivmuldivd 14108
[Apostol] p. 18	Theorem I.15	divdivdivap 8860
[Apostol] p. 20	Axiom 7	rpaddcl 9873  rpaddcld 9908  rpmulcl 9874  rpmulcld 9909
[Apostol] p. 20	Axiom 9	0nrp 9885
[Apostol] p. 20	Theorem I.17	lttri 8251
[Apostol] p. 20	Theorem I.18	ltadd1d 8685  ltadd1dd 8703  ltadd1i 8649
[Apostol] p. 20	Theorem I.19	ltmul1 8739  ltmul1a 8738  ltmul1i 9067  ltmul1ii 9075  ltmul2 9003  ltmul2d 9935  ltmul2dd 9949  ltmul2i 9070
[Apostol] p. 20	Theorem I.21	0lt1 8273
[Apostol] p. 20	Theorem I.23	lt0neg1 8615  lt0neg1d 8662  ltneg 8609  ltnegd 8670  ltnegi 8640
[Apostol] p. 20	Theorem I.25	lt2add 8592  lt2addd 8714  lt2addi 8657
[Apostol] p. 20	Definition of positive numbers	df-rp 9850
[Apostol] p. 21	Exercise 4	recgt0 8997  recgt0d 9081  recgt0i 9053  recgt0ii 9054
[Apostol] p. 22	Definition of integers	df-z 9447
[Apostol] p. 22	Definition of rationals	df-q 9815
[Apostol] p. 24	Theorem I.26	supeuti 7161
[Apostol] p. 26	Theorem I.29	arch 9366
[Apostol] p. 28	Exercise 2	btwnz 9566
[Apostol] p. 28	Exercise 3	nnrecl 9367
[Apostol] p. 28	Exercise 6	qbtwnre 10476
[Apostol] p. 28	Exercise 10(a)	zeneo 12382  zneo 9548
[Apostol] p. 29	Theorem I.35	resqrtth 11542  sqrtthi 11630
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9113
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12557
[Apostol] p. 363	Remark	absgt0api 11657
[Apostol] p. 363	Example	abssubd 11704  abssubi 11661
[ApostolNT] p. 14	Definition	df-dvds 12299
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 12315
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12339
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12335
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12329
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12331
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 12316
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 12317
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 12322
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12356
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12358
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12360
[ApostolNT] p. 15	Definition	dfgcd2 12535
[ApostolNT] p. 16	Definition	isprm2 12639
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12614
[ApostolNT] p. 16	Theorem 1.7	prminf 13026
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12494
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12536
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12538
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12508
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12501
[ApostolNT] p. 17	Theorem 1.8	coprm 12666
[ApostolNT] p. 17	Theorem 1.9	euclemma 12668
[ApostolNT] p. 17	Theorem 1.10	1arith2 12891
[ApostolNT] p. 19	Theorem 1.14	divalg 12435
[ApostolNT] p. 20	Theorem 1.15	eucalg 12581
[ApostolNT] p. 25	Definition	df-phi 12733
[ApostolNT] p. 26	Theorem 2.2	phisum 12763
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12744
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12748
[ApostolNT] p. 38	Remark	df-sgm 15656
[ApostolNT] p. 38	Definition	df-sgm 15656
[ApostolNT] p. 104	Definition	congr 12622
[ApostolNT] p. 106	Remark	dvdsval3 12302
[ApostolNT] p. 106	Definition	moddvds 12310
[ApostolNT] p. 107	Example 2	mod2eq0even 12389
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12390
[ApostolNT] p. 107	Example 4	zmod1congr 10563
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10600
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10888
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12334
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12625
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 12944
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12627
[ApostolNT] p. 113	Theorem 5.17	eulerth 12755
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12774
[ApostolNT] p. 114	Theorem 5.19	fermltl 12756
[ApostolNT] p. 179	Definition	df-lgs 15677  lgsprme0 15721
[ApostolNT] p. 180	Example 1	1lgs 15722
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 15698
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 15713
[ApostolNT] p. 181	Theorem 9.4	m1lgs 15764
[ApostolNT] p. 181	Theorem 9.5	2lgs 15783  2lgsoddprm 15792
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 15748
[ApostolNT] p. 185	Theorem 9.8	lgsquad 15759
[ApostolNT] p. 188	Definition	df-lgs 15677  lgs1 15723
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 15714
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 15716
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 15724
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 15725
[Bauer] p. 482	Section 1.2	pm2.01 619  pm2.65 663
[Bauer] p. 483	Theorem 1.3	acexmid 6000  onsucelsucexmidlem 4621
[Bauer], p. 481	Section 1.1	pwtrufal 16363
[Bauer], p. 483	Definition	n0rf 3504
[Bauer], p. 483	Theorem 1.2	2irrexpq 15650  2irrexpqap 15652
[Bauer], p. 485	Theorem 2.1	ssfiexmid 7038
[Bauer], p. 493	Section 5.1	ivthdich 15327
[Bauer], p. 494	Theorem 5.5	ivthinc 15317
[BauerHanson], p. 27	Proposition 5.2	cnstab 8792
[BauerSwan], p. 14	Remark	0ct 7274  ctm 7276
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 16366
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7282
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7688
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7601
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7690
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7724  addlocpr 7723
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7750
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7753
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7758
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2080
[BellMachover] p. 460	Notation	df-mo 2081
[BellMachover] p. 460	Definition	mo3 2132  mo3h 2131
[BellMachover] p. 462	Theorem 1.1	bm1.1 2214
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4205
[BellMachover] p. 466	Axiom Pow	axpow3 4261
[BellMachover] p. 466	Axiom Union	axun2 4526
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4634
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4475
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4637
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4588
[BellMachover] p. 471	Definition of Lim	df-ilim 4460
[BellMachover] p. 472	Axiom Inf	zfinf2 4681
[BellMachover] p. 473	Theorem 2.8	limom 4706
[Bobzien] p. 116	Statement T3	stoic3 1473
[Bobzien] p. 117	Statement T2	stoic2a 1471
[Bobzien] p. 117	Statement T4	stoic4a 1474
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1469
[Bollobas] p. 1	Section I.1	df-edg 15859  isuhgropm 15881  isusgropen 15963  isuspgropen 15962
[Bollobas] p. 4	Definition	df-wlks 16031
[Bollobas] p. 7	Section I.1	df-ushgrm 15870
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13389
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13435
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13450
[BourbakiAlg1] p. 92	Definition 1	df-ring 13961
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 13896
[BourbakiEns] p.	Proposition 8	fcof1 5907  fcofo 5908
[BourbakiTop1] p.	Remark	xnegmnf 10025  xnegpnf 10024
[BourbakiTop1] p.	Remark	rexneg 10026
[BourbakiTop1] p.	Proposition	ishmeo 14978
[BourbakiTop1] p.	Property V_i	ssnei2 14831
[BourbakiTop1] p.	Property V_ii	innei 14837
[BourbakiTop1] p.	Property V_iv	neissex 14839
[BourbakiTop1] p.	Proposition 1	neipsm 14828  neiss 14824
[BourbakiTop1] p.	Proposition 2	cnptopco 14896
[BourbakiTop1] p.	Proposition 4	imasnopn 14973
[BourbakiTop1] p.	Property V_iii	elnei 14826
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14672
[Bruck] p. 1	Section I.1	df-mgm 13389
[Bruck] p. 23	Section II.1	df-sgrp 13435
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13632
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4147
[Church] p. 129	Section II.24	df-ifp 984  dfifp2dc 987
[Cohen] p. 301	Remark	relogoprlem 15542
[Cohen] p. 301	Property 2	relogmul 15543  relogmuld 15558
[Cohen] p. 301	Property 3	relogdiv 15544  relogdivd 15559
[Cohen] p. 301	Property 4	relogexp 15546
[Cohen] p. 301	Property 1a	log1 15540
[Cohen] p. 301	Property 1b	loge 15541
[Cohen4] p. 348	Observation	relogbcxpbap 15639
[Cohen4] p. 352	Definition	rpelogb 15623
[Cohen4] p. 361	Property 2	rprelogbmul 15629
[Cohen4] p. 361	Property 3	logbrec 15634  rprelogbdiv 15631
[Cohen4] p. 361	Property 4	rplogbreexp 15627
[Cohen4] p. 361	Property 6	relogbexpap 15632
[Cohen4] p. 361	Property 1(a)	rplogbid1 15621
[Cohen4] p. 361	Property 1(b)	rplogb1 15622
[Cohen4] p. 367	Property	rplogbchbase 15624
[Cohen4] p. 377	Property 2	logblt 15636
[Crosilla] p.	Axiom 1	ax-ext 2211
[Crosilla] p.	Axiom 2	ax-pr 4293
[Crosilla] p.	Axiom 3	ax-un 4524
[Crosilla] p.	Axiom 4	ax-nul 4210
[Crosilla] p.	Axiom 5	ax-iinf 4680
[Crosilla] p.	Axiom 6	ru 3027
[Crosilla] p.	Axiom 8	ax-pow 4258
[Crosilla] p.	Axiom 9	ax-setind 4629
[Crosilla], p.	Axiom 6	ax-sep 4202
[Crosilla], p.	Axiom 7	ax-coll 4199
[Crosilla], p.	Axiom 7'	repizf 4200
[Crosilla], p.	Theorem is stated	ordtriexmid 4613
[Crosilla], p.	Axiom of choice implies instances	acexmid 6000
[Crosilla], p.	Definition of ordinal	df-iord 4457
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4627
[Diestel] p. 27	Section 1.10	df-ushgrm 15870
[Eisenberg] p. 67	Definition 5.3	df-dif 3199
[Eisenberg] p. 82	Definition 6.3	df-iom 4683
[Eisenberg] p. 125	Definition 8.21	df-map 6797
[Enderton] p. 18	Axiom of Empty Set	axnul 4209
[Enderton] p. 19	Definition	df-tp 3674
[Enderton] p. 26	Exercise 5	unissb 3918
[Enderton] p. 26	Exercise 10	pwel 4304
[Enderton] p. 28	Exercise 7(b)	pwunim 4377
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 4035  iinin2m 4034  iunin1 4030  iunin2 4029
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 4033  iundif2ss 4031
[Enderton] p. 33	Exercise 23	iinuniss 4048
[Enderton] p. 33	Exercise 25	iununir 4049
[Enderton] p. 33	Exercise 24(a)	iinpw 4056
[Enderton] p. 33	Exercise 24(b)	iunpw 4571  iunpwss 4057
[Enderton] p. 38	Exercise 6(a)	unipw 4303
[Enderton] p. 38	Exercise 6(b)	pwuni 4276
[Enderton] p. 41	Lemma 3D	opeluu 4541  rnex 4992  rnexg 4989
[Enderton] p. 41	Exercise 8	dmuni 4933  rnuni 5140
[Enderton] p. 42	Definition of a function	dffun7 5345  dffun8 5346
[Enderton] p. 43	Definition of function value	funfvdm2 5698
[Enderton] p. 43	Definition of single-rooted	funcnv 5382
[Enderton] p. 44	Definition (d)	dfima2 5070  dfima3 5071
[Enderton] p. 47	Theorem 3H	fvco2 5703
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7388
[Enderton] p. 50	Theorem 3K(a)	imauni 5885
[Enderton] p. 52	Definition	df-map 6797
[Enderton] p. 53	Exercise 21	coass 5247
[Enderton] p. 53	Exercise 27	dmco 5237
[Enderton] p. 53	Exercise 14(a)	funin 5392
[Enderton] p. 53	Exercise 22(a)	imass2 5104
[Enderton] p. 54	Remark	ixpf 6867  ixpssmap 6879
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6846
[Enderton] p. 56	Theorem 3M	erref 6700
[Enderton] p. 57	Lemma 3N	erthi 6728
[Enderton] p. 57	Definition	df-ec 6682
[Enderton] p. 58	Definition	df-qs 6686
[Enderton] p. 60	Theorem 3Q	th3q 6787  th3qcor 6786  th3qlem1 6784  th3qlem2 6785
[Enderton] p. 61	Exercise 35	df-ec 6682
[Enderton] p. 65	Exercise 56(a)	dmun 4930
[Enderton] p. 68	Definition of successor	df-suc 4462
[Enderton] p. 71	Definition	df-tr 4183  dftr4 4187
[Enderton] p. 72	Theorem 4E	unisuc 4504  unisucg 4505
[Enderton] p. 73	Exercise 6	unisuc 4504  unisucg 4505
[Enderton] p. 73	Exercise 5(a)	truni 4196
[Enderton] p. 73	Exercise 5(b)	trint 4197
[Enderton] p. 79	Theorem 4I(A1)	nna0 6620
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6622  onasuc 6612
[Enderton] p. 79	Definition of operation value	df-ov 6004
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6621
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6623  onmsuc 6619
[Enderton] p. 81	Theorem 4K(1)	nnaass 6631
[Enderton] p. 81	Theorem 4K(2)	nna0r 6624  nnacom 6630
[Enderton] p. 81	Theorem 4K(3)	nndi 6632
[Enderton] p. 81	Theorem 4K(4)	nnmass 6633
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6635
[Enderton] p. 82	Exercise 16	nnm0r 6625  nnmsucr 6634
[Enderton] p. 88	Exercise 23	nnaordex 6674
[Enderton] p. 129	Definition	df-en 6888
[Enderton] p. 132	Theorem 6B(b)	canth 5952
[Enderton] p. 133	Exercise 1	xpomen 12966
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 7027
[Enderton] p. 136	Corollary 6E	nneneq 7018
[Enderton] p. 139	Theorem 6H(c)	mapen 7007
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7400
[Enderton] p. 143	Theorem 6J	dju0en 7396  dju1en 7395
[Enderton] p. 144	Corollary 6K	undif2ss 3567
[Enderton] p. 145	Figure 38	ffoss 5604
[Enderton] p. 145	Definition	df-dom 6889
[Enderton] p. 146	Example 1	domen 6900  domeng 6901
[Enderton] p. 146	Example 3	nndomo 7025
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6994  xpdom1g 6992  xpdom2g 6991
[Enderton] p. 168	Definition	df-po 4387
[Enderton] p. 192	Theorem 7M(a)	oneli 4519
[Enderton] p. 192	Theorem 7M(b)	ontr1 4480
[Enderton] p. 192	Theorem 7M(c)	onirri 4635
[Enderton] p. 193	Corollary 7N(b)	0elon 4483
[Enderton] p. 193	Corollary 7N(c)	onsuci 4608
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4581
[Enderton] p. 194	Remark	onprc 4644
[Enderton] p. 194	Exercise 16	suc11 4650
[Enderton] p. 197	Definition	df-card 7351
[Enderton] p. 200	Exercise 25	tfis 4675
[Enderton] p. 206	Theorem 7X(b)	en2lp 4646
[Enderton] p. 207	Exercise 34	opthreg 4648
[Enderton] p. 208	Exercise 35	suc11g 4649
[Geuvers], p. 1	Remark	expap0 10791
[Geuvers], p. 6	Lemma 2.13	mulap0r 8762
[Geuvers], p. 6	Lemma 2.15	mulap0 8801
[Geuvers], p. 9	Lemma 2.35	msqge0 8763
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8118
[Geuvers], p. 10	Lemma 3.9	maxcom 11714
[Geuvers], p. 10	Lemma 3.10	maxle1 11722  maxle2 11723
[Geuvers], p. 10	Lemma 3.11	maxleast 11724
[Geuvers], p. 10	Lemma 3.12	maxleb 11727
[Geuvers], p. 11	Definition 3.13	dfabsmax 11728
[Geuvers], p. 17	Definition 6.1	df-ap 8729
[Gleason] p. 117	Proposition 9-2.1	df-enq 7534  enqer 7545
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7538  df-nqqs 7535
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7531  df-plqqs 7536
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7532  df-mqqs 7537
[Gleason] p. 119	Proposition 9-2.5	df-rq 7539
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7595
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7598  ltbtwnnq 7603  ltbtwnnqq 7602
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7587
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7588
[Gleason] p. 123	Proposition 9-3.5	addclpr 7724
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7766
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7765
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7784
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7800
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7806  ltaprlem 7805
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7803
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7759
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7779
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7768
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7767
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7775
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7825
[Gleason] p. 126	Proposition 9-4.1	df-enr 7913  enrer 7922
[Gleason] p. 126	Proposition 9-4.2	df-0r 7918  df-1r 7919  df-nr 7914
[Gleason] p. 126	Proposition 9-4.3	df-mr 7916  df-plr 7915  negexsr 7959  recexsrlem 7961
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7917
[Gleason] p. 130	Proposition 10-1.3	creui 9107  creur 9106  cru 8749
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8110  axcnre 8068
[Gleason] p. 132	Definition 10-3.1	crim 11369  crimd 11488  crimi 11448  crre 11368  crred 11487  crrei 11447
[Gleason] p. 132	Definition 10-3.2	remim 11371  remimd 11453
[Gleason] p. 133	Definition 10.36	absval2 11568  absval2d 11696  absval2i 11655
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11395  cjaddd 11476  cjaddi 11443
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11396  cjmuld 11477  cjmuli 11444
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11394  cjcjd 11454  cjcji 11426
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11393  cjreb 11377  cjrebd 11457  cjrebi 11429  cjred 11482  rere 11376  rereb 11374  rerebd 11456  rerebi 11428  rered 11480
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11402  addcjd 11468  addcji 11438
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11512
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11563  abscjd 11701  abscji 11659
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11575  abs00d 11697  abs00i 11656  absne0d 11698
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11607  releabsd 11702  releabsi 11660
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11580  absmuld 11705  absmuli 11662
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11566  sqabsaddi 11663
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11615  abstrid 11707  abstrii 11666
[Gleason] p. 134	Definition 10-4.1	df-exp 10761  exp0 10765  expp1 10768  expp1d 10896
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10803  expaddd 10897
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15586  cxpmuld 15611  expmul 10806  expmuld 10898
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10800  mulexpd 10910  rpmulcxp 15583
[Gleason] p. 141	Definition 11-2.1	fzval 10206
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11837
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11839
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11838
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11842
[Gleason] p. 172	Corollary 12-2.5	climrecl 11835
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11831  climcj 11832  climim 11834  climre 11833
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8186  df-xr 8185  ltxr 9971
[Gleason] p. 180	Theorem 12-5.3	climcau 11858
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10520
[Gleason] p. 223	Definition 14-1.1	df-met 14509
[Gleason] p. 223	Definition 14-1.1(a)	met0 15038  xmet0 15037
[Gleason] p. 223	Definition 14-1.1(c)	metsym 15045
[Gleason] p. 223	Definition 14-1.1(d)	mettri 15047  mstri 15147  xmettri 15046  xmstri 15146
[Gleason] p. 230	Proposition 14-2.6	txlm 14953
[Gleason] p. 240	Proposition 14-4.2	metcnp3 15185
[Gleason] p. 243	Proposition 14-4.16	addcn2 11821  addcncntop 15236  mulcn2 11823  mulcncntop 15238  subcn2 11822  subcncntop 15237
[Gleason] p. 295	Remark	bcval3 10973  bcval4 10974
[Gleason] p. 295	Equation 2	bcpasc 10988
[Gleason] p. 295	Definition of binomial coefficient	bcval 10971  df-bc 10970
[Gleason] p. 296	Remark	bcn0 10977  bcnn 10979
[Gleason] p. 296	Theorem 15-2.8	binom 11995
[Gleason] p. 308	Equation 2	ef0 12183
[Gleason] p. 308	Equation 3	efcj 12184
[Gleason] p. 309	Corollary 15-4.3	efne0 12189
[Gleason] p. 309	Corollary 15-4.4	efexp 12193
[Gleason] p. 310	Equation 14	sinadd 12247
[Gleason] p. 310	Equation 15	cosadd 12248
[Gleason] p. 311	Equation 17	sincossq 12259
[Gleason] p. 311	Equation 18	cosbnd 12264  sinbnd 12263
[Gleason] p. 311	Definition of ` `	df-pi 12164
[Golan] p. 1	Remark	srgisid 13949
[Golan] p. 1	Definition	df-srg 13927
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1495
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13544  mndideu 13459
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13571
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13600
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13611
[Herstein] p. 57	Exercise 1	dfgrp3me 13633
[Heyting] p. 127	Axiom #1	ax1hfs 16442
[Hitchcock] p. 5	Rule A3	mptnan 1465
[Hitchcock] p. 5	Rule A4	mptxor 1466
[Hitchcock] p. 5	Rule A5	mtpxor 1468
[HoTT], p.	Lemma 10.4.1	exmidontriim 7407
[HoTT], p.	Theorem 7.2.6	nndceq 6645
[HoTT], p.	Exercise 11.10	neapmkv 16436
[HoTT], p.	Exercise 11.11	mulap0bd 8804
[HoTT], p.	Section 11.2.1	df-iltp 7657  df-imp 7656  df-iplp 7655  df-reap 8722
[HoTT], p.	Theorem 11.2.4	recapb 8818  rerecapb 8990
[HoTT], p.	Corollary 3.9.2	uchoice 6283
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7849
[HoTT], p.	Corollary 11.4.3	conventions 16085
[HoTT], p.	Exercise 11.6(i)	dcapnconst 16429  dceqnconst 16428
[HoTT], p.	Corollary 11.2.13	axcaucvg 8087  caucvgpr 7869  caucvgprpr 7899  caucvgsr 7989
[HoTT], p.	Definition 11.2.1	df-inp 7653
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 16434
[HoTT], p.	Proposition 11.2.3	df-iso 4388  ltpopr 7782  ltsopr 7783
[HoTT], p.	Definition 11.2.7(v)	apsym 8753  reapcotr 8745  reapirr 8724
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8273  gt0add 8720  leadd1 8577  lelttr 8235  lemul1a 9005  lenlt 8222  ltadd1 8576  ltletr 8236  ltmul1 8739  reaplt 8735
[Jech] p. 4	Definition of class	cv 1394  cvjust 2224
[Jech] p. 78	Note	opthprc 4770
[KalishMontague] p. 81	Note 1	ax-i9 1576
[Kreyszig] p. 3	Property M1	metcl 15027  xmetcl 15026
[Kreyszig] p. 4	Property M2	meteq0 15034
[Kreyszig] p. 12	Equation 5	muleqadd 8815
[Kreyszig] p. 18	Definition 1.3-2	mopnval 15116
[Kreyszig] p. 19	Remark	mopntopon 15117
[Kreyszig] p. 19	Theorem T1	mopn0 15162  mopnm 15122
[Kreyszig] p. 19	Theorem T2	unimopn 15160
[Kreyszig] p. 19	Definition of neighborhood	neibl 15165
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 15187
[Kreyszig] p. 25	Definition 1.4-1	lmbr 14887
[Kreyszig] p. 51	Equation 2	lmodvneg1 14294
[Kreyszig] p. 51	Equation 1a	lmod0vs 14285
[Kreyszig] p. 51	Equation 1b	lmodvs0 14286
[Kunen] p. 10	Axiom 0	a9e 1742
[Kunen] p. 12	Axiom 6	zfrep6 4201
[Kunen] p. 24	Definition 10.24	mapval 6807  mapvalg 6805
[Kunen] p. 31	Definition 10.24	mapex 6801
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3975
[Lang] p. 3	Statement	lidrideqd 13414  mndbn0 13464
[Lang] p. 3	Definition	df-mnd 13450
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 13431
[Lang] p. 5	Equation	gsumfzreidx 13874
[Lang] p. 6	Definition	mulgnn0gsum 13665
[Lang] p. 7	Definition	dfgrp2e 13561
[Levy] p. 338	Axiom	df-clab 2216  df-clel 2225  df-cleq 2222
[Lopez-Astorga] p. 12	Rule 1	mptnan 1465
[Lopez-Astorga] p. 12	Rule 2	mptxor 1466
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1468
[Margaris] p. 40	Rule C	exlimiv 1644
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 858
[Margaris] p. 49	Definition	dfbi2 388  dfordc 897  exalim 1548
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 655
[Margaris] p. 89	Theorem 19.2	19.2 1684  r19.2m 3578
[Margaris] p. 89	Theorem 19.3	19.3 1600  19.3h 1599  rr19.3v 2942
[Margaris] p. 89	Theorem 19.5	alcom 1524
[Margaris] p. 89	Theorem 19.6	alexdc 1665  alexim 1691
[Margaris] p. 89	Theorem 19.7	alnex 1545
[Margaris] p. 89	Theorem 19.8	19.8a 1636  spsbe 1888
[Margaris] p. 89	Theorem 19.9	19.9 1690  19.9h 1689  19.9v 1917  exlimd 1643
[Margaris] p. 89	Theorem 19.11	excom 1710  excomim 1709
[Margaris] p. 89	Theorem 19.12	19.12 1711  r19.12 2637
[Margaris] p. 90	Theorem 19.14	exnalim 1692
[Margaris] p. 90	Theorem 19.15	albi 1514  ralbi 2663
[Margaris] p. 90	Theorem 19.16	19.16 1601
[Margaris] p. 90	Theorem 19.17	19.17 1602
[Margaris] p. 90	Theorem 19.18	exbi 1650  rexbi 2664
[Margaris] p. 90	Theorem 19.19	19.19 1712
[Margaris] p. 90	Theorem 19.20	alim 1503  alimd 1567  alimdh 1513  alimdv 1925  ralimdaa 2596  ralimdv 2598  ralimdva 2597  ralimdvva 2599  sbcimdv 3094
[Margaris] p. 90	Theorem 19.21	19.21-2 1713  19.21 1629  19.21bi 1604  19.21h 1603  19.21ht 1627  19.21t 1628  19.21v 1919  alrimd 1656  alrimdd 1655  alrimdh 1525  alrimdv 1922  alrimi 1568  alrimih 1515  alrimiv 1920  alrimivv 1921  r19.21 2606  r19.21be 2621  r19.21bi 2618  r19.21t 2605  r19.21v 2607  ralrimd 2608  ralrimdv 2609  ralrimdva 2610  ralrimdvv 2614  ralrimdvva 2615  ralrimi 2601  ralrimiv 2602  ralrimiva 2603  ralrimivv 2611  ralrimivva 2612  ralrimivvva 2613  ralrimivw 2604  rexlimi 2641
[Margaris] p. 90	Theorem 19.22	2alimdv 1927  2eximdv 1928  exim 1645  eximd 1658  eximdh 1657  eximdv 1926  rexim 2624  reximdai 2628  reximddv 2633  reximddv2 2635  reximdv 2631  reximdv2 2629  reximdva 2632  reximdvai 2630  reximi2 2626
[Margaris] p. 90	Theorem 19.23	19.23 1724  19.23bi 1638  19.23h 1544  19.23ht 1543  19.23t 1723  19.23v 1929  19.23vv 1930  exlimd2 1641  exlimdh 1642  exlimdv 1865  exlimdvv 1944  exlimi 1640  exlimih 1639  exlimiv 1644  exlimivv 1943  r19.23 2639  r19.23v 2640  rexlimd 2645  rexlimdv 2647  rexlimdv3a 2650  rexlimdva 2648  rexlimdva2 2651  rexlimdvaa 2649  rexlimdvv 2655  rexlimdvva 2656  rexlimdvw 2652  rexlimiv 2642  rexlimiva 2643  rexlimivv 2654
[Margaris] p. 90	Theorem 19.24	i19.24 1685
[Margaris] p. 90	Theorem 19.25	19.25 1672
[Margaris] p. 90	Theorem 19.26	19.26-2 1528  19.26-3an 1529  19.26 1527  r19.26-2 2660  r19.26-3 2661  r19.26 2657  r19.26m 2662
[Margaris] p. 90	Theorem 19.27	19.27 1607  19.27h 1606  19.27v 1946  r19.27av 2666  r19.27m 3587  r19.27mv 3588
[Margaris] p. 90	Theorem 19.28	19.28 1609  19.28h 1608  19.28v 1947  r19.28av 2667  r19.28m 3581  r19.28mv 3584  rr19.28v 2943
[Margaris] p. 90	Theorem 19.29	19.29 1666  19.29r 1667  19.29r2 1668  19.29x 1669  r19.29 2668  r19.29d2r 2675  r19.29r 2669
[Margaris] p. 90	Theorem 19.30	19.30dc 1673
[Margaris] p. 90	Theorem 19.31	19.31r 1727
[Margaris] p. 90	Theorem 19.32	19.32dc 1725  19.32r 1726  r19.32r 2677  r19.32vdc 2680  r19.32vr 2679
[Margaris] p. 90	Theorem 19.33	19.33 1530  19.33b2 1675  19.33bdc 1676
[Margaris] p. 90	Theorem 19.34	19.34 1730
[Margaris] p. 90	Theorem 19.35	19.35-1 1670  19.35i 1671
[Margaris] p. 90	Theorem 19.36	19.36-1 1719  19.36aiv 1948  19.36i 1718  r19.36av 2682
[Margaris] p. 90	Theorem 19.37	19.37-1 1720  19.37aiv 1721  r19.37 2683  r19.37av 2684
[Margaris] p. 90	Theorem 19.38	19.38 1722
[Margaris] p. 90	Theorem 19.39	i19.39 1686
[Margaris] p. 90	Theorem 19.40	19.40-2 1678  19.40 1677  r19.40 2685
[Margaris] p. 90	Theorem 19.41	19.41 1732  19.41h 1731  19.41v 1949  19.41vv 1950  19.41vvv 1951  19.41vvvv 1952  r19.41 2686  r19.41v 2687
[Margaris] p. 90	Theorem 19.42	19.42 1734  19.42h 1733  19.42v 1953  19.42vv 1958  19.42vvv 1959  19.42vvvv 1960  r19.42v 2688
[Margaris] p. 90	Theorem 19.43	19.43 1674  r19.43 2689
[Margaris] p. 90	Theorem 19.44	19.44 1728  r19.44av 2690  r19.44mv 3586
[Margaris] p. 90	Theorem 19.45	19.45 1729  r19.45av 2691  r19.45mv 3585
[Margaris] p. 110	Exercise 2(b)	eu1 2102
[Megill] p. 444	Axiom C5	ax-17 1572
[Megill] p. 445	Lemma L12	alequcom 1561  ax-10 1551
[Megill] p. 446	Lemma L17	equtrr 1756
[Megill] p. 446	Lemma L19	hbnae 1767
[Megill] p. 447	Remark 9.1	df-sb 1809  sbid 1820
[Megill] p. 448	Scheme C5'	ax-4 1556
[Megill] p. 448	Scheme C6'	ax-7 1494
[Megill] p. 448	Scheme C8'	ax-8 1550
[Megill] p. 448	Scheme C9'	ax-i12 1553
[Megill] p. 448	Scheme C11'	ax-10o 1762
[Megill] p. 448	Scheme C12'	ax-13 2202
[Megill] p. 448	Scheme C13'	ax-14 2203
[Megill] p. 448	Scheme C15'	ax-11o 1869
[Megill] p. 448	Scheme C16'	ax-16 1860
[Megill] p. 448	Theorem 9.4	dral1 1776  dral2 1777  drex1 1844  drex2 1778  drsb1 1845  drsb2 1887
[Megill] p. 449	Theorem 9.7	sbcom2 2038  sbequ 1886  sbid2v 2047
[Megill] p. 450	Example in Appendix	hba1 1586
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3112  rspsbca 3113  stdpc4 1821
[Mendelson] p. 69	Axiom 5	ra5 3118  stdpc5 1630
[Mendelson] p. 81	Rule C	exlimiv 1644
[Mendelson] p. 95	Axiom 6	stdpc6 1749
[Mendelson] p. 95	Axiom 7	stdpc7 1816
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3528
[Mendelson] p. 231	Exercise 4.10(l)	unv 3529
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3444
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3492
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3445
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3335
[Mendelson] p. 231	Definition of union	unssin 3443
[Mendelson] p. 235	Exercise 4.12(c)	univ 4567
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3887
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4373
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4374
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4375
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3908
[Mendelson] p. 235	Exercise 4.12(p)	reli 4851
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5249
[Mendelson] p. 246	Definition of successor	df-suc 4462
[Mendelson] p. 254	Proposition 4.22(b)	xpen 7006
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6980  xpsneng 6981
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6986  xpcomeng 6987
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6989
[Mendelson] p. 255	Exercise 4.39	endisj 6983
[Mendelson] p. 255	Exercise 4.41	mapprc 6799
[Mendelson] p. 255	Exercise 4.43	mapsnen 6964
[Mendelson] p. 255	Exercise 4.47	xpmapen 7011
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6833
[Mendelson] p. 255	Exercise 4.42(b)	map1 6965
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7399  djucomen 7398
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7397
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6613
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3426
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4807
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4808
[Monk1] p. 34	Definition 3.3	df-opab 4146
[Monk1] p. 36	Theorem 3.7(i)	coi1 5244  coi2 5245
[Monk1] p. 36	Theorem 3.8(v)	dm0 4937  rn0 4980
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5133
[Monk1] p. 37	Theorem 3.13(i)	relxp 4828
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4944  rnxpm 5158
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4799  xp0 5148
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5087
[Monk1] p. 38	Theorem 3.16(viii)	imai 5084
[Monk1] p. 39	Theorem 3.17	imaex 5083  imaexg 5082
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5079
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5765  funfvop 5747
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5675
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5685
[Monk1] p. 43	Theorem 4.6	funun 5362
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5892  dff13f 5894
[Monk1] p. 46	Theorem 4.15(v)	funex 5862  funrnex 6259
[Monk1] p. 50	Definition 5.4	fniunfv 5886
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5212
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3939
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6301  df-1st 6286
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6302  df-2nd 6287
[Monk2] p. 105	Axiom C4	ax-5 1493
[Monk2] p. 105	Axiom C7	ax-8 1550
[Monk2] p. 105	Axiom C8	ax-11 1552  ax-11o 1869
[Monk2] p. 105	Axiom (C8)	ax11v 1873
[Monk2] p. 109	Lemma 12	ax-7 1494
[Monk2] p. 109	Lemma 15	equvin 1909  equvini 1804  eqvinop 4329
[Monk2] p. 113	Axiom C5-1	ax-17 1572
[Monk2] p. 113	Axiom C5-2	ax6b 1697
[Monk2] p. 113	Axiom C5-3	ax-7 1494
[Monk2] p. 114	Lemma 22	hba1 1586
[Monk2] p. 114	Lemma 23	hbia1 1598  nfia1 1626
[Monk2] p. 114	Lemma 24	hba2 1597  nfa2 1625
[Moschovakis] p. 2	Chapter 2	df-stab 836  dftest 16443
[Munkres] p. 77	Example 2	distop 14759
[Munkres] p. 78	Definition of basis	df-bases 14717  isbasis3g 14720
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 13293  tgval2 14725
[Munkres] p. 79	Remark	tgcl 14738
[Munkres] p. 80	Lemma 2.1	tgval3 14732
[Munkres] p. 80	Lemma 2.2	tgss2 14753  tgss3 14752
[Munkres] p. 81	Lemma 2.3	basgen 14754  basgen2 14755
[Munkres] p. 89	Definition of subspace topology	resttop 14844
[Munkres] p. 93	Theorem 6.1(1)	0cld 14786  topcld 14783
[Munkres] p. 93	Theorem 6.1(3)	uncld 14787
[Munkres] p. 94	Definition of closure	clsval 14785
[Munkres] p. 94	Definition of interior	ntrval 14784
[Munkres] p. 102	Definition of continuous function	df-cn 14862  iscn 14871  iscn2 14874
[Munkres] p. 107	Theorem 7.2(g)	cncnp 14904  cncnp2m 14905  cncnpi 14902  df-cnp 14863  iscnp 14873
[Munkres] p. 127	Theorem 10.1	metcn 15188
[Pierik], p. 8	Section 2.2.1	dfrex2fin 7065
[Pierik], p. 9	Definition 2.4	df-womni 7331
[Pierik], p. 9	Definition 2.5	df-markov 7319  omniwomnimkv 7334
[Pierik], p. 10	Section 2.3	dfdif3 3314
[Pierik], p. 14	Definition 3.1	df-omni 7302  exmidomniim 7308  finomni 7307
[Pierik], p. 15	Section 3.1	df-nninf 7287
[Pradic2025], p. 2	Section 1.1	nnnninfen 16387
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 16391
[PradicBrown2022], p. 2	Remark	exmidpw 7070
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7379
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7380  exmidfodomrlemrALT 7381
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7316
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 16373  peano4nninf 16372
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 16375
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 16383
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 16385
[PradicBrown2022], p. 5	Definition 3.3	nnsf 16371
[Quine] p. 16	Definition 2.1	df-clab 2216  rabid 2707
[Quine] p. 17	Definition 2.1''	dfsb7 2042
[Quine] p. 18	Definition 2.7	df-cleq 2222
[Quine] p. 19	Definition 2.9	df-v 2801
[Quine] p. 34	Theorem 5.1	abeq2 2338
[Quine] p. 35	Theorem 5.2	abid2 2350  abid2f 2398
[Quine] p. 40	Theorem 6.1	sb5 1934
[Quine] p. 40	Theorem 6.2	sb56 1932  sb6 1933
[Quine] p. 41	Theorem 6.3	df-clel 2225
[Quine] p. 41	Theorem 6.4	eqid 2229
[Quine] p. 41	Theorem 6.5	eqcom 2231
[Quine] p. 42	Theorem 6.6	df-sbc 3029
[Quine] p. 42	Theorem 6.7	dfsbcq 3030  dfsbcq2 3031
[Quine] p. 43	Theorem 6.8	vex 2802
[Quine] p. 43	Theorem 6.9	isset 2806
[Quine] p. 44	Theorem 7.3	spcgf 2885  spcgv 2890  spcimgf 2883
[Quine] p. 44	Theorem 6.11	spsbc 3040  spsbcd 3041
[Quine] p. 44	Theorem 6.12	elex 2811
[Quine] p. 44	Theorem 6.13	elab 2947  elabg 2949  elabgf 2945
[Quine] p. 44	Theorem 6.14	noel 3495
[Quine] p. 48	Theorem 7.2	snprc 3731
[Quine] p. 48	Definition 7.1	df-pr 3673  df-sn 3672
[Quine] p. 49	Theorem 7.4	snss 3803  snssg 3802
[Quine] p. 49	Theorem 7.5	prss 3824  prssg 3825
[Quine] p. 49	Theorem 7.6	prid1 3772  prid1g 3770  prid2 3773  prid2g 3771  snid 3697  snidg 3695
[Quine] p. 51	Theorem 7.12	snexg 4268  snexprc 4270
[Quine] p. 51	Theorem 7.13	prexg 4295
[Quine] p. 53	Theorem 8.2	unisn 3904  unisng 3905
[Quine] p. 53	Theorem 8.3	uniun 3907
[Quine] p. 54	Theorem 8.6	elssuni 3916
[Quine] p. 54	Theorem 8.7	uni0 3915
[Quine] p. 56	Theorem 8.17	uniabio 5289
[Quine] p. 56	Definition 8.18	dfiota2 5279
[Quine] p. 57	Theorem 8.19	iotaval 5290
[Quine] p. 57	Theorem 8.22	iotanul 5294
[Quine] p. 58	Theorem 8.23	euiotaex 5295
[Quine] p. 58	Definition 9.1	df-op 3675
[Quine] p. 61	Theorem 9.5	opabid 4344  opabidw 4345  opelopab 4360  opelopaba 4354  opelopabaf 4362  opelopabf 4363  opelopabg 4356  opelopabga 4351  opelopabgf 4358  oprabid 6033
[Quine] p. 64	Definition 9.11	df-xp 4725
[Quine] p. 64	Definition 9.12	df-cnv 4727
[Quine] p. 64	Definition 9.15	df-id 4384
[Quine] p. 65	Theorem 10.3	fun0 5379
[Quine] p. 65	Theorem 10.4	funi 5350
[Quine] p. 65	Theorem 10.5	funsn 5369  funsng 5367
[Quine] p. 65	Definition 10.1	df-fun 5320
[Quine] p. 65	Definition 10.2	args 5097  dffv4g 5624
[Quine] p. 68	Definition 10.11	df-fv 5326  fv2 5622
[Quine] p. 124	Theorem 17.3	nn0opth2 10946  nn0opth2d 10945  nn0opthd 10944
[Quine] p. 284	Axiom 39(vi)	funimaex 5406  funimaexg 5405
[Roman] p. 18	Part Preliminaries	df-rng 13896
[Roman] p. 19	Part Preliminaries	df-ring 13961
[Rudin] p. 164	Equation 27	efcan 12187
[Rudin] p. 164	Equation 30	efzval 12194
[Rudin] p. 167	Equation 48	absefi 12280
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1468
[Sanford] p. 39	Rule 4	mptxor 1466
[Sanford] p. 40	Rule 1	mptnan 1465
[Schechter] p. 51	Definition of antisymmetry	intasym 5113
[Schechter] p. 51	Definition of irreflexivity	intirr 5115
[Schechter] p. 51	Definition of symmetry	cnvsym 5112
[Schechter] p. 51	Definition of transitivity	cotr 5110
[Schechter] p. 187	Definition of "ring with unit"	isring 13963
[Schechter] p. 428	Definition 15.35	bastop1 14757
[Stoll] p. 13	Definition of symmetric difference	symdif1 3469
[Stoll] p. 16	Exercise 4.4	0dif 3563  dif0 3562
[Stoll] p. 16	Exercise 4.8	difdifdirss 3576
[Stoll] p. 19	Theorem 5.2(13)	undm 3462
[Stoll] p. 19	Theorem 5.2(13')	indmss 3463
[Stoll] p. 20	Remark	invdif 3446
[Stoll] p. 25	Definition of ordered triple	df-ot 3676
[Stoll] p. 43	Definition	uniiun 4019
[Stoll] p. 44	Definition	intiin 4020
[Stoll] p. 45	Definition	df-iin 3968
[Stoll] p. 45	Definition indexed union	df-iun 3967
[Stoll] p. 176	Theorem 3.4(27)	imandc 894  imanst 893
[Stoll] p. 262	Example 4.1	symdif1 3469
[Suppes] p. 22	Theorem 2	eq0 3510
[Suppes] p. 22	Theorem 4	eqss 3239  eqssd 3241  eqssi 3240
[Suppes] p. 23	Theorem 5	ss0 3532  ss0b 3531
[Suppes] p. 23	Theorem 6	sstr 3232
[Suppes] p. 25	Theorem 12	elin 3387  elun 3345
[Suppes] p. 26	Theorem 15	inidm 3413
[Suppes] p. 26	Theorem 16	in0 3526
[Suppes] p. 27	Theorem 23	unidm 3347
[Suppes] p. 27	Theorem 24	un0 3525
[Suppes] p. 27	Theorem 25	ssun1 3367
[Suppes] p. 27	Theorem 26	ssequn1 3374
[Suppes] p. 27	Theorem 27	unss 3378
[Suppes] p. 27	Theorem 28	indir 3453
[Suppes] p. 27	Theorem 29	undir 3454
[Suppes] p. 28	Theorem 32	difid 3560  difidALT 3561
[Suppes] p. 29	Theorem 33	difin 3441
[Suppes] p. 29	Theorem 34	indif 3447
[Suppes] p. 29	Theorem 35	undif1ss 3566
[Suppes] p. 29	Theorem 36	difun2 3571
[Suppes] p. 29	Theorem 37	difin0 3565
[Suppes] p. 29	Theorem 38	disjdif 3564
[Suppes] p. 29	Theorem 39	difundi 3456
[Suppes] p. 29	Theorem 40	difindiss 3458
[Suppes] p. 30	Theorem 41	nalset 4214
[Suppes] p. 39	Theorem 61	uniss 3909
[Suppes] p. 39	Theorem 65	uniop 4342
[Suppes] p. 41	Theorem 70	intsn 3958
[Suppes] p. 42	Theorem 71	intpr 3955  intprg 3956
[Suppes] p. 42	Theorem 73	op1stb 4569  op1stbg 4570
[Suppes] p. 42	Theorem 78	intun 3954
[Suppes] p. 44	Definition 15(a)	dfiun2 3999  dfiun2g 3997
[Suppes] p. 44	Definition 15(b)	dfiin2 4000
[Suppes] p. 47	Theorem 86	elpw 3655  elpw2 4241  elpw2g 4240  elpwg 3657
[Suppes] p. 47	Theorem 87	pwid 3664
[Suppes] p. 47	Theorem 89	pw0 3815
[Suppes] p. 48	Theorem 90	pwpw0ss 3883
[Suppes] p. 52	Theorem 101	xpss12 4826
[Suppes] p. 52	Theorem 102	xpindi 4857  xpindir 4858
[Suppes] p. 52	Theorem 103	xpundi 4775  xpundir 4776
[Suppes] p. 54	Theorem 105	elirrv 4640
[Suppes] p. 58	Theorem 2	relss 4806
[Suppes] p. 59	Theorem 4	eldm 4920  eldm2 4921  eldm2g 4919  eldmg 4918
[Suppes] p. 59	Definition 3	df-dm 4729
[Suppes] p. 60	Theorem 6	dmin 4931
[Suppes] p. 60	Theorem 8	rnun 5137
[Suppes] p. 60	Theorem 9	rnin 5138
[Suppes] p. 60	Definition 4	dfrn2 4910
[Suppes] p. 61	Theorem 11	brcnv 4905  brcnvg 4903
[Suppes] p. 62	Equation 5	elcnv 4899  elcnv2 4900
[Suppes] p. 62	Theorem 12	relcnv 5106
[Suppes] p. 62	Theorem 15	cnvin 5136
[Suppes] p. 62	Theorem 16	cnvun 5134
[Suppes] p. 63	Theorem 20	co02 5242
[Suppes] p. 63	Theorem 21	dmcoss 4994
[Suppes] p. 63	Definition 7	df-co 4728
[Suppes] p. 64	Theorem 26	cnvco 4907
[Suppes] p. 64	Theorem 27	coass 5247
[Suppes] p. 65	Theorem 31	resundi 5018
[Suppes] p. 65	Theorem 34	elima 5073  elima2 5074  elima3 5075  elimag 5072
[Suppes] p. 65	Theorem 35	imaundi 5141
[Suppes] p. 66	Theorem 40	dminss 5143
[Suppes] p. 66	Theorem 41	imainss 5144
[Suppes] p. 67	Exercise 11	cnvxp 5147
[Suppes] p. 81	Definition 34	dfec2 6683
[Suppes] p. 82	Theorem 72	elec 6721  elecg 6720
[Suppes] p. 82	Theorem 73	erth 6726  erth2 6727
[Suppes] p. 89	Theorem 96	map0b 6834
[Suppes] p. 89	Theorem 97	map0 6836  map0g 6835
[Suppes] p. 89	Theorem 98	mapsn 6837
[Suppes] p. 89	Theorem 99	mapss 6838
[Suppes] p. 92	Theorem 1	enref 6916  enrefg 6915
[Suppes] p. 92	Theorem 2	ensym 6933  ensymb 6932  ensymi 6934
[Suppes] p. 92	Theorem 3	entr 6936
[Suppes] p. 92	Theorem 4	unen 6969
[Suppes] p. 94	Theorem 15	endom 6914
[Suppes] p. 94	Theorem 16	ssdomg 6930
[Suppes] p. 94	Theorem 17	domtr 6937
[Suppes] p. 95	Theorem 18	isbth 7134
[Suppes] p. 98	Exercise 4	fundmen 6959  fundmeng 6960
[Suppes] p. 98	Exercise 6	xpdom3m 6993
[Suppes] p. 130	Definition 3	df-tr 4183
[Suppes] p. 132	Theorem 9	ssonuni 4580
[Suppes] p. 134	Definition 6	df-suc 4462
[Suppes] p. 136	Theorem Schema 22	findes 4695  finds 4692  finds1 4694  finds2 4693
[Suppes] p. 162	Definition 5	df-ltnqqs 7540  df-ltpq 7533
[Suppes] p. 228	Theorem Schema 61	onintss 4481
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2211
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2222
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2225
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2224
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2247
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 6005
[TakeutiZaring] p. 14	Proposition 4.14	ru 3027
[TakeutiZaring] p. 15	Exercise 1	elpr 3687  elpr2 3688  elprg 3686
[TakeutiZaring] p. 15	Exercise 2	elsn 3682  elsn2 3700  elsn2g 3699  elsng 3681  velsn 3683
[TakeutiZaring] p. 15	Exercise 3	elop 4317
[TakeutiZaring] p. 15	Exercise 4	sneq 3677  sneqr 3838
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3685  dfsn2 3680
[TakeutiZaring] p. 16	Axiom 3	uniex 4528
[TakeutiZaring] p. 16	Exercise 6	opth 4323
[TakeutiZaring] p. 16	Exercise 8	rext 4301
[TakeutiZaring] p. 16	Corollary 5.8	unex 4532  unexg 4534
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3715
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3889
[TakeutiZaring] p. 16	Definition 5.6	df-in 3203  df-un 3201
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3902  uniprg 3903
[TakeutiZaring] p. 17	Axiom 4	vpwex 4263
[TakeutiZaring] p. 17	Exercise 1	eltp 3714
[TakeutiZaring] p. 17	Exercise 5	elsuc 4497  elsucg 4495  sstr2 3231
[TakeutiZaring] p. 17	Exercise 6	uncom 3348
[TakeutiZaring] p. 17	Exercise 7	incom 3396
[TakeutiZaring] p. 17	Exercise 8	unass 3361
[TakeutiZaring] p. 17	Exercise 9	inass 3414
[TakeutiZaring] p. 17	Exercise 10	indi 3451
[TakeutiZaring] p. 17	Exercise 11	undi 3452
[TakeutiZaring] p. 17	Definition 5.9	ssalel 3212
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3651
[TakeutiZaring] p. 18	Exercise 7	unss2 3375
[TakeutiZaring] p. 18	Exercise 9	df-ss 3210  dfss2 3214  sseqin2 3423
[TakeutiZaring] p. 18	Exercise 10	ssid 3244
[TakeutiZaring] p. 18	Exercise 12	inss1 3424  inss2 3425
[TakeutiZaring] p. 18	Exercise 13	nssr 3284
[TakeutiZaring] p. 18	Exercise 15	unieq 3897
[TakeutiZaring] p. 18	Exercise 18	sspwb 4302
[TakeutiZaring] p. 18	Exercise 19	pweqb 4309
[TakeutiZaring] p. 20	Definition	df-rab 2517
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4211
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3199
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3493
[TakeutiZaring] p. 20	Proposition 5.15	difid 3560  difidALT 3561
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3504
[TakeutiZaring] p. 21	Theorem 5.22	setind 4631
[TakeutiZaring] p. 21	Definition 5.20	df-v 2801
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4216
[TakeutiZaring] p. 22	Exercise 1	0ss 3530
[TakeutiZaring] p. 22	Exercise 3	ssex 4221  ssexg 4223
[TakeutiZaring] p. 22	Exercise 4	inex1 4218
[TakeutiZaring] p. 22	Exercise 5	ruv 4642
[TakeutiZaring] p. 22	Exercise 6	elirr 4633
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3556
[TakeutiZaring] p. 22	Exercise 11	difdif 3329
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3465
[TakeutiZaring] p. 22	Exercise 14	difss 3330
[TakeutiZaring] p. 22	Exercise 15	sscon 3338
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2513
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2514
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4834  xpexg 4833  xpexgALT 6278
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4726
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5385
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5542  fun11 5388
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5329  svrelfun 5386
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4909
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4911
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4731
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4732
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4728
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5183  dfrel2 5179
[TakeutiZaring] p. 25	Exercise 3	xpss 4827
[TakeutiZaring] p. 25	Exercise 5	relun 4836
[TakeutiZaring] p. 25	Exercise 6	reluni 4842
[TakeutiZaring] p. 25	Exercise 9	inxp 4856
[TakeutiZaring] p. 25	Exercise 12	relres 5033
[TakeutiZaring] p. 25	Exercise 13	opelres 5010  opelresg 5012
[TakeutiZaring] p. 25	Exercise 14	dmres 5026
[TakeutiZaring] p. 25	Exercise 15	resss 5029
[TakeutiZaring] p. 25	Exercise 17	resabs1 5034
[TakeutiZaring] p. 25	Exercise 18	funres 5359
[TakeutiZaring] p. 25	Exercise 24	relco 5227
[TakeutiZaring] p. 25	Exercise 29	funco 5358
[TakeutiZaring] p. 25	Exercise 30	f1co 5543
[TakeutiZaring] p. 26	Definition 6.10	eu2 2122
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5326  fv3 5650
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5267  cnvexg 5266
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4991  dmexg 4988
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4992  rnexg 4989
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5644
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5654  tz6.12 5655  tz6.12c 5657
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5618
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5321
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5322
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5324  wfo 5316
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5323  wf1 5315
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5325  wf1o 5317
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5732  eqfnfv2 5733  eqfnfv2f 5736
[TakeutiZaring] p. 28	Exercise 5	fvco 5704
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5861  fnexALT 6256
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5860  resfunexgALT 6253
[TakeutiZaring] p. 29	Exercise 9	funimaex 5406  funimaexg 5405
[TakeutiZaring] p. 29	Definition 6.18	df-br 4084
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5098  iniseg 5100
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4380
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5327
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5934
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5935
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5940
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5942
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5950
[TakeutiZaring] p. 35	Notation	wtr 4182
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4445
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4186
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4668
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4472
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4476
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4584
[TakeutiZaring] p. 38	Definition 7.11	df-on 4459
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4578
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4644
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4674
[TakeutiZaring] p. 40	Exercise 7	dftr2 4184
[TakeutiZaring] p. 40	Exercise 11	unon 4603
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4579
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3916
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4462
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4506  sucidg 4507
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4593
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4460
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4598  ordelsuc 4597
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4686
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4687
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4688
[TakeutiZaring] p. 43	Axiom 7	omex 4685
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4699
[TakeutiZaring] p. 43	Corollary 7.31	find 4691
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4689
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4690
[TakeutiZaring] p. 44	Exercise 2	int0 3937
[TakeutiZaring] p. 44	Exercise 3	trintssm 4198
[TakeutiZaring] p. 44	Exercise 4	intss1 3938
[TakeutiZaring] p. 44	Exercise 6	onintonm 4609
[TakeutiZaring] p. 44	Definition 7.35	df-int 3924
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6454
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6511  tfri1d 6481
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6512  tfri2d 6482
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6513
[TakeutiZaring] p. 50	Exercise 3	smoiso 6448
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6432
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6610
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6606
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6603
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6607
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6655  nnaordi 6654
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 4010  uniss2 3919
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6616
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6626
[TakeutiZaring] p. 62	Exercise 5	oaword1 6617
[TakeutiZaring] p. 62	Definition 8.15	om0 6604  omsuc 6618
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6627
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6663  nnmordi 6662
[TakeutiZaring] p. 67	Definition 8.30	oei0 6605
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7359
[TakeutiZaring] p. 88	Exercise 1	en0 6947
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 7018
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 7019
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6890  isfi 6912
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6990
[TakeutiZaring] p. 95	Definition 10.42	df-map 6797
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 6996
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 7009
[Tarski] p. 67	Axiom B5	ax-4 1556
[Tarski] p. 68	Lemma 6	equid 1747
[Tarski] p. 69	Lemma 7	equcomi 1750
[Tarski] p. 70	Lemma 14	spim 1784  spime 1787  spimeh 1785  spimh 1783
[Tarski] p. 70	Lemma 16	ax-11 1552  ax-11o 1869  ax11i 1760
[Tarski] p. 70	Lemmas 16 and 17	sb6 1933
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1572
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2202  ax-14 2203
[WhiteheadRussell] p. 96	Axiom *1.3	olc 716
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 732
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 761
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 770
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 794
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 619
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 646
[WhiteheadRussell] p. 100	Theorem *2.04	pm2.04 82
[WhiteheadRussell] p. 100	Theorem *2.05	imim2 55
[WhiteheadRussell] p. 100	Theorem *2.06	imim1 76
[WhiteheadRussell] p. 101	Theorem *2.1	pm2.1dc 842
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2176  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 742
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 841
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 632
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 890
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 848
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 861
[WhiteheadRussell] p. 103	Theorem *2.16	con3 645
[WhiteheadRussell] p. 103	Theorem *2.17	condc 858
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 860
[WhiteheadRussell] p. 104	Theorem *2.2	orc 717
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 780
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 620
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 624
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 898
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 912
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 773
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 774
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 809
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 810
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 808
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 1003
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 783
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 781
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 782
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 743
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 744
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 872  pm2.5gdc 871
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 867
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 745
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 746
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 747
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 659
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 660
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 727
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 896
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 730
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 731
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 870
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 753
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 805
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 806
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 663
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 718  pm2.67 748
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 874  pm2.521gdc 873
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 752
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 815
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 899
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 920
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 811
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 812
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 814
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 813
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 816
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 817
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 910
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 759
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 963
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 964
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 965
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 758
[WhiteheadRussell] p. 111	Theorem *3.21	pm3.21 264
[WhiteheadRussell] p. 111	Theorem *3.22	pm3.22 265
[WhiteheadRussell] p. 111	Theorem *3.24	pm3.24 698
[WhiteheadRussell] p. 112	Theorem *3.35	pm3.35 347
[WhiteheadRussell] p. 112	Theorem *3.3 (Exp)	pm3.3 261
[WhiteheadRussell] p. 112	Theorem *3.31 (Imp)	pm3.31 262
[WhiteheadRussell] p. 112	Theorem *3.26 (Simp)	simpl 109  simplimdc 865
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 864
[WhiteheadRussell] p. 112	Theorem *3.33 (Syll)	pm3.33 345
[WhiteheadRussell] p. 112	Theorem *3.34 (Syll)	pm3.34 346
[WhiteheadRussell] p. 112	Theorem *3.37 (Transp)	pm3.37 693
[WhiteheadRussell] p. 113	Fact)	pm3.45 599
[WhiteheadRussell] p. 113	Theorem *3.4	pm3.4 333
[WhiteheadRussell] p. 113	Theorem *3.41	pm3.41 331
[WhiteheadRussell] p. 113	Theorem *3.42	pm3.42 332
[WhiteheadRussell] p. 113	Theorem *3.44	jao 760  pm3.44 720
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 344
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 604
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 790
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 876
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 877
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 895
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 699
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 958  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 762  pm4.25 763
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 823
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 733
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 772
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 797
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 607
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 827
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 1004
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 821
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 977
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 955
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 784
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 819  pm4.45 789  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1527
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 962
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 902  imorr 726
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 904
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 755
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 756
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 907
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 944
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 757  pm4.56 785
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 945  oranim 786
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 690
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 903
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 891
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 905
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 691
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 906
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 892
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 389  pm4.71d 393  pm4.71i 391  pm4.71r 390  pm4.71rd 394  pm4.71ri 392
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 832
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 749
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 605  pm4.76 606
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 715  pm4.77 804
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 787
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 908
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 712
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 913
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 956
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 957
[WhiteheadRussell] p. 122	Theorem *4.84	imbi1 236
[WhiteheadRussell] p. 122	Theorem *4.85	imbi2 237
[WhiteheadRussell] p. 122	Theorem *4.86	bibi1 240
[WhiteheadRussell] p. 122	Theorem *4.87	bi2.04 248  impexp 263  pm4.87 557
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 603
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 914
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 915
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 917
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 916
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1431
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 833
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 909
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1436  pm5.18dc 888
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 711
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 700
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1434
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1439
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1440
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 900
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 475
[WhiteheadRussell] p. 125	Theorem *5.4	pm5.4 249
[WhiteheadRussell] p. 125	Theorem *5.5	pm5.5 242
[WhiteheadRussell] p. 125	Theorem *5.6	pm5.6dc 931  pm5.6r 932
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 960
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 348
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 453
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 611
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 922
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 612
[WhiteheadRussell] p. 125	Theorem *5.41	imdi 250  pm5.41 251
[WhiteheadRussell] p. 125	Theorem *5.42	pm5.42 320
[WhiteheadRussell] p. 125	Theorem *5.44	pm5.44 930
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 807
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 923
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 918
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 799
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 951
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 952
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 967
[WhiteheadRussell] p. 125	Theorem *5.501	pm5.501 244
[WhiteheadRussell] p. 126	Theorem *5.74	pm5.74 179
[WhiteheadRussell] p. 126	Theorem *5.75	pm5.75 968
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1681
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1531
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1678
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1942
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2080
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2481
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2482
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2941
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3085
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5298
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5299
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2157  eupickbi 2160
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5326
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7363