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 7217  fidcenum 7058
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7058
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7217
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12796
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7029
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 7015
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12811
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12813
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12802  znnen 12769
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12814
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12815
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10921
[AczelRathjen], p. 183	Chapter 20	ax-setind 4585
[AhoHopUll] p. 318	Section 9.1	df-concat 11047  df-substr 11099  df-word 10995  lencl 10998  wrd0 11019
[Apostol] p. 18	Theorem I.1	addcan 8252  addcan2d 8257  addcan2i 8255  addcand 8256  addcani 8254
[Apostol] p. 18	Theorem I.2	negeu 8263
[Apostol] p. 18	Theorem I.3	negsub 8320  negsubd 8389  negsubi 8350
[Apostol] p. 18	Theorem I.4	negneg 8322  negnegd 8374  negnegi 8342
[Apostol] p. 18	Theorem I.5	subdi 8457  subdid 8486  subdii 8479  subdir 8458  subdird 8487  subdiri 8480
[Apostol] p. 18	Theorem I.6	mul01 8461  mul01d 8465  mul01i 8463  mul02 8459  mul02d 8464  mul02i 8462
[Apostol] p. 18	Theorem I.9	divrecapd 8866
[Apostol] p. 18	Theorem I.10	recrecapi 8817
[Apostol] p. 18	Theorem I.12	mul2neg 8470  mul2negd 8485  mul2negi 8478  mulneg1 8467  mulneg1d 8483  mulneg1i 8476
[Apostol] p. 18	Theorem I.14	rdivmuldivd 13906
[Apostol] p. 18	Theorem I.15	divdivdivap 8786
[Apostol] p. 20	Axiom 7	rpaddcl 9799  rpaddcld 9834  rpmulcl 9800  rpmulcld 9835
[Apostol] p. 20	Axiom 9	0nrp 9811
[Apostol] p. 20	Theorem I.17	lttri 8177
[Apostol] p. 20	Theorem I.18	ltadd1d 8611  ltadd1dd 8629  ltadd1i 8575
[Apostol] p. 20	Theorem I.19	ltmul1 8665  ltmul1a 8664  ltmul1i 8993  ltmul1ii 9001  ltmul2 8929  ltmul2d 9861  ltmul2dd 9875  ltmul2i 8996
[Apostol] p. 20	Theorem I.21	0lt1 8199
[Apostol] p. 20	Theorem I.23	lt0neg1 8541  lt0neg1d 8588  ltneg 8535  ltnegd 8596  ltnegi 8566
[Apostol] p. 20	Theorem I.25	lt2add 8518  lt2addd 8640  lt2addi 8583
[Apostol] p. 20	Definition of positive numbers	df-rp 9776
[Apostol] p. 21	Exercise 4	recgt0 8923  recgt0d 9007  recgt0i 8979  recgt0ii 8980
[Apostol] p. 22	Definition of integers	df-z 9373
[Apostol] p. 22	Definition of rationals	df-q 9741
[Apostol] p. 24	Theorem I.26	supeuti 7096
[Apostol] p. 26	Theorem I.29	arch 9292
[Apostol] p. 28	Exercise 2	btwnz 9492
[Apostol] p. 28	Exercise 3	nnrecl 9293
[Apostol] p. 28	Exercise 6	qbtwnre 10399
[Apostol] p. 28	Exercise 10(a)	zeneo 12182  zneo 9474
[Apostol] p. 29	Theorem I.35	resqrtth 11342  sqrtthi 11430
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9039
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12357
[Apostol] p. 363	Remark	absgt0api 11457
[Apostol] p. 363	Example	abssubd 11504  abssubi 11461
[ApostolNT] p. 14	Definition	df-dvds 12099
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 12115
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12139
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12135
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12129
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12131
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 12116
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 12117
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 12122
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12156
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12158
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12160
[ApostolNT] p. 15	Definition	dfgcd2 12335
[ApostolNT] p. 16	Definition	isprm2 12439
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12414
[ApostolNT] p. 16	Theorem 1.7	prminf 12826
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12294
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12336
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12338
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12308
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12301
[ApostolNT] p. 17	Theorem 1.8	coprm 12466
[ApostolNT] p. 17	Theorem 1.9	euclemma 12468
[ApostolNT] p. 17	Theorem 1.10	1arith2 12691
[ApostolNT] p. 19	Theorem 1.14	divalg 12235
[ApostolNT] p. 20	Theorem 1.15	eucalg 12381
[ApostolNT] p. 25	Definition	df-phi 12533
[ApostolNT] p. 26	Theorem 2.2	phisum 12563
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12544
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12548
[ApostolNT] p. 38	Remark	df-sgm 15454
[ApostolNT] p. 38	Definition	df-sgm 15454
[ApostolNT] p. 104	Definition	congr 12422
[ApostolNT] p. 106	Remark	dvdsval3 12102
[ApostolNT] p. 106	Definition	moddvds 12110
[ApostolNT] p. 107	Example 2	mod2eq0even 12189
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12190
[ApostolNT] p. 107	Example 4	zmod1congr 10486
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10523
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10811
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12134
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12425
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 12744
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12427
[ApostolNT] p. 113	Theorem 5.17	eulerth 12555
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12574
[ApostolNT] p. 114	Theorem 5.19	fermltl 12556
[ApostolNT] p. 179	Definition	df-lgs 15475  lgsprme0 15519
[ApostolNT] p. 180	Example 1	1lgs 15520
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 15496
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 15511
[ApostolNT] p. 181	Theorem 9.4	m1lgs 15562
[ApostolNT] p. 181	Theorem 9.5	2lgs 15581  2lgsoddprm 15590
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 15546
[ApostolNT] p. 185	Theorem 9.8	lgsquad 15557
[ApostolNT] p. 188	Definition	df-lgs 15475  lgs1 15521
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 15512
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 15514
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 15522
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 15523
[Bauer] p. 482	Section 1.2	pm2.01 617  pm2.65 661
[Bauer] p. 483	Theorem 1.3	acexmid 5943  onsucelsucexmidlem 4577
[Bauer], p. 481	Section 1.1	pwtrufal 15934
[Bauer], p. 483	Definition	n0rf 3473
[Bauer], p. 483	Theorem 1.2	2irrexpq 15448  2irrexpqap 15450
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6973
[Bauer], p. 493	Section 5.1	ivthdich 15125
[Bauer], p. 494	Theorem 5.5	ivthinc 15115
[BauerHanson], p. 27	Proposition 5.2	cnstab 8718
[BauerSwan], p. 14	Remark	0ct 7209  ctm 7211
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 15937
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7217
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7614
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7527
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7616
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7650  addlocpr 7649
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7676
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7679
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7684
[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 4165
[BellMachover] p. 466	Axiom Pow	axpow3 4221
[BellMachover] p. 466	Axiom Union	axun2 4482
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4590
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4431
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4593
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4544
[BellMachover] p. 471	Definition of Lim	df-ilim 4416
[BellMachover] p. 472	Axiom Inf	zfinf2 4637
[BellMachover] p. 473	Theorem 2.8	limom 4662
[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 15653
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13188
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13234
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13249
[BourbakiAlg1] p. 92	Definition 1	df-ring 13760
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 13695
[BourbakiEns] p.	Proposition 8	fcof1 5852  fcofo 5853
[BourbakiTop1] p.	Remark	xnegmnf 9951  xnegpnf 9950
[BourbakiTop1] p.	Remark	rexneg 9952
[BourbakiTop1] p.	Proposition	ishmeo 14776
[BourbakiTop1] p.	Property V_i	ssnei2 14629
[BourbakiTop1] p.	Property V_ii	innei 14635
[BourbakiTop1] p.	Property V_iv	neissex 14637
[BourbakiTop1] p.	Proposition 1	neipsm 14626  neiss 14622
[BourbakiTop1] p.	Proposition 2	cnptopco 14694
[BourbakiTop1] p.	Proposition 4	imasnopn 14771
[BourbakiTop1] p.	Property V_iii	elnei 14624
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14470
[Bruck] p. 1	Section I.1	df-mgm 13188
[Bruck] p. 23	Section II.1	df-sgrp 13234
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13431
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4107
[Cohen] p. 301	Remark	relogoprlem 15340
[Cohen] p. 301	Property 2	relogmul 15341  relogmuld 15356
[Cohen] p. 301	Property 3	relogdiv 15342  relogdivd 15357
[Cohen] p. 301	Property 4	relogexp 15344
[Cohen] p. 301	Property 1a	log1 15338
[Cohen] p. 301	Property 1b	loge 15339
[Cohen4] p. 348	Observation	relogbcxpbap 15437
[Cohen4] p. 352	Definition	rpelogb 15421
[Cohen4] p. 361	Property 2	rprelogbmul 15427
[Cohen4] p. 361	Property 3	logbrec 15432  rprelogbdiv 15429
[Cohen4] p. 361	Property 4	rplogbreexp 15425
[Cohen4] p. 361	Property 6	relogbexpap 15430
[Cohen4] p. 361	Property 1(a)	rplogbid1 15419
[Cohen4] p. 361	Property 1(b)	rplogb1 15420
[Cohen4] p. 367	Property	rplogbchbase 15422
[Cohen4] p. 377	Property 2	logblt 15434
[Crosilla] p.	Axiom 1	ax-ext 2187
[Crosilla] p.	Axiom 2	ax-pr 4253
[Crosilla] p.	Axiom 3	ax-un 4480
[Crosilla] p.	Axiom 4	ax-nul 4170
[Crosilla] p.	Axiom 5	ax-iinf 4636
[Crosilla] p.	Axiom 6	ru 2997
[Crosilla] p.	Axiom 8	ax-pow 4218
[Crosilla] p.	Axiom 9	ax-setind 4585
[Crosilla], p.	Axiom 6	ax-sep 4162
[Crosilla], p.	Axiom 7	ax-coll 4159
[Crosilla], p.	Axiom 7'	repizf 4160
[Crosilla], p.	Theorem is stated	ordtriexmid 4569
[Crosilla], p.	Axiom of choice implies instances	acexmid 5943
[Crosilla], p.	Definition of ordinal	df-iord 4413
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4583
[Eisenberg] p. 67	Definition 5.3	df-dif 3168
[Eisenberg] p. 82	Definition 6.3	df-iom 4639
[Eisenberg] p. 125	Definition 8.21	df-map 6737
[Enderton] p. 18	Axiom of Empty Set	axnul 4169
[Enderton] p. 19	Definition	df-tp 3641
[Enderton] p. 26	Exercise 5	unissb 3880
[Enderton] p. 26	Exercise 10	pwel 4262
[Enderton] p. 28	Exercise 7(b)	pwunim 4333
[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 4527  iunpwss 4019
[Enderton] p. 38	Exercise 6(a)	unipw 4261
[Enderton] p. 38	Exercise 6(b)	pwuni 4236
[Enderton] p. 41	Lemma 3D	opeluu 4497  rnex 4946  rnexg 4943
[Enderton] p. 41	Exercise 8	dmuni 4888  rnuni 5094
[Enderton] p. 42	Definition of a function	dffun7 5298  dffun8 5299
[Enderton] p. 43	Definition of function value	funfvdm2 5643
[Enderton] p. 43	Definition of single-rooted	funcnv 5335
[Enderton] p. 44	Definition (d)	dfima2 5024  dfima3 5025
[Enderton] p. 47	Theorem 3H	fvco2 5648
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7318
[Enderton] p. 50	Theorem 3K(a)	imauni 5830
[Enderton] p. 52	Definition	df-map 6737
[Enderton] p. 53	Exercise 21	coass 5201
[Enderton] p. 53	Exercise 27	dmco 5191
[Enderton] p. 53	Exercise 14(a)	funin 5345
[Enderton] p. 53	Exercise 22(a)	imass2 5058
[Enderton] p. 54	Remark	ixpf 6807  ixpssmap 6819
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6786
[Enderton] p. 56	Theorem 3M	erref 6640
[Enderton] p. 57	Lemma 3N	erthi 6668
[Enderton] p. 57	Definition	df-ec 6622
[Enderton] p. 58	Definition	df-qs 6626
[Enderton] p. 60	Theorem 3Q	th3q 6727  th3qcor 6726  th3qlem1 6724  th3qlem2 6725
[Enderton] p. 61	Exercise 35	df-ec 6622
[Enderton] p. 65	Exercise 56(a)	dmun 4885
[Enderton] p. 68	Definition of successor	df-suc 4418
[Enderton] p. 71	Definition	df-tr 4143  dftr4 4147
[Enderton] p. 72	Theorem 4E	unisuc 4460  unisucg 4461
[Enderton] p. 73	Exercise 6	unisuc 4460  unisucg 4461
[Enderton] p. 73	Exercise 5(a)	truni 4156
[Enderton] p. 73	Exercise 5(b)	trint 4157
[Enderton] p. 79	Theorem 4I(A1)	nna0 6560
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6562  onasuc 6552
[Enderton] p. 79	Definition of operation value	df-ov 5947
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6561
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6563  onmsuc 6559
[Enderton] p. 81	Theorem 4K(1)	nnaass 6571
[Enderton] p. 81	Theorem 4K(2)	nna0r 6564  nnacom 6570
[Enderton] p. 81	Theorem 4K(3)	nndi 6572
[Enderton] p. 81	Theorem 4K(4)	nnmass 6573
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6575
[Enderton] p. 82	Exercise 16	nnm0r 6565  nnmsucr 6574
[Enderton] p. 88	Exercise 23	nnaordex 6614
[Enderton] p. 129	Definition	df-en 6828
[Enderton] p. 132	Theorem 6B(b)	canth 5897
[Enderton] p. 133	Exercise 1	xpomen 12766
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6962
[Enderton] p. 136	Corollary 6E	nneneq 6954
[Enderton] p. 139	Theorem 6H(c)	mapen 6943
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7330
[Enderton] p. 143	Theorem 6J	dju0en 7326  dju1en 7325
[Enderton] p. 144	Corollary 6K	undif2ss 3536
[Enderton] p. 145	Figure 38	ffoss 5554
[Enderton] p. 145	Definition	df-dom 6829
[Enderton] p. 146	Example 1	domen 6840  domeng 6841
[Enderton] p. 146	Example 3	nndomo 6961
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6930  xpdom1g 6928  xpdom2g 6927
[Enderton] p. 168	Definition	df-po 4343
[Enderton] p. 192	Theorem 7M(a)	oneli 4475
[Enderton] p. 192	Theorem 7M(b)	ontr1 4436
[Enderton] p. 192	Theorem 7M(c)	onirri 4591
[Enderton] p. 193	Corollary 7N(b)	0elon 4439
[Enderton] p. 193	Corollary 7N(c)	onsuci 4564
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4537
[Enderton] p. 194	Remark	onprc 4600
[Enderton] p. 194	Exercise 16	suc11 4606
[Enderton] p. 197	Definition	df-card 7286
[Enderton] p. 200	Exercise 25	tfis 4631
[Enderton] p. 206	Theorem 7X(b)	en2lp 4602
[Enderton] p. 207	Exercise 34	opthreg 4604
[Enderton] p. 208	Exercise 35	suc11g 4605
[Geuvers], p. 1	Remark	expap0 10714
[Geuvers], p. 6	Lemma 2.13	mulap0r 8688
[Geuvers], p. 6	Lemma 2.15	mulap0 8727
[Geuvers], p. 9	Lemma 2.35	msqge0 8689
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8044
[Geuvers], p. 10	Lemma 3.9	maxcom 11514
[Geuvers], p. 10	Lemma 3.10	maxle1 11522  maxle2 11523
[Geuvers], p. 10	Lemma 3.11	maxleast 11524
[Geuvers], p. 10	Lemma 3.12	maxleb 11527
[Geuvers], p. 11	Definition 3.13	dfabsmax 11528
[Geuvers], p. 17	Definition 6.1	df-ap 8655
[Gleason] p. 117	Proposition 9-2.1	df-enq 7460  enqer 7471
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7464  df-nqqs 7461
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7457  df-plqqs 7462
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7458  df-mqqs 7463
[Gleason] p. 119	Proposition 9-2.5	df-rq 7465
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7521
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7524  ltbtwnnq 7529  ltbtwnnqq 7528
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7513
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7514
[Gleason] p. 123	Proposition 9-3.5	addclpr 7650
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7692
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7691
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7710
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7726
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7732  ltaprlem 7731
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7729
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7685
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7705
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7694
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7693
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7701
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7751
[Gleason] p. 126	Proposition 9-4.1	df-enr 7839  enrer 7848
[Gleason] p. 126	Proposition 9-4.2	df-0r 7844  df-1r 7845  df-nr 7840
[Gleason] p. 126	Proposition 9-4.3	df-mr 7842  df-plr 7841  negexsr 7885  recexsrlem 7887
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7843
[Gleason] p. 130	Proposition 10-1.3	creui 9033  creur 9032  cru 8675
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8036  axcnre 7994
[Gleason] p. 132	Definition 10-3.1	crim 11169  crimd 11288  crimi 11248  crre 11168  crred 11287  crrei 11247
[Gleason] p. 132	Definition 10-3.2	remim 11171  remimd 11253
[Gleason] p. 133	Definition 10.36	absval2 11368  absval2d 11496  absval2i 11455
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11195  cjaddd 11276  cjaddi 11243
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11196  cjmuld 11277  cjmuli 11244
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11194  cjcjd 11254  cjcji 11226
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11193  cjreb 11177  cjrebd 11257  cjrebi 11229  cjred 11282  rere 11176  rereb 11174  rerebd 11256  rerebi 11228  rered 11280
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11202  addcjd 11268  addcji 11238
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11312
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11363  abscjd 11501  abscji 11459
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11375  abs00d 11497  abs00i 11456  absne0d 11498
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11407  releabsd 11502  releabsi 11460
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11380  absmuld 11505  absmuli 11462
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11366  sqabsaddi 11463
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11415  abstrid 11507  abstrii 11466
[Gleason] p. 134	Definition 10-4.1	df-exp 10684  exp0 10688  expp1 10691  expp1d 10819
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10726  expaddd 10820
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15384  cxpmuld 15409  expmul 10729  expmuld 10821
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10723  mulexpd 10833  rpmulcxp 15381
[Gleason] p. 141	Definition 11-2.1	fzval 10132
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11637
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11639
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11638
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11642
[Gleason] p. 172	Corollary 12-2.5	climrecl 11635
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11631  climcj 11632  climim 11634  climre 11633
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8112  df-xr 8111  ltxr 9897
[Gleason] p. 180	Theorem 12-5.3	climcau 11658
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10443
[Gleason] p. 223	Definition 14-1.1	df-met 14307
[Gleason] p. 223	Definition 14-1.1(a)	met0 14836  xmet0 14835
[Gleason] p. 223	Definition 14-1.1(c)	metsym 14843
[Gleason] p. 223	Definition 14-1.1(d)	mettri 14845  mstri 14945  xmettri 14844  xmstri 14944
[Gleason] p. 230	Proposition 14-2.6	txlm 14751
[Gleason] p. 240	Proposition 14-4.2	metcnp3 14983
[Gleason] p. 243	Proposition 14-4.16	addcn2 11621  addcncntop 15034  mulcn2 11623  mulcncntop 15036  subcn2 11622  subcncntop 15035
[Gleason] p. 295	Remark	bcval3 10896  bcval4 10897
[Gleason] p. 295	Equation 2	bcpasc 10911
[Gleason] p. 295	Definition of binomial coefficient	bcval 10894  df-bc 10893
[Gleason] p. 296	Remark	bcn0 10900  bcnn 10902
[Gleason] p. 296	Theorem 15-2.8	binom 11795
[Gleason] p. 308	Equation 2	ef0 11983
[Gleason] p. 308	Equation 3	efcj 11984
[Gleason] p. 309	Corollary 15-4.3	efne0 11989
[Gleason] p. 309	Corollary 15-4.4	efexp 11993
[Gleason] p. 310	Equation 14	sinadd 12047
[Gleason] p. 310	Equation 15	cosadd 12048
[Gleason] p. 311	Equation 17	sincossq 12059
[Gleason] p. 311	Equation 18	cosbnd 12064  sinbnd 12063
[Gleason] p. 311	Definition of ` `	df-pi 11964
[Golan] p. 1	Remark	srgisid 13748
[Golan] p. 1	Definition	df-srg 13726
[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 13343  mndideu 13258
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13370
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13399
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13410
[Herstein] p. 57	Exercise 1	dfgrp3me 13432
[Heyting] p. 127	Axiom #1	ax1hfs 16013
[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 7337
[HoTT], p.	Theorem 7.2.6	nndceq 6585
[HoTT], p.	Exercise 11.10	neapmkv 16007
[HoTT], p.	Exercise 11.11	mulap0bd 8730
[HoTT], p.	Section 11.2.1	df-iltp 7583  df-imp 7582  df-iplp 7581  df-reap 8648
[HoTT], p.	Theorem 11.2.4	recapb 8744  rerecapb 8916
[HoTT], p.	Corollary 3.9.2	uchoice 6223
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7775
[HoTT], p.	Corollary 11.4.3	conventions 15657
[HoTT], p.	Exercise 11.6(i)	dcapnconst 16000  dceqnconst 15999
[HoTT], p.	Corollary 11.2.13	axcaucvg 8013  caucvgpr 7795  caucvgprpr 7825  caucvgsr 7915
[HoTT], p.	Definition 11.2.1	df-inp 7579
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 16005
[HoTT], p.	Proposition 11.2.3	df-iso 4344  ltpopr 7708  ltsopr 7709
[HoTT], p.	Definition 11.2.7(v)	apsym 8679  reapcotr 8671  reapirr 8650
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8199  gt0add 8646  leadd1 8503  lelttr 8161  lemul1a 8931  lenlt 8148  ltadd1 8502  ltletr 8162  ltmul1 8665  reaplt 8661
[Jech] p. 4	Definition of class	cv 1372  cvjust 2200
[Jech] p. 78	Note	opthprc 4726
[KalishMontague] p. 81	Note 1	ax-i9 1553
[Kreyszig] p. 3	Property M1	metcl 14825  xmetcl 14824
[Kreyszig] p. 4	Property M2	meteq0 14832
[Kreyszig] p. 12	Equation 5	muleqadd 8741
[Kreyszig] p. 18	Definition 1.3-2	mopnval 14914
[Kreyszig] p. 19	Remark	mopntopon 14915
[Kreyszig] p. 19	Theorem T1	mopn0 14960  mopnm 14920
[Kreyszig] p. 19	Theorem T2	unimopn 14958
[Kreyszig] p. 19	Definition of neighborhood	neibl 14963
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 14985
[Kreyszig] p. 25	Definition 1.4-1	lmbr 14685
[Kreyszig] p. 51	Equation 2	lmodvneg1 14092
[Kreyszig] p. 51	Equation 1a	lmod0vs 14083
[Kreyszig] p. 51	Equation 1b	lmodvs0 14084
[Kunen] p. 10	Axiom 0	a9e 1719
[Kunen] p. 12	Axiom 6	zfrep6 4161
[Kunen] p. 24	Definition 10.24	mapval 6747  mapvalg 6745
[Kunen] p. 31	Definition 10.24	mapex 6741
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3937
[Lang] p. 3	Statement	lidrideqd 13213  mndbn0 13263
[Lang] p. 3	Definition	df-mnd 13249
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 13230
[Lang] p. 5	Equation	gsumfzreidx 13673
[Lang] p. 6	Definition	mulgnn0gsum 13464
[Lang] p. 7	Definition	dfgrp2e 13360
[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 4523
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3849
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4329
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4330
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4331
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3870
[Mendelson] p. 235	Exercise 4.12(p)	reli 4807
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5203
[Mendelson] p. 246	Definition of successor	df-suc 4418
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6942
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6916  xpsneng 6917
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6922  xpcomeng 6923
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6925
[Mendelson] p. 255	Exercise 4.39	endisj 6919
[Mendelson] p. 255	Exercise 4.41	mapprc 6739
[Mendelson] p. 255	Exercise 4.43	mapsnen 6903
[Mendelson] p. 255	Exercise 4.47	xpmapen 6947
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6773
[Mendelson] p. 255	Exercise 4.42(b)	map1 6904
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7329  djucomen 7328
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7327
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6553
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3395
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4763
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4764
[Monk1] p. 34	Definition 3.3	df-opab 4106
[Monk1] p. 36	Theorem 3.7(i)	coi1 5198  coi2 5199
[Monk1] p. 36	Theorem 3.8(v)	dm0 4892  rn0 4934
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5087
[Monk1] p. 37	Theorem 3.13(i)	relxp 4784
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4898  rnxpm 5112
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4755  xp0 5102
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5041
[Monk1] p. 38	Theorem 3.16(viii)	imai 5038
[Monk1] p. 39	Theorem 3.17	imaex 5037  imaexg 5036
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5033
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5710  funfvop 5692
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5622
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5630
[Monk1] p. 43	Theorem 4.6	funun 5315
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5837  dff13f 5839
[Monk1] p. 46	Theorem 4.15(v)	funex 5807  funrnex 6199
[Monk1] p. 50	Definition 5.4	fniunfv 5831
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5166
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3901
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6241  df-1st 6226
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6242  df-2nd 6227
[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 4287
[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 16014
[Munkres] p. 77	Example 2	distop 14557
[Munkres] p. 78	Definition of basis	df-bases 14515  isbasis3g 14518
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 13092  tgval2 14523
[Munkres] p. 79	Remark	tgcl 14536
[Munkres] p. 80	Lemma 2.1	tgval3 14530
[Munkres] p. 80	Lemma 2.2	tgss2 14551  tgss3 14550
[Munkres] p. 81	Lemma 2.3	basgen 14552  basgen2 14553
[Munkres] p. 89	Definition of subspace topology	resttop 14642
[Munkres] p. 93	Theorem 6.1(1)	0cld 14584  topcld 14581
[Munkres] p. 93	Theorem 6.1(3)	uncld 14585
[Munkres] p. 94	Definition of closure	clsval 14583
[Munkres] p. 94	Definition of interior	ntrval 14582
[Munkres] p. 102	Definition of continuous function	df-cn 14660  iscn 14669  iscn2 14672
[Munkres] p. 107	Theorem 7.2(g)	cncnp 14702  cncnp2m 14703  cncnpi 14700  df-cnp 14661  iscnp 14671
[Munkres] p. 127	Theorem 10.1	metcn 14986
[Pierik], p. 8	Section 2.2.1	dfrex2fin 7000
[Pierik], p. 9	Definition 2.4	df-womni 7266
[Pierik], p. 9	Definition 2.5	df-markov 7254  omniwomnimkv 7269
[Pierik], p. 10	Section 2.3	dfdif3 3283
[Pierik], p. 14	Definition 3.1	df-omni 7237  exmidomniim 7243  finomni 7242
[Pierik], p. 15	Section 3.1	df-nninf 7222
[Pradic2025], p. 2	Section 1.1	nnnninfen 15958
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 15962
[PradicBrown2022], p. 2	Remark	exmidpw 7005
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7309
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7310  exmidfodomrlemrALT 7311
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7251
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 15944  peano4nninf 15943
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 15946
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 15954
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 15956
[PradicBrown2022], p. 5	Definition 3.3	nnsf 15942
[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 4228  snexprc 4230
[Quine] p. 51	Theorem 7.13	prexg 4255
[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 5242
[Quine] p. 56	Definition 8.18	dfiota2 5233
[Quine] p. 57	Theorem 8.19	iotaval 5243
[Quine] p. 57	Theorem 8.22	iotanul 5247
[Quine] p. 58	Theorem 8.23	euiotaex 5248
[Quine] p. 58	Definition 9.1	df-op 3642
[Quine] p. 61	Theorem 9.5	opabid 4302  opabidw 4303  opelopab 4318  opelopaba 4312  opelopabaf 4320  opelopabf 4321  opelopabg 4314  opelopabga 4309  opelopabgf 4316  oprabid 5976
[Quine] p. 64	Definition 9.11	df-xp 4681
[Quine] p. 64	Definition 9.12	df-cnv 4683
[Quine] p. 64	Definition 9.15	df-id 4340
[Quine] p. 65	Theorem 10.3	fun0 5332
[Quine] p. 65	Theorem 10.4	funi 5303
[Quine] p. 65	Theorem 10.5	funsn 5322  funsng 5320
[Quine] p. 65	Definition 10.1	df-fun 5273
[Quine] p. 65	Definition 10.2	args 5051  dffv4g 5573
[Quine] p. 68	Definition 10.11	df-fv 5279  fv2 5571
[Quine] p. 124	Theorem 17.3	nn0opth2 10869  nn0opth2d 10868  nn0opthd 10867
[Quine] p. 284	Axiom 39(vi)	funimaex 5359  funimaexg 5358
[Roman] p. 18	Part Preliminaries	df-rng 13695
[Roman] p. 19	Part Preliminaries	df-ring 13760
[Rudin] p. 164	Equation 27	efcan 11987
[Rudin] p. 164	Equation 30	efzval 11994
[Rudin] p. 167	Equation 48	absefi 12080
[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 5067
[Schechter] p. 51	Definition of irreflexivity	intirr 5069
[Schechter] p. 51	Definition of symmetry	cnvsym 5066
[Schechter] p. 51	Definition of transitivity	cotr 5064
[Schechter] p. 187	Definition of "ring with unit"	isring 13762
[Schechter] p. 428	Definition 15.35	bastop1 14555
[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 4174
[Suppes] p. 39	Theorem 61	uniss 3871
[Suppes] p. 39	Theorem 65	uniop 4300
[Suppes] p. 41	Theorem 70	intsn 3920
[Suppes] p. 42	Theorem 71	intpr 3917  intprg 3918
[Suppes] p. 42	Theorem 73	op1stb 4525  op1stbg 4526
[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 4201  elpw2g 4200  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 4782
[Suppes] p. 52	Theorem 102	xpindi 4813  xpindir 4814
[Suppes] p. 52	Theorem 103	xpundi 4731  xpundir 4732
[Suppes] p. 54	Theorem 105	elirrv 4596
[Suppes] p. 58	Theorem 2	relss 4762
[Suppes] p. 59	Theorem 4	eldm 4875  eldm2 4876  eldm2g 4874  eldmg 4873
[Suppes] p. 59	Definition 3	df-dm 4685
[Suppes] p. 60	Theorem 6	dmin 4886
[Suppes] p. 60	Theorem 8	rnun 5091
[Suppes] p. 60	Theorem 9	rnin 5092
[Suppes] p. 60	Definition 4	dfrn2 4866
[Suppes] p. 61	Theorem 11	brcnv 4861  brcnvg 4859
[Suppes] p. 62	Equation 5	elcnv 4855  elcnv2 4856
[Suppes] p. 62	Theorem 12	relcnv 5060
[Suppes] p. 62	Theorem 15	cnvin 5090
[Suppes] p. 62	Theorem 16	cnvun 5088
[Suppes] p. 63	Theorem 20	co02 5196
[Suppes] p. 63	Theorem 21	dmcoss 4948
[Suppes] p. 63	Definition 7	df-co 4684
[Suppes] p. 64	Theorem 26	cnvco 4863
[Suppes] p. 64	Theorem 27	coass 5201
[Suppes] p. 65	Theorem 31	resundi 4972
[Suppes] p. 65	Theorem 34	elima 5027  elima2 5028  elima3 5029  elimag 5026
[Suppes] p. 65	Theorem 35	imaundi 5095
[Suppes] p. 66	Theorem 40	dminss 5097
[Suppes] p. 66	Theorem 41	imainss 5098
[Suppes] p. 67	Exercise 11	cnvxp 5101
[Suppes] p. 81	Definition 34	dfec2 6623
[Suppes] p. 82	Theorem 72	elec 6661  elecg 6660
[Suppes] p. 82	Theorem 73	erth 6666  erth2 6667
[Suppes] p. 89	Theorem 96	map0b 6774
[Suppes] p. 89	Theorem 97	map0 6776  map0g 6775
[Suppes] p. 89	Theorem 98	mapsn 6777
[Suppes] p. 89	Theorem 99	mapss 6778
[Suppes] p. 92	Theorem 1	enref 6856  enrefg 6855
[Suppes] p. 92	Theorem 2	ensym 6873  ensymb 6872  ensymi 6874
[Suppes] p. 92	Theorem 3	entr 6876
[Suppes] p. 92	Theorem 4	unen 6908
[Suppes] p. 94	Theorem 15	endom 6854
[Suppes] p. 94	Theorem 16	ssdomg 6870
[Suppes] p. 94	Theorem 17	domtr 6877
[Suppes] p. 95	Theorem 18	isbth 7069
[Suppes] p. 98	Exercise 4	fundmen 6898  fundmeng 6899
[Suppes] p. 98	Exercise 6	xpdom3m 6929
[Suppes] p. 130	Definition 3	df-tr 4143
[Suppes] p. 132	Theorem 9	ssonuni 4536
[Suppes] p. 134	Definition 6	df-suc 4418
[Suppes] p. 136	Theorem Schema 22	findes 4651  finds 4648  finds1 4650  finds2 4649
[Suppes] p. 162	Definition 5	df-ltnqqs 7466  df-ltpq 7459
[Suppes] p. 228	Theorem Schema 61	onintss 4437
[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 5948
[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 4275
[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 4484
[TakeutiZaring] p. 16	Exercise 6	opth 4281
[TakeutiZaring] p. 16	Exercise 8	rext 4259
[TakeutiZaring] p. 16	Corollary 5.8	unex 4488  unexg 4490
[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 4223
[TakeutiZaring] p. 17	Exercise 1	eltp 3681
[TakeutiZaring] p. 17	Exercise 5	elsuc 4453  elsucg 4451  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 4260
[TakeutiZaring] p. 18	Exercise 19	pweqb 4267
[TakeutiZaring] p. 20	Definition	df-rab 2493
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4171
[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 4587
[TakeutiZaring] p. 21	Definition 5.20	df-v 2774
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4176
[TakeutiZaring] p. 22	Exercise 1	0ss 3499
[TakeutiZaring] p. 22	Exercise 3	ssex 4181  ssexg 4183
[TakeutiZaring] p. 22	Exercise 4	inex1 4178
[TakeutiZaring] p. 22	Exercise 5	ruv 4598
[TakeutiZaring] p. 22	Exercise 6	elirr 4589
[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 4790  xpexg 4789  xpexgALT 6218
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4682
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5338
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5492  fun11 5341
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5282  svrelfun 5339
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4865
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4867
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4687
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4688
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4684
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5137  dfrel2 5133
[TakeutiZaring] p. 25	Exercise 3	xpss 4783
[TakeutiZaring] p. 25	Exercise 5	relun 4792
[TakeutiZaring] p. 25	Exercise 6	reluni 4798
[TakeutiZaring] p. 25	Exercise 9	inxp 4812
[TakeutiZaring] p. 25	Exercise 12	relres 4987
[TakeutiZaring] p. 25	Exercise 13	opelres 4964  opelresg 4966
[TakeutiZaring] p. 25	Exercise 14	dmres 4980
[TakeutiZaring] p. 25	Exercise 15	resss 4983
[TakeutiZaring] p. 25	Exercise 17	resabs1 4988
[TakeutiZaring] p. 25	Exercise 18	funres 5312
[TakeutiZaring] p. 25	Exercise 24	relco 5181
[TakeutiZaring] p. 25	Exercise 29	funco 5311
[TakeutiZaring] p. 25	Exercise 30	f1co 5493
[TakeutiZaring] p. 26	Definition 6.10	eu2 2098
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5279  fv3 5599
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5221  cnvexg 5220
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4945  dmexg 4942
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4946  rnexg 4943
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5593
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5603  tz6.12 5604  tz6.12c 5606
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5567
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5274
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5275
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5277  wfo 5269
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5276  wf1 5268
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5278  wf1o 5270
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5677  eqfnfv2 5678  eqfnfv2f 5681
[TakeutiZaring] p. 28	Exercise 5	fvco 5649
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5806  fnexALT 6196
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5805  resfunexgALT 6193
[TakeutiZaring] p. 29	Exercise 9	funimaex 5359  funimaexg 5358
[TakeutiZaring] p. 29	Definition 6.18	df-br 4045
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5052  iniseg 5054
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4336
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5280
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5879
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5880
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5885
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5887
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5895
[TakeutiZaring] p. 35	Notation	wtr 4142
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4401
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4146
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4624
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4428
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4432
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4540
[TakeutiZaring] p. 38	Definition 7.11	df-on 4415
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4534
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4600
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4630
[TakeutiZaring] p. 40	Exercise 7	dftr2 4144
[TakeutiZaring] p. 40	Exercise 11	unon 4559
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4535
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3878
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4418
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4462  sucidg 4463
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4549
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4416
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4554  ordelsuc 4553
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4642
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4643
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4644
[TakeutiZaring] p. 43	Axiom 7	omex 4641
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4655
[TakeutiZaring] p. 43	Corollary 7.31	find 4647
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4645
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4646
[TakeutiZaring] p. 44	Exercise 2	int0 3899
[TakeutiZaring] p. 44	Exercise 3	trintssm 4158
[TakeutiZaring] p. 44	Exercise 4	intss1 3900
[TakeutiZaring] p. 44	Exercise 6	onintonm 4565
[TakeutiZaring] p. 44	Definition 7.35	df-int 3886
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6394
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6451  tfri1d 6421
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6452  tfri2d 6422
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6453
[TakeutiZaring] p. 50	Exercise 3	smoiso 6388
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6372
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6550
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6546
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6543
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6547
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6595  nnaordi 6594
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3972  uniss2 3881
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6556
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6566
[TakeutiZaring] p. 62	Exercise 5	oaword1 6557
[TakeutiZaring] p. 62	Definition 8.15	om0 6544  omsuc 6558
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6567
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6603  nnmordi 6602
[TakeutiZaring] p. 67	Definition 8.30	oei0 6545
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7294
[TakeutiZaring] p. 88	Exercise 1	en0 6887
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6954
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6955
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6830  isfi 6852
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6926
[TakeutiZaring] p. 95	Definition 10.42	df-map 6737
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 6932
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6945
[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 5251
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5252
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2133  eupickbi 2136
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5279
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7298