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 7219  fidcenum 7060
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7060
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7219
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12829
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7031
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 7017
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12844
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12846
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12835  znnen 12802
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12847
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12848
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10923
[AczelRathjen], p. 183	Chapter 20	ax-setind 4586
[AhoHopUll] p. 318	Section 9.1	df-concat 11050  df-pfx 11129  df-substr 11102  df-word 10997  lencl 11000  wrd0 11021
[Apostol] p. 18	Theorem I.1	addcan 8254  addcan2d 8259  addcan2i 8257  addcand 8258  addcani 8256
[Apostol] p. 18	Theorem I.2	negeu 8265
[Apostol] p. 18	Theorem I.3	negsub 8322  negsubd 8391  negsubi 8352
[Apostol] p. 18	Theorem I.4	negneg 8324  negnegd 8376  negnegi 8344
[Apostol] p. 18	Theorem I.5	subdi 8459  subdid 8488  subdii 8481  subdir 8460  subdird 8489  subdiri 8482
[Apostol] p. 18	Theorem I.6	mul01 8463  mul01d 8467  mul01i 8465  mul02 8461  mul02d 8466  mul02i 8464
[Apostol] p. 18	Theorem I.9	divrecapd 8868
[Apostol] p. 18	Theorem I.10	recrecapi 8819
[Apostol] p. 18	Theorem I.12	mul2neg 8472  mul2negd 8487  mul2negi 8480  mulneg1 8469  mulneg1d 8485  mulneg1i 8478
[Apostol] p. 18	Theorem I.14	rdivmuldivd 13939
[Apostol] p. 18	Theorem I.15	divdivdivap 8788
[Apostol] p. 20	Axiom 7	rpaddcl 9801  rpaddcld 9836  rpmulcl 9802  rpmulcld 9837
[Apostol] p. 20	Axiom 9	0nrp 9813
[Apostol] p. 20	Theorem I.17	lttri 8179
[Apostol] p. 20	Theorem I.18	ltadd1d 8613  ltadd1dd 8631  ltadd1i 8577
[Apostol] p. 20	Theorem I.19	ltmul1 8667  ltmul1a 8666  ltmul1i 8995  ltmul1ii 9003  ltmul2 8931  ltmul2d 9863  ltmul2dd 9877  ltmul2i 8998
[Apostol] p. 20	Theorem I.21	0lt1 8201
[Apostol] p. 20	Theorem I.23	lt0neg1 8543  lt0neg1d 8590  ltneg 8537  ltnegd 8598  ltnegi 8568
[Apostol] p. 20	Theorem I.25	lt2add 8520  lt2addd 8642  lt2addi 8585
[Apostol] p. 20	Definition of positive numbers	df-rp 9778
[Apostol] p. 21	Exercise 4	recgt0 8925  recgt0d 9009  recgt0i 8981  recgt0ii 8982
[Apostol] p. 22	Definition of integers	df-z 9375
[Apostol] p. 22	Definition of rationals	df-q 9743
[Apostol] p. 24	Theorem I.26	supeuti 7098
[Apostol] p. 26	Theorem I.29	arch 9294
[Apostol] p. 28	Exercise 2	btwnz 9494
[Apostol] p. 28	Exercise 3	nnrecl 9295
[Apostol] p. 28	Exercise 6	qbtwnre 10401
[Apostol] p. 28	Exercise 10(a)	zeneo 12215  zneo 9476
[Apostol] p. 29	Theorem I.35	resqrtth 11375  sqrtthi 11463
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9041
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12390
[Apostol] p. 363	Remark	absgt0api 11490
[Apostol] p. 363	Example	abssubd 11537  abssubi 11494
[ApostolNT] p. 14	Definition	df-dvds 12132
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 12148
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12172
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12168
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12162
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12164
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 12149
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 12150
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 12155
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12189
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12191
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12193
[ApostolNT] p. 15	Definition	dfgcd2 12368
[ApostolNT] p. 16	Definition	isprm2 12472
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12447
[ApostolNT] p. 16	Theorem 1.7	prminf 12859
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12327
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12369
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12371
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12341
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12334
[ApostolNT] p. 17	Theorem 1.8	coprm 12499
[ApostolNT] p. 17	Theorem 1.9	euclemma 12501
[ApostolNT] p. 17	Theorem 1.10	1arith2 12724
[ApostolNT] p. 19	Theorem 1.14	divalg 12268
[ApostolNT] p. 20	Theorem 1.15	eucalg 12414
[ApostolNT] p. 25	Definition	df-phi 12566
[ApostolNT] p. 26	Theorem 2.2	phisum 12596
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12577
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12581
[ApostolNT] p. 38	Remark	df-sgm 15487
[ApostolNT] p. 38	Definition	df-sgm 15487
[ApostolNT] p. 104	Definition	congr 12455
[ApostolNT] p. 106	Remark	dvdsval3 12135
[ApostolNT] p. 106	Definition	moddvds 12143
[ApostolNT] p. 107	Example 2	mod2eq0even 12222
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12223
[ApostolNT] p. 107	Example 4	zmod1congr 10488
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10525
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10813
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12167
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12458
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 12777
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12460
[ApostolNT] p. 113	Theorem 5.17	eulerth 12588
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12607
[ApostolNT] p. 114	Theorem 5.19	fermltl 12589
[ApostolNT] p. 179	Definition	df-lgs 15508  lgsprme0 15552
[ApostolNT] p. 180	Example 1	1lgs 15553
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 15529
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 15544
[ApostolNT] p. 181	Theorem 9.4	m1lgs 15595
[ApostolNT] p. 181	Theorem 9.5	2lgs 15614  2lgsoddprm 15623
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 15579
[ApostolNT] p. 185	Theorem 9.8	lgsquad 15590
[ApostolNT] p. 188	Definition	df-lgs 15508  lgs1 15554
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 15545
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 15547
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 15555
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 15556
[Bauer] p. 482	Section 1.2	pm2.01 617  pm2.65 661
[Bauer] p. 483	Theorem 1.3	acexmid 5945  onsucelsucexmidlem 4578
[Bauer], p. 481	Section 1.1	pwtrufal 15971
[Bauer], p. 483	Definition	n0rf 3473
[Bauer], p. 483	Theorem 1.2	2irrexpq 15481  2irrexpqap 15483
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6975
[Bauer], p. 493	Section 5.1	ivthdich 15158
[Bauer], p. 494	Theorem 5.5	ivthinc 15148
[BauerHanson], p. 27	Proposition 5.2	cnstab 8720
[BauerSwan], p. 14	Remark	0ct 7211  ctm 7213
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 15974
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7219
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7616
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7529
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7618
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7652  addlocpr 7651
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7678
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7681
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7686
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2057
[BellMachover] p. 460	Notation	df-mo 2058
[BellMachover] p. 460	Definition	mo3 2108  mo3h 2107
[BellMachover] p. 462	Theorem 1.1	bm1.1 2190
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4166
[BellMachover] p. 466	Axiom Pow	axpow3 4222
[BellMachover] p. 466	Axiom Union	axun2 4483
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4591
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4432
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4594
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4545
[BellMachover] p. 471	Definition of Lim	df-ilim 4417
[BellMachover] p. 472	Axiom Inf	zfinf2 4638
[BellMachover] p. 473	Theorem 2.8	limom 4663
[Bobzien] p. 116	Statement T3	stoic3 1451
[Bobzien] p. 117	Statement T2	stoic2a 1449
[Bobzien] p. 117	Statement T4	stoic4a 1452
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1447
[Bollobas] p. 1	Section I.1	df-edg 15686
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13221
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13267
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13282
[BourbakiAlg1] p. 92	Definition 1	df-ring 13793
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 13728
[BourbakiEns] p.	Proposition 8	fcof1 5854  fcofo 5855
[BourbakiTop1] p.	Remark	xnegmnf 9953  xnegpnf 9952
[BourbakiTop1] p.	Remark	rexneg 9954
[BourbakiTop1] p.	Proposition	ishmeo 14809
[BourbakiTop1] p.	Property V_i	ssnei2 14662
[BourbakiTop1] p.	Property V_ii	innei 14668
[BourbakiTop1] p.	Property V_iv	neissex 14670
[BourbakiTop1] p.	Proposition 1	neipsm 14659  neiss 14655
[BourbakiTop1] p.	Proposition 2	cnptopco 14727
[BourbakiTop1] p.	Proposition 4	imasnopn 14804
[BourbakiTop1] p.	Property V_iii	elnei 14657
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14503
[Bruck] p. 1	Section I.1	df-mgm 13221
[Bruck] p. 23	Section II.1	df-sgrp 13267
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13464
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4108
[Cohen] p. 301	Remark	relogoprlem 15373
[Cohen] p. 301	Property 2	relogmul 15374  relogmuld 15389
[Cohen] p. 301	Property 3	relogdiv 15375  relogdivd 15390
[Cohen] p. 301	Property 4	relogexp 15377
[Cohen] p. 301	Property 1a	log1 15371
[Cohen] p. 301	Property 1b	loge 15372
[Cohen4] p. 348	Observation	relogbcxpbap 15470
[Cohen4] p. 352	Definition	rpelogb 15454
[Cohen4] p. 361	Property 2	rprelogbmul 15460
[Cohen4] p. 361	Property 3	logbrec 15465  rprelogbdiv 15462
[Cohen4] p. 361	Property 4	rplogbreexp 15458
[Cohen4] p. 361	Property 6	relogbexpap 15463
[Cohen4] p. 361	Property 1(a)	rplogbid1 15452
[Cohen4] p. 361	Property 1(b)	rplogb1 15453
[Cohen4] p. 367	Property	rplogbchbase 15455
[Cohen4] p. 377	Property 2	logblt 15467
[Crosilla] p.	Axiom 1	ax-ext 2187
[Crosilla] p.	Axiom 2	ax-pr 4254
[Crosilla] p.	Axiom 3	ax-un 4481
[Crosilla] p.	Axiom 4	ax-nul 4171
[Crosilla] p.	Axiom 5	ax-iinf 4637
[Crosilla] p.	Axiom 6	ru 2997
[Crosilla] p.	Axiom 8	ax-pow 4219
[Crosilla] p.	Axiom 9	ax-setind 4586
[Crosilla], p.	Axiom 6	ax-sep 4163
[Crosilla], p.	Axiom 7	ax-coll 4160
[Crosilla], p.	Axiom 7'	repizf 4161
[Crosilla], p.	Theorem is stated	ordtriexmid 4570
[Crosilla], p.	Axiom of choice implies instances	acexmid 5945
[Crosilla], p.	Definition of ordinal	df-iord 4414
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4584
[Eisenberg] p. 67	Definition 5.3	df-dif 3168
[Eisenberg] p. 82	Definition 6.3	df-iom 4640
[Eisenberg] p. 125	Definition 8.21	df-map 6739
[Enderton] p. 18	Axiom of Empty Set	axnul 4170
[Enderton] p. 19	Definition	df-tp 3641
[Enderton] p. 26	Exercise 5	unissb 3880
[Enderton] p. 26	Exercise 10	pwel 4263
[Enderton] p. 28	Exercise 7(b)	pwunim 4334
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3997  iinin2m 3996  iunin1 3992  iunin2 3991
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3995  iundif2ss 3993
[Enderton] p. 33	Exercise 23	iinuniss 4010
[Enderton] p. 33	Exercise 25	iununir 4011
[Enderton] p. 33	Exercise 24(a)	iinpw 4018
[Enderton] p. 33	Exercise 24(b)	iunpw 4528  iunpwss 4019
[Enderton] p. 38	Exercise 6(a)	unipw 4262
[Enderton] p. 38	Exercise 6(b)	pwuni 4237
[Enderton] p. 41	Lemma 3D	opeluu 4498  rnex 4947  rnexg 4944
[Enderton] p. 41	Exercise 8	dmuni 4889  rnuni 5095
[Enderton] p. 42	Definition of a function	dffun7 5299  dffun8 5300
[Enderton] p. 43	Definition of function value	funfvdm2 5645
[Enderton] p. 43	Definition of single-rooted	funcnv 5336
[Enderton] p. 44	Definition (d)	dfima2 5025  dfima3 5026
[Enderton] p. 47	Theorem 3H	fvco2 5650
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7320
[Enderton] p. 50	Theorem 3K(a)	imauni 5832
[Enderton] p. 52	Definition	df-map 6739
[Enderton] p. 53	Exercise 21	coass 5202
[Enderton] p. 53	Exercise 27	dmco 5192
[Enderton] p. 53	Exercise 14(a)	funin 5346
[Enderton] p. 53	Exercise 22(a)	imass2 5059
[Enderton] p. 54	Remark	ixpf 6809  ixpssmap 6821
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6788
[Enderton] p. 56	Theorem 3M	erref 6642
[Enderton] p. 57	Lemma 3N	erthi 6670
[Enderton] p. 57	Definition	df-ec 6624
[Enderton] p. 58	Definition	df-qs 6628
[Enderton] p. 60	Theorem 3Q	th3q 6729  th3qcor 6728  th3qlem1 6726  th3qlem2 6727
[Enderton] p. 61	Exercise 35	df-ec 6624
[Enderton] p. 65	Exercise 56(a)	dmun 4886
[Enderton] p. 68	Definition of successor	df-suc 4419
[Enderton] p. 71	Definition	df-tr 4144  dftr4 4148
[Enderton] p. 72	Theorem 4E	unisuc 4461  unisucg 4462
[Enderton] p. 73	Exercise 6	unisuc 4461  unisucg 4462
[Enderton] p. 73	Exercise 5(a)	truni 4157
[Enderton] p. 73	Exercise 5(b)	trint 4158
[Enderton] p. 79	Theorem 4I(A1)	nna0 6562
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6564  onasuc 6554
[Enderton] p. 79	Definition of operation value	df-ov 5949
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6563
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6565  onmsuc 6561
[Enderton] p. 81	Theorem 4K(1)	nnaass 6573
[Enderton] p. 81	Theorem 4K(2)	nna0r 6566  nnacom 6572
[Enderton] p. 81	Theorem 4K(3)	nndi 6574
[Enderton] p. 81	Theorem 4K(4)	nnmass 6575
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6577
[Enderton] p. 82	Exercise 16	nnm0r 6567  nnmsucr 6576
[Enderton] p. 88	Exercise 23	nnaordex 6616
[Enderton] p. 129	Definition	df-en 6830
[Enderton] p. 132	Theorem 6B(b)	canth 5899
[Enderton] p. 133	Exercise 1	xpomen 12799
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6964
[Enderton] p. 136	Corollary 6E	nneneq 6956
[Enderton] p. 139	Theorem 6H(c)	mapen 6945
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7332
[Enderton] p. 143	Theorem 6J	dju0en 7328  dju1en 7327
[Enderton] p. 144	Corollary 6K	undif2ss 3536
[Enderton] p. 145	Figure 38	ffoss 5556
[Enderton] p. 145	Definition	df-dom 6831
[Enderton] p. 146	Example 1	domen 6842  domeng 6843
[Enderton] p. 146	Example 3	nndomo 6963
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6932  xpdom1g 6930  xpdom2g 6929
[Enderton] p. 168	Definition	df-po 4344
[Enderton] p. 192	Theorem 7M(a)	oneli 4476
[Enderton] p. 192	Theorem 7M(b)	ontr1 4437
[Enderton] p. 192	Theorem 7M(c)	onirri 4592
[Enderton] p. 193	Corollary 7N(b)	0elon 4440
[Enderton] p. 193	Corollary 7N(c)	onsuci 4565
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4538
[Enderton] p. 194	Remark	onprc 4601
[Enderton] p. 194	Exercise 16	suc11 4607
[Enderton] p. 197	Definition	df-card 7288
[Enderton] p. 200	Exercise 25	tfis 4632
[Enderton] p. 206	Theorem 7X(b)	en2lp 4603
[Enderton] p. 207	Exercise 34	opthreg 4605
[Enderton] p. 208	Exercise 35	suc11g 4606
[Geuvers], p. 1	Remark	expap0 10716
[Geuvers], p. 6	Lemma 2.13	mulap0r 8690
[Geuvers], p. 6	Lemma 2.15	mulap0 8729
[Geuvers], p. 9	Lemma 2.35	msqge0 8691
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8046
[Geuvers], p. 10	Lemma 3.9	maxcom 11547
[Geuvers], p. 10	Lemma 3.10	maxle1 11555  maxle2 11556
[Geuvers], p. 10	Lemma 3.11	maxleast 11557
[Geuvers], p. 10	Lemma 3.12	maxleb 11560
[Geuvers], p. 11	Definition 3.13	dfabsmax 11561
[Geuvers], p. 17	Definition 6.1	df-ap 8657
[Gleason] p. 117	Proposition 9-2.1	df-enq 7462  enqer 7473
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7466  df-nqqs 7463
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7459  df-plqqs 7464
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7460  df-mqqs 7465
[Gleason] p. 119	Proposition 9-2.5	df-rq 7467
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7523
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7526  ltbtwnnq 7531  ltbtwnnqq 7530
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7515
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7516
[Gleason] p. 123	Proposition 9-3.5	addclpr 7652
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7694
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7693
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7712
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7728
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7734  ltaprlem 7733
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7731
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7687
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7707
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7696
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7695
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7703
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7753
[Gleason] p. 126	Proposition 9-4.1	df-enr 7841  enrer 7850
[Gleason] p. 126	Proposition 9-4.2	df-0r 7846  df-1r 7847  df-nr 7842
[Gleason] p. 126	Proposition 9-4.3	df-mr 7844  df-plr 7843  negexsr 7887  recexsrlem 7889
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7845
[Gleason] p. 130	Proposition 10-1.3	creui 9035  creur 9034  cru 8677
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8038  axcnre 7996
[Gleason] p. 132	Definition 10-3.1	crim 11202  crimd 11321  crimi 11281  crre 11201  crred 11320  crrei 11280
[Gleason] p. 132	Definition 10-3.2	remim 11204  remimd 11286
[Gleason] p. 133	Definition 10.36	absval2 11401  absval2d 11529  absval2i 11488
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11228  cjaddd 11309  cjaddi 11276
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11229  cjmuld 11310  cjmuli 11277
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11227  cjcjd 11287  cjcji 11259
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11226  cjreb 11210  cjrebd 11290  cjrebi 11262  cjred 11315  rere 11209  rereb 11207  rerebd 11289  rerebi 11261  rered 11313
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11235  addcjd 11301  addcji 11271
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11345
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11396  abscjd 11534  abscji 11492
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11408  abs00d 11530  abs00i 11489  absne0d 11531
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11440  releabsd 11535  releabsi 11493
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11413  absmuld 11538  absmuli 11495
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11399  sqabsaddi 11496
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11448  abstrid 11540  abstrii 11499
[Gleason] p. 134	Definition 10-4.1	df-exp 10686  exp0 10690  expp1 10693  expp1d 10821
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10728  expaddd 10822
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15417  cxpmuld 15442  expmul 10731  expmuld 10823
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10725  mulexpd 10835  rpmulcxp 15414
[Gleason] p. 141	Definition 11-2.1	fzval 10134
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11670
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11672
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11671
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11675
[Gleason] p. 172	Corollary 12-2.5	climrecl 11668
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11664  climcj 11665  climim 11667  climre 11666
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8114  df-xr 8113  ltxr 9899
[Gleason] p. 180	Theorem 12-5.3	climcau 11691
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10445
[Gleason] p. 223	Definition 14-1.1	df-met 14340
[Gleason] p. 223	Definition 14-1.1(a)	met0 14869  xmet0 14868
[Gleason] p. 223	Definition 14-1.1(c)	metsym 14876
[Gleason] p. 223	Definition 14-1.1(d)	mettri 14878  mstri 14978  xmettri 14877  xmstri 14977
[Gleason] p. 230	Proposition 14-2.6	txlm 14784
[Gleason] p. 240	Proposition 14-4.2	metcnp3 15016
[Gleason] p. 243	Proposition 14-4.16	addcn2 11654  addcncntop 15067  mulcn2 11656  mulcncntop 15069  subcn2 11655  subcncntop 15068
[Gleason] p. 295	Remark	bcval3 10898  bcval4 10899
[Gleason] p. 295	Equation 2	bcpasc 10913
[Gleason] p. 295	Definition of binomial coefficient	bcval 10896  df-bc 10895
[Gleason] p. 296	Remark	bcn0 10902  bcnn 10904
[Gleason] p. 296	Theorem 15-2.8	binom 11828
[Gleason] p. 308	Equation 2	ef0 12016
[Gleason] p. 308	Equation 3	efcj 12017
[Gleason] p. 309	Corollary 15-4.3	efne0 12022
[Gleason] p. 309	Corollary 15-4.4	efexp 12026
[Gleason] p. 310	Equation 14	sinadd 12080
[Gleason] p. 310	Equation 15	cosadd 12081
[Gleason] p. 311	Equation 17	sincossq 12092
[Gleason] p. 311	Equation 18	cosbnd 12097  sinbnd 12096
[Gleason] p. 311	Definition of ` `	df-pi 11997
[Golan] p. 1	Remark	srgisid 13781
[Golan] p. 1	Definition	df-srg 13759
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1472
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13376  mndideu 13291
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13403
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13432
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13443
[Herstein] p. 57	Exercise 1	dfgrp3me 13465
[Heyting] p. 127	Axiom #1	ax1hfs 16050
[Hitchcock] p. 5	Rule A3	mptnan 1443
[Hitchcock] p. 5	Rule A4	mptxor 1444
[Hitchcock] p. 5	Rule A5	mtpxor 1446
[HoTT], p.	Lemma 10.4.1	exmidontriim 7339
[HoTT], p.	Theorem 7.2.6	nndceq 6587
[HoTT], p.	Exercise 11.10	neapmkv 16044
[HoTT], p.	Exercise 11.11	mulap0bd 8732
[HoTT], p.	Section 11.2.1	df-iltp 7585  df-imp 7584  df-iplp 7583  df-reap 8650
[HoTT], p.	Theorem 11.2.4	recapb 8746  rerecapb 8918
[HoTT], p.	Corollary 3.9.2	uchoice 6225
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7777
[HoTT], p.	Corollary 11.4.3	conventions 15694
[HoTT], p.	Exercise 11.6(i)	dcapnconst 16037  dceqnconst 16036
[HoTT], p.	Corollary 11.2.13	axcaucvg 8015  caucvgpr 7797  caucvgprpr 7827  caucvgsr 7917
[HoTT], p.	Definition 11.2.1	df-inp 7581
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 16042
[HoTT], p.	Proposition 11.2.3	df-iso 4345  ltpopr 7710  ltsopr 7711
[HoTT], p.	Definition 11.2.7(v)	apsym 8681  reapcotr 8673  reapirr 8652
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8201  gt0add 8648  leadd1 8505  lelttr 8163  lemul1a 8933  lenlt 8150  ltadd1 8504  ltletr 8164  ltmul1 8667  reaplt 8663
[Jech] p. 4	Definition of class	cv 1372  cvjust 2200
[Jech] p. 78	Note	opthprc 4727
[KalishMontague] p. 81	Note 1	ax-i9 1553
[Kreyszig] p. 3	Property M1	metcl 14858  xmetcl 14857
[Kreyszig] p. 4	Property M2	meteq0 14865
[Kreyszig] p. 12	Equation 5	muleqadd 8743
[Kreyszig] p. 18	Definition 1.3-2	mopnval 14947
[Kreyszig] p. 19	Remark	mopntopon 14948
[Kreyszig] p. 19	Theorem T1	mopn0 14993  mopnm 14953
[Kreyszig] p. 19	Theorem T2	unimopn 14991
[Kreyszig] p. 19	Definition of neighborhood	neibl 14996
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 15018
[Kreyszig] p. 25	Definition 1.4-1	lmbr 14718
[Kreyszig] p. 51	Equation 2	lmodvneg1 14125
[Kreyszig] p. 51	Equation 1a	lmod0vs 14116
[Kreyszig] p. 51	Equation 1b	lmodvs0 14117
[Kunen] p. 10	Axiom 0	a9e 1719
[Kunen] p. 12	Axiom 6	zfrep6 4162
[Kunen] p. 24	Definition 10.24	mapval 6749  mapvalg 6747
[Kunen] p. 31	Definition 10.24	mapex 6743
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3937
[Lang] p. 3	Statement	lidrideqd 13246  mndbn0 13296
[Lang] p. 3	Definition	df-mnd 13282
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 13263
[Lang] p. 5	Equation	gsumfzreidx 13706
[Lang] p. 6	Definition	mulgnn0gsum 13497
[Lang] p. 7	Definition	dfgrp2e 13393
[Levy] p. 338	Axiom	df-clab 2192  df-clel 2201  df-cleq 2198
[Lopez-Astorga] p. 12	Rule 1	mptnan 1443
[Lopez-Astorga] p. 12	Rule 2	mptxor 1444
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1446
[Margaris] p. 40	Rule C	exlimiv 1621
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 855
[Margaris] p. 49	Definition	dfbi2 388  dfordc 894  exalim 1525
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 653
[Margaris] p. 89	Theorem 19.2	19.2 1661  r19.2m 3547
[Margaris] p. 89	Theorem 19.3	19.3 1577  19.3h 1576  rr19.3v 2912
[Margaris] p. 89	Theorem 19.5	alcom 1501
[Margaris] p. 89	Theorem 19.6	alexdc 1642  alexim 1668
[Margaris] p. 89	Theorem 19.7	alnex 1522
[Margaris] p. 89	Theorem 19.8	19.8a 1613  spsbe 1865
[Margaris] p. 89	Theorem 19.9	19.9 1667  19.9h 1666  19.9v 1894  exlimd 1620
[Margaris] p. 89	Theorem 19.11	excom 1687  excomim 1686
[Margaris] p. 89	Theorem 19.12	19.12 1688  r19.12 2612
[Margaris] p. 90	Theorem 19.14	exnalim 1669
[Margaris] p. 90	Theorem 19.15	albi 1491  ralbi 2638
[Margaris] p. 90	Theorem 19.16	19.16 1578
[Margaris] p. 90	Theorem 19.17	19.17 1579
[Margaris] p. 90	Theorem 19.18	exbi 1627  rexbi 2639
[Margaris] p. 90	Theorem 19.19	19.19 1689
[Margaris] p. 90	Theorem 19.20	alim 1480  alimd 1544  alimdh 1490  alimdv 1902  ralimdaa 2572  ralimdv 2574  ralimdva 2573  ralimdvva 2575  sbcimdv 3064
[Margaris] p. 90	Theorem 19.21	19.21-2 1690  19.21 1606  19.21bi 1581  19.21h 1580  19.21ht 1604  19.21t 1605  19.21v 1896  alrimd 1633  alrimdd 1632  alrimdh 1502  alrimdv 1899  alrimi 1545  alrimih 1492  alrimiv 1897  alrimivv 1898  r19.21 2582  r19.21be 2597  r19.21bi 2594  r19.21t 2581  r19.21v 2583  ralrimd 2584  ralrimdv 2585  ralrimdva 2586  ralrimdvv 2590  ralrimdvva 2591  ralrimi 2577  ralrimiv 2578  ralrimiva 2579  ralrimivv 2587  ralrimivva 2588  ralrimivvva 2589  ralrimivw 2580  rexlimi 2616
[Margaris] p. 90	Theorem 19.22	2alimdv 1904  2eximdv 1905  exim 1622  eximd 1635  eximdh 1634  eximdv 1903  rexim 2600  reximdai 2604  reximddv 2609  reximddv2 2611  reximdv 2607  reximdv2 2605  reximdva 2608  reximdvai 2606  reximi2 2602
[Margaris] p. 90	Theorem 19.23	19.23 1701  19.23bi 1615  19.23h 1521  19.23ht 1520  19.23t 1700  19.23v 1906  19.23vv 1907  exlimd2 1618  exlimdh 1619  exlimdv 1842  exlimdvv 1921  exlimi 1617  exlimih 1616  exlimiv 1621  exlimivv 1920  r19.23 2614  r19.23v 2615  rexlimd 2620  rexlimdv 2622  rexlimdv3a 2625  rexlimdva 2623  rexlimdva2 2626  rexlimdvaa 2624  rexlimdvv 2630  rexlimdvva 2631  rexlimdvw 2627  rexlimiv 2617  rexlimiva 2618  rexlimivv 2629
[Margaris] p. 90	Theorem 19.24	i19.24 1662
[Margaris] p. 90	Theorem 19.25	19.25 1649
[Margaris] p. 90	Theorem 19.26	19.26-2 1505  19.26-3an 1506  19.26 1504  r19.26-2 2635  r19.26-3 2636  r19.26 2632  r19.26m 2637
[Margaris] p. 90	Theorem 19.27	19.27 1584  19.27h 1583  19.27v 1923  r19.27av 2641  r19.27m 3556  r19.27mv 3557
[Margaris] p. 90	Theorem 19.28	19.28 1586  19.28h 1585  19.28v 1924  r19.28av 2642  r19.28m 3550  r19.28mv 3553  rr19.28v 2913
[Margaris] p. 90	Theorem 19.29	19.29 1643  19.29r 1644  19.29r2 1645  19.29x 1646  r19.29 2643  r19.29d2r 2650  r19.29r 2644
[Margaris] p. 90	Theorem 19.30	19.30dc 1650
[Margaris] p. 90	Theorem 19.31	19.31r 1704
[Margaris] p. 90	Theorem 19.32	19.32dc 1702  19.32r 1703  r19.32r 2652  r19.32vdc 2655  r19.32vr 2654
[Margaris] p. 90	Theorem 19.33	19.33 1507  19.33b2 1652  19.33bdc 1653
[Margaris] p. 90	Theorem 19.34	19.34 1707
[Margaris] p. 90	Theorem 19.35	19.35-1 1647  19.35i 1648
[Margaris] p. 90	Theorem 19.36	19.36-1 1696  19.36aiv 1925  19.36i 1695  r19.36av 2657
[Margaris] p. 90	Theorem 19.37	19.37-1 1697  19.37aiv 1698  r19.37 2658  r19.37av 2659
[Margaris] p. 90	Theorem 19.38	19.38 1699
[Margaris] p. 90	Theorem 19.39	i19.39 1663
[Margaris] p. 90	Theorem 19.40	19.40-2 1655  19.40 1654  r19.40 2660
[Margaris] p. 90	Theorem 19.41	19.41 1709  19.41h 1708  19.41v 1926  19.41vv 1927  19.41vvv 1928  19.41vvvv 1929  r19.41 2661  r19.41v 2662
[Margaris] p. 90	Theorem 19.42	19.42 1711  19.42h 1710  19.42v 1930  19.42vv 1935  19.42vvv 1936  19.42vvvv 1937  r19.42v 2663
[Margaris] p. 90	Theorem 19.43	19.43 1651  r19.43 2664
[Margaris] p. 90	Theorem 19.44	19.44 1705  r19.44av 2665  r19.44mv 3555
[Margaris] p. 90	Theorem 19.45	19.45 1706  r19.45av 2666  r19.45mv 3554
[Margaris] p. 110	Exercise 2(b)	eu1 2079
[Megill] p. 444	Axiom C5	ax-17 1549
[Megill] p. 445	Lemma L12	alequcom 1538  ax-10 1528
[Megill] p. 446	Lemma L17	equtrr 1733
[Megill] p. 446	Lemma L19	hbnae 1744
[Megill] p. 447	Remark 9.1	df-sb 1786  sbid 1797
[Megill] p. 448	Scheme C5'	ax-4 1533
[Megill] p. 448	Scheme C6'	ax-7 1471
[Megill] p. 448	Scheme C8'	ax-8 1527
[Megill] p. 448	Scheme C9'	ax-i12 1530
[Megill] p. 448	Scheme C11'	ax-10o 1739
[Megill] p. 448	Scheme C12'	ax-13 2178
[Megill] p. 448	Scheme C13'	ax-14 2179
[Megill] p. 448	Scheme C15'	ax-11o 1846
[Megill] p. 448	Scheme C16'	ax-16 1837
[Megill] p. 448	Theorem 9.4	dral1 1753  dral2 1754  drex1 1821  drex2 1755  drsb1 1822  drsb2 1864
[Megill] p. 449	Theorem 9.7	sbcom2 2015  sbequ 1863  sbid2v 2024
[Megill] p. 450	Example in Appendix	hba1 1563
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3081  rspsbca 3082  stdpc4 1798
[Mendelson] p. 69	Axiom 5	ra5 3087  stdpc5 1607
[Mendelson] p. 81	Rule C	exlimiv 1621
[Mendelson] p. 95	Axiom 6	stdpc6 1726
[Mendelson] p. 95	Axiom 7	stdpc7 1793
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3497
[Mendelson] p. 231	Exercise 4.10(l)	unv 3498
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3413
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3461
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3414
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3304
[Mendelson] p. 231	Definition of union	unssin 3412
[Mendelson] p. 235	Exercise 4.12(c)	univ 4524
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3849
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4330
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4331
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4332
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3870
[Mendelson] p. 235	Exercise 4.12(p)	reli 4808
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5204
[Mendelson] p. 246	Definition of successor	df-suc 4419
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6944
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6918  xpsneng 6919
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6924  xpcomeng 6925
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6927
[Mendelson] p. 255	Exercise 4.39	endisj 6921
[Mendelson] p. 255	Exercise 4.41	mapprc 6741
[Mendelson] p. 255	Exercise 4.43	mapsnen 6905
[Mendelson] p. 255	Exercise 4.47	xpmapen 6949
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6775
[Mendelson] p. 255	Exercise 4.42(b)	map1 6906
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7331  djucomen 7330
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7329
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6555
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3395
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4764
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4765
[Monk1] p. 34	Definition 3.3	df-opab 4107
[Monk1] p. 36	Theorem 3.7(i)	coi1 5199  coi2 5200
[Monk1] p. 36	Theorem 3.8(v)	dm0 4893  rn0 4935
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5088
[Monk1] p. 37	Theorem 3.13(i)	relxp 4785
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4899  rnxpm 5113
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4756  xp0 5103
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5042
[Monk1] p. 38	Theorem 3.16(viii)	imai 5039
[Monk1] p. 39	Theorem 3.17	imaex 5038  imaexg 5037
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5034
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5712  funfvop 5694
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5624
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5632
[Monk1] p. 43	Theorem 4.6	funun 5316
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5839  dff13f 5841
[Monk1] p. 46	Theorem 4.15(v)	funex 5809  funrnex 6201
[Monk1] p. 50	Definition 5.4	fniunfv 5833
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5167
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3901
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6243  df-1st 6228
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6244  df-2nd 6229
[Monk2] p. 105	Axiom C4	ax-5 1470
[Monk2] p. 105	Axiom C7	ax-8 1527
[Monk2] p. 105	Axiom C8	ax-11 1529  ax-11o 1846
[Monk2] p. 105	Axiom (C8)	ax11v 1850
[Monk2] p. 109	Lemma 12	ax-7 1471
[Monk2] p. 109	Lemma 15	equvin 1886  equvini 1781  eqvinop 4288
[Monk2] p. 113	Axiom C5-1	ax-17 1549
[Monk2] p. 113	Axiom C5-2	ax6b 1674
[Monk2] p. 113	Axiom C5-3	ax-7 1471
[Monk2] p. 114	Lemma 22	hba1 1563
[Monk2] p. 114	Lemma 23	hbia1 1575  nfia1 1603
[Monk2] p. 114	Lemma 24	hba2 1574  nfa2 1602
[Moschovakis] p. 2	Chapter 2	df-stab 833  dftest 16051
[Munkres] p. 77	Example 2	distop 14590
[Munkres] p. 78	Definition of basis	df-bases 14548  isbasis3g 14551
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 13125  tgval2 14556
[Munkres] p. 79	Remark	tgcl 14569
[Munkres] p. 80	Lemma 2.1	tgval3 14563
[Munkres] p. 80	Lemma 2.2	tgss2 14584  tgss3 14583
[Munkres] p. 81	Lemma 2.3	basgen 14585  basgen2 14586
[Munkres] p. 89	Definition of subspace topology	resttop 14675
[Munkres] p. 93	Theorem 6.1(1)	0cld 14617  topcld 14614
[Munkres] p. 93	Theorem 6.1(3)	uncld 14618
[Munkres] p. 94	Definition of closure	clsval 14616
[Munkres] p. 94	Definition of interior	ntrval 14615
[Munkres] p. 102	Definition of continuous function	df-cn 14693  iscn 14702  iscn2 14705
[Munkres] p. 107	Theorem 7.2(g)	cncnp 14735  cncnp2m 14736  cncnpi 14733  df-cnp 14694  iscnp 14704
[Munkres] p. 127	Theorem 10.1	metcn 15019
[Pierik], p. 8	Section 2.2.1	dfrex2fin 7002
[Pierik], p. 9	Definition 2.4	df-womni 7268
[Pierik], p. 9	Definition 2.5	df-markov 7256  omniwomnimkv 7271
[Pierik], p. 10	Section 2.3	dfdif3 3283
[Pierik], p. 14	Definition 3.1	df-omni 7239  exmidomniim 7245  finomni 7244
[Pierik], p. 15	Section 3.1	df-nninf 7224
[Pradic2025], p. 2	Section 1.1	nnnninfen 15995
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 15999
[PradicBrown2022], p. 2	Remark	exmidpw 7007
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7311
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7312  exmidfodomrlemrALT 7313
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7253
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 15981  peano4nninf 15980
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 15983
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 15991
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 15993
[PradicBrown2022], p. 5	Definition 3.3	nnsf 15979
[Quine] p. 16	Definition 2.1	df-clab 2192  rabid 2682
[Quine] p. 17	Definition 2.1''	dfsb7 2019
[Quine] p. 18	Definition 2.7	df-cleq 2198
[Quine] p. 19	Definition 2.9	df-v 2774
[Quine] p. 34	Theorem 5.1	abeq2 2314
[Quine] p. 35	Theorem 5.2	abid2 2326  abid2f 2374
[Quine] p. 40	Theorem 6.1	sb5 1911
[Quine] p. 40	Theorem 6.2	sb56 1909  sb6 1910
[Quine] p. 41	Theorem 6.3	df-clel 2201
[Quine] p. 41	Theorem 6.4	eqid 2205
[Quine] p. 41	Theorem 6.5	eqcom 2207
[Quine] p. 42	Theorem 6.6	df-sbc 2999
[Quine] p. 42	Theorem 6.7	dfsbcq 3000  dfsbcq2 3001
[Quine] p. 43	Theorem 6.8	vex 2775
[Quine] p. 43	Theorem 6.9	isset 2778
[Quine] p. 44	Theorem 7.3	spcgf 2855  spcgv 2860  spcimgf 2853
[Quine] p. 44	Theorem 6.11	spsbc 3010  spsbcd 3011
[Quine] p. 44	Theorem 6.12	elex 2783
[Quine] p. 44	Theorem 6.13	elab 2917  elabg 2919  elabgf 2915
[Quine] p. 44	Theorem 6.14	noel 3464
[Quine] p. 48	Theorem 7.2	snprc 3698
[Quine] p. 48	Definition 7.1	df-pr 3640  df-sn 3639
[Quine] p. 49	Theorem 7.4	snss 3768  snssg 3767
[Quine] p. 49	Theorem 7.5	prss 3789  prssg 3790
[Quine] p. 49	Theorem 7.6	prid1 3739  prid1g 3737  prid2 3740  prid2g 3738  snid 3664  snidg 3662
[Quine] p. 51	Theorem 7.12	snexg 4229  snexprc 4231
[Quine] p. 51	Theorem 7.13	prexg 4256
[Quine] p. 53	Theorem 8.2	unisn 3866  unisng 3867
[Quine] p. 53	Theorem 8.3	uniun 3869
[Quine] p. 54	Theorem 8.6	elssuni 3878
[Quine] p. 54	Theorem 8.7	uni0 3877
[Quine] p. 56	Theorem 8.17	uniabio 5243
[Quine] p. 56	Definition 8.18	dfiota2 5234
[Quine] p. 57	Theorem 8.19	iotaval 5244
[Quine] p. 57	Theorem 8.22	iotanul 5248
[Quine] p. 58	Theorem 8.23	euiotaex 5249
[Quine] p. 58	Definition 9.1	df-op 3642
[Quine] p. 61	Theorem 9.5	opabid 4303  opabidw 4304  opelopab 4319  opelopaba 4313  opelopabaf 4321  opelopabf 4322  opelopabg 4315  opelopabga 4310  opelopabgf 4317  oprabid 5978
[Quine] p. 64	Definition 9.11	df-xp 4682
[Quine] p. 64	Definition 9.12	df-cnv 4684
[Quine] p. 64	Definition 9.15	df-id 4341
[Quine] p. 65	Theorem 10.3	fun0 5333
[Quine] p. 65	Theorem 10.4	funi 5304
[Quine] p. 65	Theorem 10.5	funsn 5323  funsng 5321
[Quine] p. 65	Definition 10.1	df-fun 5274
[Quine] p. 65	Definition 10.2	args 5052  dffv4g 5575
[Quine] p. 68	Definition 10.11	df-fv 5280  fv2 5573
[Quine] p. 124	Theorem 17.3	nn0opth2 10871  nn0opth2d 10870  nn0opthd 10869
[Quine] p. 284	Axiom 39(vi)	funimaex 5360  funimaexg 5359
[Roman] p. 18	Part Preliminaries	df-rng 13728
[Roman] p. 19	Part Preliminaries	df-ring 13793
[Rudin] p. 164	Equation 27	efcan 12020
[Rudin] p. 164	Equation 30	efzval 12027
[Rudin] p. 167	Equation 48	absefi 12113
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1446
[Sanford] p. 39	Rule 4	mptxor 1444
[Sanford] p. 40	Rule 1	mptnan 1443
[Schechter] p. 51	Definition of antisymmetry	intasym 5068
[Schechter] p. 51	Definition of irreflexivity	intirr 5070
[Schechter] p. 51	Definition of symmetry	cnvsym 5067
[Schechter] p. 51	Definition of transitivity	cotr 5065
[Schechter] p. 187	Definition of "ring with unit"	isring 13795
[Schechter] p. 428	Definition 15.35	bastop1 14588
[Stoll] p. 13	Definition of symmetric difference	symdif1 3438
[Stoll] p. 16	Exercise 4.4	0dif 3532  dif0 3531
[Stoll] p. 16	Exercise 4.8	difdifdirss 3545
[Stoll] p. 19	Theorem 5.2(13)	undm 3431
[Stoll] p. 19	Theorem 5.2(13')	indmss 3432
[Stoll] p. 20	Remark	invdif 3415
[Stoll] p. 25	Definition of ordered triple	df-ot 3643
[Stoll] p. 43	Definition	uniiun 3981
[Stoll] p. 44	Definition	intiin 3982
[Stoll] p. 45	Definition	df-iin 3930
[Stoll] p. 45	Definition indexed union	df-iun 3929
[Stoll] p. 176	Theorem 3.4(27)	imandc 891  imanst 890
[Stoll] p. 262	Example 4.1	symdif1 3438
[Suppes] p. 22	Theorem 2	eq0 3479
[Suppes] p. 22	Theorem 4	eqss 3208  eqssd 3210  eqssi 3209
[Suppes] p. 23	Theorem 5	ss0 3501  ss0b 3500
[Suppes] p. 23	Theorem 6	sstr 3201
[Suppes] p. 25	Theorem 12	elin 3356  elun 3314
[Suppes] p. 26	Theorem 15	inidm 3382
[Suppes] p. 26	Theorem 16	in0 3495
[Suppes] p. 27	Theorem 23	unidm 3316
[Suppes] p. 27	Theorem 24	un0 3494
[Suppes] p. 27	Theorem 25	ssun1 3336
[Suppes] p. 27	Theorem 26	ssequn1 3343
[Suppes] p. 27	Theorem 27	unss 3347
[Suppes] p. 27	Theorem 28	indir 3422
[Suppes] p. 27	Theorem 29	undir 3423
[Suppes] p. 28	Theorem 32	difid 3529  difidALT 3530
[Suppes] p. 29	Theorem 33	difin 3410
[Suppes] p. 29	Theorem 34	indif 3416
[Suppes] p. 29	Theorem 35	undif1ss 3535
[Suppes] p. 29	Theorem 36	difun2 3540
[Suppes] p. 29	Theorem 37	difin0 3534
[Suppes] p. 29	Theorem 38	disjdif 3533
[Suppes] p. 29	Theorem 39	difundi 3425
[Suppes] p. 29	Theorem 40	difindiss 3427
[Suppes] p. 30	Theorem 41	nalset 4175
[Suppes] p. 39	Theorem 61	uniss 3871
[Suppes] p. 39	Theorem 65	uniop 4301
[Suppes] p. 41	Theorem 70	intsn 3920
[Suppes] p. 42	Theorem 71	intpr 3917  intprg 3918
[Suppes] p. 42	Theorem 73	op1stb 4526  op1stbg 4527
[Suppes] p. 42	Theorem 78	intun 3916
[Suppes] p. 44	Definition 15(a)	dfiun2 3961  dfiun2g 3959
[Suppes] p. 44	Definition 15(b)	dfiin2 3962
[Suppes] p. 47	Theorem 86	elpw 3622  elpw2 4202  elpw2g 4201  elpwg 3624
[Suppes] p. 47	Theorem 87	pwid 3631
[Suppes] p. 47	Theorem 89	pw0 3780
[Suppes] p. 48	Theorem 90	pwpw0ss 3845
[Suppes] p. 52	Theorem 101	xpss12 4783
[Suppes] p. 52	Theorem 102	xpindi 4814  xpindir 4815
[Suppes] p. 52	Theorem 103	xpundi 4732  xpundir 4733
[Suppes] p. 54	Theorem 105	elirrv 4597
[Suppes] p. 58	Theorem 2	relss 4763
[Suppes] p. 59	Theorem 4	eldm 4876  eldm2 4877  eldm2g 4875  eldmg 4874
[Suppes] p. 59	Definition 3	df-dm 4686
[Suppes] p. 60	Theorem 6	dmin 4887
[Suppes] p. 60	Theorem 8	rnun 5092
[Suppes] p. 60	Theorem 9	rnin 5093
[Suppes] p. 60	Definition 4	dfrn2 4867
[Suppes] p. 61	Theorem 11	brcnv 4862  brcnvg 4860
[Suppes] p. 62	Equation 5	elcnv 4856  elcnv2 4857
[Suppes] p. 62	Theorem 12	relcnv 5061
[Suppes] p. 62	Theorem 15	cnvin 5091
[Suppes] p. 62	Theorem 16	cnvun 5089
[Suppes] p. 63	Theorem 20	co02 5197
[Suppes] p. 63	Theorem 21	dmcoss 4949
[Suppes] p. 63	Definition 7	df-co 4685
[Suppes] p. 64	Theorem 26	cnvco 4864
[Suppes] p. 64	Theorem 27	coass 5202
[Suppes] p. 65	Theorem 31	resundi 4973
[Suppes] p. 65	Theorem 34	elima 5028  elima2 5029  elima3 5030  elimag 5027
[Suppes] p. 65	Theorem 35	imaundi 5096
[Suppes] p. 66	Theorem 40	dminss 5098
[Suppes] p. 66	Theorem 41	imainss 5099
[Suppes] p. 67	Exercise 11	cnvxp 5102
[Suppes] p. 81	Definition 34	dfec2 6625
[Suppes] p. 82	Theorem 72	elec 6663  elecg 6662
[Suppes] p. 82	Theorem 73	erth 6668  erth2 6669
[Suppes] p. 89	Theorem 96	map0b 6776
[Suppes] p. 89	Theorem 97	map0 6778  map0g 6777
[Suppes] p. 89	Theorem 98	mapsn 6779
[Suppes] p. 89	Theorem 99	mapss 6780
[Suppes] p. 92	Theorem 1	enref 6858  enrefg 6857
[Suppes] p. 92	Theorem 2	ensym 6875  ensymb 6874  ensymi 6876
[Suppes] p. 92	Theorem 3	entr 6878
[Suppes] p. 92	Theorem 4	unen 6910
[Suppes] p. 94	Theorem 15	endom 6856
[Suppes] p. 94	Theorem 16	ssdomg 6872
[Suppes] p. 94	Theorem 17	domtr 6879
[Suppes] p. 95	Theorem 18	isbth 7071
[Suppes] p. 98	Exercise 4	fundmen 6900  fundmeng 6901
[Suppes] p. 98	Exercise 6	xpdom3m 6931
[Suppes] p. 130	Definition 3	df-tr 4144
[Suppes] p. 132	Theorem 9	ssonuni 4537
[Suppes] p. 134	Definition 6	df-suc 4419
[Suppes] p. 136	Theorem Schema 22	findes 4652  finds 4649  finds1 4651  finds2 4650
[Suppes] p. 162	Definition 5	df-ltnqqs 7468  df-ltpq 7461
[Suppes] p. 228	Theorem Schema 61	onintss 4438
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2187
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2198
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2201
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2200
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2223
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5950
[TakeutiZaring] p. 14	Proposition 4.14	ru 2997
[TakeutiZaring] p. 15	Exercise 1	elpr 3654  elpr2 3655  elprg 3653
[TakeutiZaring] p. 15	Exercise 2	elsn 3649  elsn2 3667  elsn2g 3666  elsng 3648  velsn 3650
[TakeutiZaring] p. 15	Exercise 3	elop 4276
[TakeutiZaring] p. 15	Exercise 4	sneq 3644  sneqr 3801
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3652  dfsn2 3647
[TakeutiZaring] p. 16	Axiom 3	uniex 4485
[TakeutiZaring] p. 16	Exercise 6	opth 4282
[TakeutiZaring] p. 16	Exercise 8	rext 4260
[TakeutiZaring] p. 16	Corollary 5.8	unex 4489  unexg 4491
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3682
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3851
[TakeutiZaring] p. 16	Definition 5.6	df-in 3172  df-un 3170
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3864  uniprg 3865
[TakeutiZaring] p. 17	Axiom 4	vpwex 4224
[TakeutiZaring] p. 17	Exercise 1	eltp 3681
[TakeutiZaring] p. 17	Exercise 5	elsuc 4454  elsucg 4452  sstr2 3200
[TakeutiZaring] p. 17	Exercise 6	uncom 3317
[TakeutiZaring] p. 17	Exercise 7	incom 3365
[TakeutiZaring] p. 17	Exercise 8	unass 3330
[TakeutiZaring] p. 17	Exercise 9	inass 3383
[TakeutiZaring] p. 17	Exercise 10	indi 3420
[TakeutiZaring] p. 17	Exercise 11	undi 3421
[TakeutiZaring] p. 17	Definition 5.9	ssalel 3181
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3618
[TakeutiZaring] p. 18	Exercise 7	unss2 3344
[TakeutiZaring] p. 18	Exercise 9	df-ss 3179  dfss2 3183  sseqin2 3392
[TakeutiZaring] p. 18	Exercise 10	ssid 3213
[TakeutiZaring] p. 18	Exercise 12	inss1 3393  inss2 3394
[TakeutiZaring] p. 18	Exercise 13	nssr 3253
[TakeutiZaring] p. 18	Exercise 15	unieq 3859
[TakeutiZaring] p. 18	Exercise 18	sspwb 4261
[TakeutiZaring] p. 18	Exercise 19	pweqb 4268
[TakeutiZaring] p. 20	Definition	df-rab 2493
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4172
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3168
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3462
[TakeutiZaring] p. 20	Proposition 5.15	difid 3529  difidALT 3530
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3473
[TakeutiZaring] p. 21	Theorem 5.22	setind 4588
[TakeutiZaring] p. 21	Definition 5.20	df-v 2774
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4177
[TakeutiZaring] p. 22	Exercise 1	0ss 3499
[TakeutiZaring] p. 22	Exercise 3	ssex 4182  ssexg 4184
[TakeutiZaring] p. 22	Exercise 4	inex1 4179
[TakeutiZaring] p. 22	Exercise 5	ruv 4599
[TakeutiZaring] p. 22	Exercise 6	elirr 4590
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3525
[TakeutiZaring] p. 22	Exercise 11	difdif 3298
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3434
[TakeutiZaring] p. 22	Exercise 14	difss 3299
[TakeutiZaring] p. 22	Exercise 15	sscon 3307
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2489
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2490
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4791  xpexg 4790  xpexgALT 6220
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4683
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5339
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5494  fun11 5342
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5283  svrelfun 5340
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4866
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4868
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4688
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4689
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4685
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5138  dfrel2 5134
[TakeutiZaring] p. 25	Exercise 3	xpss 4784
[TakeutiZaring] p. 25	Exercise 5	relun 4793
[TakeutiZaring] p. 25	Exercise 6	reluni 4799
[TakeutiZaring] p. 25	Exercise 9	inxp 4813
[TakeutiZaring] p. 25	Exercise 12	relres 4988
[TakeutiZaring] p. 25	Exercise 13	opelres 4965  opelresg 4967
[TakeutiZaring] p. 25	Exercise 14	dmres 4981
[TakeutiZaring] p. 25	Exercise 15	resss 4984
[TakeutiZaring] p. 25	Exercise 17	resabs1 4989
[TakeutiZaring] p. 25	Exercise 18	funres 5313
[TakeutiZaring] p. 25	Exercise 24	relco 5182
[TakeutiZaring] p. 25	Exercise 29	funco 5312
[TakeutiZaring] p. 25	Exercise 30	f1co 5495
[TakeutiZaring] p. 26	Definition 6.10	eu2 2098
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5280  fv3 5601
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5222  cnvexg 5221
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4946  dmexg 4943
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4947  rnexg 4944
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5595
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5605  tz6.12 5606  tz6.12c 5608
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5569
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5275
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5276
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5278  wfo 5270
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5277  wf1 5269
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5279  wf1o 5271
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5679  eqfnfv2 5680  eqfnfv2f 5683
[TakeutiZaring] p. 28	Exercise 5	fvco 5651
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5808  fnexALT 6198
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5807  resfunexgALT 6195
[TakeutiZaring] p. 29	Exercise 9	funimaex 5360  funimaexg 5359
[TakeutiZaring] p. 29	Definition 6.18	df-br 4046
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5053  iniseg 5055
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4337
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5281
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5881
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5882
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5887
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5889
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5897
[TakeutiZaring] p. 35	Notation	wtr 4143
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4402
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4147
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4625
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4429
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4433
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4541
[TakeutiZaring] p. 38	Definition 7.11	df-on 4416
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4535
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4601
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4631
[TakeutiZaring] p. 40	Exercise 7	dftr2 4145
[TakeutiZaring] p. 40	Exercise 11	unon 4560
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4536
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3878
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4419
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4463  sucidg 4464
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4550
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4417
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4555  ordelsuc 4554
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4643
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4644
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4645
[TakeutiZaring] p. 43	Axiom 7	omex 4642
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4656
[TakeutiZaring] p. 43	Corollary 7.31	find 4648
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4646
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4647
[TakeutiZaring] p. 44	Exercise 2	int0 3899
[TakeutiZaring] p. 44	Exercise 3	trintssm 4159
[TakeutiZaring] p. 44	Exercise 4	intss1 3900
[TakeutiZaring] p. 44	Exercise 6	onintonm 4566
[TakeutiZaring] p. 44	Definition 7.35	df-int 3886
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6396
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6453  tfri1d 6423
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6454  tfri2d 6424
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6455
[TakeutiZaring] p. 50	Exercise 3	smoiso 6390
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6374
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6552
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6548
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6545
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6549
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6597  nnaordi 6596
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3972  uniss2 3881
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6558
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6568
[TakeutiZaring] p. 62	Exercise 5	oaword1 6559
[TakeutiZaring] p. 62	Definition 8.15	om0 6546  omsuc 6560
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6569
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6605  nnmordi 6604
[TakeutiZaring] p. 67	Definition 8.30	oei0 6547
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7296
[TakeutiZaring] p. 88	Exercise 1	en0 6889
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6956
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6957
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6832  isfi 6854
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6928
[TakeutiZaring] p. 95	Definition 10.42	df-map 6739
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 6934
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6947
[Tarski] p. 67	Axiom B5	ax-4 1533
[Tarski] p. 68	Lemma 6	equid 1724
[Tarski] p. 69	Lemma 7	equcomi 1727
[Tarski] p. 70	Lemma 14	spim 1761  spime 1764  spimeh 1762  spimh 1760
[Tarski] p. 70	Lemma 16	ax-11 1529  ax-11o 1846  ax11i 1737
[Tarski] p. 70	Lemmas 16 and 17	sb6 1910
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1549
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2178  ax-14 2179
[WhiteheadRussell] p. 96	Axiom *1.3	olc 713
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 729
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 758
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 767
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 791
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 617
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 644
[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 839
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2152  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 739
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 838
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 630
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 887
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 845
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 858
[WhiteheadRussell] p. 103	Theorem *2.16	con3 643
[WhiteheadRussell] p. 103	Theorem *2.17	condc 855
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 857
[WhiteheadRussell] p. 104	Theorem *2.2	orc 714
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 777
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 618
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 622
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 895
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 909
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 770
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 771
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 806
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 807
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 805
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 982
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 780
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 778
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 779
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 740
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 741
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 869  pm2.5gdc 868
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 864
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 742
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 743
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 744
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 657
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 658
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 724
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 893
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 727
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 728
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 867
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 750
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 802
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 803
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 661
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 715  pm2.67 745
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 871  pm2.521gdc 870
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 749
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 812
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 896
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 917
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 808
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 809
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 811
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 810
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 813
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 814
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 907
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 756
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 960
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 961
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 962
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 755
[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 695
[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 862
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 861
[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 691
[WhiteheadRussell] p. 113	Fact)	pm3.45 597
[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 757  pm3.44 717
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 344
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 602
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 787
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 873
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 874
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 892
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 696
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 955  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 759  pm4.25 760
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 820
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 730
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 769
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 794
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 605
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 824
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 983
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 818
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 974
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 952
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 781
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 816  pm4.45 786  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1504
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 959
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 899  imorr 723
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 901
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 752
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 753
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 904
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 941
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 754  pm4.56 782
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 942  oranim 783
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 688
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 900
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 888
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 902
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 689
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 903
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 889
[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 829
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 746
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 603  pm4.76 604
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 712  pm4.77 801
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 784
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 905
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 709
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 910
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 953
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 954
[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 601
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 911
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 912
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 914
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 913
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1409
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 830
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 906
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1414  pm5.18dc 885
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 708
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 697
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1412
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1417
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1418
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 897
[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 928  pm5.6r 929
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 957
[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 609
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 919
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 610
[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 927
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 804
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 920
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 915
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 796
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 948
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 949
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 964
[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 965
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1658
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1508
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1655
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1919
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2057
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2457
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2458
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2911
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3055
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5252
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5253
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2133  eupickbi 2136
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5280
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7300