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 7190  fidcenum 7031
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7031
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7190
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12669
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7002
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6988
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12684
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12686
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12675  znnen 12642
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12687
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12688
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10887
[AczelRathjen], p. 183	Chapter 20	ax-setind 4574
[AhoHopUll] p. 318	Section 9.1	df-word 10955  lencl 10958  wrd0 10979
[Apostol] p. 18	Theorem I.1	addcan 8225  addcan2d 8230  addcan2i 8228  addcand 8229  addcani 8227
[Apostol] p. 18	Theorem I.2	negeu 8236
[Apostol] p. 18	Theorem I.3	negsub 8293  negsubd 8362  negsubi 8323
[Apostol] p. 18	Theorem I.4	negneg 8295  negnegd 8347  negnegi 8315
[Apostol] p. 18	Theorem I.5	subdi 8430  subdid 8459  subdii 8452  subdir 8431  subdird 8460  subdiri 8453
[Apostol] p. 18	Theorem I.6	mul01 8434  mul01d 8438  mul01i 8436  mul02 8432  mul02d 8437  mul02i 8435
[Apostol] p. 18	Theorem I.9	divrecapd 8839
[Apostol] p. 18	Theorem I.10	recrecapi 8790
[Apostol] p. 18	Theorem I.12	mul2neg 8443  mul2negd 8458  mul2negi 8451  mulneg1 8440  mulneg1d 8456  mulneg1i 8449
[Apostol] p. 18	Theorem I.14	rdivmuldivd 13778
[Apostol] p. 18	Theorem I.15	divdivdivap 8759
[Apostol] p. 20	Axiom 7	rpaddcl 9771  rpaddcld 9806  rpmulcl 9772  rpmulcld 9807
[Apostol] p. 20	Axiom 9	0nrp 9783
[Apostol] p. 20	Theorem I.17	lttri 8150
[Apostol] p. 20	Theorem I.18	ltadd1d 8584  ltadd1dd 8602  ltadd1i 8548
[Apostol] p. 20	Theorem I.19	ltmul1 8638  ltmul1a 8637  ltmul1i 8966  ltmul1ii 8974  ltmul2 8902  ltmul2d 9833  ltmul2dd 9847  ltmul2i 8969
[Apostol] p. 20	Theorem I.21	0lt1 8172
[Apostol] p. 20	Theorem I.23	lt0neg1 8514  lt0neg1d 8561  ltneg 8508  ltnegd 8569  ltnegi 8539
[Apostol] p. 20	Theorem I.25	lt2add 8491  lt2addd 8613  lt2addi 8556
[Apostol] p. 20	Definition of positive numbers	df-rp 9748
[Apostol] p. 21	Exercise 4	recgt0 8896  recgt0d 8980  recgt0i 8952  recgt0ii 8953
[Apostol] p. 22	Definition of integers	df-z 9346
[Apostol] p. 22	Definition of rationals	df-q 9713
[Apostol] p. 24	Theorem I.26	supeuti 7069
[Apostol] p. 26	Theorem I.29	arch 9265
[Apostol] p. 28	Exercise 2	btwnz 9464
[Apostol] p. 28	Exercise 3	nnrecl 9266
[Apostol] p. 28	Exercise 6	qbtwnre 10365
[Apostol] p. 28	Exercise 10(a)	zeneo 12055  zneo 9446
[Apostol] p. 29	Theorem I.35	resqrtth 11215  sqrtthi 11303
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9012
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12230
[Apostol] p. 363	Remark	absgt0api 11330
[Apostol] p. 363	Example	abssubd 11377  abssubi 11334
[ApostolNT] p. 14	Definition	df-dvds 11972
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11988
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12012
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12008
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12002
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12004
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11989
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11990
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11995
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12029
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12031
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12033
[ApostolNT] p. 15	Definition	dfgcd2 12208
[ApostolNT] p. 16	Definition	isprm2 12312
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12287
[ApostolNT] p. 16	Theorem 1.7	prminf 12699
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12167
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12209
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12211
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12181
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12174
[ApostolNT] p. 17	Theorem 1.8	coprm 12339
[ApostolNT] p. 17	Theorem 1.9	euclemma 12341
[ApostolNT] p. 17	Theorem 1.10	1arith2 12564
[ApostolNT] p. 19	Theorem 1.14	divalg 12108
[ApostolNT] p. 20	Theorem 1.15	eucalg 12254
[ApostolNT] p. 25	Definition	df-phi 12406
[ApostolNT] p. 26	Theorem 2.2	phisum 12436
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12417
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12421
[ApostolNT] p. 38	Remark	df-sgm 15326
[ApostolNT] p. 38	Definition	df-sgm 15326
[ApostolNT] p. 104	Definition	congr 12295
[ApostolNT] p. 106	Remark	dvdsval3 11975
[ApostolNT] p. 106	Definition	moddvds 11983
[ApostolNT] p. 107	Example 2	mod2eq0even 12062
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12063
[ApostolNT] p. 107	Example 4	zmod1congr 10452
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10489
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10777
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12007
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12298
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 12617
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12300
[ApostolNT] p. 113	Theorem 5.17	eulerth 12428
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12447
[ApostolNT] p. 114	Theorem 5.19	fermltl 12429
[ApostolNT] p. 179	Definition	df-lgs 15347  lgsprme0 15391
[ApostolNT] p. 180	Example 1	1lgs 15392
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 15368
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 15383
[ApostolNT] p. 181	Theorem 9.4	m1lgs 15434
[ApostolNT] p. 181	Theorem 9.5	2lgs 15453  2lgsoddprm 15462
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 15418
[ApostolNT] p. 185	Theorem 9.8	lgsquad 15429
[ApostolNT] p. 188	Definition	df-lgs 15347  lgs1 15393
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 15384
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 15386
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 15394
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 15395
[Bauer] p. 482	Section 1.2	pm2.01 617  pm2.65 660
[Bauer] p. 483	Theorem 1.3	acexmid 5924  onsucelsucexmidlem 4566
[Bauer], p. 481	Section 1.1	pwtrufal 15752
[Bauer], p. 483	Definition	n0rf 3464
[Bauer], p. 483	Theorem 1.2	2irrexpq 15320  2irrexpqap 15322
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6946
[Bauer], p. 493	Section 5.1	ivthdich 14997
[Bauer], p. 494	Theorem 5.5	ivthinc 14987
[BauerHanson], p. 27	Proposition 5.2	cnstab 8691
[BauerSwan], p. 14	Remark	0ct 7182  ctm 7184
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 15755
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7190
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7587
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7500
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7589
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7623  addlocpr 7622
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7649
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7652
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7657
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2048
[BellMachover] p. 460	Notation	df-mo 2049
[BellMachover] p. 460	Definition	mo3 2099  mo3h 2098
[BellMachover] p. 462	Theorem 1.1	bm1.1 2181
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4155
[BellMachover] p. 466	Axiom Pow	axpow3 4211
[BellMachover] p. 466	Axiom Union	axun2 4471
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4579
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4420
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4582
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4533
[BellMachover] p. 471	Definition of Lim	df-ilim 4405
[BellMachover] p. 472	Axiom Inf	zfinf2 4626
[BellMachover] p. 473	Theorem 2.8	limom 4651
[Bobzien] p. 116	Statement T3	stoic3 1442
[Bobzien] p. 117	Statement T2	stoic2a 1440
[Bobzien] p. 117	Statement T4	stoic4a 1443
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1438
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13060
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13106
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13121
[BourbakiAlg1] p. 92	Definition 1	df-ring 13632
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 13567
[BourbakiEns] p.	Proposition 8	fcof1 5833  fcofo 5834
[BourbakiTop1] p.	Remark	xnegmnf 9923  xnegpnf 9922
[BourbakiTop1] p.	Remark	rexneg 9924
[BourbakiTop1] p.	Proposition	ishmeo 14648
[BourbakiTop1] p.	Property V_i	ssnei2 14501
[BourbakiTop1] p.	Property V_ii	innei 14507
[BourbakiTop1] p.	Property V_iv	neissex 14509
[BourbakiTop1] p.	Proposition 1	neipsm 14498  neiss 14494
[BourbakiTop1] p.	Proposition 2	cnptopco 14566
[BourbakiTop1] p.	Proposition 4	imasnopn 14643
[BourbakiTop1] p.	Property V_iii	elnei 14496
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14342
[Bruck] p. 1	Section I.1	df-mgm 13060
[Bruck] p. 23	Section II.1	df-sgrp 13106
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13303
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4097
[Cohen] p. 301	Remark	relogoprlem 15212
[Cohen] p. 301	Property 2	relogmul 15213  relogmuld 15228
[Cohen] p. 301	Property 3	relogdiv 15214  relogdivd 15229
[Cohen] p. 301	Property 4	relogexp 15216
[Cohen] p. 301	Property 1a	log1 15210
[Cohen] p. 301	Property 1b	loge 15211
[Cohen4] p. 348	Observation	relogbcxpbap 15309
[Cohen4] p. 352	Definition	rpelogb 15293
[Cohen4] p. 361	Property 2	rprelogbmul 15299
[Cohen4] p. 361	Property 3	logbrec 15304  rprelogbdiv 15301
[Cohen4] p. 361	Property 4	rplogbreexp 15297
[Cohen4] p. 361	Property 6	relogbexpap 15302
[Cohen4] p. 361	Property 1(a)	rplogbid1 15291
[Cohen4] p. 361	Property 1(b)	rplogb1 15292
[Cohen4] p. 367	Property	rplogbchbase 15294
[Cohen4] p. 377	Property 2	logblt 15306
[Crosilla] p.	Axiom 1	ax-ext 2178
[Crosilla] p.	Axiom 2	ax-pr 4243
[Crosilla] p.	Axiom 3	ax-un 4469
[Crosilla] p.	Axiom 4	ax-nul 4160
[Crosilla] p.	Axiom 5	ax-iinf 4625
[Crosilla] p.	Axiom 6	ru 2988
[Crosilla] p.	Axiom 8	ax-pow 4208
[Crosilla] p.	Axiom 9	ax-setind 4574
[Crosilla], p.	Axiom 6	ax-sep 4152
[Crosilla], p.	Axiom 7	ax-coll 4149
[Crosilla], p.	Axiom 7'	repizf 4150
[Crosilla], p.	Theorem is stated	ordtriexmid 4558
[Crosilla], p.	Axiom of choice implies instances	acexmid 5924
[Crosilla], p.	Definition of ordinal	df-iord 4402
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4572
[Eisenberg] p. 67	Definition 5.3	df-dif 3159
[Eisenberg] p. 82	Definition 6.3	df-iom 4628
[Eisenberg] p. 125	Definition 8.21	df-map 6718
[Enderton] p. 18	Axiom of Empty Set	axnul 4159
[Enderton] p. 19	Definition	df-tp 3631
[Enderton] p. 26	Exercise 5	unissb 3870
[Enderton] p. 26	Exercise 10	pwel 4252
[Enderton] p. 28	Exercise 7(b)	pwunim 4322
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3987  iinin2m 3986  iunin1 3982  iunin2 3981
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3985  iundif2ss 3983
[Enderton] p. 33	Exercise 23	iinuniss 4000
[Enderton] p. 33	Exercise 25	iununir 4001
[Enderton] p. 33	Exercise 24(a)	iinpw 4008
[Enderton] p. 33	Exercise 24(b)	iunpw 4516  iunpwss 4009
[Enderton] p. 38	Exercise 6(a)	unipw 4251
[Enderton] p. 38	Exercise 6(b)	pwuni 4226
[Enderton] p. 41	Lemma 3D	opeluu 4486  rnex 4934  rnexg 4932
[Enderton] p. 41	Exercise 8	dmuni 4877  rnuni 5082
[Enderton] p. 42	Definition of a function	dffun7 5286  dffun8 5287
[Enderton] p. 43	Definition of function value	funfvdm2 5628
[Enderton] p. 43	Definition of single-rooted	funcnv 5320
[Enderton] p. 44	Definition (d)	dfima2 5012  dfima3 5013
[Enderton] p. 47	Theorem 3H	fvco2 5633
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7291
[Enderton] p. 50	Theorem 3K(a)	imauni 5811
[Enderton] p. 52	Definition	df-map 6718
[Enderton] p. 53	Exercise 21	coass 5189
[Enderton] p. 53	Exercise 27	dmco 5179
[Enderton] p. 53	Exercise 14(a)	funin 5330
[Enderton] p. 53	Exercise 22(a)	imass2 5046
[Enderton] p. 54	Remark	ixpf 6788  ixpssmap 6800
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6767
[Enderton] p. 56	Theorem 3M	erref 6621
[Enderton] p. 57	Lemma 3N	erthi 6649
[Enderton] p. 57	Definition	df-ec 6603
[Enderton] p. 58	Definition	df-qs 6607
[Enderton] p. 60	Theorem 3Q	th3q 6708  th3qcor 6707  th3qlem1 6705  th3qlem2 6706
[Enderton] p. 61	Exercise 35	df-ec 6603
[Enderton] p. 65	Exercise 56(a)	dmun 4874
[Enderton] p. 68	Definition of successor	df-suc 4407
[Enderton] p. 71	Definition	df-tr 4133  dftr4 4137
[Enderton] p. 72	Theorem 4E	unisuc 4449  unisucg 4450
[Enderton] p. 73	Exercise 6	unisuc 4449  unisucg 4450
[Enderton] p. 73	Exercise 5(a)	truni 4146
[Enderton] p. 73	Exercise 5(b)	trint 4147
[Enderton] p. 79	Theorem 4I(A1)	nna0 6541
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6543  onasuc 6533
[Enderton] p. 79	Definition of operation value	df-ov 5928
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6542
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6544  onmsuc 6540
[Enderton] p. 81	Theorem 4K(1)	nnaass 6552
[Enderton] p. 81	Theorem 4K(2)	nna0r 6545  nnacom 6551
[Enderton] p. 81	Theorem 4K(3)	nndi 6553
[Enderton] p. 81	Theorem 4K(4)	nnmass 6554
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6556
[Enderton] p. 82	Exercise 16	nnm0r 6546  nnmsucr 6555
[Enderton] p. 88	Exercise 23	nnaordex 6595
[Enderton] p. 129	Definition	df-en 6809
[Enderton] p. 132	Theorem 6B(b)	canth 5878
[Enderton] p. 133	Exercise 1	xpomen 12639
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6935
[Enderton] p. 136	Corollary 6E	nneneq 6927
[Enderton] p. 139	Theorem 6H(c)	mapen 6916
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7303
[Enderton] p. 143	Theorem 6J	dju0en 7299  dju1en 7298
[Enderton] p. 144	Corollary 6K	undif2ss 3527
[Enderton] p. 145	Figure 38	ffoss 5539
[Enderton] p. 145	Definition	df-dom 6810
[Enderton] p. 146	Example 1	domen 6819  domeng 6820
[Enderton] p. 146	Example 3	nndomo 6934
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6903  xpdom1g 6901  xpdom2g 6900
[Enderton] p. 168	Definition	df-po 4332
[Enderton] p. 192	Theorem 7M(a)	oneli 4464
[Enderton] p. 192	Theorem 7M(b)	ontr1 4425
[Enderton] p. 192	Theorem 7M(c)	onirri 4580
[Enderton] p. 193	Corollary 7N(b)	0elon 4428
[Enderton] p. 193	Corollary 7N(c)	onsuci 4553
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4526
[Enderton] p. 194	Remark	onprc 4589
[Enderton] p. 194	Exercise 16	suc11 4595
[Enderton] p. 197	Definition	df-card 7259
[Enderton] p. 200	Exercise 25	tfis 4620
[Enderton] p. 206	Theorem 7X(b)	en2lp 4591
[Enderton] p. 207	Exercise 34	opthreg 4593
[Enderton] p. 208	Exercise 35	suc11g 4594
[Geuvers], p. 1	Remark	expap0 10680
[Geuvers], p. 6	Lemma 2.13	mulap0r 8661
[Geuvers], p. 6	Lemma 2.15	mulap0 8700
[Geuvers], p. 9	Lemma 2.35	msqge0 8662
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8017
[Geuvers], p. 10	Lemma 3.9	maxcom 11387
[Geuvers], p. 10	Lemma 3.10	maxle1 11395  maxle2 11396
[Geuvers], p. 10	Lemma 3.11	maxleast 11397
[Geuvers], p. 10	Lemma 3.12	maxleb 11400
[Geuvers], p. 11	Definition 3.13	dfabsmax 11401
[Geuvers], p. 17	Definition 6.1	df-ap 8628
[Gleason] p. 117	Proposition 9-2.1	df-enq 7433  enqer 7444
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7437  df-nqqs 7434
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7430  df-plqqs 7435
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7431  df-mqqs 7436
[Gleason] p. 119	Proposition 9-2.5	df-rq 7438
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7494
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7497  ltbtwnnq 7502  ltbtwnnqq 7501
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7486
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7487
[Gleason] p. 123	Proposition 9-3.5	addclpr 7623
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7665
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7664
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7683
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7699
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7705  ltaprlem 7704
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7702
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7658
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7678
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7667
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7666
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7674
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7724
[Gleason] p. 126	Proposition 9-4.1	df-enr 7812  enrer 7821
[Gleason] p. 126	Proposition 9-4.2	df-0r 7817  df-1r 7818  df-nr 7813
[Gleason] p. 126	Proposition 9-4.3	df-mr 7815  df-plr 7814  negexsr 7858  recexsrlem 7860
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7816
[Gleason] p. 130	Proposition 10-1.3	creui 9006  creur 9005  cru 8648
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8009  axcnre 7967
[Gleason] p. 132	Definition 10-3.1	crim 11042  crimd 11161  crimi 11121  crre 11041  crred 11160  crrei 11120
[Gleason] p. 132	Definition 10-3.2	remim 11044  remimd 11126
[Gleason] p. 133	Definition 10.36	absval2 11241  absval2d 11369  absval2i 11328
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11068  cjaddd 11149  cjaddi 11116
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11069  cjmuld 11150  cjmuli 11117
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11067  cjcjd 11127  cjcji 11099
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11066  cjreb 11050  cjrebd 11130  cjrebi 11102  cjred 11155  rere 11049  rereb 11047  rerebd 11129  rerebi 11101  rered 11153
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11075  addcjd 11141  addcji 11111
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11185
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11236  abscjd 11374  abscji 11332
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11248  abs00d 11370  abs00i 11329  absne0d 11371
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11280  releabsd 11375  releabsi 11333
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11253  absmuld 11378  absmuli 11335
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11239  sqabsaddi 11336
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11288  abstrid 11380  abstrii 11339
[Gleason] p. 134	Definition 10-4.1	df-exp 10650  exp0 10654  expp1 10657  expp1d 10785
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10692  expaddd 10786
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15256  cxpmuld 15281  expmul 10695  expmuld 10787
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10689  mulexpd 10799  rpmulcxp 15253
[Gleason] p. 141	Definition 11-2.1	fzval 10104
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11510
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11512
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11511
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11515
[Gleason] p. 172	Corollary 12-2.5	climrecl 11508
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11504  climcj 11505  climim 11507  climre 11506
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8085  df-xr 8084  ltxr 9869
[Gleason] p. 180	Theorem 12-5.3	climcau 11531
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10409
[Gleason] p. 223	Definition 14-1.1	df-met 14179
[Gleason] p. 223	Definition 14-1.1(a)	met0 14708  xmet0 14707
[Gleason] p. 223	Definition 14-1.1(c)	metsym 14715
[Gleason] p. 223	Definition 14-1.1(d)	mettri 14717  mstri 14817  xmettri 14716  xmstri 14816
[Gleason] p. 230	Proposition 14-2.6	txlm 14623
[Gleason] p. 240	Proposition 14-4.2	metcnp3 14855
[Gleason] p. 243	Proposition 14-4.16	addcn2 11494  addcncntop 14906  mulcn2 11496  mulcncntop 14908  subcn2 11495  subcncntop 14907
[Gleason] p. 295	Remark	bcval3 10862  bcval4 10863
[Gleason] p. 295	Equation 2	bcpasc 10877
[Gleason] p. 295	Definition of binomial coefficient	bcval 10860  df-bc 10859
[Gleason] p. 296	Remark	bcn0 10866  bcnn 10868
[Gleason] p. 296	Theorem 15-2.8	binom 11668
[Gleason] p. 308	Equation 2	ef0 11856
[Gleason] p. 308	Equation 3	efcj 11857
[Gleason] p. 309	Corollary 15-4.3	efne0 11862
[Gleason] p. 309	Corollary 15-4.4	efexp 11866
[Gleason] p. 310	Equation 14	sinadd 11920
[Gleason] p. 310	Equation 15	cosadd 11921
[Gleason] p. 311	Equation 17	sincossq 11932
[Gleason] p. 311	Equation 18	cosbnd 11937  sinbnd 11936
[Gleason] p. 311	Definition of ` `	df-pi 11837
[Golan] p. 1	Remark	srgisid 13620
[Golan] p. 1	Definition	df-srg 13598
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1463
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13215  mndideu 13130
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13242
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13271
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13282
[Herstein] p. 57	Exercise 1	dfgrp3me 13304
[Heyting] p. 127	Axiom #1	ax1hfs 15831
[Hitchcock] p. 5	Rule A3	mptnan 1434
[Hitchcock] p. 5	Rule A4	mptxor 1435
[Hitchcock] p. 5	Rule A5	mtpxor 1437
[HoTT], p.	Lemma 10.4.1	exmidontriim 7310
[HoTT], p.	Theorem 7.2.6	nndceq 6566
[HoTT], p.	Exercise 11.10	neapmkv 15825
[HoTT], p.	Exercise 11.11	mulap0bd 8703
[HoTT], p.	Section 11.2.1	df-iltp 7556  df-imp 7555  df-iplp 7554  df-reap 8621
[HoTT], p.	Theorem 11.2.4	recapb 8717  rerecapb 8889
[HoTT], p.	Corollary 3.9.2	uchoice 6204
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7748
[HoTT], p.	Corollary 11.4.3	conventions 15475
[HoTT], p.	Exercise 11.6(i)	dcapnconst 15818  dceqnconst 15817
[HoTT], p.	Corollary 11.2.13	axcaucvg 7986  caucvgpr 7768  caucvgprpr 7798  caucvgsr 7888
[HoTT], p.	Definition 11.2.1	df-inp 7552
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 15823
[HoTT], p.	Proposition 11.2.3	df-iso 4333  ltpopr 7681  ltsopr 7682
[HoTT], p.	Definition 11.2.7(v)	apsym 8652  reapcotr 8644  reapirr 8623
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8172  gt0add 8619  leadd1 8476  lelttr 8134  lemul1a 8904  lenlt 8121  ltadd1 8475  ltletr 8135  ltmul1 8638  reaplt 8634
[Jech] p. 4	Definition of class	cv 1363  cvjust 2191
[Jech] p. 78	Note	opthprc 4715
[KalishMontague] p. 81	Note 1	ax-i9 1544
[Kreyszig] p. 3	Property M1	metcl 14697  xmetcl 14696
[Kreyszig] p. 4	Property M2	meteq0 14704
[Kreyszig] p. 12	Equation 5	muleqadd 8714
[Kreyszig] p. 18	Definition 1.3-2	mopnval 14786
[Kreyszig] p. 19	Remark	mopntopon 14787
[Kreyszig] p. 19	Theorem T1	mopn0 14832  mopnm 14792
[Kreyszig] p. 19	Theorem T2	unimopn 14830
[Kreyszig] p. 19	Definition of neighborhood	neibl 14835
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 14857
[Kreyszig] p. 25	Definition 1.4-1	lmbr 14557
[Kreyszig] p. 51	Equation 2	lmodvneg1 13964
[Kreyszig] p. 51	Equation 1a	lmod0vs 13955
[Kreyszig] p. 51	Equation 1b	lmodvs0 13956
[Kunen] p. 10	Axiom 0	a9e 1710
[Kunen] p. 12	Axiom 6	zfrep6 4151
[Kunen] p. 24	Definition 10.24	mapval 6728  mapvalg 6726
[Kunen] p. 31	Definition 10.24	mapex 6722
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3927
[Lang] p. 3	Statement	lidrideqd 13085  mndbn0 13135
[Lang] p. 3	Definition	df-mnd 13121
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 13102
[Lang] p. 5	Equation	gsumfzreidx 13545
[Lang] p. 6	Definition	mulgnn0gsum 13336
[Lang] p. 7	Definition	dfgrp2e 13232
[Levy] p. 338	Axiom	df-clab 2183  df-clel 2192  df-cleq 2189
[Lopez-Astorga] p. 12	Rule 1	mptnan 1434
[Lopez-Astorga] p. 12	Rule 2	mptxor 1435
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1437
[Margaris] p. 40	Rule C	exlimiv 1612
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 854
[Margaris] p. 49	Definition	dfbi2 388  dfordc 893  exalim 1516
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 652
[Margaris] p. 89	Theorem 19.2	19.2 1652  r19.2m 3538
[Margaris] p. 89	Theorem 19.3	19.3 1568  19.3h 1567  rr19.3v 2903
[Margaris] p. 89	Theorem 19.5	alcom 1492
[Margaris] p. 89	Theorem 19.6	alexdc 1633  alexim 1659
[Margaris] p. 89	Theorem 19.7	alnex 1513
[Margaris] p. 89	Theorem 19.8	19.8a 1604  spsbe 1856
[Margaris] p. 89	Theorem 19.9	19.9 1658  19.9h 1657  19.9v 1885  exlimd 1611
[Margaris] p. 89	Theorem 19.11	excom 1678  excomim 1677
[Margaris] p. 89	Theorem 19.12	19.12 1679  r19.12 2603
[Margaris] p. 90	Theorem 19.14	exnalim 1660
[Margaris] p. 90	Theorem 19.15	albi 1482  ralbi 2629
[Margaris] p. 90	Theorem 19.16	19.16 1569
[Margaris] p. 90	Theorem 19.17	19.17 1570
[Margaris] p. 90	Theorem 19.18	exbi 1618  rexbi 2630
[Margaris] p. 90	Theorem 19.19	19.19 1680
[Margaris] p. 90	Theorem 19.20	alim 1471  alimd 1535  alimdh 1481  alimdv 1893  ralimdaa 2563  ralimdv 2565  ralimdva 2564  ralimdvva 2566  sbcimdv 3055
[Margaris] p. 90	Theorem 19.21	19.21-2 1681  19.21 1597  19.21bi 1572  19.21h 1571  19.21ht 1595  19.21t 1596  19.21v 1887  alrimd 1624  alrimdd 1623  alrimdh 1493  alrimdv 1890  alrimi 1536  alrimih 1483  alrimiv 1888  alrimivv 1889  r19.21 2573  r19.21be 2588  r19.21bi 2585  r19.21t 2572  r19.21v 2574  ralrimd 2575  ralrimdv 2576  ralrimdva 2577  ralrimdvv 2581  ralrimdvva 2582  ralrimi 2568  ralrimiv 2569  ralrimiva 2570  ralrimivv 2578  ralrimivva 2579  ralrimivvva 2580  ralrimivw 2571  rexlimi 2607
[Margaris] p. 90	Theorem 19.22	2alimdv 1895  2eximdv 1896  exim 1613  eximd 1626  eximdh 1625  eximdv 1894  rexim 2591  reximdai 2595  reximddv 2600  reximddv2 2602  reximdv 2598  reximdv2 2596  reximdva 2599  reximdvai 2597  reximi2 2593
[Margaris] p. 90	Theorem 19.23	19.23 1692  19.23bi 1606  19.23h 1512  19.23ht 1511  19.23t 1691  19.23v 1897  19.23vv 1898  exlimd2 1609  exlimdh 1610  exlimdv 1833  exlimdvv 1912  exlimi 1608  exlimih 1607  exlimiv 1612  exlimivv 1911  r19.23 2605  r19.23v 2606  rexlimd 2611  rexlimdv 2613  rexlimdv3a 2616  rexlimdva 2614  rexlimdva2 2617  rexlimdvaa 2615  rexlimdvv 2621  rexlimdvva 2622  rexlimdvw 2618  rexlimiv 2608  rexlimiva 2609  rexlimivv 2620
[Margaris] p. 90	Theorem 19.24	i19.24 1653
[Margaris] p. 90	Theorem 19.25	19.25 1640
[Margaris] p. 90	Theorem 19.26	19.26-2 1496  19.26-3an 1497  19.26 1495  r19.26-2 2626  r19.26-3 2627  r19.26 2623  r19.26m 2628
[Margaris] p. 90	Theorem 19.27	19.27 1575  19.27h 1574  19.27v 1914  r19.27av 2632  r19.27m 3547  r19.27mv 3548
[Margaris] p. 90	Theorem 19.28	19.28 1577  19.28h 1576  19.28v 1915  r19.28av 2633  r19.28m 3541  r19.28mv 3544  rr19.28v 2904
[Margaris] p. 90	Theorem 19.29	19.29 1634  19.29r 1635  19.29r2 1636  19.29x 1637  r19.29 2634  r19.29d2r 2641  r19.29r 2635
[Margaris] p. 90	Theorem 19.30	19.30dc 1641
[Margaris] p. 90	Theorem 19.31	19.31r 1695
[Margaris] p. 90	Theorem 19.32	19.32dc 1693  19.32r 1694  r19.32r 2643  r19.32vdc 2646  r19.32vr 2645
[Margaris] p. 90	Theorem 19.33	19.33 1498  19.33b2 1643  19.33bdc 1644
[Margaris] p. 90	Theorem 19.34	19.34 1698
[Margaris] p. 90	Theorem 19.35	19.35-1 1638  19.35i 1639
[Margaris] p. 90	Theorem 19.36	19.36-1 1687  19.36aiv 1916  19.36i 1686  r19.36av 2648
[Margaris] p. 90	Theorem 19.37	19.37-1 1688  19.37aiv 1689  r19.37 2649  r19.37av 2650
[Margaris] p. 90	Theorem 19.38	19.38 1690
[Margaris] p. 90	Theorem 19.39	i19.39 1654
[Margaris] p. 90	Theorem 19.40	19.40-2 1646  19.40 1645  r19.40 2651
[Margaris] p. 90	Theorem 19.41	19.41 1700  19.41h 1699  19.41v 1917  19.41vv 1918  19.41vvv 1919  19.41vvvv 1920  r19.41 2652  r19.41v 2653
[Margaris] p. 90	Theorem 19.42	19.42 1702  19.42h 1701  19.42v 1921  19.42vv 1926  19.42vvv 1927  19.42vvvv 1928  r19.42v 2654
[Margaris] p. 90	Theorem 19.43	19.43 1642  r19.43 2655
[Margaris] p. 90	Theorem 19.44	19.44 1696  r19.44av 2656  r19.44mv 3546
[Margaris] p. 90	Theorem 19.45	19.45 1697  r19.45av 2657  r19.45mv 3545
[Margaris] p. 110	Exercise 2(b)	eu1 2070
[Megill] p. 444	Axiom C5	ax-17 1540
[Megill] p. 445	Lemma L12	alequcom 1529  ax-10 1519
[Megill] p. 446	Lemma L17	equtrr 1724
[Megill] p. 446	Lemma L19	hbnae 1735
[Megill] p. 447	Remark 9.1	df-sb 1777  sbid 1788
[Megill] p. 448	Scheme C5'	ax-4 1524
[Megill] p. 448	Scheme C6'	ax-7 1462
[Megill] p. 448	Scheme C8'	ax-8 1518
[Megill] p. 448	Scheme C9'	ax-i12 1521
[Megill] p. 448	Scheme C11'	ax-10o 1730
[Megill] p. 448	Scheme C12'	ax-13 2169
[Megill] p. 448	Scheme C13'	ax-14 2170
[Megill] p. 448	Scheme C15'	ax-11o 1837
[Megill] p. 448	Scheme C16'	ax-16 1828
[Megill] p. 448	Theorem 9.4	dral1 1744  dral2 1745  drex1 1812  drex2 1746  drsb1 1813  drsb2 1855
[Megill] p. 449	Theorem 9.7	sbcom2 2006  sbequ 1854  sbid2v 2015
[Megill] p. 450	Example in Appendix	hba1 1554
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3072  rspsbca 3073  stdpc4 1789
[Mendelson] p. 69	Axiom 5	ra5 3078  stdpc5 1598
[Mendelson] p. 81	Rule C	exlimiv 1612
[Mendelson] p. 95	Axiom 6	stdpc6 1717
[Mendelson] p. 95	Axiom 7	stdpc7 1784
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3488
[Mendelson] p. 231	Exercise 4.10(l)	unv 3489
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3404
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3452
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3405
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3295
[Mendelson] p. 231	Definition of union	unssin 3403
[Mendelson] p. 235	Exercise 4.12(c)	univ 4512
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3839
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4318
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4319
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4320
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3860
[Mendelson] p. 235	Exercise 4.12(p)	reli 4796
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5191
[Mendelson] p. 246	Definition of successor	df-suc 4407
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6915
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6889  xpsneng 6890
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6895  xpcomeng 6896
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6898
[Mendelson] p. 255	Exercise 4.39	endisj 6892
[Mendelson] p. 255	Exercise 4.41	mapprc 6720
[Mendelson] p. 255	Exercise 4.43	mapsnen 6879
[Mendelson] p. 255	Exercise 4.47	xpmapen 6920
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6754
[Mendelson] p. 255	Exercise 4.42(b)	map1 6880
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7302  djucomen 7301
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7300
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6534
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3386
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4752
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4753
[Monk1] p. 34	Definition 3.3	df-opab 4096
[Monk1] p. 36	Theorem 3.7(i)	coi1 5186  coi2 5187
[Monk1] p. 36	Theorem 3.8(v)	dm0 4881  rn0 4923
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5075
[Monk1] p. 37	Theorem 3.13(i)	relxp 4773
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4887  rnxpm 5100
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4744  xp0 5090
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5029
[Monk1] p. 38	Theorem 3.16(viii)	imai 5026
[Monk1] p. 39	Theorem 3.17	imaex 5025  imaexg 5024
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5021
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5695  funfvop 5677
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5607
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5615
[Monk1] p. 43	Theorem 4.6	funun 5303
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5818  dff13f 5820
[Monk1] p. 46	Theorem 4.15(v)	funex 5788  funrnex 6180
[Monk1] p. 50	Definition 5.4	fniunfv 5812
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5154
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3891
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6222  df-1st 6207
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6223  df-2nd 6208
[Monk2] p. 105	Axiom C4	ax-5 1461
[Monk2] p. 105	Axiom C7	ax-8 1518
[Monk2] p. 105	Axiom C8	ax-11 1520  ax-11o 1837
[Monk2] p. 105	Axiom (C8)	ax11v 1841
[Monk2] p. 109	Lemma 12	ax-7 1462
[Monk2] p. 109	Lemma 15	equvin 1877  equvini 1772  eqvinop 4277
[Monk2] p. 113	Axiom C5-1	ax-17 1540
[Monk2] p. 113	Axiom C5-2	ax6b 1665
[Monk2] p. 113	Axiom C5-3	ax-7 1462
[Monk2] p. 114	Lemma 22	hba1 1554
[Monk2] p. 114	Lemma 23	hbia1 1566  nfia1 1594
[Monk2] p. 114	Lemma 24	hba2 1565  nfa2 1593
[Moschovakis] p. 2	Chapter 2	df-stab 832  dftest 15832
[Munkres] p. 77	Example 2	distop 14429
[Munkres] p. 78	Definition of basis	df-bases 14387  isbasis3g 14390
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12964  tgval2 14395
[Munkres] p. 79	Remark	tgcl 14408
[Munkres] p. 80	Lemma 2.1	tgval3 14402
[Munkres] p. 80	Lemma 2.2	tgss2 14423  tgss3 14422
[Munkres] p. 81	Lemma 2.3	basgen 14424  basgen2 14425
[Munkres] p. 89	Definition of subspace topology	resttop 14514
[Munkres] p. 93	Theorem 6.1(1)	0cld 14456  topcld 14453
[Munkres] p. 93	Theorem 6.1(3)	uncld 14457
[Munkres] p. 94	Definition of closure	clsval 14455
[Munkres] p. 94	Definition of interior	ntrval 14454
[Munkres] p. 102	Definition of continuous function	df-cn 14532  iscn 14541  iscn2 14544
[Munkres] p. 107	Theorem 7.2(g)	cncnp 14574  cncnp2m 14575  cncnpi 14572  df-cnp 14533  iscnp 14543
[Munkres] p. 127	Theorem 10.1	metcn 14858
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6973
[Pierik], p. 9	Definition 2.4	df-womni 7239
[Pierik], p. 9	Definition 2.5	df-markov 7227  omniwomnimkv 7242
[Pierik], p. 10	Section 2.3	dfdif3 3274
[Pierik], p. 14	Definition 3.1	df-omni 7210  exmidomniim 7216  finomni 7215
[Pierik], p. 15	Section 3.1	df-nninf 7195
[Pradic2025], p. 2	Section 1.1	nnnninfen 15776
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 15780
[PradicBrown2022], p. 2	Remark	exmidpw 6978
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7282
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7283  exmidfodomrlemrALT 7284
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7224
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 15762  peano4nninf 15761
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 15764
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 15772
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 15774
[PradicBrown2022], p. 5	Definition 3.3	nnsf 15760
[Quine] p. 16	Definition 2.1	df-clab 2183  rabid 2673
[Quine] p. 17	Definition 2.1''	dfsb7 2010
[Quine] p. 18	Definition 2.7	df-cleq 2189
[Quine] p. 19	Definition 2.9	df-v 2765
[Quine] p. 34	Theorem 5.1	abeq2 2305
[Quine] p. 35	Theorem 5.2	abid2 2317  abid2f 2365
[Quine] p. 40	Theorem 6.1	sb5 1902
[Quine] p. 40	Theorem 6.2	sb56 1900  sb6 1901
[Quine] p. 41	Theorem 6.3	df-clel 2192
[Quine] p. 41	Theorem 6.4	eqid 2196
[Quine] p. 41	Theorem 6.5	eqcom 2198
[Quine] p. 42	Theorem 6.6	df-sbc 2990
[Quine] p. 42	Theorem 6.7	dfsbcq 2991  dfsbcq2 2992
[Quine] p. 43	Theorem 6.8	vex 2766
[Quine] p. 43	Theorem 6.9	isset 2769
[Quine] p. 44	Theorem 7.3	spcgf 2846  spcgv 2851  spcimgf 2844
[Quine] p. 44	Theorem 6.11	spsbc 3001  spsbcd 3002
[Quine] p. 44	Theorem 6.12	elex 2774
[Quine] p. 44	Theorem 6.13	elab 2908  elabg 2910  elabgf 2906
[Quine] p. 44	Theorem 6.14	noel 3455
[Quine] p. 48	Theorem 7.2	snprc 3688
[Quine] p. 48	Definition 7.1	df-pr 3630  df-sn 3629
[Quine] p. 49	Theorem 7.4	snss 3758  snssg 3757
[Quine] p. 49	Theorem 7.5	prss 3779  prssg 3780
[Quine] p. 49	Theorem 7.6	prid1 3729  prid1g 3727  prid2 3730  prid2g 3728  snid 3654  snidg 3652
[Quine] p. 51	Theorem 7.12	snexg 4218  snexprc 4220
[Quine] p. 51	Theorem 7.13	prexg 4245
[Quine] p. 53	Theorem 8.2	unisn 3856  unisng 3857
[Quine] p. 53	Theorem 8.3	uniun 3859
[Quine] p. 54	Theorem 8.6	elssuni 3868
[Quine] p. 54	Theorem 8.7	uni0 3867
[Quine] p. 56	Theorem 8.17	uniabio 5230
[Quine] p. 56	Definition 8.18	dfiota2 5221
[Quine] p. 57	Theorem 8.19	iotaval 5231
[Quine] p. 57	Theorem 8.22	iotanul 5235
[Quine] p. 58	Theorem 8.23	euiotaex 5236
[Quine] p. 58	Definition 9.1	df-op 3632
[Quine] p. 61	Theorem 9.5	opabid 4291  opabidw 4292  opelopab 4307  opelopaba 4301  opelopabaf 4309  opelopabf 4310  opelopabg 4303  opelopabga 4298  opelopabgf 4305  oprabid 5957
[Quine] p. 64	Definition 9.11	df-xp 4670
[Quine] p. 64	Definition 9.12	df-cnv 4672
[Quine] p. 64	Definition 9.15	df-id 4329
[Quine] p. 65	Theorem 10.3	fun0 5317
[Quine] p. 65	Theorem 10.4	funi 5291
[Quine] p. 65	Theorem 10.5	funsn 5307  funsng 5305
[Quine] p. 65	Definition 10.1	df-fun 5261
[Quine] p. 65	Definition 10.2	args 5039  dffv4g 5558
[Quine] p. 68	Definition 10.11	df-fv 5267  fv2 5556
[Quine] p. 124	Theorem 17.3	nn0opth2 10835  nn0opth2d 10834  nn0opthd 10833
[Quine] p. 284	Axiom 39(vi)	funimaex 5344  funimaexg 5343
[Roman] p. 18	Part Preliminaries	df-rng 13567
[Roman] p. 19	Part Preliminaries	df-ring 13632
[Rudin] p. 164	Equation 27	efcan 11860
[Rudin] p. 164	Equation 30	efzval 11867
[Rudin] p. 167	Equation 48	absefi 11953
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1437
[Sanford] p. 39	Rule 4	mptxor 1435
[Sanford] p. 40	Rule 1	mptnan 1434
[Schechter] p. 51	Definition of antisymmetry	intasym 5055
[Schechter] p. 51	Definition of irreflexivity	intirr 5057
[Schechter] p. 51	Definition of symmetry	cnvsym 5054
[Schechter] p. 51	Definition of transitivity	cotr 5052
[Schechter] p. 187	Definition of "ring with unit"	isring 13634
[Schechter] p. 428	Definition 15.35	bastop1 14427
[Stoll] p. 13	Definition of symmetric difference	symdif1 3429
[Stoll] p. 16	Exercise 4.4	0dif 3523  dif0 3522
[Stoll] p. 16	Exercise 4.8	difdifdirss 3536
[Stoll] p. 19	Theorem 5.2(13)	undm 3422
[Stoll] p. 19	Theorem 5.2(13')	indmss 3423
[Stoll] p. 20	Remark	invdif 3406
[Stoll] p. 25	Definition of ordered triple	df-ot 3633
[Stoll] p. 43	Definition	uniiun 3971
[Stoll] p. 44	Definition	intiin 3972
[Stoll] p. 45	Definition	df-iin 3920
[Stoll] p. 45	Definition indexed union	df-iun 3919
[Stoll] p. 176	Theorem 3.4(27)	imandc 890  imanst 889
[Stoll] p. 262	Example 4.1	symdif1 3429
[Suppes] p. 22	Theorem 2	eq0 3470
[Suppes] p. 22	Theorem 4	eqss 3199  eqssd 3201  eqssi 3200
[Suppes] p. 23	Theorem 5	ss0 3492  ss0b 3491
[Suppes] p. 23	Theorem 6	sstr 3192
[Suppes] p. 25	Theorem 12	elin 3347  elun 3305
[Suppes] p. 26	Theorem 15	inidm 3373
[Suppes] p. 26	Theorem 16	in0 3486
[Suppes] p. 27	Theorem 23	unidm 3307
[Suppes] p. 27	Theorem 24	un0 3485
[Suppes] p. 27	Theorem 25	ssun1 3327
[Suppes] p. 27	Theorem 26	ssequn1 3334
[Suppes] p. 27	Theorem 27	unss 3338
[Suppes] p. 27	Theorem 28	indir 3413
[Suppes] p. 27	Theorem 29	undir 3414
[Suppes] p. 28	Theorem 32	difid 3520  difidALT 3521
[Suppes] p. 29	Theorem 33	difin 3401
[Suppes] p. 29	Theorem 34	indif 3407
[Suppes] p. 29	Theorem 35	undif1ss 3526
[Suppes] p. 29	Theorem 36	difun2 3531
[Suppes] p. 29	Theorem 37	difin0 3525
[Suppes] p. 29	Theorem 38	disjdif 3524
[Suppes] p. 29	Theorem 39	difundi 3416
[Suppes] p. 29	Theorem 40	difindiss 3418
[Suppes] p. 30	Theorem 41	nalset 4164
[Suppes] p. 39	Theorem 61	uniss 3861
[Suppes] p. 39	Theorem 65	uniop 4289
[Suppes] p. 41	Theorem 70	intsn 3910
[Suppes] p. 42	Theorem 71	intpr 3907  intprg 3908
[Suppes] p. 42	Theorem 73	op1stb 4514  op1stbg 4515
[Suppes] p. 42	Theorem 78	intun 3906
[Suppes] p. 44	Definition 15(a)	dfiun2 3951  dfiun2g 3949
[Suppes] p. 44	Definition 15(b)	dfiin2 3952
[Suppes] p. 47	Theorem 86	elpw 3612  elpw2 4191  elpw2g 4190  elpwg 3614
[Suppes] p. 47	Theorem 87	pwid 3621
[Suppes] p. 47	Theorem 89	pw0 3770
[Suppes] p. 48	Theorem 90	pwpw0ss 3835
[Suppes] p. 52	Theorem 101	xpss12 4771
[Suppes] p. 52	Theorem 102	xpindi 4802  xpindir 4803
[Suppes] p. 52	Theorem 103	xpundi 4720  xpundir 4721
[Suppes] p. 54	Theorem 105	elirrv 4585
[Suppes] p. 58	Theorem 2	relss 4751
[Suppes] p. 59	Theorem 4	eldm 4864  eldm2 4865  eldm2g 4863  eldmg 4862
[Suppes] p. 59	Definition 3	df-dm 4674
[Suppes] p. 60	Theorem 6	dmin 4875
[Suppes] p. 60	Theorem 8	rnun 5079
[Suppes] p. 60	Theorem 9	rnin 5080
[Suppes] p. 60	Definition 4	dfrn2 4855
[Suppes] p. 61	Theorem 11	brcnv 4850  brcnvg 4848
[Suppes] p. 62	Equation 5	elcnv 4844  elcnv2 4845
[Suppes] p. 62	Theorem 12	relcnv 5048
[Suppes] p. 62	Theorem 15	cnvin 5078
[Suppes] p. 62	Theorem 16	cnvun 5076
[Suppes] p. 63	Theorem 20	co02 5184
[Suppes] p. 63	Theorem 21	dmcoss 4936
[Suppes] p. 63	Definition 7	df-co 4673
[Suppes] p. 64	Theorem 26	cnvco 4852
[Suppes] p. 64	Theorem 27	coass 5189
[Suppes] p. 65	Theorem 31	resundi 4960
[Suppes] p. 65	Theorem 34	elima 5015  elima2 5016  elima3 5017  elimag 5014
[Suppes] p. 65	Theorem 35	imaundi 5083
[Suppes] p. 66	Theorem 40	dminss 5085
[Suppes] p. 66	Theorem 41	imainss 5086
[Suppes] p. 67	Exercise 11	cnvxp 5089
[Suppes] p. 81	Definition 34	dfec2 6604
[Suppes] p. 82	Theorem 72	elec 6642  elecg 6641
[Suppes] p. 82	Theorem 73	erth 6647  erth2 6648
[Suppes] p. 89	Theorem 96	map0b 6755
[Suppes] p. 89	Theorem 97	map0 6757  map0g 6756
[Suppes] p. 89	Theorem 98	mapsn 6758
[Suppes] p. 89	Theorem 99	mapss 6759
[Suppes] p. 92	Theorem 1	enref 6833  enrefg 6832
[Suppes] p. 92	Theorem 2	ensym 6849  ensymb 6848  ensymi 6850
[Suppes] p. 92	Theorem 3	entr 6852
[Suppes] p. 92	Theorem 4	unen 6884
[Suppes] p. 94	Theorem 15	endom 6831
[Suppes] p. 94	Theorem 16	ssdomg 6846
[Suppes] p. 94	Theorem 17	domtr 6853
[Suppes] p. 95	Theorem 18	isbth 7042
[Suppes] p. 98	Exercise 4	fundmen 6874  fundmeng 6875
[Suppes] p. 98	Exercise 6	xpdom3m 6902
[Suppes] p. 130	Definition 3	df-tr 4133
[Suppes] p. 132	Theorem 9	ssonuni 4525
[Suppes] p. 134	Definition 6	df-suc 4407
[Suppes] p. 136	Theorem Schema 22	findes 4640  finds 4637  finds1 4639  finds2 4638
[Suppes] p. 162	Definition 5	df-ltnqqs 7439  df-ltpq 7432
[Suppes] p. 228	Theorem Schema 61	onintss 4426
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2178
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2189
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2192
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2191
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2214
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5929
[TakeutiZaring] p. 14	Proposition 4.14	ru 2988
[TakeutiZaring] p. 15	Exercise 1	elpr 3644  elpr2 3645  elprg 3643
[TakeutiZaring] p. 15	Exercise 2	elsn 3639  elsn2 3657  elsn2g 3656  elsng 3638  velsn 3640
[TakeutiZaring] p. 15	Exercise 3	elop 4265
[TakeutiZaring] p. 15	Exercise 4	sneq 3634  sneqr 3791
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3642  dfsn2 3637
[TakeutiZaring] p. 16	Axiom 3	uniex 4473
[TakeutiZaring] p. 16	Exercise 6	opth 4271
[TakeutiZaring] p. 16	Exercise 8	rext 4249
[TakeutiZaring] p. 16	Corollary 5.8	unex 4477  unexg 4479
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3672
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3841
[TakeutiZaring] p. 16	Definition 5.6	df-in 3163  df-un 3161
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3854  uniprg 3855
[TakeutiZaring] p. 17	Axiom 4	vpwex 4213
[TakeutiZaring] p. 17	Exercise 1	eltp 3671
[TakeutiZaring] p. 17	Exercise 5	elsuc 4442  elsucg 4440  sstr2 3191
[TakeutiZaring] p. 17	Exercise 6	uncom 3308
[TakeutiZaring] p. 17	Exercise 7	incom 3356
[TakeutiZaring] p. 17	Exercise 8	unass 3321
[TakeutiZaring] p. 17	Exercise 9	inass 3374
[TakeutiZaring] p. 17	Exercise 10	indi 3411
[TakeutiZaring] p. 17	Exercise 11	undi 3412
[TakeutiZaring] p. 17	Definition 5.9	ssalel 3172
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3608
[TakeutiZaring] p. 18	Exercise 7	unss2 3335
[TakeutiZaring] p. 18	Exercise 9	df-ss 3170  dfss2 3174  sseqin2 3383
[TakeutiZaring] p. 18	Exercise 10	ssid 3204
[TakeutiZaring] p. 18	Exercise 12	inss1 3384  inss2 3385
[TakeutiZaring] p. 18	Exercise 13	nssr 3244
[TakeutiZaring] p. 18	Exercise 15	unieq 3849
[TakeutiZaring] p. 18	Exercise 18	sspwb 4250
[TakeutiZaring] p. 18	Exercise 19	pweqb 4257
[TakeutiZaring] p. 20	Definition	df-rab 2484
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4161
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3159
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3453
[TakeutiZaring] p. 20	Proposition 5.15	difid 3520  difidALT 3521
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3464
[TakeutiZaring] p. 21	Theorem 5.22	setind 4576
[TakeutiZaring] p. 21	Definition 5.20	df-v 2765
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4166
[TakeutiZaring] p. 22	Exercise 1	0ss 3490
[TakeutiZaring] p. 22	Exercise 3	ssex 4171  ssexg 4173
[TakeutiZaring] p. 22	Exercise 4	inex1 4168
[TakeutiZaring] p. 22	Exercise 5	ruv 4587
[TakeutiZaring] p. 22	Exercise 6	elirr 4578
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3516
[TakeutiZaring] p. 22	Exercise 11	difdif 3289
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3425
[TakeutiZaring] p. 22	Exercise 14	difss 3290
[TakeutiZaring] p. 22	Exercise 15	sscon 3298
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2480
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2481
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4779  xpexg 4778  xpexgALT 6199
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4671
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5323
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5477  fun11 5326
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5270  svrelfun 5324
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4854
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4856
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4676
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4677
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4673
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5125  dfrel2 5121
[TakeutiZaring] p. 25	Exercise 3	xpss 4772
[TakeutiZaring] p. 25	Exercise 5	relun 4781
[TakeutiZaring] p. 25	Exercise 6	reluni 4787
[TakeutiZaring] p. 25	Exercise 9	inxp 4801
[TakeutiZaring] p. 25	Exercise 12	relres 4975
[TakeutiZaring] p. 25	Exercise 13	opelres 4952  opelresg 4954
[TakeutiZaring] p. 25	Exercise 14	dmres 4968
[TakeutiZaring] p. 25	Exercise 15	resss 4971
[TakeutiZaring] p. 25	Exercise 17	resabs1 4976
[TakeutiZaring] p. 25	Exercise 18	funres 5300
[TakeutiZaring] p. 25	Exercise 24	relco 5169
[TakeutiZaring] p. 25	Exercise 29	funco 5299
[TakeutiZaring] p. 25	Exercise 30	f1co 5478
[TakeutiZaring] p. 26	Definition 6.10	eu2 2089
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5267  fv3 5584
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5209  cnvexg 5208
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4933  dmexg 4931
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4934  rnexg 4932
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5578
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5588  tz6.12 5589  tz6.12c 5591
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5552
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5262
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5263
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5265  wfo 5257
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5264  wf1 5256
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5266  wf1o 5258
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5662  eqfnfv2 5663  eqfnfv2f 5666
[TakeutiZaring] p. 28	Exercise 5	fvco 5634
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5787  fnexALT 6177
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5786  resfunexgALT 6174
[TakeutiZaring] p. 29	Exercise 9	funimaex 5344  funimaexg 5343
[TakeutiZaring] p. 29	Definition 6.18	df-br 4035
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5040  iniseg 5042
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4325
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5268
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5860
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5861
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5866
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5868
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5876
[TakeutiZaring] p. 35	Notation	wtr 4132
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4390
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4136
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4613
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4417
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4421
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4529
[TakeutiZaring] p. 38	Definition 7.11	df-on 4404
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4523
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4589
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4619
[TakeutiZaring] p. 40	Exercise 7	dftr2 4134
[TakeutiZaring] p. 40	Exercise 11	unon 4548
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4524
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3868
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4407
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4451  sucidg 4452
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4538
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4405
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4543  ordelsuc 4542
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4631
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4632
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4633
[TakeutiZaring] p. 43	Axiom 7	omex 4630
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4644
[TakeutiZaring] p. 43	Corollary 7.31	find 4636
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4634
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4635
[TakeutiZaring] p. 44	Exercise 2	int0 3889
[TakeutiZaring] p. 44	Exercise 3	trintssm 4148
[TakeutiZaring] p. 44	Exercise 4	intss1 3890
[TakeutiZaring] p. 44	Exercise 6	onintonm 4554
[TakeutiZaring] p. 44	Definition 7.35	df-int 3876
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6375
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6432  tfri1d 6402
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6433  tfri2d 6403
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6434
[TakeutiZaring] p. 50	Exercise 3	smoiso 6369
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6353
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6531
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6527
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6524
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6528
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6576  nnaordi 6575
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3962  uniss2 3871
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6537
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6547
[TakeutiZaring] p. 62	Exercise 5	oaword1 6538
[TakeutiZaring] p. 62	Definition 8.15	om0 6525  omsuc 6539
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6548
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6584  nnmordi 6583
[TakeutiZaring] p. 67	Definition 8.30	oei0 6526
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7267
[TakeutiZaring] p. 88	Exercise 1	en0 6863
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6927
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6928
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6811  isfi 6829
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6899
[TakeutiZaring] p. 95	Definition 10.42	df-map 6718
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 6905
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6918
[Tarski] p. 67	Axiom B5	ax-4 1524
[Tarski] p. 68	Lemma 6	equid 1715
[Tarski] p. 69	Lemma 7	equcomi 1718
[Tarski] p. 70	Lemma 14	spim 1752  spime 1755  spimeh 1753  spimh 1751
[Tarski] p. 70	Lemma 16	ax-11 1520  ax-11o 1837  ax11i 1728
[Tarski] p. 70	Lemmas 16 and 17	sb6 1901
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1540
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2169  ax-14 2170
[WhiteheadRussell] p. 96	Axiom *1.3	olc 712
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 728
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 757
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 766
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 790
[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 838
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2143  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 738
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 837
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 630
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 886
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 844
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 857
[WhiteheadRussell] p. 103	Theorem *2.16	con3 643
[WhiteheadRussell] p. 103	Theorem *2.17	condc 854
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 856
[WhiteheadRussell] p. 104	Theorem *2.2	orc 713
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 776
[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 894
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 908
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 769
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 770
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 805
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 806
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 804
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 981
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 779
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 777
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 778
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 739
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 740
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 868  pm2.5gdc 867
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 863
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 741
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 742
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 743
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 656
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 657
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 723
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 892
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 726
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 727
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 866
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 749
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 801
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 802
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 660
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 714  pm2.67 744
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 870  pm2.521gdc 869
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 748
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 811
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 895
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 916
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 807
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 808
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 810
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 809
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 812
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 813
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 906
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 755
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 959
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 960
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 961
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 754
[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 694
[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 861
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 860
[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 690
[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 756  pm3.44 716
[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 786
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 872
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 873
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 891
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 695
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 954  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 758  pm4.25 759
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 819
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 729
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 768
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 793
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 605
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 823
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 982
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 817
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 973
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 951
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 780
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 815  pm4.45 785  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1495
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 958
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 898  imorr 722
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 900
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 751
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 752
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 903
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 940
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 753  pm4.56 781
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 941  oranim 782
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 687
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 899
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 887
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 901
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 688
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 902
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 888
[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 828
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 745
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 603  pm4.76 604
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 711  pm4.77 800
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 783
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 904
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 708
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 909
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 952
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 953
[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 910
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 911
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 913
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 912
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1400
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 829
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 905
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1405  pm5.18dc 884
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 707
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 696
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1403
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1408
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1409
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 896
[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 927  pm5.6r 928
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 956
[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 918
[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 926
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 803
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 919
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 914
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 795
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 947
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 948
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 963
[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 964
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1649
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1499
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1646
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1910
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2048
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2448
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2449
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2902
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3046
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5239
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5240
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2124  eupickbi 2127
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5267
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7271