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 7116  fidcenum 6957
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6957
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7116
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12428
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6931
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6919
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12443
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12445
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12434  znnen 12401
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12446
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12447
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10758
[AczelRathjen], p. 183	Chapter 20	ax-setind 4538
[Apostol] p. 18	Theorem I.1	addcan 8139  addcan2d 8144  addcan2i 8142  addcand 8143  addcani 8141
[Apostol] p. 18	Theorem I.2	negeu 8150
[Apostol] p. 18	Theorem I.3	negsub 8207  negsubd 8276  negsubi 8237
[Apostol] p. 18	Theorem I.4	negneg 8209  negnegd 8261  negnegi 8229
[Apostol] p. 18	Theorem I.5	subdi 8344  subdid 8373  subdii 8366  subdir 8345  subdird 8374  subdiri 8367
[Apostol] p. 18	Theorem I.6	mul01 8348  mul01d 8352  mul01i 8350  mul02 8346  mul02d 8351  mul02i 8349
[Apostol] p. 18	Theorem I.9	divrecapd 8752
[Apostol] p. 18	Theorem I.10	recrecapi 8703
[Apostol] p. 18	Theorem I.12	mul2neg 8357  mul2negd 8372  mul2negi 8365  mulneg1 8354  mulneg1d 8370  mulneg1i 8363
[Apostol] p. 18	Theorem I.14	rdivmuldivd 13318
[Apostol] p. 18	Theorem I.15	divdivdivap 8672
[Apostol] p. 20	Axiom 7	rpaddcl 9679  rpaddcld 9714  rpmulcl 9680  rpmulcld 9715
[Apostol] p. 20	Axiom 9	0nrp 9691
[Apostol] p. 20	Theorem I.17	lttri 8064
[Apostol] p. 20	Theorem I.18	ltadd1d 8497  ltadd1dd 8515  ltadd1i 8461
[Apostol] p. 20	Theorem I.19	ltmul1 8551  ltmul1a 8550  ltmul1i 8879  ltmul1ii 8887  ltmul2 8815  ltmul2d 9741  ltmul2dd 9755  ltmul2i 8882
[Apostol] p. 20	Theorem I.21	0lt1 8086
[Apostol] p. 20	Theorem I.23	lt0neg1 8427  lt0neg1d 8474  ltneg 8421  ltnegd 8482  ltnegi 8452
[Apostol] p. 20	Theorem I.25	lt2add 8404  lt2addd 8526  lt2addi 8469
[Apostol] p. 20	Definition of positive numbers	df-rp 9656
[Apostol] p. 21	Exercise 4	recgt0 8809  recgt0d 8893  recgt0i 8865  recgt0ii 8866
[Apostol] p. 22	Definition of integers	df-z 9256
[Apostol] p. 22	Definition of rationals	df-q 9622
[Apostol] p. 24	Theorem I.26	supeuti 6995
[Apostol] p. 26	Theorem I.29	arch 9175
[Apostol] p. 28	Exercise 2	btwnz 9374
[Apostol] p. 28	Exercise 3	nnrecl 9176
[Apostol] p. 28	Exercise 6	qbtwnre 10259
[Apostol] p. 28	Exercise 10(a)	zeneo 11878  zneo 9356
[Apostol] p. 29	Theorem I.35	resqrtth 11042  sqrtthi 11130
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8924
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12039
[Apostol] p. 363	Remark	absgt0api 11157
[Apostol] p. 363	Example	abssubd 11204  abssubi 11161
[ApostolNT] p. 14	Definition	df-dvds 11797
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11813
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11837
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11833
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11827
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11829
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11814
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11815
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11820
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11853
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11855
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11857
[ApostolNT] p. 15	Definition	dfgcd2 12017
[ApostolNT] p. 16	Definition	isprm2 12119
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12094
[ApostolNT] p. 16	Theorem 1.7	prminf 12458
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11976
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12018
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12020
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11990
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11983
[ApostolNT] p. 17	Theorem 1.8	coprm 12146
[ApostolNT] p. 17	Theorem 1.9	euclemma 12148
[ApostolNT] p. 17	Theorem 1.10	1arith2 12368
[ApostolNT] p. 19	Theorem 1.14	divalg 11931
[ApostolNT] p. 20	Theorem 1.15	eucalg 12061
[ApostolNT] p. 25	Definition	df-phi 12213
[ApostolNT] p. 26	Theorem 2.2	phisum 12242
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12224
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12228
[ApostolNT] p. 104	Definition	congr 12102
[ApostolNT] p. 106	Remark	dvdsval3 11800
[ApostolNT] p. 106	Definition	moddvds 11808
[ApostolNT] p. 107	Example 2	mod2eq0even 11885
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11886
[ApostolNT] p. 107	Example 4	zmod1congr 10343
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10380
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10649
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11832
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12105
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12107
[ApostolNT] p. 113	Theorem 5.17	eulerth 12235
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12253
[ApostolNT] p. 114	Theorem 5.19	fermltl 12236
[ApostolNT] p. 179	Definition	df-lgs 14438  lgsprme0 14482
[ApostolNT] p. 180	Example 1	1lgs 14483
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 14459
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 14474
[ApostolNT] p. 181	Theorem 9.4	m1lgs 14491
[ApostolNT] p. 188	Definition	df-lgs 14438  lgs1 14484
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 14475
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 14477
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 14485
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 14486
[Bauer] p. 482	Section 1.2	pm2.01 616  pm2.65 659
[Bauer] p. 483	Theorem 1.3	acexmid 5876  onsucelsucexmidlem 4530
[Bauer], p. 481	Section 1.1	pwtrufal 14786
[Bauer], p. 483	Definition	n0rf 3437
[Bauer], p. 483	Theorem 1.2	2irrexpq 14433  2irrexpqap 14435
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6878
[Bauer], p. 494	Theorem 5.5	ivthinc 14160
[BauerHanson], p. 27	Proposition 5.2	cnstab 8604
[BauerSwan], p. 14	Remark	0ct 7108  ctm 7110
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 14789
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7116
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7502
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7415
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7504
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7538  addlocpr 7537
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7564
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7567
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7572
[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 4126
[BellMachover] p. 466	Axiom Pow	axpow3 4179
[BellMachover] p. 466	Axiom Union	axun2 4437
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4543
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4386
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4546
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4497
[BellMachover] p. 471	Definition of Lim	df-ilim 4371
[BellMachover] p. 472	Axiom Inf	zfinf2 4590
[BellMachover] p. 473	Theorem 2.8	limom 4615
[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 12780
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 12813
[BourbakiAlg1] p. 12	Definition 2	df-mnd 12823
[BourbakiAlg1] p. 92	Definition 1	df-ring 13186
[BourbakiEns] p.	Proposition 8	fcof1 5786  fcofo 5787
[BourbakiTop1] p.	Remark	xnegmnf 9831  xnegpnf 9830
[BourbakiTop1] p.	Remark	rexneg 9832
[BourbakiTop1] p.	Proposition	ishmeo 13843
[BourbakiTop1] p.	Property V_i	ssnei2 13696
[BourbakiTop1] p.	Property V_ii	innei 13702
[BourbakiTop1] p.	Property V_iv	neissex 13704
[BourbakiTop1] p.	Proposition 1	neipsm 13693  neiss 13689
[BourbakiTop1] p.	Proposition 2	cnptopco 13761
[BourbakiTop1] p.	Proposition 4	imasnopn 13838
[BourbakiTop1] p.	Property V_iii	elnei 13691
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 13537
[Bruck] p. 1	Section I.1	df-mgm 12780
[Bruck] p. 23	Section II.1	df-sgrp 12813
[Bruck] p. 28	Theorem 3.2	dfgrp3m 12974
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4068
[Cohen] p. 301	Remark	relogoprlem 14328
[Cohen] p. 301	Property 2	relogmul 14329  relogmuld 14344
[Cohen] p. 301	Property 3	relogdiv 14330  relogdivd 14345
[Cohen] p. 301	Property 4	relogexp 14332
[Cohen] p. 301	Property 1a	log1 14326
[Cohen] p. 301	Property 1b	loge 14327
[Cohen4] p. 348	Observation	relogbcxpbap 14422
[Cohen4] p. 352	Definition	rpelogb 14406
[Cohen4] p. 361	Property 2	rprelogbmul 14412
[Cohen4] p. 361	Property 3	logbrec 14417  rprelogbdiv 14414
[Cohen4] p. 361	Property 4	rplogbreexp 14410
[Cohen4] p. 361	Property 6	relogbexpap 14415
[Cohen4] p. 361	Property 1(a)	rplogbid1 14404
[Cohen4] p. 361	Property 1(b)	rplogb1 14405
[Cohen4] p. 367	Property	rplogbchbase 14407
[Cohen4] p. 377	Property 2	logblt 14419
[Crosilla] p.	Axiom 1	ax-ext 2159
[Crosilla] p.	Axiom 2	ax-pr 4211
[Crosilla] p.	Axiom 3	ax-un 4435
[Crosilla] p.	Axiom 4	ax-nul 4131
[Crosilla] p.	Axiom 5	ax-iinf 4589
[Crosilla] p.	Axiom 6	ru 2963
[Crosilla] p.	Axiom 8	ax-pow 4176
[Crosilla] p.	Axiom 9	ax-setind 4538
[Crosilla], p.	Axiom 6	ax-sep 4123
[Crosilla], p.	Axiom 7	ax-coll 4120
[Crosilla], p.	Axiom 7'	repizf 4121
[Crosilla], p.	Theorem is stated	ordtriexmid 4522
[Crosilla], p.	Axiom of choice implies instances	acexmid 5876
[Crosilla], p.	Definition of ordinal	df-iord 4368
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4536
[Eisenberg] p. 67	Definition 5.3	df-dif 3133
[Eisenberg] p. 82	Definition 6.3	df-iom 4592
[Eisenberg] p. 125	Definition 8.21	df-map 6652
[Enderton] p. 18	Axiom of Empty Set	axnul 4130
[Enderton] p. 19	Definition	df-tp 3602
[Enderton] p. 26	Exercise 5	unissb 3841
[Enderton] p. 26	Exercise 10	pwel 4220
[Enderton] p. 28	Exercise 7(b)	pwunim 4288
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3958  iinin2m 3957  iunin1 3953  iunin2 3952
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3956  iundif2ss 3954
[Enderton] p. 33	Exercise 23	iinuniss 3971
[Enderton] p. 33	Exercise 25	iununir 3972
[Enderton] p. 33	Exercise 24(a)	iinpw 3979
[Enderton] p. 33	Exercise 24(b)	iunpw 4482  iunpwss 3980
[Enderton] p. 38	Exercise 6(a)	unipw 4219
[Enderton] p. 38	Exercise 6(b)	pwuni 4194
[Enderton] p. 41	Lemma 3D	opeluu 4452  rnex 4896  rnexg 4894
[Enderton] p. 41	Exercise 8	dmuni 4839  rnuni 5042
[Enderton] p. 42	Definition of a function	dffun7 5245  dffun8 5246
[Enderton] p. 43	Definition of function value	funfvdm2 5582
[Enderton] p. 43	Definition of single-rooted	funcnv 5279
[Enderton] p. 44	Definition (d)	dfima2 4974  dfima3 4975
[Enderton] p. 47	Theorem 3H	fvco2 5587
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7207
[Enderton] p. 50	Theorem 3K(a)	imauni 5764
[Enderton] p. 52	Definition	df-map 6652
[Enderton] p. 53	Exercise 21	coass 5149
[Enderton] p. 53	Exercise 27	dmco 5139
[Enderton] p. 53	Exercise 14(a)	funin 5289
[Enderton] p. 53	Exercise 22(a)	imass2 5006
[Enderton] p. 54	Remark	ixpf 6722  ixpssmap 6734
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6701
[Enderton] p. 56	Theorem 3M	erref 6557
[Enderton] p. 57	Lemma 3N	erthi 6583
[Enderton] p. 57	Definition	df-ec 6539
[Enderton] p. 58	Definition	df-qs 6543
[Enderton] p. 60	Theorem 3Q	th3q 6642  th3qcor 6641  th3qlem1 6639  th3qlem2 6640
[Enderton] p. 61	Exercise 35	df-ec 6539
[Enderton] p. 65	Exercise 56(a)	dmun 4836
[Enderton] p. 68	Definition of successor	df-suc 4373
[Enderton] p. 71	Definition	df-tr 4104  dftr4 4108
[Enderton] p. 72	Theorem 4E	unisuc 4415  unisucg 4416
[Enderton] p. 73	Exercise 6	unisuc 4415  unisucg 4416
[Enderton] p. 73	Exercise 5(a)	truni 4117
[Enderton] p. 73	Exercise 5(b)	trint 4118
[Enderton] p. 79	Theorem 4I(A1)	nna0 6477
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6479  onasuc 6469
[Enderton] p. 79	Definition of operation value	df-ov 5880
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6478
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6480  onmsuc 6476
[Enderton] p. 81	Theorem 4K(1)	nnaass 6488
[Enderton] p. 81	Theorem 4K(2)	nna0r 6481  nnacom 6487
[Enderton] p. 81	Theorem 4K(3)	nndi 6489
[Enderton] p. 81	Theorem 4K(4)	nnmass 6490
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6492
[Enderton] p. 82	Exercise 16	nnm0r 6482  nnmsucr 6491
[Enderton] p. 88	Exercise 23	nnaordex 6531
[Enderton] p. 129	Definition	df-en 6743
[Enderton] p. 132	Theorem 6B(b)	canth 5831
[Enderton] p. 133	Exercise 1	xpomen 12398
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6867
[Enderton] p. 136	Corollary 6E	nneneq 6859
[Enderton] p. 139	Theorem 6H(c)	mapen 6848
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7219
[Enderton] p. 143	Theorem 6J	dju0en 7215  dju1en 7214
[Enderton] p. 144	Corollary 6K	undif2ss 3500
[Enderton] p. 145	Figure 38	ffoss 5495
[Enderton] p. 145	Definition	df-dom 6744
[Enderton] p. 146	Example 1	domen 6753  domeng 6754
[Enderton] p. 146	Example 3	nndomo 6866
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6837  xpdom1g 6835  xpdom2g 6834
[Enderton] p. 168	Definition	df-po 4298
[Enderton] p. 192	Theorem 7M(a)	oneli 4430
[Enderton] p. 192	Theorem 7M(b)	ontr1 4391
[Enderton] p. 192	Theorem 7M(c)	onirri 4544
[Enderton] p. 193	Corollary 7N(b)	0elon 4394
[Enderton] p. 193	Corollary 7N(c)	onsuci 4517
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4490
[Enderton] p. 194	Remark	onprc 4553
[Enderton] p. 194	Exercise 16	suc11 4559
[Enderton] p. 197	Definition	df-card 7181
[Enderton] p. 200	Exercise 25	tfis 4584
[Enderton] p. 206	Theorem 7X(b)	en2lp 4555
[Enderton] p. 207	Exercise 34	opthreg 4557
[Enderton] p. 208	Exercise 35	suc11g 4558
[Geuvers], p. 1	Remark	expap0 10552
[Geuvers], p. 6	Lemma 2.13	mulap0r 8574
[Geuvers], p. 6	Lemma 2.15	mulap0 8613
[Geuvers], p. 9	Lemma 2.35	msqge0 8575
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7932
[Geuvers], p. 10	Lemma 3.9	maxcom 11214
[Geuvers], p. 10	Lemma 3.10	maxle1 11222  maxle2 11223
[Geuvers], p. 10	Lemma 3.11	maxleast 11224
[Geuvers], p. 10	Lemma 3.12	maxleb 11227
[Geuvers], p. 11	Definition 3.13	dfabsmax 11228
[Geuvers], p. 17	Definition 6.1	df-ap 8541
[Gleason] p. 117	Proposition 9-2.1	df-enq 7348  enqer 7359
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7352  df-nqqs 7349
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7345  df-plqqs 7350
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7346  df-mqqs 7351
[Gleason] p. 119	Proposition 9-2.5	df-rq 7353
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7409
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7412  ltbtwnnq 7417  ltbtwnnqq 7416
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7401
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7402
[Gleason] p. 123	Proposition 9-3.5	addclpr 7538
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7580
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7579
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7598
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7614
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7620  ltaprlem 7619
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7617
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7573
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7593
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7582
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7581
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7589
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7639
[Gleason] p. 126	Proposition 9-4.1	df-enr 7727  enrer 7736
[Gleason] p. 126	Proposition 9-4.2	df-0r 7732  df-1r 7733  df-nr 7728
[Gleason] p. 126	Proposition 9-4.3	df-mr 7730  df-plr 7729  negexsr 7773  recexsrlem 7775
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7731
[Gleason] p. 130	Proposition 10-1.3	creui 8919  creur 8918  cru 8561
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7924  axcnre 7882
[Gleason] p. 132	Definition 10-3.1	crim 10869  crimd 10988  crimi 10948  crre 10868  crred 10987  crrei 10947
[Gleason] p. 132	Definition 10-3.2	remim 10871  remimd 10953
[Gleason] p. 133	Definition 10.36	absval2 11068  absval2d 11196  absval2i 11155
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10895  cjaddd 10976  cjaddi 10943
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10896  cjmuld 10977  cjmuli 10944
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10894  cjcjd 10954  cjcji 10926
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10893  cjreb 10877  cjrebd 10957  cjrebi 10929  cjred 10982  rere 10876  rereb 10874  rerebd 10956  rerebi 10928  rered 10980
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10902  addcjd 10968  addcji 10938
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11012
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11063  abscjd 11201  abscji 11159
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11075  abs00d 11197  abs00i 11156  absne0d 11198
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11107  releabsd 11202  releabsi 11160
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11080  absmuld 11205  absmuli 11162
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11066  sqabsaddi 11163
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11115  abstrid 11207  abstrii 11166
[Gleason] p. 134	Definition 10-4.1	df-exp 10522  exp0 10526  expp1 10529  expp1d 10657
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10564  expaddd 10658
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 14372  cxpmuld 14395  expmul 10567  expmuld 10659
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10561  mulexpd 10671  rpmulcxp 14369
[Gleason] p. 141	Definition 11-2.1	fzval 10012
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11336
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11338
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11337
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11341
[Gleason] p. 172	Corollary 12-2.5	climrecl 11334
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11330  climcj 11331  climim 11333  climre 11332
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7999  df-xr 7998  ltxr 9777
[Gleason] p. 180	Theorem 12-5.3	climcau 11357
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10302
[Gleason] p. 223	Definition 14-1.1	df-met 13488
[Gleason] p. 223	Definition 14-1.1(a)	met0 13903  xmet0 13902
[Gleason] p. 223	Definition 14-1.1(c)	metsym 13910
[Gleason] p. 223	Definition 14-1.1(d)	mettri 13912  mstri 14012  xmettri 13911  xmstri 14011
[Gleason] p. 230	Proposition 14-2.6	txlm 13818
[Gleason] p. 240	Proposition 14-4.2	metcnp3 14050
[Gleason] p. 243	Proposition 14-4.16	addcn2 11320  addcncntop 14091  mulcn2 11322  mulcncntop 14093  subcn2 11321  subcncntop 14092
[Gleason] p. 295	Remark	bcval3 10733  bcval4 10734
[Gleason] p. 295	Equation 2	bcpasc 10748
[Gleason] p. 295	Definition of binomial coefficient	bcval 10731  df-bc 10730
[Gleason] p. 296	Remark	bcn0 10737  bcnn 10739
[Gleason] p. 296	Theorem 15-2.8	binom 11494
[Gleason] p. 308	Equation 2	ef0 11682
[Gleason] p. 308	Equation 3	efcj 11683
[Gleason] p. 309	Corollary 15-4.3	efne0 11688
[Gleason] p. 309	Corollary 15-4.4	efexp 11692
[Gleason] p. 310	Equation 14	sinadd 11746
[Gleason] p. 310	Equation 15	cosadd 11747
[Gleason] p. 311	Equation 17	sincossq 11758
[Gleason] p. 311	Equation 18	cosbnd 11763  sinbnd 11762
[Gleason] p. 311	Definition of ` `	df-pi 11663
[Golan] p. 1	Remark	srgisid 13174
[Golan] p. 1	Definition	df-srg 13152
[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 12893  mndideu 12832
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 12916
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 12942
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 12953
[Herstein] p. 57	Exercise 1	dfgrp3me 12975
[Heyting] p. 127	Axiom #1	ax1hfs 14861
[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 7226
[HoTT], p.	Theorem 7.2.6	nndceq 6502
[HoTT], p.	Exercise 11.10	neapmkv 14855
[HoTT], p.	Exercise 11.11	mulap0bd 8616
[HoTT], p.	Section 11.2.1	df-iltp 7471  df-imp 7470  df-iplp 7469  df-reap 8534
[HoTT], p.	Theorem 11.2.4	recapb 8630  rerecapb 8802
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7663
[HoTT], p.	Corollary 11.4.3	conventions 14512
[HoTT], p.	Exercise 11.6(i)	dcapnconst 14848  dceqnconst 14847
[HoTT], p.	Corollary 11.2.13	axcaucvg 7901  caucvgpr 7683  caucvgprpr 7713  caucvgsr 7803
[HoTT], p.	Definition 11.2.1	df-inp 7467
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 14853
[HoTT], p.	Proposition 11.2.3	df-iso 4299  ltpopr 7596  ltsopr 7597
[HoTT], p.	Definition 11.2.7(v)	apsym 8565  reapcotr 8557  reapirr 8536
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8086  gt0add 8532  leadd1 8389  lelttr 8048  lemul1a 8817  lenlt 8035  ltadd1 8388  ltletr 8049  ltmul1 8551  reaplt 8547
[Jech] p. 4	Definition of class	cv 1352  cvjust 2172
[Jech] p. 78	Note	opthprc 4679
[KalishMontague] p. 81	Note 1	ax-i9 1530
[Kreyszig] p. 3	Property M1	metcl 13892  xmetcl 13891
[Kreyszig] p. 4	Property M2	meteq0 13899
[Kreyszig] p. 12	Equation 5	muleqadd 8627
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13981
[Kreyszig] p. 19	Remark	mopntopon 13982
[Kreyszig] p. 19	Theorem T1	mopn0 14027  mopnm 13987
[Kreyszig] p. 19	Theorem T2	unimopn 14025
[Kreyszig] p. 19	Definition of neighborhood	neibl 14030
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 14052
[Kreyszig] p. 25	Definition 1.4-1	lmbr 13752
[Kreyszig] p. 51	Equation 2	lmodvneg1 13425
[Kreyszig] p. 51	Equation 1a	lmod0vs 13416
[Kreyszig] p. 51	Equation 1b	lmodvs0 13417
[Kunen] p. 10	Axiom 0	a9e 1696
[Kunen] p. 12	Axiom 6	zfrep6 4122
[Kunen] p. 24	Definition 10.24	mapval 6662  mapvalg 6660
[Kunen] p. 31	Definition 10.24	mapex 6656
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3898
[Lang] p. 3	Statement	lidrideqd 12805  mndbn0 12837
[Lang] p. 3	Definition	df-mnd 12823
[Lang] p. 7	Definition	dfgrp2e 12908
[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 3511
[Margaris] p. 89	Theorem 19.3	19.3 1554  19.3h 1553  rr19.3v 2878
[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 3030
[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 3520  r19.27mv 3521
[Margaris] p. 90	Theorem 19.28	19.28 1563  19.28h 1562  19.28v 1900  r19.28av 2613  r19.28m 3514  r19.28mv 3517  rr19.28v 2879
[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 3519
[Margaris] p. 90	Theorem 19.45	19.45 1683  r19.45av 2637  r19.45mv 3518
[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 3047  rspsbca 3048  stdpc4 1775
[Mendelson] p. 69	Axiom 5	ra5 3053  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 3461
[Mendelson] p. 231	Exercise 4.10(l)	unv 3462
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3377
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3425
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3378
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3268
[Mendelson] p. 231	Definition of union	unssin 3376
[Mendelson] p. 235	Exercise 4.12(c)	univ 4478
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3810
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4284
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4285
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4286
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3831
[Mendelson] p. 235	Exercise 4.12(p)	reli 4758
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5151
[Mendelson] p. 246	Definition of successor	df-suc 4373
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6847
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6823  xpsneng 6824
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6829  xpcomeng 6830
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6832
[Mendelson] p. 255	Exercise 4.39	endisj 6826
[Mendelson] p. 255	Exercise 4.41	mapprc 6654
[Mendelson] p. 255	Exercise 4.43	mapsnen 6813
[Mendelson] p. 255	Exercise 4.47	xpmapen 6852
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6688
[Mendelson] p. 255	Exercise 4.42(b)	map1 6814
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7218  djucomen 7217
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7216
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6470
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3359
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4716
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4717
[Monk1] p. 34	Definition 3.3	df-opab 4067
[Monk1] p. 36	Theorem 3.7(i)	coi1 5146  coi2 5147
[Monk1] p. 36	Theorem 3.8(v)	dm0 4843  rn0 4885
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5035
[Monk1] p. 37	Theorem 3.13(i)	relxp 4737
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4849  rnxpm 5060
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4708  xp0 5050
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4989
[Monk1] p. 38	Theorem 3.16(viii)	imai 4986
[Monk1] p. 39	Theorem 3.17	imaex 4985  imaexg 4984
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4983
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5648  funfvop 5630
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5561
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5569
[Monk1] p. 43	Theorem 4.6	funun 5262
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5771  dff13f 5773
[Monk1] p. 46	Theorem 4.15(v)	funex 5741  funrnex 6117
[Monk1] p. 50	Definition 5.4	fniunfv 5765
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5114
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3862
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6158  df-1st 6143
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6159  df-2nd 6144
[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 4245
[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 14862
[Munkres] p. 77	Example 2	distop 13624
[Munkres] p. 78	Definition of basis	df-bases 13582  isbasis3g 13585
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12714  tgval2 13590
[Munkres] p. 79	Remark	tgcl 13603
[Munkres] p. 80	Lemma 2.1	tgval3 13597
[Munkres] p. 80	Lemma 2.2	tgss2 13618  tgss3 13617
[Munkres] p. 81	Lemma 2.3	basgen 13619  basgen2 13620
[Munkres] p. 89	Definition of subspace topology	resttop 13709
[Munkres] p. 93	Theorem 6.1(1)	0cld 13651  topcld 13648
[Munkres] p. 93	Theorem 6.1(3)	uncld 13652
[Munkres] p. 94	Definition of closure	clsval 13650
[Munkres] p. 94	Definition of interior	ntrval 13649
[Munkres] p. 102	Definition of continuous function	df-cn 13727  iscn 13736  iscn2 13739
[Munkres] p. 107	Theorem 7.2(g)	cncnp 13769  cncnp2m 13770  cncnpi 13767  df-cnp 13728  iscnp 13738
[Munkres] p. 127	Theorem 10.1	metcn 14053
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6905
[Pierik], p. 9	Definition 2.4	df-womni 7164
[Pierik], p. 9	Definition 2.5	df-markov 7152  omniwomnimkv 7167
[Pierik], p. 10	Section 2.3	dfdif3 3247
[Pierik], p. 14	Definition 3.1	df-omni 7135  exmidomniim 7141  finomni 7140
[Pierik], p. 15	Section 3.1	df-nninf 7121
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 14810
[PradicBrown2022], p. 2	Remark	exmidpw 6910
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7202
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7203  exmidfodomrlemrALT 7204
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7149
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 14795  peano4nninf 14794
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 14797
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 14805
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 14807
[PradicBrown2022], p. 5	Definition 3.3	nnsf 14793
[Quine] p. 16	Definition 2.1	df-clab 2164  rabid 2653
[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 2741
[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 2965
[Quine] p. 42	Theorem 6.7	dfsbcq 2966  dfsbcq2 2967
[Quine] p. 43	Theorem 6.8	vex 2742
[Quine] p. 43	Theorem 6.9	isset 2745
[Quine] p. 44	Theorem 7.3	spcgf 2821  spcgv 2826  spcimgf 2819
[Quine] p. 44	Theorem 6.11	spsbc 2976  spsbcd 2977
[Quine] p. 44	Theorem 6.12	elex 2750
[Quine] p. 44	Theorem 6.13	elab 2883  elabg 2885  elabgf 2881
[Quine] p. 44	Theorem 6.14	noel 3428
[Quine] p. 48	Theorem 7.2	snprc 3659
[Quine] p. 48	Definition 7.1	df-pr 3601  df-sn 3600
[Quine] p. 49	Theorem 7.4	snss 3729  snssg 3728
[Quine] p. 49	Theorem 7.5	prss 3750  prssg 3751
[Quine] p. 49	Theorem 7.6	prid1 3700  prid1g 3698  prid2 3701  prid2g 3699  snid 3625  snidg 3623
[Quine] p. 51	Theorem 7.12	snexg 4186  snexprc 4188
[Quine] p. 51	Theorem 7.13	prexg 4213
[Quine] p. 53	Theorem 8.2	unisn 3827  unisng 3828
[Quine] p. 53	Theorem 8.3	uniun 3830
[Quine] p. 54	Theorem 8.6	elssuni 3839
[Quine] p. 54	Theorem 8.7	uni0 3838
[Quine] p. 56	Theorem 8.17	uniabio 5190
[Quine] p. 56	Definition 8.18	dfiota2 5181
[Quine] p. 57	Theorem 8.19	iotaval 5191
[Quine] p. 57	Theorem 8.22	iotanul 5195
[Quine] p. 58	Theorem 8.23	euiotaex 5196
[Quine] p. 58	Definition 9.1	df-op 3603
[Quine] p. 61	Theorem 9.5	opabid 4259  opelopab 4273  opelopaba 4268  opelopabaf 4275  opelopabf 4276  opelopabg 4270  opelopabga 4265  oprabid 5909
[Quine] p. 64	Definition 9.11	df-xp 4634
[Quine] p. 64	Definition 9.12	df-cnv 4636
[Quine] p. 64	Definition 9.15	df-id 4295
[Quine] p. 65	Theorem 10.3	fun0 5276
[Quine] p. 65	Theorem 10.4	funi 5250
[Quine] p. 65	Theorem 10.5	funsn 5266  funsng 5264
[Quine] p. 65	Definition 10.1	df-fun 5220
[Quine] p. 65	Definition 10.2	args 4999  dffv4g 5514
[Quine] p. 68	Definition 10.11	df-fv 5226  fv2 5512
[Quine] p. 124	Theorem 17.3	nn0opth2 10706  nn0opth2d 10705  nn0opthd 10704
[Quine] p. 284	Axiom 39(vi)	funimaex 5303  funimaexg 5302
[Roman] p. 19	Part Preliminaries	df-ring 13186
[Rudin] p. 164	Equation 27	efcan 11686
[Rudin] p. 164	Equation 30	efzval 11693
[Rudin] p. 167	Equation 48	absefi 11778
[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 5015
[Schechter] p. 51	Definition of irreflexivity	intirr 5017
[Schechter] p. 51	Definition of symmetry	cnvsym 5014
[Schechter] p. 51	Definition of transitivity	cotr 5012
[Schechter] p. 187	Definition of "ring with unit"	isring 13188
[Schechter] p. 428	Definition 15.35	bastop1 13622
[Stoll] p. 13	Definition of symmetric difference	symdif1 3402
[Stoll] p. 16	Exercise 4.4	0dif 3496  dif0 3495
[Stoll] p. 16	Exercise 4.8	difdifdirss 3509
[Stoll] p. 19	Theorem 5.2(13)	undm 3395
[Stoll] p. 19	Theorem 5.2(13')	indmss 3396
[Stoll] p. 20	Remark	invdif 3379
[Stoll] p. 25	Definition of ordered triple	df-ot 3604
[Stoll] p. 43	Definition	uniiun 3942
[Stoll] p. 44	Definition	intiin 3943
[Stoll] p. 45	Definition	df-iin 3891
[Stoll] p. 45	Definition indexed union	df-iun 3890
[Stoll] p. 176	Theorem 3.4(27)	imandc 889  imanst 888
[Stoll] p. 262	Example 4.1	symdif1 3402
[Suppes] p. 22	Theorem 2	eq0 3443
[Suppes] p. 22	Theorem 4	eqss 3172  eqssd 3174  eqssi 3173
[Suppes] p. 23	Theorem 5	ss0 3465  ss0b 3464
[Suppes] p. 23	Theorem 6	sstr 3165
[Suppes] p. 25	Theorem 12	elin 3320  elun 3278
[Suppes] p. 26	Theorem 15	inidm 3346
[Suppes] p. 26	Theorem 16	in0 3459
[Suppes] p. 27	Theorem 23	unidm 3280
[Suppes] p. 27	Theorem 24	un0 3458
[Suppes] p. 27	Theorem 25	ssun1 3300
[Suppes] p. 27	Theorem 26	ssequn1 3307
[Suppes] p. 27	Theorem 27	unss 3311
[Suppes] p. 27	Theorem 28	indir 3386
[Suppes] p. 27	Theorem 29	undir 3387
[Suppes] p. 28	Theorem 32	difid 3493  difidALT 3494
[Suppes] p. 29	Theorem 33	difin 3374
[Suppes] p. 29	Theorem 34	indif 3380
[Suppes] p. 29	Theorem 35	undif1ss 3499
[Suppes] p. 29	Theorem 36	difun2 3504
[Suppes] p. 29	Theorem 37	difin0 3498
[Suppes] p. 29	Theorem 38	disjdif 3497
[Suppes] p. 29	Theorem 39	difundi 3389
[Suppes] p. 29	Theorem 40	difindiss 3391
[Suppes] p. 30	Theorem 41	nalset 4135
[Suppes] p. 39	Theorem 61	uniss 3832
[Suppes] p. 39	Theorem 65	uniop 4257
[Suppes] p. 41	Theorem 70	intsn 3881
[Suppes] p. 42	Theorem 71	intpr 3878  intprg 3879
[Suppes] p. 42	Theorem 73	op1stb 4480  op1stbg 4481
[Suppes] p. 42	Theorem 78	intun 3877
[Suppes] p. 44	Definition 15(a)	dfiun2 3922  dfiun2g 3920
[Suppes] p. 44	Definition 15(b)	dfiin2 3923
[Suppes] p. 47	Theorem 86	elpw 3583  elpw2 4159  elpw2g 4158  elpwg 3585
[Suppes] p. 47	Theorem 87	pwid 3592
[Suppes] p. 47	Theorem 89	pw0 3741
[Suppes] p. 48	Theorem 90	pwpw0ss 3806
[Suppes] p. 52	Theorem 101	xpss12 4735
[Suppes] p. 52	Theorem 102	xpindi 4764  xpindir 4765
[Suppes] p. 52	Theorem 103	xpundi 4684  xpundir 4685
[Suppes] p. 54	Theorem 105	elirrv 4549
[Suppes] p. 58	Theorem 2	relss 4715
[Suppes] p. 59	Theorem 4	eldm 4826  eldm2 4827  eldm2g 4825  eldmg 4824
[Suppes] p. 59	Definition 3	df-dm 4638
[Suppes] p. 60	Theorem 6	dmin 4837
[Suppes] p. 60	Theorem 8	rnun 5039
[Suppes] p. 60	Theorem 9	rnin 5040
[Suppes] p. 60	Definition 4	dfrn2 4817
[Suppes] p. 61	Theorem 11	brcnv 4812  brcnvg 4810
[Suppes] p. 62	Equation 5	elcnv 4806  elcnv2 4807
[Suppes] p. 62	Theorem 12	relcnv 5008
[Suppes] p. 62	Theorem 15	cnvin 5038
[Suppes] p. 62	Theorem 16	cnvun 5036
[Suppes] p. 63	Theorem 20	co02 5144
[Suppes] p. 63	Theorem 21	dmcoss 4898
[Suppes] p. 63	Definition 7	df-co 4637
[Suppes] p. 64	Theorem 26	cnvco 4814
[Suppes] p. 64	Theorem 27	coass 5149
[Suppes] p. 65	Theorem 31	resundi 4922
[Suppes] p. 65	Theorem 34	elima 4977  elima2 4978  elima3 4979  elimag 4976
[Suppes] p. 65	Theorem 35	imaundi 5043
[Suppes] p. 66	Theorem 40	dminss 5045
[Suppes] p. 66	Theorem 41	imainss 5046
[Suppes] p. 67	Exercise 11	cnvxp 5049
[Suppes] p. 81	Definition 34	dfec2 6540
[Suppes] p. 82	Theorem 72	elec 6576  elecg 6575
[Suppes] p. 82	Theorem 73	erth 6581  erth2 6582
[Suppes] p. 89	Theorem 96	map0b 6689
[Suppes] p. 89	Theorem 97	map0 6691  map0g 6690
[Suppes] p. 89	Theorem 98	mapsn 6692
[Suppes] p. 89	Theorem 99	mapss 6693
[Suppes] p. 92	Theorem 1	enref 6767  enrefg 6766
[Suppes] p. 92	Theorem 2	ensym 6783  ensymb 6782  ensymi 6784
[Suppes] p. 92	Theorem 3	entr 6786
[Suppes] p. 92	Theorem 4	unen 6818
[Suppes] p. 94	Theorem 15	endom 6765
[Suppes] p. 94	Theorem 16	ssdomg 6780
[Suppes] p. 94	Theorem 17	domtr 6787
[Suppes] p. 95	Theorem 18	isbth 6968
[Suppes] p. 98	Exercise 4	fundmen 6808  fundmeng 6809
[Suppes] p. 98	Exercise 6	xpdom3m 6836
[Suppes] p. 130	Definition 3	df-tr 4104
[Suppes] p. 132	Theorem 9	ssonuni 4489
[Suppes] p. 134	Definition 6	df-suc 4373
[Suppes] p. 136	Theorem Schema 22	findes 4604  finds 4601  finds1 4603  finds2 4602
[Suppes] p. 162	Definition 5	df-ltnqqs 7354  df-ltpq 7347
[Suppes] p. 228	Theorem Schema 61	onintss 4392
[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 5881
[TakeutiZaring] p. 14	Proposition 4.14	ru 2963
[TakeutiZaring] p. 15	Exercise 1	elpr 3615  elpr2 3616  elprg 3614
[TakeutiZaring] p. 15	Exercise 2	elsn 3610  elsn2 3628  elsn2g 3627  elsng 3609  velsn 3611
[TakeutiZaring] p. 15	Exercise 3	elop 4233
[TakeutiZaring] p. 15	Exercise 4	sneq 3605  sneqr 3762
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3613  dfsn2 3608
[TakeutiZaring] p. 16	Axiom 3	uniex 4439
[TakeutiZaring] p. 16	Exercise 6	opth 4239
[TakeutiZaring] p. 16	Exercise 8	rext 4217
[TakeutiZaring] p. 16	Corollary 5.8	unex 4443  unexg 4445
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3643
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3812
[TakeutiZaring] p. 16	Definition 5.6	df-in 3137  df-un 3135
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3825  uniprg 3826
[TakeutiZaring] p. 17	Axiom 4	vpwex 4181
[TakeutiZaring] p. 17	Exercise 1	eltp 3642
[TakeutiZaring] p. 17	Exercise 5	elsuc 4408  elsucg 4406  sstr2 3164
[TakeutiZaring] p. 17	Exercise 6	uncom 3281
[TakeutiZaring] p. 17	Exercise 7	incom 3329
[TakeutiZaring] p. 17	Exercise 8	unass 3294
[TakeutiZaring] p. 17	Exercise 9	inass 3347
[TakeutiZaring] p. 17	Exercise 10	indi 3384
[TakeutiZaring] p. 17	Exercise 11	undi 3385
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3146
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3579
[TakeutiZaring] p. 18	Exercise 7	unss2 3308
[TakeutiZaring] p. 18	Exercise 9	df-ss 3144  sseqin2 3356
[TakeutiZaring] p. 18	Exercise 10	ssid 3177
[TakeutiZaring] p. 18	Exercise 12	inss1 3357  inss2 3358
[TakeutiZaring] p. 18	Exercise 13	nssr 3217
[TakeutiZaring] p. 18	Exercise 15	unieq 3820
[TakeutiZaring] p. 18	Exercise 18	sspwb 4218
[TakeutiZaring] p. 18	Exercise 19	pweqb 4225
[TakeutiZaring] p. 20	Definition	df-rab 2464
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4132
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3133
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3426
[TakeutiZaring] p. 20	Proposition 5.15	difid 3493  difidALT 3494
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3437
[TakeutiZaring] p. 21	Theorem 5.22	setind 4540
[TakeutiZaring] p. 21	Definition 5.20	df-v 2741
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4137
[TakeutiZaring] p. 22	Exercise 1	0ss 3463
[TakeutiZaring] p. 22	Exercise 3	ssex 4142  ssexg 4144
[TakeutiZaring] p. 22	Exercise 4	inex1 4139
[TakeutiZaring] p. 22	Exercise 5	ruv 4551
[TakeutiZaring] p. 22	Exercise 6	elirr 4542
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3489
[TakeutiZaring] p. 22	Exercise 11	difdif 3262
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3398
[TakeutiZaring] p. 22	Exercise 14	difss 3263
[TakeutiZaring] p. 22	Exercise 15	sscon 3271
[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 4743  xpexg 4742  xpexgALT 6136
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4635
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5282
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5434  fun11 5285
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5229  svrelfun 5283
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4816
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4818
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4640
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4641
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4637
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5085  dfrel2 5081
[TakeutiZaring] p. 25	Exercise 3	xpss 4736
[TakeutiZaring] p. 25	Exercise 5	relun 4745
[TakeutiZaring] p. 25	Exercise 6	reluni 4751
[TakeutiZaring] p. 25	Exercise 9	inxp 4763
[TakeutiZaring] p. 25	Exercise 12	relres 4937
[TakeutiZaring] p. 25	Exercise 13	opelres 4914  opelresg 4916
[TakeutiZaring] p. 25	Exercise 14	dmres 4930
[TakeutiZaring] p. 25	Exercise 15	resss 4933
[TakeutiZaring] p. 25	Exercise 17	resabs1 4938
[TakeutiZaring] p. 25	Exercise 18	funres 5259
[TakeutiZaring] p. 25	Exercise 24	relco 5129
[TakeutiZaring] p. 25	Exercise 29	funco 5258
[TakeutiZaring] p. 25	Exercise 30	f1co 5435
[TakeutiZaring] p. 26	Definition 6.10	eu2 2070
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5226  fv3 5540
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5169  cnvexg 5168
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4895  dmexg 4893
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4896  rnexg 4894
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5534
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5544  tz6.12 5545  tz6.12c 5547
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5508
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5221
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5222
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5224  wfo 5216
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5223  wf1 5215
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5225  wf1o 5217
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5615  eqfnfv2 5616  eqfnfv2f 5619
[TakeutiZaring] p. 28	Exercise 5	fvco 5588
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5740  fnexALT 6114
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5739  resfunexgALT 6111
[TakeutiZaring] p. 29	Exercise 9	funimaex 5303  funimaexg 5302
[TakeutiZaring] p. 29	Definition 6.18	df-br 4006
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5000  iniseg 5002
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4291
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5227
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5813
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5814
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5819
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5821
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5829
[TakeutiZaring] p. 35	Notation	wtr 4103
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4356
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4107
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4577
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4383
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4387
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4493
[TakeutiZaring] p. 38	Definition 7.11	df-on 4370
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4487
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4553
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4583
[TakeutiZaring] p. 40	Exercise 7	dftr2 4105
[TakeutiZaring] p. 40	Exercise 11	unon 4512
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4488
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3839
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4373
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4417  sucidg 4418
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4502
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4371
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4507  ordelsuc 4506
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4595
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4596
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4597
[TakeutiZaring] p. 43	Axiom 7	omex 4594
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4608
[TakeutiZaring] p. 43	Corollary 7.31	find 4600
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4598
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4599
[TakeutiZaring] p. 44	Exercise 2	int0 3860
[TakeutiZaring] p. 44	Exercise 3	trintssm 4119
[TakeutiZaring] p. 44	Exercise 4	intss1 3861
[TakeutiZaring] p. 44	Exercise 6	onintonm 4518
[TakeutiZaring] p. 44	Definition 7.35	df-int 3847
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6311
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6368  tfri1d 6338
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6369  tfri2d 6339
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6370
[TakeutiZaring] p. 50	Exercise 3	smoiso 6305
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6289
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6467
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6463
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6460
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6464
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6512  nnaordi 6511
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3933  uniss2 3842
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6473
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6483
[TakeutiZaring] p. 62	Exercise 5	oaword1 6474
[TakeutiZaring] p. 62	Definition 8.15	om0 6461  omsuc 6475
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6484
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6520  nnmordi 6519
[TakeutiZaring] p. 67	Definition 8.30	oei0 6462
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7188
[TakeutiZaring] p. 88	Exercise 1	en0 6797
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6859
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6860
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6745  isfi 6763
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6833
[TakeutiZaring] p. 95	Definition 10.42	df-map 6652
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6850
[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 2877
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3021
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5198
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5199
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2105  eupickbi 2108
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5226
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7191