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 7104  fidcenum 6945
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6945
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7104
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12391
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6919
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6907
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12406
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12408
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12397  znnen 12364
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12409
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12410
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10722
[AczelRathjen], p. 183	Chapter 20	ax-setind 4530
[Apostol] p. 18	Theorem I.1	addcan 8111  addcan2d 8116  addcan2i 8114  addcand 8115  addcani 8113
[Apostol] p. 18	Theorem I.2	negeu 8122
[Apostol] p. 18	Theorem I.3	negsub 8179  negsubd 8248  negsubi 8209
[Apostol] p. 18	Theorem I.4	negneg 8181  negnegd 8233  negnegi 8201
[Apostol] p. 18	Theorem I.5	subdi 8316  subdid 8345  subdii 8338  subdir 8317  subdird 8346  subdiri 8339
[Apostol] p. 18	Theorem I.6	mul01 8320  mul01d 8324  mul01i 8322  mul02 8318  mul02d 8323  mul02i 8321
[Apostol] p. 18	Theorem I.9	divrecapd 8722
[Apostol] p. 18	Theorem I.10	recrecapi 8673
[Apostol] p. 18	Theorem I.12	mul2neg 8329  mul2negd 8344  mul2negi 8337  mulneg1 8326  mulneg1d 8342  mulneg1i 8335
[Apostol] p. 18	Theorem I.15	divdivdivap 8642
[Apostol] p. 20	Axiom 7	rpaddcl 9646  rpaddcld 9681  rpmulcl 9647  rpmulcld 9682
[Apostol] p. 20	Axiom 9	0nrp 9658
[Apostol] p. 20	Theorem I.17	lttri 8036
[Apostol] p. 20	Theorem I.18	ltadd1d 8469  ltadd1dd 8487  ltadd1i 8433
[Apostol] p. 20	Theorem I.19	ltmul1 8523  ltmul1a 8522  ltmul1i 8848  ltmul1ii 8856  ltmul2 8784  ltmul2d 9708  ltmul2dd 9722  ltmul2i 8851
[Apostol] p. 20	Theorem I.21	0lt1 8058
[Apostol] p. 20	Theorem I.23	lt0neg1 8399  lt0neg1d 8446  ltneg 8393  ltnegd 8454  ltnegi 8424
[Apostol] p. 20	Theorem I.25	lt2add 8376  lt2addd 8498  lt2addi 8441
[Apostol] p. 20	Definition of positive numbers	df-rp 9623
[Apostol] p. 21	Exercise 4	recgt0 8778  recgt0d 8862  recgt0i 8834  recgt0ii 8835
[Apostol] p. 22	Definition of integers	df-z 9225
[Apostol] p. 22	Definition of rationals	df-q 9591
[Apostol] p. 24	Theorem I.26	supeuti 6983
[Apostol] p. 26	Theorem I.29	arch 9144
[Apostol] p. 28	Exercise 2	btwnz 9343
[Apostol] p. 28	Exercise 3	nnrecl 9145
[Apostol] p. 28	Exercise 6	qbtwnre 10225
[Apostol] p. 28	Exercise 10(a)	zeneo 11841  zneo 9325
[Apostol] p. 29	Theorem I.35	resqrtth 11006  sqrtthi 11094
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8893
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12002
[Apostol] p. 363	Remark	absgt0api 11121
[Apostol] p. 363	Example	abssubd 11168  abssubi 11125
[ApostolNT] p. 14	Definition	df-dvds 11761
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11777
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11801
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11797
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11791
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11793
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11778
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11779
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11784
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11816
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11818
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11820
[ApostolNT] p. 15	Definition	dfgcd2 11980
[ApostolNT] p. 16	Definition	isprm2 12082
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12057
[ApostolNT] p. 16	Theorem 1.7	prminf 12421
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11939
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11981
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 11983
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11953
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11946
[ApostolNT] p. 17	Theorem 1.8	coprm 12109
[ApostolNT] p. 17	Theorem 1.9	euclemma 12111
[ApostolNT] p. 17	Theorem 1.10	1arith2 12331
[ApostolNT] p. 19	Theorem 1.14	divalg 11894
[ApostolNT] p. 20	Theorem 1.15	eucalg 12024
[ApostolNT] p. 25	Definition	df-phi 12176
[ApostolNT] p. 26	Theorem 2.2	phisum 12205
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12187
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12191
[ApostolNT] p. 104	Definition	congr 12065
[ApostolNT] p. 106	Remark	dvdsval3 11764
[ApostolNT] p. 106	Definition	moddvds 11772
[ApostolNT] p. 107	Example 2	mod2eq0even 11848
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11849
[ApostolNT] p. 107	Example 4	zmod1congr 10309
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10346
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10614
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11796
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12068
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12070
[ApostolNT] p. 113	Theorem 5.17	eulerth 12198
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12216
[ApostolNT] p. 114	Theorem 5.19	fermltl 12199
[ApostolNT] p. 179	Definition	df-lgs 13950  lgsprme0 13994
[ApostolNT] p. 180	Example 1	1lgs 13995
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 13971
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 13986
[ApostolNT] p. 188	Definition	df-lgs 13950  lgs1 13996
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 13987
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 13989
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 13997
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 13998
[Bauer] p. 482	Section 1.2	pm2.01 616  pm2.65 659
[Bauer] p. 483	Theorem 1.3	acexmid 5864  onsucelsucexmidlem 4522
[Bauer], p. 481	Section 1.1	pwtrufal 14287
[Bauer], p. 483	Definition	n0rf 3433
[Bauer], p. 483	Theorem 1.2	2irrexpq 13945  2irrexpqap 13947
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6866
[Bauer], p. 494	Theorem 5.5	ivthinc 13672
[BauerHanson], p. 27	Proposition 5.2	cnstab 8576
[BauerSwan], p. 14	Remark	0ct 7096  ctm 7098
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 14291
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7104
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7475
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7388
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7477
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7511  addlocpr 7510
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7537
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7540
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7545
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2027
[BellMachover] p. 460	Notation	df-mo 2028
[BellMachover] p. 460	Definition	mo3 2078  mo3h 2077
[BellMachover] p. 462	Theorem 1.1	bm1.1 2160
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4119
[BellMachover] p. 466	Axiom Pow	axpow3 4172
[BellMachover] p. 466	Axiom Union	axun2 4429
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4535
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4378
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4538
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4489
[BellMachover] p. 471	Definition of Lim	df-ilim 4363
[BellMachover] p. 472	Axiom Inf	zfinf2 4582
[BellMachover] p. 473	Theorem 2.8	limom 4607
[Bobzien] p. 116	Statement T3	stoic3 1429
[Bobzien] p. 117	Statement T2	stoic2a 1427
[Bobzien] p. 117	Statement T4	stoic4a 1430
[BourbakiAlg1] p. 1	Definition 1	df-mgm 12639
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 12672
[BourbakiAlg1] p. 12	Definition 2	df-mnd 12682
[BourbakiAlg1] p. 92	Definition 1	df-ring 12974
[BourbakiEns] p.	Proposition 8	fcof1 5774  fcofo 5775
[BourbakiTop1] p.	Remark	xnegmnf 9798  xnegpnf 9797
[BourbakiTop1] p.	Remark	rexneg 9799
[BourbakiTop1] p.	Proposition	ishmeo 13355
[BourbakiTop1] p.	Property V_i	ssnei2 13208
[BourbakiTop1] p.	Property V_ii	innei 13214
[BourbakiTop1] p.	Property V_iv	neissex 13216
[BourbakiTop1] p.	Proposition 1	neipsm 13205  neiss 13201
[BourbakiTop1] p.	Proposition 2	cnptopco 13273
[BourbakiTop1] p.	Proposition 4	imasnopn 13350
[BourbakiTop1] p.	Property V_iii	elnei 13203
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 13047
[Bruck] p. 1	Section I.1	df-mgm 12639
[Bruck] p. 23	Section II.1	df-sgrp 12672
[Bruck] p. 28	Theorem 3.2	dfgrp3m 12828
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4061
[Cohen] p. 301	Remark	relogoprlem 13840
[Cohen] p. 301	Property 2	relogmul 13841  relogmuld 13856
[Cohen] p. 301	Property 3	relogdiv 13842  relogdivd 13857
[Cohen] p. 301	Property 4	relogexp 13844
[Cohen] p. 301	Property 1a	log1 13838
[Cohen] p. 301	Property 1b	loge 13839
[Cohen4] p. 348	Observation	relogbcxpbap 13934
[Cohen4] p. 352	Definition	rpelogb 13918
[Cohen4] p. 361	Property 2	rprelogbmul 13924
[Cohen4] p. 361	Property 3	logbrec 13929  rprelogbdiv 13926
[Cohen4] p. 361	Property 4	rplogbreexp 13922
[Cohen4] p. 361	Property 6	relogbexpap 13927
[Cohen4] p. 361	Property 1(a)	rplogbid1 13916
[Cohen4] p. 361	Property 1(b)	rplogb1 13917
[Cohen4] p. 367	Property	rplogbchbase 13919
[Cohen4] p. 377	Property 2	logblt 13931
[Crosilla] p.	Axiom 1	ax-ext 2157
[Crosilla] p.	Axiom 2	ax-pr 4203
[Crosilla] p.	Axiom 3	ax-un 4427
[Crosilla] p.	Axiom 4	ax-nul 4124
[Crosilla] p.	Axiom 5	ax-iinf 4581
[Crosilla] p.	Axiom 6	ru 2959
[Crosilla] p.	Axiom 8	ax-pow 4169
[Crosilla] p.	Axiom 9	ax-setind 4530
[Crosilla], p.	Axiom 6	ax-sep 4116
[Crosilla], p.	Axiom 7	ax-coll 4113
[Crosilla], p.	Axiom 7'	repizf 4114
[Crosilla], p.	Theorem is stated	ordtriexmid 4514
[Crosilla], p.	Axiom of choice implies instances	acexmid 5864
[Crosilla], p.	Definition of ordinal	df-iord 4360
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4528
[Eisenberg] p. 67	Definition 5.3	df-dif 3129
[Eisenberg] p. 82	Definition 6.3	df-iom 4584
[Eisenberg] p. 125	Definition 8.21	df-map 6640
[Enderton] p. 18	Axiom of Empty Set	axnul 4123
[Enderton] p. 19	Definition	df-tp 3597
[Enderton] p. 26	Exercise 5	unissb 3835
[Enderton] p. 26	Exercise 10	pwel 4212
[Enderton] p. 28	Exercise 7(b)	pwunim 4280
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3951  iinin2m 3950  iunin1 3946  iunin2 3945
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3949  iundif2ss 3947
[Enderton] p. 33	Exercise 23	iinuniss 3964
[Enderton] p. 33	Exercise 25	iununir 3965
[Enderton] p. 33	Exercise 24(a)	iinpw 3972
[Enderton] p. 33	Exercise 24(b)	iunpw 4474  iunpwss 3973
[Enderton] p. 38	Exercise 6(a)	unipw 4211
[Enderton] p. 38	Exercise 6(b)	pwuni 4187
[Enderton] p. 41	Lemma 3D	opeluu 4444  rnex 4887  rnexg 4885
[Enderton] p. 41	Exercise 8	dmuni 4830  rnuni 5032
[Enderton] p. 42	Definition of a function	dffun7 5235  dffun8 5236
[Enderton] p. 43	Definition of function value	funfvdm2 5572
[Enderton] p. 43	Definition of single-rooted	funcnv 5269
[Enderton] p. 44	Definition (d)	dfima2 4965  dfima3 4966
[Enderton] p. 47	Theorem 3H	fvco2 5577
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7195
[Enderton] p. 50	Theorem 3K(a)	imauni 5752
[Enderton] p. 52	Definition	df-map 6640
[Enderton] p. 53	Exercise 21	coass 5139
[Enderton] p. 53	Exercise 27	dmco 5129
[Enderton] p. 53	Exercise 14(a)	funin 5279
[Enderton] p. 53	Exercise 22(a)	imass2 4997
[Enderton] p. 54	Remark	ixpf 6710  ixpssmap 6722
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6689
[Enderton] p. 56	Theorem 3M	erref 6545
[Enderton] p. 57	Lemma 3N	erthi 6571
[Enderton] p. 57	Definition	df-ec 6527
[Enderton] p. 58	Definition	df-qs 6531
[Enderton] p. 60	Theorem 3Q	th3q 6630  th3qcor 6629  th3qlem1 6627  th3qlem2 6628
[Enderton] p. 61	Exercise 35	df-ec 6527
[Enderton] p. 65	Exercise 56(a)	dmun 4827
[Enderton] p. 68	Definition of successor	df-suc 4365
[Enderton] p. 71	Definition	df-tr 4097  dftr4 4101
[Enderton] p. 72	Theorem 4E	unisuc 4407  unisucg 4408
[Enderton] p. 73	Exercise 6	unisuc 4407  unisucg 4408
[Enderton] p. 73	Exercise 5(a)	truni 4110
[Enderton] p. 73	Exercise 5(b)	trint 4111
[Enderton] p. 79	Theorem 4I(A1)	nna0 6465
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6467  onasuc 6457
[Enderton] p. 79	Definition of operation value	df-ov 5868
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6466
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6468  onmsuc 6464
[Enderton] p. 81	Theorem 4K(1)	nnaass 6476
[Enderton] p. 81	Theorem 4K(2)	nna0r 6469  nnacom 6475
[Enderton] p. 81	Theorem 4K(3)	nndi 6477
[Enderton] p. 81	Theorem 4K(4)	nnmass 6478
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6480
[Enderton] p. 82	Exercise 16	nnm0r 6470  nnmsucr 6479
[Enderton] p. 88	Exercise 23	nnaordex 6519
[Enderton] p. 129	Definition	df-en 6731
[Enderton] p. 132	Theorem 6B(b)	canth 5819
[Enderton] p. 133	Exercise 1	xpomen 12361
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6855
[Enderton] p. 136	Corollary 6E	nneneq 6847
[Enderton] p. 139	Theorem 6H(c)	mapen 6836
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7207
[Enderton] p. 143	Theorem 6J	dju0en 7203  dju1en 7202
[Enderton] p. 144	Corollary 6K	undif2ss 3496
[Enderton] p. 145	Figure 38	ffoss 5485
[Enderton] p. 145	Definition	df-dom 6732
[Enderton] p. 146	Example 1	domen 6741  domeng 6742
[Enderton] p. 146	Example 3	nndomo 6854
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6825  xpdom1g 6823  xpdom2g 6822
[Enderton] p. 168	Definition	df-po 4290
[Enderton] p. 192	Theorem 7M(a)	oneli 4422
[Enderton] p. 192	Theorem 7M(b)	ontr1 4383
[Enderton] p. 192	Theorem 7M(c)	onirri 4536
[Enderton] p. 193	Corollary 7N(b)	0elon 4386
[Enderton] p. 193	Corollary 7N(c)	onsuci 4509
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4482
[Enderton] p. 194	Remark	onprc 4545
[Enderton] p. 194	Exercise 16	suc11 4551
[Enderton] p. 197	Definition	df-card 7169
[Enderton] p. 200	Exercise 25	tfis 4576
[Enderton] p. 206	Theorem 7X(b)	en2lp 4547
[Enderton] p. 207	Exercise 34	opthreg 4549
[Enderton] p. 208	Exercise 35	suc11g 4550
[Geuvers], p. 1	Remark	expap0 10518
[Geuvers], p. 6	Lemma 2.13	mulap0r 8546
[Geuvers], p. 6	Lemma 2.15	mulap0 8584
[Geuvers], p. 9	Lemma 2.35	msqge0 8547
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7905
[Geuvers], p. 10	Lemma 3.9	maxcom 11178
[Geuvers], p. 10	Lemma 3.10	maxle1 11186  maxle2 11187
[Geuvers], p. 10	Lemma 3.11	maxleast 11188
[Geuvers], p. 10	Lemma 3.12	maxleb 11191
[Geuvers], p. 11	Definition 3.13	dfabsmax 11192
[Geuvers], p. 17	Definition 6.1	df-ap 8513
[Gleason] p. 117	Proposition 9-2.1	df-enq 7321  enqer 7332
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7325  df-nqqs 7322
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7318  df-plqqs 7323
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7319  df-mqqs 7324
[Gleason] p. 119	Proposition 9-2.5	df-rq 7326
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7382
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7385  ltbtwnnq 7390  ltbtwnnqq 7389
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7374
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7375
[Gleason] p. 123	Proposition 9-3.5	addclpr 7511
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7553
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7552
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7571
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7587
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7593  ltaprlem 7592
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7590
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7546
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7566
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7555
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7554
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7562
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7612
[Gleason] p. 126	Proposition 9-4.1	df-enr 7700  enrer 7709
[Gleason] p. 126	Proposition 9-4.2	df-0r 7705  df-1r 7706  df-nr 7701
[Gleason] p. 126	Proposition 9-4.3	df-mr 7703  df-plr 7702  negexsr 7746  recexsrlem 7748
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7704
[Gleason] p. 130	Proposition 10-1.3	creui 8888  creur 8887  cru 8533
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7897  axcnre 7855
[Gleason] p. 132	Definition 10-3.1	crim 10833  crimd 10952  crimi 10912  crre 10832  crred 10951  crrei 10911
[Gleason] p. 132	Definition 10-3.2	remim 10835  remimd 10917
[Gleason] p. 133	Definition 10.36	absval2 11032  absval2d 11160  absval2i 11119
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10859  cjaddd 10940  cjaddi 10907
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10860  cjmuld 10941  cjmuli 10908
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10858  cjcjd 10918  cjcji 10890
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10857  cjreb 10841  cjrebd 10921  cjrebi 10893  cjred 10946  rere 10840  rereb 10838  rerebd 10920  rerebi 10892  rered 10944
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10866  addcjd 10932  addcji 10902
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10976
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11027  abscjd 11165  abscji 11123
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11039  abs00d 11161  abs00i 11120  absne0d 11162
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11071  releabsd 11166  releabsi 11124
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11044  absmuld 11169  absmuli 11126
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11030  sqabsaddi 11127
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11079  abstrid 11171  abstrii 11130
[Gleason] p. 134	Definition 10-4.1	df-exp 10488  exp0 10492  expp1 10495  expp1d 10622
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10530  expaddd 10623
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 13884  cxpmuld 13907  expmul 10533  expmuld 10624
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10527  mulexpd 10636  rpmulcxp 13881
[Gleason] p. 141	Definition 11-2.1	fzval 9979
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11300
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11302
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11301
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11305
[Gleason] p. 172	Corollary 12-2.5	climrecl 11298
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11294  climcj 11295  climim 11297  climre 11296
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7971  df-xr 7970  ltxr 9744
[Gleason] p. 180	Theorem 12-5.3	climcau 11321
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10268
[Gleason] p. 223	Definition 14-1.1	df-met 13040
[Gleason] p. 223	Definition 14-1.1(a)	met0 13415  xmet0 13414
[Gleason] p. 223	Definition 14-1.1(c)	metsym 13422
[Gleason] p. 223	Definition 14-1.1(d)	mettri 13424  mstri 13524  xmettri 13423  xmstri 13523
[Gleason] p. 230	Proposition 14-2.6	txlm 13330
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13562
[Gleason] p. 243	Proposition 14-4.16	addcn2 11284  addcncntop 13603  mulcn2 11286  mulcncntop 13605  subcn2 11285  subcncntop 13604
[Gleason] p. 295	Remark	bcval3 10697  bcval4 10698
[Gleason] p. 295	Equation 2	bcpasc 10712
[Gleason] p. 295	Definition of binomial coefficient	bcval 10695  df-bc 10694
[Gleason] p. 296	Remark	bcn0 10701  bcnn 10703
[Gleason] p. 296	Theorem 15-2.8	binom 11458
[Gleason] p. 308	Equation 2	ef0 11646
[Gleason] p. 308	Equation 3	efcj 11647
[Gleason] p. 309	Corollary 15-4.3	efne0 11652
[Gleason] p. 309	Corollary 15-4.4	efexp 11656
[Gleason] p. 310	Equation 14	sinadd 11710
[Gleason] p. 310	Equation 15	cosadd 11711
[Gleason] p. 311	Equation 17	sincossq 11722
[Gleason] p. 311	Equation 18	cosbnd 11727  sinbnd 11726
[Gleason] p. 311	Definition of ` `	df-pi 11627
[Golan] p. 1	Remark	srgisid 12962
[Golan] p. 1	Definition	df-srg 12940
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1447
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 12748  mndideu 12691
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 12771
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 12796
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 12807
[Herstein] p. 57	Exercise 1	dfgrp3me 12829
[Heyting] p. 127	Axiom #1	ax1hfs 14360
[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 7214
[HoTT], p.	Theorem 7.2.6	nndceq 6490
[HoTT], p.	Exercise 11.10	neapmkv 14356
[HoTT], p.	Exercise 11.11	mulap0bd 8587
[HoTT], p.	Section 11.2.1	df-iltp 7444  df-imp 7443  df-iplp 7442  df-reap 8506
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7636
[HoTT], p.	Corollary 11.4.3	conventions 14013
[HoTT], p.	Exercise 11.6(i)	dcapnconst 14349  dceqnconst 14348
[HoTT], p.	Corollary 11.2.13	axcaucvg 7874  caucvgpr 7656  caucvgprpr 7686  caucvgsr 7776
[HoTT], p.	Definition 11.2.1	df-inp 7440
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 14354
[HoTT], p.	Proposition 11.2.3	df-iso 4291  ltpopr 7569  ltsopr 7570
[HoTT], p.	Definition 11.2.7(v)	apsym 8537  reapcotr 8529  reapirr 8508
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8058  gt0add 8504  leadd1 8361  lelttr 8020  lemul1a 8786  lenlt 8007  ltadd1 8360  ltletr 8021  ltmul1 8523  reaplt 8519
[Jech] p. 4	Definition of class	cv 1352  cvjust 2170
[Jech] p. 78	Note	opthprc 4671
[KalishMontague] p. 81	Note 1	ax-i9 1528
[Kreyszig] p. 3	Property M1	metcl 13404  xmetcl 13403
[Kreyszig] p. 4	Property M2	meteq0 13411
[Kreyszig] p. 12	Equation 5	muleqadd 8598
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13493
[Kreyszig] p. 19	Remark	mopntopon 13494
[Kreyszig] p. 19	Theorem T1	mopn0 13539  mopnm 13499
[Kreyszig] p. 19	Theorem T2	unimopn 13537
[Kreyszig] p. 19	Definition of neighborhood	neibl 13542
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13564
[Kreyszig] p. 25	Definition 1.4-1	lmbr 13264
[Kunen] p. 10	Axiom 0	a9e 1694
[Kunen] p. 12	Axiom 6	zfrep6 4115
[Kunen] p. 24	Definition 10.24	mapval 6650  mapvalg 6648
[Kunen] p. 31	Definition 10.24	mapex 6644
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3892
[Lang] p. 3	Statement	lidrideqd 12664  mndbn0 12696
[Lang] p. 3	Definition	df-mnd 12682
[Lang] p. 7	Definition	dfgrp2e 12763
[Levy] p. 338	Axiom	df-clab 2162  df-clel 2171  df-cleq 2168
[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 1596
[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 1500
[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 1636  r19.2m 3507
[Margaris] p. 89	Theorem 19.3	19.3 1552  19.3h 1551  rr19.3v 2874
[Margaris] p. 89	Theorem 19.5	alcom 1476
[Margaris] p. 89	Theorem 19.6	alexdc 1617  alexim 1643
[Margaris] p. 89	Theorem 19.7	alnex 1497
[Margaris] p. 89	Theorem 19.8	19.8a 1588  spsbe 1840
[Margaris] p. 89	Theorem 19.9	19.9 1642  19.9h 1641  19.9v 1869  exlimd 1595
[Margaris] p. 89	Theorem 19.11	excom 1662  excomim 1661
[Margaris] p. 89	Theorem 19.12	19.12 1663  r19.12 2581
[Margaris] p. 90	Theorem 19.14	exnalim 1644
[Margaris] p. 90	Theorem 19.15	albi 1466  ralbi 2607
[Margaris] p. 90	Theorem 19.16	19.16 1553
[Margaris] p. 90	Theorem 19.17	19.17 1554
[Margaris] p. 90	Theorem 19.18	exbi 1602  rexbi 2608
[Margaris] p. 90	Theorem 19.19	19.19 1664
[Margaris] p. 90	Theorem 19.20	alim 1455  alimd 1519  alimdh 1465  alimdv 1877  ralimdaa 2541  ralimdv 2543  ralimdva 2542  ralimdvva 2544  sbcimdv 3026
[Margaris] p. 90	Theorem 19.21	19.21-2 1665  19.21 1581  19.21bi 1556  19.21h 1555  19.21ht 1579  19.21t 1580  19.21v 1871  alrimd 1608  alrimdd 1607  alrimdh 1477  alrimdv 1874  alrimi 1520  alrimih 1467  alrimiv 1872  alrimivv 1873  r19.21 2551  r19.21be 2566  r19.21bi 2563  r19.21t 2550  r19.21v 2552  ralrimd 2553  ralrimdv 2554  ralrimdva 2555  ralrimdvv 2559  ralrimdvva 2560  ralrimi 2546  ralrimiv 2547  ralrimiva 2548  ralrimivv 2556  ralrimivva 2557  ralrimivvva 2558  ralrimivw 2549  rexlimi 2585
[Margaris] p. 90	Theorem 19.22	2alimdv 1879  2eximdv 1880  exim 1597  eximd 1610  eximdh 1609  eximdv 1878  rexim 2569  reximdai 2573  reximddv 2578  reximddv2 2580  reximdv 2576  reximdv2 2574  reximdva 2577  reximdvai 2575  reximi2 2571
[Margaris] p. 90	Theorem 19.23	19.23 1676  19.23bi 1590  19.23h 1496  19.23ht 1495  19.23t 1675  19.23v 1881  19.23vv 1882  exlimd2 1593  exlimdh 1594  exlimdv 1817  exlimdvv 1895  exlimi 1592  exlimih 1591  exlimiv 1596  exlimivv 1894  r19.23 2583  r19.23v 2584  rexlimd 2589  rexlimdv 2591  rexlimdv3a 2594  rexlimdva 2592  rexlimdva2 2595  rexlimdvaa 2593  rexlimdvv 2599  rexlimdvva 2600  rexlimdvw 2596  rexlimiv 2586  rexlimiva 2587  rexlimivv 2598
[Margaris] p. 90	Theorem 19.24	i19.24 1637
[Margaris] p. 90	Theorem 19.25	19.25 1624
[Margaris] p. 90	Theorem 19.26	19.26-2 1480  19.26-3an 1481  19.26 1479  r19.26-2 2604  r19.26-3 2605  r19.26 2601  r19.26m 2606
[Margaris] p. 90	Theorem 19.27	19.27 1559  19.27h 1558  19.27v 1897  r19.27av 2610  r19.27m 3516  r19.27mv 3517
[Margaris] p. 90	Theorem 19.28	19.28 1561  19.28h 1560  19.28v 1898  r19.28av 2611  r19.28m 3510  r19.28mv 3513  rr19.28v 2875
[Margaris] p. 90	Theorem 19.29	19.29 1618  19.29r 1619  19.29r2 1620  19.29x 1621  r19.29 2612  r19.29d2r 2619  r19.29r 2613
[Margaris] p. 90	Theorem 19.30	19.30dc 1625
[Margaris] p. 90	Theorem 19.31	19.31r 1679
[Margaris] p. 90	Theorem 19.32	19.32dc 1677  19.32r 1678  r19.32r 2621  r19.32vdc 2624  r19.32vr 2623
[Margaris] p. 90	Theorem 19.33	19.33 1482  19.33b2 1627  19.33bdc 1628
[Margaris] p. 90	Theorem 19.34	19.34 1682
[Margaris] p. 90	Theorem 19.35	19.35-1 1622  19.35i 1623
[Margaris] p. 90	Theorem 19.36	19.36-1 1671  19.36aiv 1899  19.36i 1670  r19.36av 2626
[Margaris] p. 90	Theorem 19.37	19.37-1 1672  19.37aiv 1673  r19.37 2627  r19.37av 2628
[Margaris] p. 90	Theorem 19.38	19.38 1674
[Margaris] p. 90	Theorem 19.39	i19.39 1638
[Margaris] p. 90	Theorem 19.40	19.40-2 1630  19.40 1629  r19.40 2629
[Margaris] p. 90	Theorem 19.41	19.41 1684  19.41h 1683  19.41v 1900  19.41vv 1901  19.41vvv 1902  19.41vvvv 1903  r19.41 2630  r19.41v 2631
[Margaris] p. 90	Theorem 19.42	19.42 1686  19.42h 1685  19.42v 1904  19.42vv 1909  19.42vvv 1910  19.42vvvv 1911  r19.42v 2632
[Margaris] p. 90	Theorem 19.43	19.43 1626  r19.43 2633
[Margaris] p. 90	Theorem 19.44	19.44 1680  r19.44av 2634  r19.44mv 3515
[Margaris] p. 90	Theorem 19.45	19.45 1681  r19.45av 2635  r19.45mv 3514
[Margaris] p. 110	Exercise 2(b)	eu1 2049
[Megill] p. 444	Axiom C5	ax-17 1524
[Megill] p. 445	Lemma L12	alequcom 1513  ax-10 1503
[Megill] p. 446	Lemma L17	equtrr 1708
[Megill] p. 446	Lemma L19	hbnae 1719
[Megill] p. 447	Remark 9.1	df-sb 1761  sbid 1772
[Megill] p. 448	Scheme C5'	ax-4 1508
[Megill] p. 448	Scheme C6'	ax-7 1446
[Megill] p. 448	Scheme C8'	ax-8 1502
[Megill] p. 448	Scheme C9'	ax-i12 1505
[Megill] p. 448	Scheme C11'	ax-10o 1714
[Megill] p. 448	Scheme C12'	ax-13 2148
[Megill] p. 448	Scheme C13'	ax-14 2149
[Megill] p. 448	Scheme C15'	ax-11o 1821
[Megill] p. 448	Scheme C16'	ax-16 1812
[Megill] p. 448	Theorem 9.4	dral1 1728  dral2 1729  drex1 1796  drex2 1730  drsb1 1797  drsb2 1839
[Megill] p. 449	Theorem 9.7	sbcom2 1985  sbequ 1838  sbid2v 1994
[Megill] p. 450	Example in Appendix	hba1 1538
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3043  rspsbca 3044  stdpc4 1773
[Mendelson] p. 69	Axiom 5	ra5 3049  stdpc5 1582
[Mendelson] p. 81	Rule C	exlimiv 1596
[Mendelson] p. 95	Axiom 6	stdpc6 1701
[Mendelson] p. 95	Axiom 7	stdpc7 1768
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3457
[Mendelson] p. 231	Exercise 4.10(l)	unv 3458
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3373
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3421
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3374
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3264
[Mendelson] p. 231	Definition of union	unssin 3372
[Mendelson] p. 235	Exercise 4.12(c)	univ 4470
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3804
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4276
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4277
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4278
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3825
[Mendelson] p. 235	Exercise 4.12(p)	reli 4749
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5141
[Mendelson] p. 246	Definition of successor	df-suc 4365
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6835
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6811  xpsneng 6812
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6817  xpcomeng 6818
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6820
[Mendelson] p. 255	Exercise 4.39	endisj 6814
[Mendelson] p. 255	Exercise 4.41	mapprc 6642
[Mendelson] p. 255	Exercise 4.43	mapsnen 6801
[Mendelson] p. 255	Exercise 4.47	xpmapen 6840
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6676
[Mendelson] p. 255	Exercise 4.42(b)	map1 6802
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7206  djucomen 7205
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7204
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6458
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3355
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4708
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4709
[Monk1] p. 34	Definition 3.3	df-opab 4060
[Monk1] p. 36	Theorem 3.7(i)	coi1 5136  coi2 5137
[Monk1] p. 36	Theorem 3.8(v)	dm0 4834  rn0 4876
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5025
[Monk1] p. 37	Theorem 3.13(i)	relxp 4729
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4840  rnxpm 5050
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4700  xp0 5040
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4980
[Monk1] p. 38	Theorem 3.16(viii)	imai 4977
[Monk1] p. 39	Theorem 3.17	imaex 4976  imaexg 4975
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4974
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5638  funfvop 5620
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5551
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5559
[Monk1] p. 43	Theorem 4.6	funun 5252
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5759  dff13f 5761
[Monk1] p. 46	Theorem 4.15(v)	funex 5731  funrnex 6105
[Monk1] p. 50	Definition 5.4	fniunfv 5753
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5104
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3856
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6146  df-1st 6131
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6147  df-2nd 6132
[Monk2] p. 105	Axiom C4	ax-5 1445
[Monk2] p. 105	Axiom C7	ax-8 1502
[Monk2] p. 105	Axiom C8	ax-11 1504  ax-11o 1821
[Monk2] p. 105	Axiom (C8)	ax11v 1825
[Monk2] p. 109	Lemma 12	ax-7 1446
[Monk2] p. 109	Lemma 15	equvin 1861  equvini 1756  eqvinop 4237
[Monk2] p. 113	Axiom C5-1	ax-17 1524
[Monk2] p. 113	Axiom C5-2	ax6b 1649
[Monk2] p. 113	Axiom C5-3	ax-7 1446
[Monk2] p. 114	Lemma 22	hba1 1538
[Monk2] p. 114	Lemma 23	hbia1 1550  nfia1 1578
[Monk2] p. 114	Lemma 24	hba2 1549  nfa2 1577
[Moschovakis] p. 2	Chapter 2	df-stab 831  dftest 14361
[Munkres] p. 77	Example 2	distop 13136
[Munkres] p. 78	Definition of basis	df-bases 13092  isbasis3g 13095
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12629  tgval2 13102
[Munkres] p. 79	Remark	tgcl 13115
[Munkres] p. 80	Lemma 2.1	tgval3 13109
[Munkres] p. 80	Lemma 2.2	tgss2 13130  tgss3 13129
[Munkres] p. 81	Lemma 2.3	basgen 13131  basgen2 13132
[Munkres] p. 89	Definition of subspace topology	resttop 13221
[Munkres] p. 93	Theorem 6.1(1)	0cld 13163  topcld 13160
[Munkres] p. 93	Theorem 6.1(3)	uncld 13164
[Munkres] p. 94	Definition of closure	clsval 13162
[Munkres] p. 94	Definition of interior	ntrval 13161
[Munkres] p. 102	Definition of continuous function	df-cn 13239  iscn 13248  iscn2 13251
[Munkres] p. 107	Theorem 7.2(g)	cncnp 13281  cncnp2m 13282  cncnpi 13279  df-cnp 13240  iscnp 13250
[Munkres] p. 127	Theorem 10.1	metcn 13565
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6893
[Pierik], p. 9	Definition 2.4	df-womni 7152
[Pierik], p. 9	Definition 2.5	df-markov 7140  omniwomnimkv 7155
[Pierik], p. 10	Section 2.3	dfdif3 3243
[Pierik], p. 14	Definition 3.1	df-omni 7123  exmidomniim 7129  finomni 7128
[Pierik], p. 15	Section 3.1	df-nninf 7109
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 14312
[PradicBrown2022], p. 2	Remark	exmidpw 6898
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7190
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7191  exmidfodomrlemrALT 7192
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7137
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 14297  peano4nninf 14296
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 14299
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 14307
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 14309
[PradicBrown2022], p. 5	Definition 3.3	nnsf 14295
[Quine] p. 16	Definition 2.1	df-clab 2162  rabid 2650
[Quine] p. 17	Definition 2.1''	dfsb7 1989
[Quine] p. 18	Definition 2.7	df-cleq 2168
[Quine] p. 19	Definition 2.9	df-v 2737
[Quine] p. 34	Theorem 5.1	abeq2 2284
[Quine] p. 35	Theorem 5.2	abid2 2296  abid2f 2343
[Quine] p. 40	Theorem 6.1	sb5 1885
[Quine] p. 40	Theorem 6.2	sb56 1883  sb6 1884
[Quine] p. 41	Theorem 6.3	df-clel 2171
[Quine] p. 41	Theorem 6.4	eqid 2175
[Quine] p. 41	Theorem 6.5	eqcom 2177
[Quine] p. 42	Theorem 6.6	df-sbc 2961
[Quine] p. 42	Theorem 6.7	dfsbcq 2962  dfsbcq2 2963
[Quine] p. 43	Theorem 6.8	vex 2738
[Quine] p. 43	Theorem 6.9	isset 2741
[Quine] p. 44	Theorem 7.3	spcgf 2817  spcgv 2822  spcimgf 2815
[Quine] p. 44	Theorem 6.11	spsbc 2972  spsbcd 2973
[Quine] p. 44	Theorem 6.12	elex 2746
[Quine] p. 44	Theorem 6.13	elab 2879  elabg 2881  elabgf 2877
[Quine] p. 44	Theorem 6.14	noel 3424
[Quine] p. 48	Theorem 7.2	snprc 3654
[Quine] p. 48	Definition 7.1	df-pr 3596  df-sn 3595
[Quine] p. 49	Theorem 7.4	snss 3724  snssg 3723
[Quine] p. 49	Theorem 7.5	prss 3745  prssg 3746
[Quine] p. 49	Theorem 7.6	prid1 3695  prid1g 3693  prid2 3696  prid2g 3694  snid 3620  snidg 3618
[Quine] p. 51	Theorem 7.12	snexg 4179  snexprc 4181
[Quine] p. 51	Theorem 7.13	prexg 4205
[Quine] p. 53	Theorem 8.2	unisn 3821  unisng 3822
[Quine] p. 53	Theorem 8.3	uniun 3824
[Quine] p. 54	Theorem 8.6	elssuni 3833
[Quine] p. 54	Theorem 8.7	uni0 3832
[Quine] p. 56	Theorem 8.17	uniabio 5180
[Quine] p. 56	Definition 8.18	dfiota2 5171
[Quine] p. 57	Theorem 8.19	iotaval 5181
[Quine] p. 57	Theorem 8.22	iotanul 5185
[Quine] p. 58	Theorem 8.23	euiotaex 5186
[Quine] p. 58	Definition 9.1	df-op 3598
[Quine] p. 61	Theorem 9.5	opabid 4251  opelopab 4265  opelopaba 4260  opelopabaf 4267  opelopabf 4268  opelopabg 4262  opelopabga 4257  oprabid 5897
[Quine] p. 64	Definition 9.11	df-xp 4626
[Quine] p. 64	Definition 9.12	df-cnv 4628
[Quine] p. 64	Definition 9.15	df-id 4287
[Quine] p. 65	Theorem 10.3	fun0 5266
[Quine] p. 65	Theorem 10.4	funi 5240
[Quine] p. 65	Theorem 10.5	funsn 5256  funsng 5254
[Quine] p. 65	Definition 10.1	df-fun 5210
[Quine] p. 65	Definition 10.2	args 4990  dffv4g 5504
[Quine] p. 68	Definition 10.11	df-fv 5216  fv2 5502
[Quine] p. 124	Theorem 17.3	nn0opth2 10670  nn0opth2d 10669  nn0opthd 10668
[Quine] p. 284	Axiom 39(vi)	funimaex 5293  funimaexg 5292
[Roman] p. 19	Part Preliminaries	df-ring 12974
[Rudin] p. 164	Equation 27	efcan 11650
[Rudin] p. 164	Equation 30	efzval 11657
[Rudin] p. 167	Equation 48	absefi 11742
[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 5005
[Schechter] p. 51	Definition of irreflexivity	intirr 5007
[Schechter] p. 51	Definition of symmetry	cnvsym 5004
[Schechter] p. 51	Definition of transitivity	cotr 5002
[Schechter] p. 187	Definition of ring with unit	isring 12976
[Schechter] p. 428	Definition 15.35	bastop1 13134
[Stoll] p. 13	Definition of symmetric difference	symdif1 3398
[Stoll] p. 16	Exercise 4.4	0dif 3492  dif0 3491
[Stoll] p. 16	Exercise 4.8	difdifdirss 3505
[Stoll] p. 19	Theorem 5.2(13)	undm 3391
[Stoll] p. 19	Theorem 5.2(13')	indmss 3392
[Stoll] p. 20	Remark	invdif 3375
[Stoll] p. 25	Definition of ordered triple	df-ot 3599
[Stoll] p. 43	Definition	uniiun 3935
[Stoll] p. 44	Definition	intiin 3936
[Stoll] p. 45	Definition	df-iin 3885
[Stoll] p. 45	Definition indexed union	df-iun 3884
[Stoll] p. 176	Theorem 3.4(27)	imandc 889  imanst 888
[Stoll] p. 262	Example 4.1	symdif1 3398
[Suppes] p. 22	Theorem 2	eq0 3439
[Suppes] p. 22	Theorem 4	eqss 3168  eqssd 3170  eqssi 3169
[Suppes] p. 23	Theorem 5	ss0 3461  ss0b 3460
[Suppes] p. 23	Theorem 6	sstr 3161
[Suppes] p. 25	Theorem 12	elin 3316  elun 3274
[Suppes] p. 26	Theorem 15	inidm 3342
[Suppes] p. 26	Theorem 16	in0 3455
[Suppes] p. 27	Theorem 23	unidm 3276
[Suppes] p. 27	Theorem 24	un0 3454
[Suppes] p. 27	Theorem 25	ssun1 3296
[Suppes] p. 27	Theorem 26	ssequn1 3303
[Suppes] p. 27	Theorem 27	unss 3307
[Suppes] p. 27	Theorem 28	indir 3382
[Suppes] p. 27	Theorem 29	undir 3383
[Suppes] p. 28	Theorem 32	difid 3489  difidALT 3490
[Suppes] p. 29	Theorem 33	difin 3370
[Suppes] p. 29	Theorem 34	indif 3376
[Suppes] p. 29	Theorem 35	undif1ss 3495
[Suppes] p. 29	Theorem 36	difun2 3500
[Suppes] p. 29	Theorem 37	difin0 3494
[Suppes] p. 29	Theorem 38	disjdif 3493
[Suppes] p. 29	Theorem 39	difundi 3385
[Suppes] p. 29	Theorem 40	difindiss 3387
[Suppes] p. 30	Theorem 41	nalset 4128
[Suppes] p. 39	Theorem 61	uniss 3826
[Suppes] p. 39	Theorem 65	uniop 4249
[Suppes] p. 41	Theorem 70	intsn 3875
[Suppes] p. 42	Theorem 71	intpr 3872  intprg 3873
[Suppes] p. 42	Theorem 73	op1stb 4472  op1stbg 4473
[Suppes] p. 42	Theorem 78	intun 3871
[Suppes] p. 44	Definition 15(a)	dfiun2 3916  dfiun2g 3914
[Suppes] p. 44	Definition 15(b)	dfiin2 3917
[Suppes] p. 47	Theorem 86	elpw 3578  elpw2 4152  elpw2g 4151  elpwg 3580
[Suppes] p. 47	Theorem 87	pwid 3587
[Suppes] p. 47	Theorem 89	pw0 3736
[Suppes] p. 48	Theorem 90	pwpw0ss 3800
[Suppes] p. 52	Theorem 101	xpss12 4727
[Suppes] p. 52	Theorem 102	xpindi 4755  xpindir 4756
[Suppes] p. 52	Theorem 103	xpundi 4676  xpundir 4677
[Suppes] p. 54	Theorem 105	elirrv 4541
[Suppes] p. 58	Theorem 2	relss 4707
[Suppes] p. 59	Theorem 4	eldm 4817  eldm2 4818  eldm2g 4816  eldmg 4815
[Suppes] p. 59	Definition 3	df-dm 4630
[Suppes] p. 60	Theorem 6	dmin 4828
[Suppes] p. 60	Theorem 8	rnun 5029
[Suppes] p. 60	Theorem 9	rnin 5030
[Suppes] p. 60	Definition 4	dfrn2 4808
[Suppes] p. 61	Theorem 11	brcnv 4803  brcnvg 4801
[Suppes] p. 62	Equation 5	elcnv 4797  elcnv2 4798
[Suppes] p. 62	Theorem 12	relcnv 4999
[Suppes] p. 62	Theorem 15	cnvin 5028
[Suppes] p. 62	Theorem 16	cnvun 5026
[Suppes] p. 63	Theorem 20	co02 5134
[Suppes] p. 63	Theorem 21	dmcoss 4889
[Suppes] p. 63	Definition 7	df-co 4629
[Suppes] p. 64	Theorem 26	cnvco 4805
[Suppes] p. 64	Theorem 27	coass 5139
[Suppes] p. 65	Theorem 31	resundi 4913
[Suppes] p. 65	Theorem 34	elima 4968  elima2 4969  elima3 4970  elimag 4967
[Suppes] p. 65	Theorem 35	imaundi 5033
[Suppes] p. 66	Theorem 40	dminss 5035
[Suppes] p. 66	Theorem 41	imainss 5036
[Suppes] p. 67	Exercise 11	cnvxp 5039
[Suppes] p. 81	Definition 34	dfec2 6528
[Suppes] p. 82	Theorem 72	elec 6564  elecg 6563
[Suppes] p. 82	Theorem 73	erth 6569  erth2 6570
[Suppes] p. 89	Theorem 96	map0b 6677
[Suppes] p. 89	Theorem 97	map0 6679  map0g 6678
[Suppes] p. 89	Theorem 98	mapsn 6680
[Suppes] p. 89	Theorem 99	mapss 6681
[Suppes] p. 92	Theorem 1	enref 6755  enrefg 6754
[Suppes] p. 92	Theorem 2	ensym 6771  ensymb 6770  ensymi 6772
[Suppes] p. 92	Theorem 3	entr 6774
[Suppes] p. 92	Theorem 4	unen 6806
[Suppes] p. 94	Theorem 15	endom 6753
[Suppes] p. 94	Theorem 16	ssdomg 6768
[Suppes] p. 94	Theorem 17	domtr 6775
[Suppes] p. 95	Theorem 18	isbth 6956
[Suppes] p. 98	Exercise 4	fundmen 6796  fundmeng 6797
[Suppes] p. 98	Exercise 6	xpdom3m 6824
[Suppes] p. 130	Definition 3	df-tr 4097
[Suppes] p. 132	Theorem 9	ssonuni 4481
[Suppes] p. 134	Definition 6	df-suc 4365
[Suppes] p. 136	Theorem Schema 22	findes 4596  finds 4593  finds1 4595  finds2 4594
[Suppes] p. 162	Definition 5	df-ltnqqs 7327  df-ltpq 7320
[Suppes] p. 228	Theorem Schema 61	onintss 4384
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2157
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2168
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2171
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2170
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2193
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5869
[TakeutiZaring] p. 14	Proposition 4.14	ru 2959
[TakeutiZaring] p. 15	Exercise 1	elpr 3610  elpr2 3611  elprg 3609
[TakeutiZaring] p. 15	Exercise 2	elsn 3605  elsn2 3623  elsn2g 3622  elsng 3604  velsn 3606
[TakeutiZaring] p. 15	Exercise 3	elop 4225
[TakeutiZaring] p. 15	Exercise 4	sneq 3600  sneqr 3756
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3608  dfsn2 3603
[TakeutiZaring] p. 16	Axiom 3	uniex 4431
[TakeutiZaring] p. 16	Exercise 6	opth 4231
[TakeutiZaring] p. 16	Exercise 8	rext 4209
[TakeutiZaring] p. 16	Corollary 5.8	unex 4435  unexg 4437
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3638
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3806
[TakeutiZaring] p. 16	Definition 5.6	df-in 3133  df-un 3131
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3819  uniprg 3820
[TakeutiZaring] p. 17	Axiom 4	vpwex 4174
[TakeutiZaring] p. 17	Exercise 1	eltp 3637
[TakeutiZaring] p. 17	Exercise 5	elsuc 4400  elsucg 4398  sstr2 3160
[TakeutiZaring] p. 17	Exercise 6	uncom 3277
[TakeutiZaring] p. 17	Exercise 7	incom 3325
[TakeutiZaring] p. 17	Exercise 8	unass 3290
[TakeutiZaring] p. 17	Exercise 9	inass 3343
[TakeutiZaring] p. 17	Exercise 10	indi 3380
[TakeutiZaring] p. 17	Exercise 11	undi 3381
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3142
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3574
[TakeutiZaring] p. 18	Exercise 7	unss2 3304
[TakeutiZaring] p. 18	Exercise 9	df-ss 3140  sseqin2 3352
[TakeutiZaring] p. 18	Exercise 10	ssid 3173
[TakeutiZaring] p. 18	Exercise 12	inss1 3353  inss2 3354
[TakeutiZaring] p. 18	Exercise 13	nssr 3213
[TakeutiZaring] p. 18	Exercise 15	unieq 3814
[TakeutiZaring] p. 18	Exercise 18	sspwb 4210
[TakeutiZaring] p. 18	Exercise 19	pweqb 4217
[TakeutiZaring] p. 20	Definition	df-rab 2462
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4125
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3129
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3422
[TakeutiZaring] p. 20	Proposition 5.15	difid 3489  difidALT 3490
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3433
[TakeutiZaring] p. 21	Theorem 5.22	setind 4532
[TakeutiZaring] p. 21	Definition 5.20	df-v 2737
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4130
[TakeutiZaring] p. 22	Exercise 1	0ss 3459
[TakeutiZaring] p. 22	Exercise 3	ssex 4135  ssexg 4137
[TakeutiZaring] p. 22	Exercise 4	inex1 4132
[TakeutiZaring] p. 22	Exercise 5	ruv 4543
[TakeutiZaring] p. 22	Exercise 6	elirr 4534
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3485
[TakeutiZaring] p. 22	Exercise 11	difdif 3258
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3394
[TakeutiZaring] p. 22	Exercise 14	difss 3259
[TakeutiZaring] p. 22	Exercise 15	sscon 3267
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2458
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2459
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4735  xpexg 4734  xpexgALT 6124
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4627
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5272
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5424  fun11 5275
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5219  svrelfun 5273
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4807
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4809
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4632
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4633
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4629
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5075  dfrel2 5071
[TakeutiZaring] p. 25	Exercise 3	xpss 4728
[TakeutiZaring] p. 25	Exercise 5	relun 4737
[TakeutiZaring] p. 25	Exercise 6	reluni 4743
[TakeutiZaring] p. 25	Exercise 9	inxp 4754
[TakeutiZaring] p. 25	Exercise 12	relres 4928
[TakeutiZaring] p. 25	Exercise 13	opelres 4905  opelresg 4907
[TakeutiZaring] p. 25	Exercise 14	dmres 4921
[TakeutiZaring] p. 25	Exercise 15	resss 4924
[TakeutiZaring] p. 25	Exercise 17	resabs1 4929
[TakeutiZaring] p. 25	Exercise 18	funres 5249
[TakeutiZaring] p. 25	Exercise 24	relco 5119
[TakeutiZaring] p. 25	Exercise 29	funco 5248
[TakeutiZaring] p. 25	Exercise 30	f1co 5425
[TakeutiZaring] p. 26	Definition 6.10	eu2 2068
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5216  fv3 5530
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5159  cnvexg 5158
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4886  dmexg 4884
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4887  rnexg 4885
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5524
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5534  tz6.12 5535  tz6.12c 5537
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5498
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5211
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5212
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5214  wfo 5206
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5213  wf1 5205
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5215  wf1o 5207
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5605  eqfnfv2 5606  eqfnfv2f 5609
[TakeutiZaring] p. 28	Exercise 5	fvco 5578
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5730  fnexALT 6102
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5729  resfunexgALT 6099
[TakeutiZaring] p. 29	Exercise 9	funimaex 5293  funimaexg 5292
[TakeutiZaring] p. 29	Definition 6.18	df-br 3999
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4991  iniseg 4993
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4283
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5217
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5801
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5802
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5807
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5809
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5817
[TakeutiZaring] p. 35	Notation	wtr 4096
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4348
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4100
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4569
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4375
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4379
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4485
[TakeutiZaring] p. 38	Definition 7.11	df-on 4362
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4479
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4545
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4575
[TakeutiZaring] p. 40	Exercise 7	dftr2 4098
[TakeutiZaring] p. 40	Exercise 11	unon 4504
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4480
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3833
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4365
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4409  sucidg 4410
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 4494
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4363
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4499  ordelsuc 4498
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4587
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4588
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4589
[TakeutiZaring] p. 43	Axiom 7	omex 4586
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4600
[TakeutiZaring] p. 43	Corollary 7.31	find 4592
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4590
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4591
[TakeutiZaring] p. 44	Exercise 2	int0 3854
[TakeutiZaring] p. 44	Exercise 3	trintssm 4112
[TakeutiZaring] p. 44	Exercise 4	intss1 3855
[TakeutiZaring] p. 44	Exercise 6	onintonm 4510
[TakeutiZaring] p. 44	Definition 7.35	df-int 3841
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6299
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6356  tfri1d 6326
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6357  tfri2d 6327
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6358
[TakeutiZaring] p. 50	Exercise 3	smoiso 6293
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6277
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6455
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6451
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6448
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6452
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6500  nnaordi 6499
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3927  uniss2 3836
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6461
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6471
[TakeutiZaring] p. 62	Exercise 5	oaword1 6462
[TakeutiZaring] p. 62	Definition 8.15	om0 6449  omsuc 6463
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6472
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6508  nnmordi 6507
[TakeutiZaring] p. 67	Definition 8.30	oei0 6450
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7176
[TakeutiZaring] p. 88	Exercise 1	en0 6785
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6847
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6848
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6733  isfi 6751
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6821
[TakeutiZaring] p. 95	Definition 10.42	df-map 6640
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6838
[Tarski] p. 67	Axiom B5	ax-4 1508
[Tarski] p. 68	Lemma 6	equid 1699
[Tarski] p. 69	Lemma 7	equcomi 1702
[Tarski] p. 70	Lemma 14	spim 1736  spime 1739  spimeh 1737  spimh 1735
[Tarski] p. 70	Lemma 16	ax-11 1504  ax-11o 1821  ax11i 1712
[Tarski] p. 70	Lemmas 16 and 17	sb6 1884
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1524
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2148  ax-14 2149
[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 2122  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 1479
[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 1633
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1483
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1630
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1893
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2027
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2426
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2427
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2873
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3017
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5188
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5189
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2103  eupickbi 2106
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5216
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7179