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 7113  fidcenum 6954
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6954
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7113
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12425
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6928
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6916
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12440
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12442
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12431  znnen 12398
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12443
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12444
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10755
[AczelRathjen], p. 183	Chapter 20	ax-setind 4536
[Apostol] p. 18	Theorem I.1	addcan 8136  addcan2d 8141  addcan2i 8139  addcand 8140  addcani 8138
[Apostol] p. 18	Theorem I.2	negeu 8147
[Apostol] p. 18	Theorem I.3	negsub 8204  negsubd 8273  negsubi 8234
[Apostol] p. 18	Theorem I.4	negneg 8206  negnegd 8258  negnegi 8226
[Apostol] p. 18	Theorem I.5	subdi 8341  subdid 8370  subdii 8363  subdir 8342  subdird 8371  subdiri 8364
[Apostol] p. 18	Theorem I.6	mul01 8345  mul01d 8349  mul01i 8347  mul02 8343  mul02d 8348  mul02i 8346
[Apostol] p. 18	Theorem I.9	divrecapd 8749
[Apostol] p. 18	Theorem I.10	recrecapi 8700
[Apostol] p. 18	Theorem I.12	mul2neg 8354  mul2negd 8369  mul2negi 8362  mulneg1 8351  mulneg1d 8367  mulneg1i 8360
[Apostol] p. 18	Theorem I.14	rdivmuldivd 13311
[Apostol] p. 18	Theorem I.15	divdivdivap 8669
[Apostol] p. 20	Axiom 7	rpaddcl 9676  rpaddcld 9711  rpmulcl 9677  rpmulcld 9712
[Apostol] p. 20	Axiom 9	0nrp 9688
[Apostol] p. 20	Theorem I.17	lttri 8061
[Apostol] p. 20	Theorem I.18	ltadd1d 8494  ltadd1dd 8512  ltadd1i 8458
[Apostol] p. 20	Theorem I.19	ltmul1 8548  ltmul1a 8547  ltmul1i 8876  ltmul1ii 8884  ltmul2 8812  ltmul2d 9738  ltmul2dd 9752  ltmul2i 8879
[Apostol] p. 20	Theorem I.21	0lt1 8083
[Apostol] p. 20	Theorem I.23	lt0neg1 8424  lt0neg1d 8471  ltneg 8418  ltnegd 8479  ltnegi 8449
[Apostol] p. 20	Theorem I.25	lt2add 8401  lt2addd 8523  lt2addi 8466
[Apostol] p. 20	Definition of positive numbers	df-rp 9653
[Apostol] p. 21	Exercise 4	recgt0 8806  recgt0d 8890  recgt0i 8862  recgt0ii 8863
[Apostol] p. 22	Definition of integers	df-z 9253
[Apostol] p. 22	Definition of rationals	df-q 9619
[Apostol] p. 24	Theorem I.26	supeuti 6992
[Apostol] p. 26	Theorem I.29	arch 9172
[Apostol] p. 28	Exercise 2	btwnz 9371
[Apostol] p. 28	Exercise 3	nnrecl 9173
[Apostol] p. 28	Exercise 6	qbtwnre 10256
[Apostol] p. 28	Exercise 10(a)	zeneo 11875  zneo 9353
[Apostol] p. 29	Theorem I.35	resqrtth 11039  sqrtthi 11127
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8921
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12036
[Apostol] p. 363	Remark	absgt0api 11154
[Apostol] p. 363	Example	abssubd 11201  abssubi 11158
[ApostolNT] p. 14	Definition	df-dvds 11794
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11810
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11834
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11830
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11824
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11826
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11811
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11812
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11817
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11850
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11852
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11854
[ApostolNT] p. 15	Definition	dfgcd2 12014
[ApostolNT] p. 16	Definition	isprm2 12116
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12091
[ApostolNT] p. 16	Theorem 1.7	prminf 12455
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11973
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12015
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12017
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11987
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11980
[ApostolNT] p. 17	Theorem 1.8	coprm 12143
[ApostolNT] p. 17	Theorem 1.9	euclemma 12145
[ApostolNT] p. 17	Theorem 1.10	1arith2 12365
[ApostolNT] p. 19	Theorem 1.14	divalg 11928
[ApostolNT] p. 20	Theorem 1.15	eucalg 12058
[ApostolNT] p. 25	Definition	df-phi 12210
[ApostolNT] p. 26	Theorem 2.2	phisum 12239
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12221
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12225
[ApostolNT] p. 104	Definition	congr 12099
[ApostolNT] p. 106	Remark	dvdsval3 11797
[ApostolNT] p. 106	Definition	moddvds 11805
[ApostolNT] p. 107	Example 2	mod2eq0even 11882
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11883
[ApostolNT] p. 107	Example 4	zmod1congr 10340
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10377
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10646
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11829
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12102
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12104
[ApostolNT] p. 113	Theorem 5.17	eulerth 12232
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12250
[ApostolNT] p. 114	Theorem 5.19	fermltl 12233
[ApostolNT] p. 179	Definition	df-lgs 14335  lgsprme0 14379
[ApostolNT] p. 180	Example 1	1lgs 14380
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 14356
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 14371
[ApostolNT] p. 181	Theorem 9.4	m1lgs 14388
[ApostolNT] p. 188	Definition	df-lgs 14335  lgs1 14381
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 14372
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 14374
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 14382
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 14383
[Bauer] p. 482	Section 1.2	pm2.01 616  pm2.65 659
[Bauer] p. 483	Theorem 1.3	acexmid 5873  onsucelsucexmidlem 4528
[Bauer], p. 481	Section 1.1	pwtrufal 14683
[Bauer], p. 483	Definition	n0rf 3435
[Bauer], p. 483	Theorem 1.2	2irrexpq 14330  2irrexpqap 14332
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6875
[Bauer], p. 494	Theorem 5.5	ivthinc 14057
[BauerHanson], p. 27	Proposition 5.2	cnstab 8601
[BauerSwan], p. 14	Remark	0ct 7105  ctm 7107
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 14686
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7113
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7499
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7412
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7501
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7535  addlocpr 7534
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7561
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7564
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7569
[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 4124
[BellMachover] p. 466	Axiom Pow	axpow3 4177
[BellMachover] p. 466	Axiom Union	axun2 4435
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4541
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4384
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4544
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4495
[BellMachover] p. 471	Definition of Lim	df-ilim 4369
[BellMachover] p. 472	Axiom Inf	zfinf2 4588
[BellMachover] p. 473	Theorem 2.8	limom 4613
[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 12774
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 12807
[BourbakiAlg1] p. 12	Definition 2	df-mnd 12817
[BourbakiAlg1] p. 92	Definition 1	df-ring 13179
[BourbakiEns] p.	Proposition 8	fcof1 5783  fcofo 5784
[BourbakiTop1] p.	Remark	xnegmnf 9828  xnegpnf 9827
[BourbakiTop1] p.	Remark	rexneg 9829
[BourbakiTop1] p.	Proposition	ishmeo 13740
[BourbakiTop1] p.	Property V_i	ssnei2 13593
[BourbakiTop1] p.	Property V_ii	innei 13599
[BourbakiTop1] p.	Property V_iv	neissex 13601
[BourbakiTop1] p.	Proposition 1	neipsm 13590  neiss 13586
[BourbakiTop1] p.	Proposition 2	cnptopco 13658
[BourbakiTop1] p.	Proposition 4	imasnopn 13735
[BourbakiTop1] p.	Property V_iii	elnei 13588
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 13434
[Bruck] p. 1	Section I.1	df-mgm 12774
[Bruck] p. 23	Section II.1	df-sgrp 12807
[Bruck] p. 28	Theorem 3.2	dfgrp3m 12968
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4066
[Cohen] p. 301	Remark	relogoprlem 14225
[Cohen] p. 301	Property 2	relogmul 14226  relogmuld 14241
[Cohen] p. 301	Property 3	relogdiv 14227  relogdivd 14242
[Cohen] p. 301	Property 4	relogexp 14229
[Cohen] p. 301	Property 1a	log1 14223
[Cohen] p. 301	Property 1b	loge 14224
[Cohen4] p. 348	Observation	relogbcxpbap 14319
[Cohen4] p. 352	Definition	rpelogb 14303
[Cohen4] p. 361	Property 2	rprelogbmul 14309
[Cohen4] p. 361	Property 3	logbrec 14314  rprelogbdiv 14311
[Cohen4] p. 361	Property 4	rplogbreexp 14307
[Cohen4] p. 361	Property 6	relogbexpap 14312
[Cohen4] p. 361	Property 1(a)	rplogbid1 14301
[Cohen4] p. 361	Property 1(b)	rplogb1 14302
[Cohen4] p. 367	Property	rplogbchbase 14304
[Cohen4] p. 377	Property 2	logblt 14316
[Crosilla] p.	Axiom 1	ax-ext 2159
[Crosilla] p.	Axiom 2	ax-pr 4209
[Crosilla] p.	Axiom 3	ax-un 4433
[Crosilla] p.	Axiom 4	ax-nul 4129
[Crosilla] p.	Axiom 5	ax-iinf 4587
[Crosilla] p.	Axiom 6	ru 2961
[Crosilla] p.	Axiom 8	ax-pow 4174
[Crosilla] p.	Axiom 9	ax-setind 4536
[Crosilla], p.	Axiom 6	ax-sep 4121
[Crosilla], p.	Axiom 7	ax-coll 4118
[Crosilla], p.	Axiom 7'	repizf 4119
[Crosilla], p.	Theorem is stated	ordtriexmid 4520
[Crosilla], p.	Axiom of choice implies instances	acexmid 5873
[Crosilla], p.	Definition of ordinal	df-iord 4366
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4534
[Eisenberg] p. 67	Definition 5.3	df-dif 3131
[Eisenberg] p. 82	Definition 6.3	df-iom 4590
[Eisenberg] p. 125	Definition 8.21	df-map 6649
[Enderton] p. 18	Axiom of Empty Set	axnul 4128
[Enderton] p. 19	Definition	df-tp 3600
[Enderton] p. 26	Exercise 5	unissb 3839
[Enderton] p. 26	Exercise 10	pwel 4218
[Enderton] p. 28	Exercise 7(b)	pwunim 4286
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3956  iinin2m 3955  iunin1 3951  iunin2 3950
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3954  iundif2ss 3952
[Enderton] p. 33	Exercise 23	iinuniss 3969
[Enderton] p. 33	Exercise 25	iununir 3970
[Enderton] p. 33	Exercise 24(a)	iinpw 3977
[Enderton] p. 33	Exercise 24(b)	iunpw 4480  iunpwss 3978
[Enderton] p. 38	Exercise 6(a)	unipw 4217
[Enderton] p. 38	Exercise 6(b)	pwuni 4192
[Enderton] p. 41	Lemma 3D	opeluu 4450  rnex 4894  rnexg 4892
[Enderton] p. 41	Exercise 8	dmuni 4837  rnuni 5040
[Enderton] p. 42	Definition of a function	dffun7 5243  dffun8 5244
[Enderton] p. 43	Definition of function value	funfvdm2 5580
[Enderton] p. 43	Definition of single-rooted	funcnv 5277
[Enderton] p. 44	Definition (d)	dfima2 4972  dfima3 4973
[Enderton] p. 47	Theorem 3H	fvco2 5585
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7204
[Enderton] p. 50	Theorem 3K(a)	imauni 5761
[Enderton] p. 52	Definition	df-map 6649
[Enderton] p. 53	Exercise 21	coass 5147
[Enderton] p. 53	Exercise 27	dmco 5137
[Enderton] p. 53	Exercise 14(a)	funin 5287
[Enderton] p. 53	Exercise 22(a)	imass2 5004
[Enderton] p. 54	Remark	ixpf 6719  ixpssmap 6731
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6698
[Enderton] p. 56	Theorem 3M	erref 6554
[Enderton] p. 57	Lemma 3N	erthi 6580
[Enderton] p. 57	Definition	df-ec 6536
[Enderton] p. 58	Definition	df-qs 6540
[Enderton] p. 60	Theorem 3Q	th3q 6639  th3qcor 6638  th3qlem1 6636  th3qlem2 6637
[Enderton] p. 61	Exercise 35	df-ec 6536
[Enderton] p. 65	Exercise 56(a)	dmun 4834
[Enderton] p. 68	Definition of successor	df-suc 4371
[Enderton] p. 71	Definition	df-tr 4102  dftr4 4106
[Enderton] p. 72	Theorem 4E	unisuc 4413  unisucg 4414
[Enderton] p. 73	Exercise 6	unisuc 4413  unisucg 4414
[Enderton] p. 73	Exercise 5(a)	truni 4115
[Enderton] p. 73	Exercise 5(b)	trint 4116
[Enderton] p. 79	Theorem 4I(A1)	nna0 6474
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6476  onasuc 6466
[Enderton] p. 79	Definition of operation value	df-ov 5877
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6475
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6477  onmsuc 6473
[Enderton] p. 81	Theorem 4K(1)	nnaass 6485
[Enderton] p. 81	Theorem 4K(2)	nna0r 6478  nnacom 6484
[Enderton] p. 81	Theorem 4K(3)	nndi 6486
[Enderton] p. 81	Theorem 4K(4)	nnmass 6487
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6489
[Enderton] p. 82	Exercise 16	nnm0r 6479  nnmsucr 6488
[Enderton] p. 88	Exercise 23	nnaordex 6528
[Enderton] p. 129	Definition	df-en 6740
[Enderton] p. 132	Theorem 6B(b)	canth 5828
[Enderton] p. 133	Exercise 1	xpomen 12395
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6864
[Enderton] p. 136	Corollary 6E	nneneq 6856
[Enderton] p. 139	Theorem 6H(c)	mapen 6845
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7216
[Enderton] p. 143	Theorem 6J	dju0en 7212  dju1en 7211
[Enderton] p. 144	Corollary 6K	undif2ss 3498
[Enderton] p. 145	Figure 38	ffoss 5493
[Enderton] p. 145	Definition	df-dom 6741
[Enderton] p. 146	Example 1	domen 6750  domeng 6751
[Enderton] p. 146	Example 3	nndomo 6863
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6834  xpdom1g 6832  xpdom2g 6831
[Enderton] p. 168	Definition	df-po 4296
[Enderton] p. 192	Theorem 7M(a)	oneli 4428
[Enderton] p. 192	Theorem 7M(b)	ontr1 4389
[Enderton] p. 192	Theorem 7M(c)	onirri 4542
[Enderton] p. 193	Corollary 7N(b)	0elon 4392
[Enderton] p. 193	Corollary 7N(c)	onsuci 4515
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4488
[Enderton] p. 194	Remark	onprc 4551
[Enderton] p. 194	Exercise 16	suc11 4557
[Enderton] p. 197	Definition	df-card 7178
[Enderton] p. 200	Exercise 25	tfis 4582
[Enderton] p. 206	Theorem 7X(b)	en2lp 4553
[Enderton] p. 207	Exercise 34	opthreg 4555
[Enderton] p. 208	Exercise 35	suc11g 4556
[Geuvers], p. 1	Remark	expap0 10549
[Geuvers], p. 6	Lemma 2.13	mulap0r 8571
[Geuvers], p. 6	Lemma 2.15	mulap0 8610
[Geuvers], p. 9	Lemma 2.35	msqge0 8572
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7929
[Geuvers], p. 10	Lemma 3.9	maxcom 11211
[Geuvers], p. 10	Lemma 3.10	maxle1 11219  maxle2 11220
[Geuvers], p. 10	Lemma 3.11	maxleast 11221
[Geuvers], p. 10	Lemma 3.12	maxleb 11224
[Geuvers], p. 11	Definition 3.13	dfabsmax 11225
[Geuvers], p. 17	Definition 6.1	df-ap 8538
[Gleason] p. 117	Proposition 9-2.1	df-enq 7345  enqer 7356
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7349  df-nqqs 7346
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7342  df-plqqs 7347
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7343  df-mqqs 7348
[Gleason] p. 119	Proposition 9-2.5	df-rq 7350
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7406
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7409  ltbtwnnq 7414  ltbtwnnqq 7413
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7398
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7399
[Gleason] p. 123	Proposition 9-3.5	addclpr 7535
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7577
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7576
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7595
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7611
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7617  ltaprlem 7616
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7614
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7570
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7590
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7579
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7578
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7586
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7636
[Gleason] p. 126	Proposition 9-4.1	df-enr 7724  enrer 7733
[Gleason] p. 126	Proposition 9-4.2	df-0r 7729  df-1r 7730  df-nr 7725
[Gleason] p. 126	Proposition 9-4.3	df-mr 7727  df-plr 7726  negexsr 7770  recexsrlem 7772
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7728
[Gleason] p. 130	Proposition 10-1.3	creui 8916  creur 8915  cru 8558
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7921  axcnre 7879
[Gleason] p. 132	Definition 10-3.1	crim 10866  crimd 10985  crimi 10945  crre 10865  crred 10984  crrei 10944
[Gleason] p. 132	Definition 10-3.2	remim 10868  remimd 10950
[Gleason] p. 133	Definition 10.36	absval2 11065  absval2d 11193  absval2i 11152
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10892  cjaddd 10973  cjaddi 10940
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10893  cjmuld 10974  cjmuli 10941
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10891  cjcjd 10951  cjcji 10923
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10890  cjreb 10874  cjrebd 10954  cjrebi 10926  cjred 10979  rere 10873  rereb 10871  rerebd 10953  rerebi 10925  rered 10977
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10899  addcjd 10965  addcji 10935
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11009
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11060  abscjd 11198  abscji 11156
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11072  abs00d 11194  abs00i 11153  absne0d 11195
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11104  releabsd 11199  releabsi 11157
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11077  absmuld 11202  absmuli 11159
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11063  sqabsaddi 11160
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11112  abstrid 11204  abstrii 11163
[Gleason] p. 134	Definition 10-4.1	df-exp 10519  exp0 10523  expp1 10526  expp1d 10654
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10561  expaddd 10655
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 14269  cxpmuld 14292  expmul 10564  expmuld 10656
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10558  mulexpd 10668  rpmulcxp 14266
[Gleason] p. 141	Definition 11-2.1	fzval 10009
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11333
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11335
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11334
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11338
[Gleason] p. 172	Corollary 12-2.5	climrecl 11331
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11327  climcj 11328  climim 11330  climre 11329
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7996  df-xr 7995  ltxr 9774
[Gleason] p. 180	Theorem 12-5.3	climcau 11354
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10299
[Gleason] p. 223	Definition 14-1.1	df-met 13385
[Gleason] p. 223	Definition 14-1.1(a)	met0 13800  xmet0 13799
[Gleason] p. 223	Definition 14-1.1(c)	metsym 13807
[Gleason] p. 223	Definition 14-1.1(d)	mettri 13809  mstri 13909  xmettri 13808  xmstri 13908
[Gleason] p. 230	Proposition 14-2.6	txlm 13715
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13947
[Gleason] p. 243	Proposition 14-4.16	addcn2 11317  addcncntop 13988  mulcn2 11319  mulcncntop 13990  subcn2 11318  subcncntop 13989
[Gleason] p. 295	Remark	bcval3 10730  bcval4 10731
[Gleason] p. 295	Equation 2	bcpasc 10745
[Gleason] p. 295	Definition of binomial coefficient	bcval 10728  df-bc 10727
[Gleason] p. 296	Remark	bcn0 10734  bcnn 10736
[Gleason] p. 296	Theorem 15-2.8	binom 11491
[Gleason] p. 308	Equation 2	ef0 11679
[Gleason] p. 308	Equation 3	efcj 11680
[Gleason] p. 309	Corollary 15-4.3	efne0 11685
[Gleason] p. 309	Corollary 15-4.4	efexp 11689
[Gleason] p. 310	Equation 14	sinadd 11743
[Gleason] p. 310	Equation 15	cosadd 11744
[Gleason] p. 311	Equation 17	sincossq 11755
[Gleason] p. 311	Equation 18	cosbnd 11760  sinbnd 11759
[Gleason] p. 311	Definition of ` `	df-pi 11660
[Golan] p. 1	Remark	srgisid 13167
[Golan] p. 1	Definition	df-srg 13145
[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 12887  mndideu 12826
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 12910
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 12936
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 12947
[Herstein] p. 57	Exercise 1	dfgrp3me 12969
[Heyting] p. 127	Axiom #1	ax1hfs 14757
[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 7223
[HoTT], p.	Theorem 7.2.6	nndceq 6499
[HoTT], p.	Exercise 11.10	neapmkv 14751
[HoTT], p.	Exercise 11.11	mulap0bd 8613
[HoTT], p.	Section 11.2.1	df-iltp 7468  df-imp 7467  df-iplp 7466  df-reap 8531
[HoTT], p.	Theorem 11.2.4	recapb 8627  rerecapb 8799
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7660
[HoTT], p.	Corollary 11.4.3	conventions 14409
[HoTT], p.	Exercise 11.6(i)	dcapnconst 14744  dceqnconst 14743
[HoTT], p.	Corollary 11.2.13	axcaucvg 7898  caucvgpr 7680  caucvgprpr 7710  caucvgsr 7800
[HoTT], p.	Definition 11.2.1	df-inp 7464
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 14749
[HoTT], p.	Proposition 11.2.3	df-iso 4297  ltpopr 7593  ltsopr 7594
[HoTT], p.	Definition 11.2.7(v)	apsym 8562  reapcotr 8554  reapirr 8533
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8083  gt0add 8529  leadd1 8386  lelttr 8045  lemul1a 8814  lenlt 8032  ltadd1 8385  ltletr 8046  ltmul1 8548  reaplt 8544
[Jech] p. 4	Definition of class	cv 1352  cvjust 2172
[Jech] p. 78	Note	opthprc 4677
[KalishMontague] p. 81	Note 1	ax-i9 1530
[Kreyszig] p. 3	Property M1	metcl 13789  xmetcl 13788
[Kreyszig] p. 4	Property M2	meteq0 13796
[Kreyszig] p. 12	Equation 5	muleqadd 8624
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13878
[Kreyszig] p. 19	Remark	mopntopon 13879
[Kreyszig] p. 19	Theorem T1	mopn0 13924  mopnm 13884
[Kreyszig] p. 19	Theorem T2	unimopn 13922
[Kreyszig] p. 19	Definition of neighborhood	neibl 13927
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13949
[Kreyszig] p. 25	Definition 1.4-1	lmbr 13649
[Kunen] p. 10	Axiom 0	a9e 1696
[Kunen] p. 12	Axiom 6	zfrep6 4120
[Kunen] p. 24	Definition 10.24	mapval 6659  mapvalg 6657
[Kunen] p. 31	Definition 10.24	mapex 6653
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3896
[Lang] p. 3	Statement	lidrideqd 12799  mndbn0 12831
[Lang] p. 3	Definition	df-mnd 12817
[Lang] p. 7	Definition	dfgrp2e 12902
[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 4476
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3808
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4282
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4283
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4284
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3829
[Mendelson] p. 235	Exercise 4.12(p)	reli 4756
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5149
[Mendelson] p. 246	Definition of successor	df-suc 4371
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6844
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6820  xpsneng 6821
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6826  xpcomeng 6827
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6829
[Mendelson] p. 255	Exercise 4.39	endisj 6823
[Mendelson] p. 255	Exercise 4.41	mapprc 6651
[Mendelson] p. 255	Exercise 4.43	mapsnen 6810
[Mendelson] p. 255	Exercise 4.47	xpmapen 6849
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6685
[Mendelson] p. 255	Exercise 4.42(b)	map1 6811
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7215  djucomen 7214
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7213
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6467
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3357
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4714
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4715
[Monk1] p. 34	Definition 3.3	df-opab 4065
[Monk1] p. 36	Theorem 3.7(i)	coi1 5144  coi2 5145
[Monk1] p. 36	Theorem 3.8(v)	dm0 4841  rn0 4883
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5033
[Monk1] p. 37	Theorem 3.13(i)	relxp 4735
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4847  rnxpm 5058
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4706  xp0 5048
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4987
[Monk1] p. 38	Theorem 3.16(viii)	imai 4984
[Monk1] p. 39	Theorem 3.17	imaex 4983  imaexg 4982
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4981
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5646  funfvop 5628
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5559
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5567
[Monk1] p. 43	Theorem 4.6	funun 5260
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5768  dff13f 5770
[Monk1] p. 46	Theorem 4.15(v)	funex 5739  funrnex 6114
[Monk1] p. 50	Definition 5.4	fniunfv 5762
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5112
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3860
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6155  df-1st 6140
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6156  df-2nd 6141
[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 4243
[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 14758
[Munkres] p. 77	Example 2	distop 13521
[Munkres] p. 78	Definition of basis	df-bases 13479  isbasis3g 13482
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12708  tgval2 13487
[Munkres] p. 79	Remark	tgcl 13500
[Munkres] p. 80	Lemma 2.1	tgval3 13494
[Munkres] p. 80	Lemma 2.2	tgss2 13515  tgss3 13514
[Munkres] p. 81	Lemma 2.3	basgen 13516  basgen2 13517
[Munkres] p. 89	Definition of subspace topology	resttop 13606
[Munkres] p. 93	Theorem 6.1(1)	0cld 13548  topcld 13545
[Munkres] p. 93	Theorem 6.1(3)	uncld 13549
[Munkres] p. 94	Definition of closure	clsval 13547
[Munkres] p. 94	Definition of interior	ntrval 13546
[Munkres] p. 102	Definition of continuous function	df-cn 13624  iscn 13633  iscn2 13636
[Munkres] p. 107	Theorem 7.2(g)	cncnp 13666  cncnp2m 13667  cncnpi 13664  df-cnp 13625  iscnp 13635
[Munkres] p. 127	Theorem 10.1	metcn 13950
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6902
[Pierik], p. 9	Definition 2.4	df-womni 7161
[Pierik], p. 9	Definition 2.5	df-markov 7149  omniwomnimkv 7164
[Pierik], p. 10	Section 2.3	dfdif3 3245
[Pierik], p. 14	Definition 3.1	df-omni 7132  exmidomniim 7138  finomni 7137
[Pierik], p. 15	Section 3.1	df-nninf 7118
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 14707
[PradicBrown2022], p. 2	Remark	exmidpw 6907
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7199
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7200  exmidfodomrlemrALT 7201
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7146
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 14692  peano4nninf 14691
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 14694
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 14702
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 14704
[PradicBrown2022], p. 5	Definition 3.3	nnsf 14690
[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 3657
[Quine] p. 48	Definition 7.1	df-pr 3599  df-sn 3598
[Quine] p. 49	Theorem 7.4	snss 3727  snssg 3726
[Quine] p. 49	Theorem 7.5	prss 3748  prssg 3749
[Quine] p. 49	Theorem 7.6	prid1 3698  prid1g 3696  prid2 3699  prid2g 3697  snid 3623  snidg 3621
[Quine] p. 51	Theorem 7.12	snexg 4184  snexprc 4186
[Quine] p. 51	Theorem 7.13	prexg 4211
[Quine] p. 53	Theorem 8.2	unisn 3825  unisng 3826
[Quine] p. 53	Theorem 8.3	uniun 3828
[Quine] p. 54	Theorem 8.6	elssuni 3837
[Quine] p. 54	Theorem 8.7	uni0 3836
[Quine] p. 56	Theorem 8.17	uniabio 5188
[Quine] p. 56	Definition 8.18	dfiota2 5179
[Quine] p. 57	Theorem 8.19	iotaval 5189
[Quine] p. 57	Theorem 8.22	iotanul 5193
[Quine] p. 58	Theorem 8.23	euiotaex 5194
[Quine] p. 58	Definition 9.1	df-op 3601
[Quine] p. 61	Theorem 9.5	opabid 4257  opelopab 4271  opelopaba 4266  opelopabaf 4273  opelopabf 4274  opelopabg 4268  opelopabga 4263  oprabid 5906
[Quine] p. 64	Definition 9.11	df-xp 4632
[Quine] p. 64	Definition 9.12	df-cnv 4634
[Quine] p. 64	Definition 9.15	df-id 4293
[Quine] p. 65	Theorem 10.3	fun0 5274
[Quine] p. 65	Theorem 10.4	funi 5248
[Quine] p. 65	Theorem 10.5	funsn 5264  funsng 5262
[Quine] p. 65	Definition 10.1	df-fun 5218
[Quine] p. 65	Definition 10.2	args 4997  dffv4g 5512
[Quine] p. 68	Definition 10.11	df-fv 5224  fv2 5510
[Quine] p. 124	Theorem 17.3	nn0opth2 10703  nn0opth2d 10702  nn0opthd 10701
[Quine] p. 284	Axiom 39(vi)	funimaex 5301  funimaexg 5300
[Roman] p. 19	Part Preliminaries	df-ring 13179
[Rudin] p. 164	Equation 27	efcan 11683
[Rudin] p. 164	Equation 30	efzval 11690
[Rudin] p. 167	Equation 48	absefi 11775
[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 5013
[Schechter] p. 51	Definition of irreflexivity	intirr 5015
[Schechter] p. 51	Definition of symmetry	cnvsym 5012
[Schechter] p. 51	Definition of transitivity	cotr 5010
[Schechter] p. 187	Definition of "ring with unit"	isring 13181
[Schechter] p. 428	Definition 15.35	bastop1 13519
[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 3602
[Stoll] p. 43	Definition	uniiun 3940
[Stoll] p. 44	Definition	intiin 3941
[Stoll] p. 45	Definition	df-iin 3889
[Stoll] p. 45	Definition indexed union	df-iun 3888
[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 4133
[Suppes] p. 39	Theorem 61	uniss 3830
[Suppes] p. 39	Theorem 65	uniop 4255
[Suppes] p. 41	Theorem 70	intsn 3879
[Suppes] p. 42	Theorem 71	intpr 3876  intprg 3877
[Suppes] p. 42	Theorem 73	op1stb 4478  op1stbg 4479
[Suppes] p. 42	Theorem 78	intun 3875
[Suppes] p. 44	Definition 15(a)	dfiun2 3920  dfiun2g 3918
[Suppes] p. 44	Definition 15(b)	dfiin2 3921
[Suppes] p. 47	Theorem 86	elpw 3581  elpw2 4157  elpw2g 4156  elpwg 3583
[Suppes] p. 47	Theorem 87	pwid 3590
[Suppes] p. 47	Theorem 89	pw0 3739
[Suppes] p. 48	Theorem 90	pwpw0ss 3804
[Suppes] p. 52	Theorem 101	xpss12 4733
[Suppes] p. 52	Theorem 102	xpindi 4762  xpindir 4763
[Suppes] p. 52	Theorem 103	xpundi 4682  xpundir 4683
[Suppes] p. 54	Theorem 105	elirrv 4547
[Suppes] p. 58	Theorem 2	relss 4713
[Suppes] p. 59	Theorem 4	eldm 4824  eldm2 4825  eldm2g 4823  eldmg 4822
[Suppes] p. 59	Definition 3	df-dm 4636
[Suppes] p. 60	Theorem 6	dmin 4835
[Suppes] p. 60	Theorem 8	rnun 5037
[Suppes] p. 60	Theorem 9	rnin 5038
[Suppes] p. 60	Definition 4	dfrn2 4815
[Suppes] p. 61	Theorem 11	brcnv 4810  brcnvg 4808
[Suppes] p. 62	Equation 5	elcnv 4804  elcnv2 4805
[Suppes] p. 62	Theorem 12	relcnv 5006
[Suppes] p. 62	Theorem 15	cnvin 5036
[Suppes] p. 62	Theorem 16	cnvun 5034
[Suppes] p. 63	Theorem 20	co02 5142
[Suppes] p. 63	Theorem 21	dmcoss 4896
[Suppes] p. 63	Definition 7	df-co 4635
[Suppes] p. 64	Theorem 26	cnvco 4812
[Suppes] p. 64	Theorem 27	coass 5147
[Suppes] p. 65	Theorem 31	resundi 4920
[Suppes] p. 65	Theorem 34	elima 4975  elima2 4976  elima3 4977  elimag 4974
[Suppes] p. 65	Theorem 35	imaundi 5041
[Suppes] p. 66	Theorem 40	dminss 5043
[Suppes] p. 66	Theorem 41	imainss 5044
[Suppes] p. 67	Exercise 11	cnvxp 5047
[Suppes] p. 81	Definition 34	dfec2 6537
[Suppes] p. 82	Theorem 72	elec 6573  elecg 6572
[Suppes] p. 82	Theorem 73	erth 6578  erth2 6579
[Suppes] p. 89	Theorem 96	map0b 6686
[Suppes] p. 89	Theorem 97	map0 6688  map0g 6687
[Suppes] p. 89	Theorem 98	mapsn 6689
[Suppes] p. 89	Theorem 99	mapss 6690
[Suppes] p. 92	Theorem 1	enref 6764  enrefg 6763
[Suppes] p. 92	Theorem 2	ensym 6780  ensymb 6779  ensymi 6781
[Suppes] p. 92	Theorem 3	entr 6783
[Suppes] p. 92	Theorem 4	unen 6815
[Suppes] p. 94	Theorem 15	endom 6762
[Suppes] p. 94	Theorem 16	ssdomg 6777
[Suppes] p. 94	Theorem 17	domtr 6784
[Suppes] p. 95	Theorem 18	isbth 6965
[Suppes] p. 98	Exercise 4	fundmen 6805  fundmeng 6806
[Suppes] p. 98	Exercise 6	xpdom3m 6833
[Suppes] p. 130	Definition 3	df-tr 4102
[Suppes] p. 132	Theorem 9	ssonuni 4487
[Suppes] p. 134	Definition 6	df-suc 4371
[Suppes] p. 136	Theorem Schema 22	findes 4602  finds 4599  finds1 4601  finds2 4600
[Suppes] p. 162	Definition 5	df-ltnqqs 7351  df-ltpq 7344
[Suppes] p. 228	Theorem Schema 61	onintss 4390
[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 5878
[TakeutiZaring] p. 14	Proposition 4.14	ru 2961
[TakeutiZaring] p. 15	Exercise 1	elpr 3613  elpr2 3614  elprg 3612
[TakeutiZaring] p. 15	Exercise 2	elsn 3608  elsn2 3626  elsn2g 3625  elsng 3607  velsn 3609
[TakeutiZaring] p. 15	Exercise 3	elop 4231
[TakeutiZaring] p. 15	Exercise 4	sneq 3603  sneqr 3760
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3611  dfsn2 3606
[TakeutiZaring] p. 16	Axiom 3	uniex 4437
[TakeutiZaring] p. 16	Exercise 6	opth 4237
[TakeutiZaring] p. 16	Exercise 8	rext 4215
[TakeutiZaring] p. 16	Corollary 5.8	unex 4441  unexg 4443
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3641
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3810
[TakeutiZaring] p. 16	Definition 5.6	df-in 3135  df-un 3133
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3823  uniprg 3824
[TakeutiZaring] p. 17	Axiom 4	vpwex 4179
[TakeutiZaring] p. 17	Exercise 1	eltp 3640
[TakeutiZaring] p. 17	Exercise 5	elsuc 4406  elsucg 4404  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 3577
[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 3818
[TakeutiZaring] p. 18	Exercise 18	sspwb 4216
[TakeutiZaring] p. 18	Exercise 19	pweqb 4223
[TakeutiZaring] p. 20	Definition	df-rab 2464
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4130
[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 4538
[TakeutiZaring] p. 21	Definition 5.20	df-v 2739
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4135
[TakeutiZaring] p. 22	Exercise 1	0ss 3461
[TakeutiZaring] p. 22	Exercise 3	ssex 4140  ssexg 4142
[TakeutiZaring] p. 22	Exercise 4	inex1 4137
[TakeutiZaring] p. 22	Exercise 5	ruv 4549
[TakeutiZaring] p. 22	Exercise 6	elirr 4540
[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 4741  xpexg 4740  xpexgALT 6133
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4633
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5280
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5432  fun11 5283
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5227  svrelfun 5281
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4814
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4816
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4638
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4639
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4635
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5083  dfrel2 5079
[TakeutiZaring] p. 25	Exercise 3	xpss 4734
[TakeutiZaring] p. 25	Exercise 5	relun 4743
[TakeutiZaring] p. 25	Exercise 6	reluni 4749
[TakeutiZaring] p. 25	Exercise 9	inxp 4761
[TakeutiZaring] p. 25	Exercise 12	relres 4935
[TakeutiZaring] p. 25	Exercise 13	opelres 4912  opelresg 4914
[TakeutiZaring] p. 25	Exercise 14	dmres 4928
[TakeutiZaring] p. 25	Exercise 15	resss 4931
[TakeutiZaring] p. 25	Exercise 17	resabs1 4936
[TakeutiZaring] p. 25	Exercise 18	funres 5257
[TakeutiZaring] p. 25	Exercise 24	relco 5127
[TakeutiZaring] p. 25	Exercise 29	funco 5256
[TakeutiZaring] p. 25	Exercise 30	f1co 5433
[TakeutiZaring] p. 26	Definition 6.10	eu2 2070
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5224  fv3 5538
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5167  cnvexg 5166
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4893  dmexg 4891
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4894  rnexg 4892
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5532
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5542  tz6.12 5543  tz6.12c 5545
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5506
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5219
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5220
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5222  wfo 5214
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5221  wf1 5213
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5223  wf1o 5215
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5613  eqfnfv2 5614  eqfnfv2f 5617
[TakeutiZaring] p. 28	Exercise 5	fvco 5586
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5738  fnexALT 6111
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5737  resfunexgALT 6108
[TakeutiZaring] p. 29	Exercise 9	funimaex 5301  funimaexg 5300
[TakeutiZaring] p. 29	Definition 6.18	df-br 4004
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4998  iniseg 5000
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4289
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5225
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5810
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5811
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5816
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5818
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5826
[TakeutiZaring] p. 35	Notation	wtr 4101
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4354
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4105
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4575
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4381
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4385
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4491
[TakeutiZaring] p. 38	Definition 7.11	df-on 4368
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4485
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4551
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4581
[TakeutiZaring] p. 40	Exercise 7	dftr2 4103
[TakeutiZaring] p. 40	Exercise 11	unon 4510
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4486
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3837
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4371
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4415  sucidg 4416
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4500
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4369
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4505  ordelsuc 4504
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4593
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4594
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4595
[TakeutiZaring] p. 43	Axiom 7	omex 4592
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4606
[TakeutiZaring] p. 43	Corollary 7.31	find 4598
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4596
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4597
[TakeutiZaring] p. 44	Exercise 2	int0 3858
[TakeutiZaring] p. 44	Exercise 3	trintssm 4117
[TakeutiZaring] p. 44	Exercise 4	intss1 3859
[TakeutiZaring] p. 44	Exercise 6	onintonm 4516
[TakeutiZaring] p. 44	Definition 7.35	df-int 3845
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6308
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6365  tfri1d 6335
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6366  tfri2d 6336
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6367
[TakeutiZaring] p. 50	Exercise 3	smoiso 6302
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6286
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6464
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6460
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6457
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6461
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6509  nnaordi 6508
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3931  uniss2 3840
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6470
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6480
[TakeutiZaring] p. 62	Exercise 5	oaword1 6471
[TakeutiZaring] p. 62	Definition 8.15	om0 6458  omsuc 6472
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6481
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6517  nnmordi 6516
[TakeutiZaring] p. 67	Definition 8.30	oei0 6459
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7185
[TakeutiZaring] p. 88	Exercise 1	en0 6794
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6856
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6857
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6742  isfi 6760
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6830
[TakeutiZaring] p. 95	Definition 10.42	df-map 6649
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6847
[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 5196
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5197
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2105  eupickbi 2108
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5224
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7188