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 7108  fidcenum 6949
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6949
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7108
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12409
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6923
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6911
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12424
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12426
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12415  znnen 12382
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12427
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12428
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10740
[AczelRathjen], p. 183	Chapter 20	ax-setind 4533
[Apostol] p. 18	Theorem I.1	addcan 8127  addcan2d 8132  addcan2i 8130  addcand 8131  addcani 8129
[Apostol] p. 18	Theorem I.2	negeu 8138
[Apostol] p. 18	Theorem I.3	negsub 8195  negsubd 8264  negsubi 8225
[Apostol] p. 18	Theorem I.4	negneg 8197  negnegd 8249  negnegi 8217
[Apostol] p. 18	Theorem I.5	subdi 8332  subdid 8361  subdii 8354  subdir 8333  subdird 8362  subdiri 8355
[Apostol] p. 18	Theorem I.6	mul01 8336  mul01d 8340  mul01i 8338  mul02 8334  mul02d 8339  mul02i 8337
[Apostol] p. 18	Theorem I.9	divrecapd 8739
[Apostol] p. 18	Theorem I.10	recrecapi 8690
[Apostol] p. 18	Theorem I.12	mul2neg 8345  mul2negd 8360  mul2negi 8353  mulneg1 8342  mulneg1d 8358  mulneg1i 8351
[Apostol] p. 18	Theorem I.15	divdivdivap 8659
[Apostol] p. 20	Axiom 7	rpaddcl 9664  rpaddcld 9699  rpmulcl 9665  rpmulcld 9700
[Apostol] p. 20	Axiom 9	0nrp 9676
[Apostol] p. 20	Theorem I.17	lttri 8052
[Apostol] p. 20	Theorem I.18	ltadd1d 8485  ltadd1dd 8503  ltadd1i 8449
[Apostol] p. 20	Theorem I.19	ltmul1 8539  ltmul1a 8538  ltmul1i 8866  ltmul1ii 8874  ltmul2 8802  ltmul2d 9726  ltmul2dd 9740  ltmul2i 8869
[Apostol] p. 20	Theorem I.21	0lt1 8074
[Apostol] p. 20	Theorem I.23	lt0neg1 8415  lt0neg1d 8462  ltneg 8409  ltnegd 8470  ltnegi 8440
[Apostol] p. 20	Theorem I.25	lt2add 8392  lt2addd 8514  lt2addi 8457
[Apostol] p. 20	Definition of positive numbers	df-rp 9641
[Apostol] p. 21	Exercise 4	recgt0 8796  recgt0d 8880  recgt0i 8852  recgt0ii 8853
[Apostol] p. 22	Definition of integers	df-z 9243
[Apostol] p. 22	Definition of rationals	df-q 9609
[Apostol] p. 24	Theorem I.26	supeuti 6987
[Apostol] p. 26	Theorem I.29	arch 9162
[Apostol] p. 28	Exercise 2	btwnz 9361
[Apostol] p. 28	Exercise 3	nnrecl 9163
[Apostol] p. 28	Exercise 6	qbtwnre 10243
[Apostol] p. 28	Exercise 10(a)	zeneo 11859  zneo 9343
[Apostol] p. 29	Theorem I.35	resqrtth 11024  sqrtthi 11112
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8911
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12020
[Apostol] p. 363	Remark	absgt0api 11139
[Apostol] p. 363	Example	abssubd 11186  abssubi 11143
[ApostolNT] p. 14	Definition	df-dvds 11779
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11795
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11819
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11815
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11809
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11811
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11796
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11797
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11802
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11834
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11836
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11838
[ApostolNT] p. 15	Definition	dfgcd2 11998
[ApostolNT] p. 16	Definition	isprm2 12100
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12075
[ApostolNT] p. 16	Theorem 1.7	prminf 12439
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11957
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11999
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12001
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11971
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11964
[ApostolNT] p. 17	Theorem 1.8	coprm 12127
[ApostolNT] p. 17	Theorem 1.9	euclemma 12129
[ApostolNT] p. 17	Theorem 1.10	1arith2 12349
[ApostolNT] p. 19	Theorem 1.14	divalg 11912
[ApostolNT] p. 20	Theorem 1.15	eucalg 12042
[ApostolNT] p. 25	Definition	df-phi 12194
[ApostolNT] p. 26	Theorem 2.2	phisum 12223
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12205
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12209
[ApostolNT] p. 104	Definition	congr 12083
[ApostolNT] p. 106	Remark	dvdsval3 11782
[ApostolNT] p. 106	Definition	moddvds 11790
[ApostolNT] p. 107	Example 2	mod2eq0even 11866
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11867
[ApostolNT] p. 107	Example 4	zmod1congr 10327
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10364
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10632
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11814
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12086
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12088
[ApostolNT] p. 113	Theorem 5.17	eulerth 12216
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12234
[ApostolNT] p. 114	Theorem 5.19	fermltl 12217
[ApostolNT] p. 179	Definition	df-lgs 14066  lgsprme0 14110
[ApostolNT] p. 180	Example 1	1lgs 14111
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 14087
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 14102
[ApostolNT] p. 188	Definition	df-lgs 14066  lgs1 14112
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 14103
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 14105
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 14113
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 14114
[Bauer] p. 482	Section 1.2	pm2.01 616  pm2.65 659
[Bauer] p. 483	Theorem 1.3	acexmid 5868  onsucelsucexmidlem 4525
[Bauer], p. 481	Section 1.1	pwtrufal 14403
[Bauer], p. 483	Definition	n0rf 3435
[Bauer], p. 483	Theorem 1.2	2irrexpq 14061  2irrexpqap 14063
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6870
[Bauer], p. 494	Theorem 5.5	ivthinc 13788
[BauerHanson], p. 27	Proposition 5.2	cnstab 8592
[BauerSwan], p. 14	Remark	0ct 7100  ctm 7102
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 14406
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7108
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7491
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7404
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7493
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7527  addlocpr 7526
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7553
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7556
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7561
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2029
[BellMachover] p. 460	Notation	df-mo 2030
[BellMachover] p. 460	Definition	mo3 2080  mo3h 2079
[BellMachover] p. 462	Theorem 1.1	bm1.1 2162
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4121
[BellMachover] p. 466	Axiom Pow	axpow3 4174
[BellMachover] p. 466	Axiom Union	axun2 4432
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4538
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4381
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4541
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4492
[BellMachover] p. 471	Definition of Lim	df-ilim 4366
[BellMachover] p. 472	Axiom Inf	zfinf2 4585
[BellMachover] p. 473	Theorem 2.8	limom 4610
[Bobzien] p. 116	Statement T3	stoic3 1431
[Bobzien] p. 117	Statement T2	stoic2a 1429
[Bobzien] p. 117	Statement T4	stoic4a 1432
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1427
[BourbakiAlg1] p. 1	Definition 1	df-mgm 12667
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 12700
[BourbakiAlg1] p. 12	Definition 2	df-mnd 12710
[BourbakiAlg1] p. 92	Definition 1	df-ring 13007
[BourbakiEns] p.	Proposition 8	fcof1 5778  fcofo 5779
[BourbakiTop1] p.	Remark	xnegmnf 9816  xnegpnf 9815
[BourbakiTop1] p.	Remark	rexneg 9817
[BourbakiTop1] p.	Proposition	ishmeo 13471
[BourbakiTop1] p.	Property V_i	ssnei2 13324
[BourbakiTop1] p.	Property V_ii	innei 13330
[BourbakiTop1] p.	Property V_iv	neissex 13332
[BourbakiTop1] p.	Proposition 1	neipsm 13321  neiss 13317
[BourbakiTop1] p.	Proposition 2	cnptopco 13389
[BourbakiTop1] p.	Proposition 4	imasnopn 13466
[BourbakiTop1] p.	Property V_iii	elnei 13319
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 13163
[Bruck] p. 1	Section I.1	df-mgm 12667
[Bruck] p. 23	Section II.1	df-sgrp 12700
[Bruck] p. 28	Theorem 3.2	dfgrp3m 12858
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4063
[Cohen] p. 301	Remark	relogoprlem 13956
[Cohen] p. 301	Property 2	relogmul 13957  relogmuld 13972
[Cohen] p. 301	Property 3	relogdiv 13958  relogdivd 13973
[Cohen] p. 301	Property 4	relogexp 13960
[Cohen] p. 301	Property 1a	log1 13954
[Cohen] p. 301	Property 1b	loge 13955
[Cohen4] p. 348	Observation	relogbcxpbap 14050
[Cohen4] p. 352	Definition	rpelogb 14034
[Cohen4] p. 361	Property 2	rprelogbmul 14040
[Cohen4] p. 361	Property 3	logbrec 14045  rprelogbdiv 14042
[Cohen4] p. 361	Property 4	rplogbreexp 14038
[Cohen4] p. 361	Property 6	relogbexpap 14043
[Cohen4] p. 361	Property 1(a)	rplogbid1 14032
[Cohen4] p. 361	Property 1(b)	rplogb1 14033
[Cohen4] p. 367	Property	rplogbchbase 14035
[Cohen4] p. 377	Property 2	logblt 14047
[Crosilla] p.	Axiom 1	ax-ext 2159
[Crosilla] p.	Axiom 2	ax-pr 4206
[Crosilla] p.	Axiom 3	ax-un 4430
[Crosilla] p.	Axiom 4	ax-nul 4126
[Crosilla] p.	Axiom 5	ax-iinf 4584
[Crosilla] p.	Axiom 6	ru 2961
[Crosilla] p.	Axiom 8	ax-pow 4171
[Crosilla] p.	Axiom 9	ax-setind 4533
[Crosilla], p.	Axiom 6	ax-sep 4118
[Crosilla], p.	Axiom 7	ax-coll 4115
[Crosilla], p.	Axiom 7'	repizf 4116
[Crosilla], p.	Theorem is stated	ordtriexmid 4517
[Crosilla], p.	Axiom of choice implies instances	acexmid 5868
[Crosilla], p.	Definition of ordinal	df-iord 4363
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4531
[Eisenberg] p. 67	Definition 5.3	df-dif 3131
[Eisenberg] p. 82	Definition 6.3	df-iom 4587
[Eisenberg] p. 125	Definition 8.21	df-map 6644
[Enderton] p. 18	Axiom of Empty Set	axnul 4125
[Enderton] p. 19	Definition	df-tp 3599
[Enderton] p. 26	Exercise 5	unissb 3837
[Enderton] p. 26	Exercise 10	pwel 4215
[Enderton] p. 28	Exercise 7(b)	pwunim 4283
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3953  iinin2m 3952  iunin1 3948  iunin2 3947
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3951  iundif2ss 3949
[Enderton] p. 33	Exercise 23	iinuniss 3966
[Enderton] p. 33	Exercise 25	iununir 3967
[Enderton] p. 33	Exercise 24(a)	iinpw 3974
[Enderton] p. 33	Exercise 24(b)	iunpw 4477  iunpwss 3975
[Enderton] p. 38	Exercise 6(a)	unipw 4214
[Enderton] p. 38	Exercise 6(b)	pwuni 4189
[Enderton] p. 41	Lemma 3D	opeluu 4447  rnex 4890  rnexg 4888
[Enderton] p. 41	Exercise 8	dmuni 4833  rnuni 5036
[Enderton] p. 42	Definition of a function	dffun7 5239  dffun8 5240
[Enderton] p. 43	Definition of function value	funfvdm2 5576
[Enderton] p. 43	Definition of single-rooted	funcnv 5273
[Enderton] p. 44	Definition (d)	dfima2 4968  dfima3 4969
[Enderton] p. 47	Theorem 3H	fvco2 5581
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7199
[Enderton] p. 50	Theorem 3K(a)	imauni 5756
[Enderton] p. 52	Definition	df-map 6644
[Enderton] p. 53	Exercise 21	coass 5143
[Enderton] p. 53	Exercise 27	dmco 5133
[Enderton] p. 53	Exercise 14(a)	funin 5283
[Enderton] p. 53	Exercise 22(a)	imass2 5000
[Enderton] p. 54	Remark	ixpf 6714  ixpssmap 6726
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6693
[Enderton] p. 56	Theorem 3M	erref 6549
[Enderton] p. 57	Lemma 3N	erthi 6575
[Enderton] p. 57	Definition	df-ec 6531
[Enderton] p. 58	Definition	df-qs 6535
[Enderton] p. 60	Theorem 3Q	th3q 6634  th3qcor 6633  th3qlem1 6631  th3qlem2 6632
[Enderton] p. 61	Exercise 35	df-ec 6531
[Enderton] p. 65	Exercise 56(a)	dmun 4830
[Enderton] p. 68	Definition of successor	df-suc 4368
[Enderton] p. 71	Definition	df-tr 4099  dftr4 4103
[Enderton] p. 72	Theorem 4E	unisuc 4410  unisucg 4411
[Enderton] p. 73	Exercise 6	unisuc 4410  unisucg 4411
[Enderton] p. 73	Exercise 5(a)	truni 4112
[Enderton] p. 73	Exercise 5(b)	trint 4113
[Enderton] p. 79	Theorem 4I(A1)	nna0 6469
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6471  onasuc 6461
[Enderton] p. 79	Definition of operation value	df-ov 5872
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6470
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6472  onmsuc 6468
[Enderton] p. 81	Theorem 4K(1)	nnaass 6480
[Enderton] p. 81	Theorem 4K(2)	nna0r 6473  nnacom 6479
[Enderton] p. 81	Theorem 4K(3)	nndi 6481
[Enderton] p. 81	Theorem 4K(4)	nnmass 6482
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6484
[Enderton] p. 82	Exercise 16	nnm0r 6474  nnmsucr 6483
[Enderton] p. 88	Exercise 23	nnaordex 6523
[Enderton] p. 129	Definition	df-en 6735
[Enderton] p. 132	Theorem 6B(b)	canth 5823
[Enderton] p. 133	Exercise 1	xpomen 12379
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6859
[Enderton] p. 136	Corollary 6E	nneneq 6851
[Enderton] p. 139	Theorem 6H(c)	mapen 6840
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7211
[Enderton] p. 143	Theorem 6J	dju0en 7207  dju1en 7206
[Enderton] p. 144	Corollary 6K	undif2ss 3498
[Enderton] p. 145	Figure 38	ffoss 5489
[Enderton] p. 145	Definition	df-dom 6736
[Enderton] p. 146	Example 1	domen 6745  domeng 6746
[Enderton] p. 146	Example 3	nndomo 6858
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6829  xpdom1g 6827  xpdom2g 6826
[Enderton] p. 168	Definition	df-po 4293
[Enderton] p. 192	Theorem 7M(a)	oneli 4425
[Enderton] p. 192	Theorem 7M(b)	ontr1 4386
[Enderton] p. 192	Theorem 7M(c)	onirri 4539
[Enderton] p. 193	Corollary 7N(b)	0elon 4389
[Enderton] p. 193	Corollary 7N(c)	onsuci 4512
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4485
[Enderton] p. 194	Remark	onprc 4548
[Enderton] p. 194	Exercise 16	suc11 4554
[Enderton] p. 197	Definition	df-card 7173
[Enderton] p. 200	Exercise 25	tfis 4579
[Enderton] p. 206	Theorem 7X(b)	en2lp 4550
[Enderton] p. 207	Exercise 34	opthreg 4552
[Enderton] p. 208	Exercise 35	suc11g 4553
[Geuvers], p. 1	Remark	expap0 10536
[Geuvers], p. 6	Lemma 2.13	mulap0r 8562
[Geuvers], p. 6	Lemma 2.15	mulap0 8600
[Geuvers], p. 9	Lemma 2.35	msqge0 8563
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7921
[Geuvers], p. 10	Lemma 3.9	maxcom 11196
[Geuvers], p. 10	Lemma 3.10	maxle1 11204  maxle2 11205
[Geuvers], p. 10	Lemma 3.11	maxleast 11206
[Geuvers], p. 10	Lemma 3.12	maxleb 11209
[Geuvers], p. 11	Definition 3.13	dfabsmax 11210
[Geuvers], p. 17	Definition 6.1	df-ap 8529
[Gleason] p. 117	Proposition 9-2.1	df-enq 7337  enqer 7348
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7341  df-nqqs 7338
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7334  df-plqqs 7339
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7335  df-mqqs 7340
[Gleason] p. 119	Proposition 9-2.5	df-rq 7342
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7398
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7401  ltbtwnnq 7406  ltbtwnnqq 7405
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7390
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7391
[Gleason] p. 123	Proposition 9-3.5	addclpr 7527
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7569
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7568
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7587
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7603
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7609  ltaprlem 7608
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7606
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7562
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7582
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7571
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7570
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7578
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7628
[Gleason] p. 126	Proposition 9-4.1	df-enr 7716  enrer 7725
[Gleason] p. 126	Proposition 9-4.2	df-0r 7721  df-1r 7722  df-nr 7717
[Gleason] p. 126	Proposition 9-4.3	df-mr 7719  df-plr 7718  negexsr 7762  recexsrlem 7764
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7720
[Gleason] p. 130	Proposition 10-1.3	creui 8906  creur 8905  cru 8549
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7913  axcnre 7871
[Gleason] p. 132	Definition 10-3.1	crim 10851  crimd 10970  crimi 10930  crre 10850  crred 10969  crrei 10929
[Gleason] p. 132	Definition 10-3.2	remim 10853  remimd 10935
[Gleason] p. 133	Definition 10.36	absval2 11050  absval2d 11178  absval2i 11137
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10877  cjaddd 10958  cjaddi 10925
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10878  cjmuld 10959  cjmuli 10926
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10876  cjcjd 10936  cjcji 10908
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10875  cjreb 10859  cjrebd 10939  cjrebi 10911  cjred 10964  rere 10858  rereb 10856  rerebd 10938  rerebi 10910  rered 10962
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10884  addcjd 10950  addcji 10920
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10994
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11045  abscjd 11183  abscji 11141
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11057  abs00d 11179  abs00i 11138  absne0d 11180
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11089  releabsd 11184  releabsi 11142
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11062  absmuld 11187  absmuli 11144
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11048  sqabsaddi 11145
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11097  abstrid 11189  abstrii 11148
[Gleason] p. 134	Definition 10-4.1	df-exp 10506  exp0 10510  expp1 10513  expp1d 10640
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10548  expaddd 10641
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 14000  cxpmuld 14023  expmul 10551  expmuld 10642
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10545  mulexpd 10654  rpmulcxp 13997
[Gleason] p. 141	Definition 11-2.1	fzval 9997
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11318
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11320
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11319
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11323
[Gleason] p. 172	Corollary 12-2.5	climrecl 11316
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11312  climcj 11313  climim 11315  climre 11314
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7987  df-xr 7986  ltxr 9762
[Gleason] p. 180	Theorem 12-5.3	climcau 11339
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10286
[Gleason] p. 223	Definition 14-1.1	df-met 13156
[Gleason] p. 223	Definition 14-1.1(a)	met0 13531  xmet0 13530
[Gleason] p. 223	Definition 14-1.1(c)	metsym 13538
[Gleason] p. 223	Definition 14-1.1(d)	mettri 13540  mstri 13640  xmettri 13539  xmstri 13639
[Gleason] p. 230	Proposition 14-2.6	txlm 13446
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13678
[Gleason] p. 243	Proposition 14-4.16	addcn2 11302  addcncntop 13719  mulcn2 11304  mulcncntop 13721  subcn2 11303  subcncntop 13720
[Gleason] p. 295	Remark	bcval3 10715  bcval4 10716
[Gleason] p. 295	Equation 2	bcpasc 10730
[Gleason] p. 295	Definition of binomial coefficient	bcval 10713  df-bc 10712
[Gleason] p. 296	Remark	bcn0 10719  bcnn 10721
[Gleason] p. 296	Theorem 15-2.8	binom 11476
[Gleason] p. 308	Equation 2	ef0 11664
[Gleason] p. 308	Equation 3	efcj 11665
[Gleason] p. 309	Corollary 15-4.3	efne0 11670
[Gleason] p. 309	Corollary 15-4.4	efexp 11674
[Gleason] p. 310	Equation 14	sinadd 11728
[Gleason] p. 310	Equation 15	cosadd 11729
[Gleason] p. 311	Equation 17	sincossq 11740
[Gleason] p. 311	Equation 18	cosbnd 11745  sinbnd 11744
[Gleason] p. 311	Definition of ` `	df-pi 11645
[Golan] p. 1	Remark	srgisid 12995
[Golan] p. 1	Definition	df-srg 12973
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1449
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 12778  mndideu 12719
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 12801
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 12826
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 12837
[Herstein] p. 57	Exercise 1	dfgrp3me 12859
[Heyting] p. 127	Axiom #1	ax1hfs 14475
[Hitchcock] p. 5	Rule A3	mptnan 1423
[Hitchcock] p. 5	Rule A4	mptxor 1424
[Hitchcock] p. 5	Rule A5	mtpxor 1426
[HoTT], p.	Lemma 10.4.1	exmidontriim 7218
[HoTT], p.	Theorem 7.2.6	nndceq 6494
[HoTT], p.	Exercise 11.10	neapmkv 14471
[HoTT], p.	Exercise 11.11	mulap0bd 8603
[HoTT], p.	Section 11.2.1	df-iltp 7460  df-imp 7459  df-iplp 7458  df-reap 8522
[HoTT], p.	Theorem 11.2.4	recapb 8617  rerecapb 8789
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7652
[HoTT], p.	Corollary 11.4.3	conventions 14129
[HoTT], p.	Exercise 11.6(i)	dcapnconst 14464  dceqnconst 14463
[HoTT], p.	Corollary 11.2.13	axcaucvg 7890  caucvgpr 7672  caucvgprpr 7702  caucvgsr 7792
[HoTT], p.	Definition 11.2.1	df-inp 7456
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 14469
[HoTT], p.	Proposition 11.2.3	df-iso 4294  ltpopr 7585  ltsopr 7586
[HoTT], p.	Definition 11.2.7(v)	apsym 8553  reapcotr 8545  reapirr 8524
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8074  gt0add 8520  leadd1 8377  lelttr 8036  lemul1a 8804  lenlt 8023  ltadd1 8376  ltletr 8037  ltmul1 8539  reaplt 8535
[Jech] p. 4	Definition of class	cv 1352  cvjust 2172
[Jech] p. 78	Note	opthprc 4674
[KalishMontague] p. 81	Note 1	ax-i9 1530
[Kreyszig] p. 3	Property M1	metcl 13520  xmetcl 13519
[Kreyszig] p. 4	Property M2	meteq0 13527
[Kreyszig] p. 12	Equation 5	muleqadd 8614
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13609
[Kreyszig] p. 19	Remark	mopntopon 13610
[Kreyszig] p. 19	Theorem T1	mopn0 13655  mopnm 13615
[Kreyszig] p. 19	Theorem T2	unimopn 13653
[Kreyszig] p. 19	Definition of neighborhood	neibl 13658
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13680
[Kreyszig] p. 25	Definition 1.4-1	lmbr 13380
[Kunen] p. 10	Axiom 0	a9e 1696
[Kunen] p. 12	Axiom 6	zfrep6 4117
[Kunen] p. 24	Definition 10.24	mapval 6654  mapvalg 6652
[Kunen] p. 31	Definition 10.24	mapex 6648
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3894
[Lang] p. 3	Statement	lidrideqd 12692  mndbn0 12724
[Lang] p. 3	Definition	df-mnd 12710
[Lang] p. 7	Definition	dfgrp2e 12793
[Levy] p. 338	Axiom	df-clab 2164  df-clel 2173  df-cleq 2170
[Lopez-Astorga] p. 12	Rule 1	mptnan 1423
[Lopez-Astorga] p. 12	Rule 2	mptxor 1424
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1426
[Margaris] p. 40	Rule C	exlimiv 1598
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 853
[Margaris] p. 49	Definition	dfbi2 388  dfordc 892  exalim 1502
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 651
[Margaris] p. 89	Theorem 19.2	19.2 1638  r19.2m 3509
[Margaris] p. 89	Theorem 19.3	19.3 1554  19.3h 1553  rr19.3v 2876
[Margaris] p. 89	Theorem 19.5	alcom 1478
[Margaris] p. 89	Theorem 19.6	alexdc 1619  alexim 1645
[Margaris] p. 89	Theorem 19.7	alnex 1499
[Margaris] p. 89	Theorem 19.8	19.8a 1590  spsbe 1842
[Margaris] p. 89	Theorem 19.9	19.9 1644  19.9h 1643  19.9v 1871  exlimd 1597
[Margaris] p. 89	Theorem 19.11	excom 1664  excomim 1663
[Margaris] p. 89	Theorem 19.12	19.12 1665  r19.12 2583
[Margaris] p. 90	Theorem 19.14	exnalim 1646
[Margaris] p. 90	Theorem 19.15	albi 1468  ralbi 2609
[Margaris] p. 90	Theorem 19.16	19.16 1555
[Margaris] p. 90	Theorem 19.17	19.17 1556
[Margaris] p. 90	Theorem 19.18	exbi 1604  rexbi 2610
[Margaris] p. 90	Theorem 19.19	19.19 1666
[Margaris] p. 90	Theorem 19.20	alim 1457  alimd 1521  alimdh 1467  alimdv 1879  ralimdaa 2543  ralimdv 2545  ralimdva 2544  ralimdvva 2546  sbcimdv 3028
[Margaris] p. 90	Theorem 19.21	19.21-2 1667  19.21 1583  19.21bi 1558  19.21h 1557  19.21ht 1581  19.21t 1582  19.21v 1873  alrimd 1610  alrimdd 1609  alrimdh 1479  alrimdv 1876  alrimi 1522  alrimih 1469  alrimiv 1874  alrimivv 1875  r19.21 2553  r19.21be 2568  r19.21bi 2565  r19.21t 2552  r19.21v 2554  ralrimd 2555  ralrimdv 2556  ralrimdva 2557  ralrimdvv 2561  ralrimdvva 2562  ralrimi 2548  ralrimiv 2549  ralrimiva 2550  ralrimivv 2558  ralrimivva 2559  ralrimivvva 2560  ralrimivw 2551  rexlimi 2587
[Margaris] p. 90	Theorem 19.22	2alimdv 1881  2eximdv 1882  exim 1599  eximd 1612  eximdh 1611  eximdv 1880  rexim 2571  reximdai 2575  reximddv 2580  reximddv2 2582  reximdv 2578  reximdv2 2576  reximdva 2579  reximdvai 2577  reximi2 2573
[Margaris] p. 90	Theorem 19.23	19.23 1678  19.23bi 1592  19.23h 1498  19.23ht 1497  19.23t 1677  19.23v 1883  19.23vv 1884  exlimd2 1595  exlimdh 1596  exlimdv 1819  exlimdvv 1897  exlimi 1594  exlimih 1593  exlimiv 1598  exlimivv 1896  r19.23 2585  r19.23v 2586  rexlimd 2591  rexlimdv 2593  rexlimdv3a 2596  rexlimdva 2594  rexlimdva2 2597  rexlimdvaa 2595  rexlimdvv 2601  rexlimdvva 2602  rexlimdvw 2598  rexlimiv 2588  rexlimiva 2589  rexlimivv 2600
[Margaris] p. 90	Theorem 19.24	i19.24 1639
[Margaris] p. 90	Theorem 19.25	19.25 1626
[Margaris] p. 90	Theorem 19.26	19.26-2 1482  19.26-3an 1483  19.26 1481  r19.26-2 2606  r19.26-3 2607  r19.26 2603  r19.26m 2608
[Margaris] p. 90	Theorem 19.27	19.27 1561  19.27h 1560  19.27v 1899  r19.27av 2612  r19.27m 3518  r19.27mv 3519
[Margaris] p. 90	Theorem 19.28	19.28 1563  19.28h 1562  19.28v 1900  r19.28av 2613  r19.28m 3512  r19.28mv 3515  rr19.28v 2877
[Margaris] p. 90	Theorem 19.29	19.29 1620  19.29r 1621  19.29r2 1622  19.29x 1623  r19.29 2614  r19.29d2r 2621  r19.29r 2615
[Margaris] p. 90	Theorem 19.30	19.30dc 1627
[Margaris] p. 90	Theorem 19.31	19.31r 1681
[Margaris] p. 90	Theorem 19.32	19.32dc 1679  19.32r 1680  r19.32r 2623  r19.32vdc 2626  r19.32vr 2625
[Margaris] p. 90	Theorem 19.33	19.33 1484  19.33b2 1629  19.33bdc 1630
[Margaris] p. 90	Theorem 19.34	19.34 1684
[Margaris] p. 90	Theorem 19.35	19.35-1 1624  19.35i 1625
[Margaris] p. 90	Theorem 19.36	19.36-1 1673  19.36aiv 1901  19.36i 1672  r19.36av 2628
[Margaris] p. 90	Theorem 19.37	19.37-1 1674  19.37aiv 1675  r19.37 2629  r19.37av 2630
[Margaris] p. 90	Theorem 19.38	19.38 1676
[Margaris] p. 90	Theorem 19.39	i19.39 1640
[Margaris] p. 90	Theorem 19.40	19.40-2 1632  19.40 1631  r19.40 2631
[Margaris] p. 90	Theorem 19.41	19.41 1686  19.41h 1685  19.41v 1902  19.41vv 1903  19.41vvv 1904  19.41vvvv 1905  r19.41 2632  r19.41v 2633
[Margaris] p. 90	Theorem 19.42	19.42 1688  19.42h 1687  19.42v 1906  19.42vv 1911  19.42vvv 1912  19.42vvvv 1913  r19.42v 2634
[Margaris] p. 90	Theorem 19.43	19.43 1628  r19.43 2635
[Margaris] p. 90	Theorem 19.44	19.44 1682  r19.44av 2636  r19.44mv 3517
[Margaris] p. 90	Theorem 19.45	19.45 1683  r19.45av 2637  r19.45mv 3516
[Margaris] p. 110	Exercise 2(b)	eu1 2051
[Megill] p. 444	Axiom C5	ax-17 1526
[Megill] p. 445	Lemma L12	alequcom 1515  ax-10 1505
[Megill] p. 446	Lemma L17	equtrr 1710
[Megill] p. 446	Lemma L19	hbnae 1721
[Megill] p. 447	Remark 9.1	df-sb 1763  sbid 1774
[Megill] p. 448	Scheme C5'	ax-4 1510
[Megill] p. 448	Scheme C6'	ax-7 1448
[Megill] p. 448	Scheme C8'	ax-8 1504
[Megill] p. 448	Scheme C9'	ax-i12 1507
[Megill] p. 448	Scheme C11'	ax-10o 1716
[Megill] p. 448	Scheme C12'	ax-13 2150
[Megill] p. 448	Scheme C13'	ax-14 2151
[Megill] p. 448	Scheme C15'	ax-11o 1823
[Megill] p. 448	Scheme C16'	ax-16 1814
[Megill] p. 448	Theorem 9.4	dral1 1730  dral2 1731  drex1 1798  drex2 1732  drsb1 1799  drsb2 1841
[Megill] p. 449	Theorem 9.7	sbcom2 1987  sbequ 1840  sbid2v 1996
[Megill] p. 450	Example in Appendix	hba1 1540
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3045  rspsbca 3046  stdpc4 1775
[Mendelson] p. 69	Axiom 5	ra5 3051  stdpc5 1584
[Mendelson] p. 81	Rule C	exlimiv 1598
[Mendelson] p. 95	Axiom 6	stdpc6 1703
[Mendelson] p. 95	Axiom 7	stdpc7 1770
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3459
[Mendelson] p. 231	Exercise 4.10(l)	unv 3460
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3375
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3423
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3376
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3266
[Mendelson] p. 231	Definition of union	unssin 3374
[Mendelson] p. 235	Exercise 4.12(c)	univ 4473
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3806
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4279
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4280
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4281
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3827
[Mendelson] p. 235	Exercise 4.12(p)	reli 4752
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5145
[Mendelson] p. 246	Definition of successor	df-suc 4368
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6839
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6815  xpsneng 6816
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6821  xpcomeng 6822
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6824
[Mendelson] p. 255	Exercise 4.39	endisj 6818
[Mendelson] p. 255	Exercise 4.41	mapprc 6646
[Mendelson] p. 255	Exercise 4.43	mapsnen 6805
[Mendelson] p. 255	Exercise 4.47	xpmapen 6844
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6680
[Mendelson] p. 255	Exercise 4.42(b)	map1 6806
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7210  djucomen 7209
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7208
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6462
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3357
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4711
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4712
[Monk1] p. 34	Definition 3.3	df-opab 4062
[Monk1] p. 36	Theorem 3.7(i)	coi1 5140  coi2 5141
[Monk1] p. 36	Theorem 3.8(v)	dm0 4837  rn0 4879
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5029
[Monk1] p. 37	Theorem 3.13(i)	relxp 4732
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4843  rnxpm 5054
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4703  xp0 5044
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4983
[Monk1] p. 38	Theorem 3.16(viii)	imai 4980
[Monk1] p. 39	Theorem 3.17	imaex 4979  imaexg 4978
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4977
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5642  funfvop 5624
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5555
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5563
[Monk1] p. 43	Theorem 4.6	funun 5256
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5763  dff13f 5765
[Monk1] p. 46	Theorem 4.15(v)	funex 5735  funrnex 6109
[Monk1] p. 50	Definition 5.4	fniunfv 5757
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5108
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3858
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6150  df-1st 6135
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6151  df-2nd 6136
[Monk2] p. 105	Axiom C4	ax-5 1447
[Monk2] p. 105	Axiom C7	ax-8 1504
[Monk2] p. 105	Axiom C8	ax-11 1506  ax-11o 1823
[Monk2] p. 105	Axiom (C8)	ax11v 1827
[Monk2] p. 109	Lemma 12	ax-7 1448
[Monk2] p. 109	Lemma 15	equvin 1863  equvini 1758  eqvinop 4240
[Monk2] p. 113	Axiom C5-1	ax-17 1526
[Monk2] p. 113	Axiom C5-2	ax6b 1651
[Monk2] p. 113	Axiom C5-3	ax-7 1448
[Monk2] p. 114	Lemma 22	hba1 1540
[Monk2] p. 114	Lemma 23	hbia1 1552  nfia1 1580
[Monk2] p. 114	Lemma 24	hba2 1551  nfa2 1579
[Moschovakis] p. 2	Chapter 2	df-stab 831  dftest 14476
[Munkres] p. 77	Example 2	distop 13252
[Munkres] p. 78	Definition of basis	df-bases 13208  isbasis3g 13211
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12657  tgval2 13218
[Munkres] p. 79	Remark	tgcl 13231
[Munkres] p. 80	Lemma 2.1	tgval3 13225
[Munkres] p. 80	Lemma 2.2	tgss2 13246  tgss3 13245
[Munkres] p. 81	Lemma 2.3	basgen 13247  basgen2 13248
[Munkres] p. 89	Definition of subspace topology	resttop 13337
[Munkres] p. 93	Theorem 6.1(1)	0cld 13279  topcld 13276
[Munkres] p. 93	Theorem 6.1(3)	uncld 13280
[Munkres] p. 94	Definition of closure	clsval 13278
[Munkres] p. 94	Definition of interior	ntrval 13277
[Munkres] p. 102	Definition of continuous function	df-cn 13355  iscn 13364  iscn2 13367
[Munkres] p. 107	Theorem 7.2(g)	cncnp 13397  cncnp2m 13398  cncnpi 13395  df-cnp 13356  iscnp 13366
[Munkres] p. 127	Theorem 10.1	metcn 13681
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6897
[Pierik], p. 9	Definition 2.4	df-womni 7156
[Pierik], p. 9	Definition 2.5	df-markov 7144  omniwomnimkv 7159
[Pierik], p. 10	Section 2.3	dfdif3 3245
[Pierik], p. 14	Definition 3.1	df-omni 7127  exmidomniim 7133  finomni 7132
[Pierik], p. 15	Section 3.1	df-nninf 7113
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 14427
[PradicBrown2022], p. 2	Remark	exmidpw 6902
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7194
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7195  exmidfodomrlemrALT 7196
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7141
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 14412  peano4nninf 14411
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 14414
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 14422
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 14424
[PradicBrown2022], p. 5	Definition 3.3	nnsf 14410
[Quine] p. 16	Definition 2.1	df-clab 2164  rabid 2652
[Quine] p. 17	Definition 2.1''	dfsb7 1991
[Quine] p. 18	Definition 2.7	df-cleq 2170
[Quine] p. 19	Definition 2.9	df-v 2739
[Quine] p. 34	Theorem 5.1	abeq2 2286
[Quine] p. 35	Theorem 5.2	abid2 2298  abid2f 2345
[Quine] p. 40	Theorem 6.1	sb5 1887
[Quine] p. 40	Theorem 6.2	sb56 1885  sb6 1886
[Quine] p. 41	Theorem 6.3	df-clel 2173
[Quine] p. 41	Theorem 6.4	eqid 2177
[Quine] p. 41	Theorem 6.5	eqcom 2179
[Quine] p. 42	Theorem 6.6	df-sbc 2963
[Quine] p. 42	Theorem 6.7	dfsbcq 2964  dfsbcq2 2965
[Quine] p. 43	Theorem 6.8	vex 2740
[Quine] p. 43	Theorem 6.9	isset 2743
[Quine] p. 44	Theorem 7.3	spcgf 2819  spcgv 2824  spcimgf 2817
[Quine] p. 44	Theorem 6.11	spsbc 2974  spsbcd 2975
[Quine] p. 44	Theorem 6.12	elex 2748
[Quine] p. 44	Theorem 6.13	elab 2881  elabg 2883  elabgf 2879
[Quine] p. 44	Theorem 6.14	noel 3426
[Quine] p. 48	Theorem 7.2	snprc 3656
[Quine] p. 48	Definition 7.1	df-pr 3598  df-sn 3597
[Quine] p. 49	Theorem 7.4	snss 3726  snssg 3725
[Quine] p. 49	Theorem 7.5	prss 3747  prssg 3748
[Quine] p. 49	Theorem 7.6	prid1 3697  prid1g 3695  prid2 3698  prid2g 3696  snid 3622  snidg 3620
[Quine] p. 51	Theorem 7.12	snexg 4181  snexprc 4183
[Quine] p. 51	Theorem 7.13	prexg 4208
[Quine] p. 53	Theorem 8.2	unisn 3823  unisng 3824
[Quine] p. 53	Theorem 8.3	uniun 3826
[Quine] p. 54	Theorem 8.6	elssuni 3835
[Quine] p. 54	Theorem 8.7	uni0 3834
[Quine] p. 56	Theorem 8.17	uniabio 5184
[Quine] p. 56	Definition 8.18	dfiota2 5175
[Quine] p. 57	Theorem 8.19	iotaval 5185
[Quine] p. 57	Theorem 8.22	iotanul 5189
[Quine] p. 58	Theorem 8.23	euiotaex 5190
[Quine] p. 58	Definition 9.1	df-op 3600
[Quine] p. 61	Theorem 9.5	opabid 4254  opelopab 4268  opelopaba 4263  opelopabaf 4270  opelopabf 4271  opelopabg 4265  opelopabga 4260  oprabid 5901
[Quine] p. 64	Definition 9.11	df-xp 4629
[Quine] p. 64	Definition 9.12	df-cnv 4631
[Quine] p. 64	Definition 9.15	df-id 4290
[Quine] p. 65	Theorem 10.3	fun0 5270
[Quine] p. 65	Theorem 10.4	funi 5244
[Quine] p. 65	Theorem 10.5	funsn 5260  funsng 5258
[Quine] p. 65	Definition 10.1	df-fun 5214
[Quine] p. 65	Definition 10.2	args 4993  dffv4g 5508
[Quine] p. 68	Definition 10.11	df-fv 5220  fv2 5506
[Quine] p. 124	Theorem 17.3	nn0opth2 10688  nn0opth2d 10687  nn0opthd 10686
[Quine] p. 284	Axiom 39(vi)	funimaex 5297  funimaexg 5296
[Roman] p. 19	Part Preliminaries	df-ring 13007
[Rudin] p. 164	Equation 27	efcan 11668
[Rudin] p. 164	Equation 30	efzval 11675
[Rudin] p. 167	Equation 48	absefi 11760
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1426
[Sanford] p. 39	Rule 4	mptxor 1424
[Sanford] p. 40	Rule 1	mptnan 1423
[Schechter] p. 51	Definition of antisymmetry	intasym 5009
[Schechter] p. 51	Definition of irreflexivity	intirr 5011
[Schechter] p. 51	Definition of symmetry	cnvsym 5008
[Schechter] p. 51	Definition of transitivity	cotr 5006
[Schechter] p. 187	Definition of "ring with unit"	isring 13009
[Schechter] p. 428	Definition 15.35	bastop1 13250
[Stoll] p. 13	Definition of symmetric difference	symdif1 3400
[Stoll] p. 16	Exercise 4.4	0dif 3494  dif0 3493
[Stoll] p. 16	Exercise 4.8	difdifdirss 3507
[Stoll] p. 19	Theorem 5.2(13)	undm 3393
[Stoll] p. 19	Theorem 5.2(13')	indmss 3394
[Stoll] p. 20	Remark	invdif 3377
[Stoll] p. 25	Definition of ordered triple	df-ot 3601
[Stoll] p. 43	Definition	uniiun 3937
[Stoll] p. 44	Definition	intiin 3938
[Stoll] p. 45	Definition	df-iin 3887
[Stoll] p. 45	Definition indexed union	df-iun 3886
[Stoll] p. 176	Theorem 3.4(27)	imandc 889  imanst 888
[Stoll] p. 262	Example 4.1	symdif1 3400
[Suppes] p. 22	Theorem 2	eq0 3441
[Suppes] p. 22	Theorem 4	eqss 3170  eqssd 3172  eqssi 3171
[Suppes] p. 23	Theorem 5	ss0 3463  ss0b 3462
[Suppes] p. 23	Theorem 6	sstr 3163
[Suppes] p. 25	Theorem 12	elin 3318  elun 3276
[Suppes] p. 26	Theorem 15	inidm 3344
[Suppes] p. 26	Theorem 16	in0 3457
[Suppes] p. 27	Theorem 23	unidm 3278
[Suppes] p. 27	Theorem 24	un0 3456
[Suppes] p. 27	Theorem 25	ssun1 3298
[Suppes] p. 27	Theorem 26	ssequn1 3305
[Suppes] p. 27	Theorem 27	unss 3309
[Suppes] p. 27	Theorem 28	indir 3384
[Suppes] p. 27	Theorem 29	undir 3385
[Suppes] p. 28	Theorem 32	difid 3491  difidALT 3492
[Suppes] p. 29	Theorem 33	difin 3372
[Suppes] p. 29	Theorem 34	indif 3378
[Suppes] p. 29	Theorem 35	undif1ss 3497
[Suppes] p. 29	Theorem 36	difun2 3502
[Suppes] p. 29	Theorem 37	difin0 3496
[Suppes] p. 29	Theorem 38	disjdif 3495
[Suppes] p. 29	Theorem 39	difundi 3387
[Suppes] p. 29	Theorem 40	difindiss 3389
[Suppes] p. 30	Theorem 41	nalset 4130
[Suppes] p. 39	Theorem 61	uniss 3828
[Suppes] p. 39	Theorem 65	uniop 4252
[Suppes] p. 41	Theorem 70	intsn 3877
[Suppes] p. 42	Theorem 71	intpr 3874  intprg 3875
[Suppes] p. 42	Theorem 73	op1stb 4475  op1stbg 4476
[Suppes] p. 42	Theorem 78	intun 3873
[Suppes] p. 44	Definition 15(a)	dfiun2 3918  dfiun2g 3916
[Suppes] p. 44	Definition 15(b)	dfiin2 3919
[Suppes] p. 47	Theorem 86	elpw 3580  elpw2 4154  elpw2g 4153  elpwg 3582
[Suppes] p. 47	Theorem 87	pwid 3589
[Suppes] p. 47	Theorem 89	pw0 3738
[Suppes] p. 48	Theorem 90	pwpw0ss 3802
[Suppes] p. 52	Theorem 101	xpss12 4730
[Suppes] p. 52	Theorem 102	xpindi 4758  xpindir 4759
[Suppes] p. 52	Theorem 103	xpundi 4679  xpundir 4680
[Suppes] p. 54	Theorem 105	elirrv 4544
[Suppes] p. 58	Theorem 2	relss 4710
[Suppes] p. 59	Theorem 4	eldm 4820  eldm2 4821  eldm2g 4819  eldmg 4818
[Suppes] p. 59	Definition 3	df-dm 4633
[Suppes] p. 60	Theorem 6	dmin 4831
[Suppes] p. 60	Theorem 8	rnun 5033
[Suppes] p. 60	Theorem 9	rnin 5034
[Suppes] p. 60	Definition 4	dfrn2 4811
[Suppes] p. 61	Theorem 11	brcnv 4806  brcnvg 4804
[Suppes] p. 62	Equation 5	elcnv 4800  elcnv2 4801
[Suppes] p. 62	Theorem 12	relcnv 5002
[Suppes] p. 62	Theorem 15	cnvin 5032
[Suppes] p. 62	Theorem 16	cnvun 5030
[Suppes] p. 63	Theorem 20	co02 5138
[Suppes] p. 63	Theorem 21	dmcoss 4892
[Suppes] p. 63	Definition 7	df-co 4632
[Suppes] p. 64	Theorem 26	cnvco 4808
[Suppes] p. 64	Theorem 27	coass 5143
[Suppes] p. 65	Theorem 31	resundi 4916
[Suppes] p. 65	Theorem 34	elima 4971  elima2 4972  elima3 4973  elimag 4970
[Suppes] p. 65	Theorem 35	imaundi 5037
[Suppes] p. 66	Theorem 40	dminss 5039
[Suppes] p. 66	Theorem 41	imainss 5040
[Suppes] p. 67	Exercise 11	cnvxp 5043
[Suppes] p. 81	Definition 34	dfec2 6532
[Suppes] p. 82	Theorem 72	elec 6568  elecg 6567
[Suppes] p. 82	Theorem 73	erth 6573  erth2 6574
[Suppes] p. 89	Theorem 96	map0b 6681
[Suppes] p. 89	Theorem 97	map0 6683  map0g 6682
[Suppes] p. 89	Theorem 98	mapsn 6684
[Suppes] p. 89	Theorem 99	mapss 6685
[Suppes] p. 92	Theorem 1	enref 6759  enrefg 6758
[Suppes] p. 92	Theorem 2	ensym 6775  ensymb 6774  ensymi 6776
[Suppes] p. 92	Theorem 3	entr 6778
[Suppes] p. 92	Theorem 4	unen 6810
[Suppes] p. 94	Theorem 15	endom 6757
[Suppes] p. 94	Theorem 16	ssdomg 6772
[Suppes] p. 94	Theorem 17	domtr 6779
[Suppes] p. 95	Theorem 18	isbth 6960
[Suppes] p. 98	Exercise 4	fundmen 6800  fundmeng 6801
[Suppes] p. 98	Exercise 6	xpdom3m 6828
[Suppes] p. 130	Definition 3	df-tr 4099
[Suppes] p. 132	Theorem 9	ssonuni 4484
[Suppes] p. 134	Definition 6	df-suc 4368
[Suppes] p. 136	Theorem Schema 22	findes 4599  finds 4596  finds1 4598  finds2 4597
[Suppes] p. 162	Definition 5	df-ltnqqs 7343  df-ltpq 7336
[Suppes] p. 228	Theorem Schema 61	onintss 4387
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2159
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2170
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2173
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2172
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2195
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5873
[TakeutiZaring] p. 14	Proposition 4.14	ru 2961
[TakeutiZaring] p. 15	Exercise 1	elpr 3612  elpr2 3613  elprg 3611
[TakeutiZaring] p. 15	Exercise 2	elsn 3607  elsn2 3625  elsn2g 3624  elsng 3606  velsn 3608
[TakeutiZaring] p. 15	Exercise 3	elop 4228
[TakeutiZaring] p. 15	Exercise 4	sneq 3602  sneqr 3758
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3610  dfsn2 3605
[TakeutiZaring] p. 16	Axiom 3	uniex 4434
[TakeutiZaring] p. 16	Exercise 6	opth 4234
[TakeutiZaring] p. 16	Exercise 8	rext 4212
[TakeutiZaring] p. 16	Corollary 5.8	unex 4438  unexg 4440
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3640
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3808
[TakeutiZaring] p. 16	Definition 5.6	df-in 3135  df-un 3133
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3821  uniprg 3822
[TakeutiZaring] p. 17	Axiom 4	vpwex 4176
[TakeutiZaring] p. 17	Exercise 1	eltp 3639
[TakeutiZaring] p. 17	Exercise 5	elsuc 4403  elsucg 4401  sstr2 3162
[TakeutiZaring] p. 17	Exercise 6	uncom 3279
[TakeutiZaring] p. 17	Exercise 7	incom 3327
[TakeutiZaring] p. 17	Exercise 8	unass 3292
[TakeutiZaring] p. 17	Exercise 9	inass 3345
[TakeutiZaring] p. 17	Exercise 10	indi 3382
[TakeutiZaring] p. 17	Exercise 11	undi 3383
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3144
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3576
[TakeutiZaring] p. 18	Exercise 7	unss2 3306
[TakeutiZaring] p. 18	Exercise 9	df-ss 3142  sseqin2 3354
[TakeutiZaring] p. 18	Exercise 10	ssid 3175
[TakeutiZaring] p. 18	Exercise 12	inss1 3355  inss2 3356
[TakeutiZaring] p. 18	Exercise 13	nssr 3215
[TakeutiZaring] p. 18	Exercise 15	unieq 3816
[TakeutiZaring] p. 18	Exercise 18	sspwb 4213
[TakeutiZaring] p. 18	Exercise 19	pweqb 4220
[TakeutiZaring] p. 20	Definition	df-rab 2464
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4127
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3131
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3424
[TakeutiZaring] p. 20	Proposition 5.15	difid 3491  difidALT 3492
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3435
[TakeutiZaring] p. 21	Theorem 5.22	setind 4535
[TakeutiZaring] p. 21	Definition 5.20	df-v 2739
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4132
[TakeutiZaring] p. 22	Exercise 1	0ss 3461
[TakeutiZaring] p. 22	Exercise 3	ssex 4137  ssexg 4139
[TakeutiZaring] p. 22	Exercise 4	inex1 4134
[TakeutiZaring] p. 22	Exercise 5	ruv 4546
[TakeutiZaring] p. 22	Exercise 6	elirr 4537
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3487
[TakeutiZaring] p. 22	Exercise 11	difdif 3260
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3396
[TakeutiZaring] p. 22	Exercise 14	difss 3261
[TakeutiZaring] p. 22	Exercise 15	sscon 3269
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2460
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2461
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4738  xpexg 4737  xpexgALT 6128
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4630
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5276
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5428  fun11 5279
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5223  svrelfun 5277
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4810
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4812
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4635
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4636
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4632
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5079  dfrel2 5075
[TakeutiZaring] p. 25	Exercise 3	xpss 4731
[TakeutiZaring] p. 25	Exercise 5	relun 4740
[TakeutiZaring] p. 25	Exercise 6	reluni 4746
[TakeutiZaring] p. 25	Exercise 9	inxp 4757
[TakeutiZaring] p. 25	Exercise 12	relres 4931
[TakeutiZaring] p. 25	Exercise 13	opelres 4908  opelresg 4910
[TakeutiZaring] p. 25	Exercise 14	dmres 4924
[TakeutiZaring] p. 25	Exercise 15	resss 4927
[TakeutiZaring] p. 25	Exercise 17	resabs1 4932
[TakeutiZaring] p. 25	Exercise 18	funres 5253
[TakeutiZaring] p. 25	Exercise 24	relco 5123
[TakeutiZaring] p. 25	Exercise 29	funco 5252
[TakeutiZaring] p. 25	Exercise 30	f1co 5429
[TakeutiZaring] p. 26	Definition 6.10	eu2 2070
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5220  fv3 5534
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5163  cnvexg 5162
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4889  dmexg 4887
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4890  rnexg 4888
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5528
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5538  tz6.12 5539  tz6.12c 5541
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5502
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5215
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5216
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5218  wfo 5210
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5217  wf1 5209
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5219  wf1o 5211
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5609  eqfnfv2 5610  eqfnfv2f 5613
[TakeutiZaring] p. 28	Exercise 5	fvco 5582
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5734  fnexALT 6106
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5733  resfunexgALT 6103
[TakeutiZaring] p. 29	Exercise 9	funimaex 5297  funimaexg 5296
[TakeutiZaring] p. 29	Definition 6.18	df-br 4001
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4994  iniseg 4996
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4286
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5221
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5805
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5806
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5811
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5813
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5821
[TakeutiZaring] p. 35	Notation	wtr 4098
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4351
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4102
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4572
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4378
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4382
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4488
[TakeutiZaring] p. 38	Definition 7.11	df-on 4365
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4482
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4548
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4578
[TakeutiZaring] p. 40	Exercise 7	dftr2 4100
[TakeutiZaring] p. 40	Exercise 11	unon 4507
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4483
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3835
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4368
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4412  sucidg 4413
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4497
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4366
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4502  ordelsuc 4501
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4590
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4591
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4592
[TakeutiZaring] p. 43	Axiom 7	omex 4589
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4603
[TakeutiZaring] p. 43	Corollary 7.31	find 4595
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4593
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4594
[TakeutiZaring] p. 44	Exercise 2	int0 3856
[TakeutiZaring] p. 44	Exercise 3	trintssm 4114
[TakeutiZaring] p. 44	Exercise 4	intss1 3857
[TakeutiZaring] p. 44	Exercise 6	onintonm 4513
[TakeutiZaring] p. 44	Definition 7.35	df-int 3843
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6303
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6360  tfri1d 6330
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6361  tfri2d 6331
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6362
[TakeutiZaring] p. 50	Exercise 3	smoiso 6297
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6281
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6459
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6455
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6452
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6456
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6504  nnaordi 6503
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3929  uniss2 3838
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6465
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6475
[TakeutiZaring] p. 62	Exercise 5	oaword1 6466
[TakeutiZaring] p. 62	Definition 8.15	om0 6453  omsuc 6467
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6476
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6512  nnmordi 6511
[TakeutiZaring] p. 67	Definition 8.30	oei0 6454
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7180
[TakeutiZaring] p. 88	Exercise 1	en0 6789
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6851
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6852
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6737  isfi 6755
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6825
[TakeutiZaring] p. 95	Definition 10.42	df-map 6644
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6842
[Tarski] p. 67	Axiom B5	ax-4 1510
[Tarski] p. 68	Lemma 6	equid 1701
[Tarski] p. 69	Lemma 7	equcomi 1704
[Tarski] p. 70	Lemma 14	spim 1738  spime 1741  spimeh 1739  spimh 1737
[Tarski] p. 70	Lemma 16	ax-11 1506  ax-11o 1823  ax11i 1714
[Tarski] p. 70	Lemmas 16 and 17	sb6 1886
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1526
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2150  ax-14 2151
[WhiteheadRussell] p. 96	Axiom *1.3	olc 711
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 727
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 756
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 765
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 789
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 616
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 643
[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 837
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2124  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 737
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 836
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 629
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 885
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 843
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 856
[WhiteheadRussell] p. 103	Theorem *2.16	con3 642
[WhiteheadRussell] p. 103	Theorem *2.17	condc 853
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 855
[WhiteheadRussell] p. 104	Theorem *2.2	orc 712
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 775
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 617
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 621
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 893
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 907
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 768
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 769
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 804
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 805
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 803
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 979
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 778
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 776
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 777
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 738
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 739
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 867  pm2.5gdc 866
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 862
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 740
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 741
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 742
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 655
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 656
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 722
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 891
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 725
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 726
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 865
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 748
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 800
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 801
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 659
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 713  pm2.67 743
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 869  pm2.521gdc 868
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 747
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 810
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 894
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 915
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 806
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 807
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 809
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 808
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 811
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 812
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 905
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 754
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 957
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 958
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 959
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 753
[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 693
[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 860
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 859
[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 689
[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 755  pm3.44 715
[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 785
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 871
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 872
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 890
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 694
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 952  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 757  pm4.25 758
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 818
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 728
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 767
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 792
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 605
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 822
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 980
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 816
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 971
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 949
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 779
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 814  pm4.45 784  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1481
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 956
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 897  imorr 721
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 899
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 750
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 751
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 902
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 938
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 752  pm4.56 780
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 939  oranim 781
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 686
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 898
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 886
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 900
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 687
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 901
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 887
[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 827
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 744
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 603  pm4.76 604
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 710  pm4.77 799
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 782
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 903
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 707
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 908
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 950
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 951
[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 909
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 910
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 912
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 911
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1389
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 828
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 904
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1394  pm5.18dc 883
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 706
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 695
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1392
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1397
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1398
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 895
[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 926  pm5.6r 927
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 954
[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 917
[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 925
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 802
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 918
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 913
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 794
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 945
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 946
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 961
[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 962
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1635
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1485
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1632
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1895
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2029
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2428
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2429
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2875
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3019
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5192
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5193
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2105  eupickbi 2108
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5220
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7183