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 7174  fidcenum 7015
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7015
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7174
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12582
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6986
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6974
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12597
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12599
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12588  znnen 12555
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12600
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12601
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10847
[AczelRathjen], p. 183	Chapter 20	ax-setind 4569
[AhoHopUll] p. 318	Section 9.1	df-word 10915  lencl 10918  wrd0 10939
[Apostol] p. 18	Theorem I.1	addcan 8199  addcan2d 8204  addcan2i 8202  addcand 8203  addcani 8201
[Apostol] p. 18	Theorem I.2	negeu 8210
[Apostol] p. 18	Theorem I.3	negsub 8267  negsubd 8336  negsubi 8297
[Apostol] p. 18	Theorem I.4	negneg 8269  negnegd 8321  negnegi 8289
[Apostol] p. 18	Theorem I.5	subdi 8404  subdid 8433  subdii 8426  subdir 8405  subdird 8434  subdiri 8427
[Apostol] p. 18	Theorem I.6	mul01 8408  mul01d 8412  mul01i 8410  mul02 8406  mul02d 8411  mul02i 8409
[Apostol] p. 18	Theorem I.9	divrecapd 8812
[Apostol] p. 18	Theorem I.10	recrecapi 8763
[Apostol] p. 18	Theorem I.12	mul2neg 8417  mul2negd 8432  mul2negi 8425  mulneg1 8414  mulneg1d 8430  mulneg1i 8423
[Apostol] p. 18	Theorem I.14	rdivmuldivd 13640
[Apostol] p. 18	Theorem I.15	divdivdivap 8732
[Apostol] p. 20	Axiom 7	rpaddcl 9743  rpaddcld 9778  rpmulcl 9744  rpmulcld 9779
[Apostol] p. 20	Axiom 9	0nrp 9755
[Apostol] p. 20	Theorem I.17	lttri 8124
[Apostol] p. 20	Theorem I.18	ltadd1d 8557  ltadd1dd 8575  ltadd1i 8521
[Apostol] p. 20	Theorem I.19	ltmul1 8611  ltmul1a 8610  ltmul1i 8939  ltmul1ii 8947  ltmul2 8875  ltmul2d 9805  ltmul2dd 9819  ltmul2i 8942
[Apostol] p. 20	Theorem I.21	0lt1 8146
[Apostol] p. 20	Theorem I.23	lt0neg1 8487  lt0neg1d 8534  ltneg 8481  ltnegd 8542  ltnegi 8512
[Apostol] p. 20	Theorem I.25	lt2add 8464  lt2addd 8586  lt2addi 8529
[Apostol] p. 20	Definition of positive numbers	df-rp 9720
[Apostol] p. 21	Exercise 4	recgt0 8869  recgt0d 8953  recgt0i 8925  recgt0ii 8926
[Apostol] p. 22	Definition of integers	df-z 9318
[Apostol] p. 22	Definition of rationals	df-q 9685
[Apostol] p. 24	Theorem I.26	supeuti 7053
[Apostol] p. 26	Theorem I.29	arch 9237
[Apostol] p. 28	Exercise 2	btwnz 9436
[Apostol] p. 28	Exercise 3	nnrecl 9238
[Apostol] p. 28	Exercise 6	qbtwnre 10325
[Apostol] p. 28	Exercise 10(a)	zeneo 12012  zneo 9418
[Apostol] p. 29	Theorem I.35	resqrtth 11175  sqrtthi 11263
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8985
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12173
[Apostol] p. 363	Remark	absgt0api 11290
[Apostol] p. 363	Example	abssubd 11337  abssubi 11294
[ApostolNT] p. 14	Definition	df-dvds 11931
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11947
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11971
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11967
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11961
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11963
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11948
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11949
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11954
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11987
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11989
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11991
[ApostolNT] p. 15	Definition	dfgcd2 12151
[ApostolNT] p. 16	Definition	isprm2 12255
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12230
[ApostolNT] p. 16	Theorem 1.7	prminf 12612
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12110
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12152
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12154
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12124
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12117
[ApostolNT] p. 17	Theorem 1.8	coprm 12282
[ApostolNT] p. 17	Theorem 1.9	euclemma 12284
[ApostolNT] p. 17	Theorem 1.10	1arith2 12506
[ApostolNT] p. 19	Theorem 1.14	divalg 12065
[ApostolNT] p. 20	Theorem 1.15	eucalg 12197
[ApostolNT] p. 25	Definition	df-phi 12349
[ApostolNT] p. 26	Theorem 2.2	phisum 12378
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12360
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12364
[ApostolNT] p. 104	Definition	congr 12238
[ApostolNT] p. 106	Remark	dvdsval3 11934
[ApostolNT] p. 106	Definition	moddvds 11942
[ApostolNT] p. 107	Example 2	mod2eq0even 12019
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12020
[ApostolNT] p. 107	Example 4	zmod1congr 10412
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10449
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10737
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11966
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12241
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12243
[ApostolNT] p. 113	Theorem 5.17	eulerth 12371
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12389
[ApostolNT] p. 114	Theorem 5.19	fermltl 12372
[ApostolNT] p. 179	Definition	df-lgs 15114  lgsprme0 15158
[ApostolNT] p. 180	Example 1	1lgs 15159
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 15135
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 15150
[ApostolNT] p. 181	Theorem 9.4	m1lgs 15192
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 15185
[ApostolNT] p. 188	Definition	df-lgs 15114  lgs1 15160
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 15151
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 15153
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 15161
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 15162
[Bauer] p. 482	Section 1.2	pm2.01 617  pm2.65 660
[Bauer] p. 483	Theorem 1.3	acexmid 5917  onsucelsucexmidlem 4561
[Bauer], p. 481	Section 1.1	pwtrufal 15488
[Bauer], p. 483	Definition	n0rf 3459
[Bauer], p. 483	Theorem 1.2	2irrexpq 15108  2irrexpqap 15110
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6932
[Bauer], p. 493	Section 5.1	ivthdich 14807
[Bauer], p. 494	Theorem 5.5	ivthinc 14797
[BauerHanson], p. 27	Proposition 5.2	cnstab 8664
[BauerSwan], p. 14	Remark	0ct 7166  ctm 7168
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 15491
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7174
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7561
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7474
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7563
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7597  addlocpr 7596
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7623
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7626
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7631
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2045
[BellMachover] p. 460	Notation	df-mo 2046
[BellMachover] p. 460	Definition	mo3 2096  mo3h 2095
[BellMachover] p. 462	Theorem 1.1	bm1.1 2178
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4150
[BellMachover] p. 466	Axiom Pow	axpow3 4206
[BellMachover] p. 466	Axiom Union	axun2 4466
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4574
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4415
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4577
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4528
[BellMachover] p. 471	Definition of Lim	df-ilim 4400
[BellMachover] p. 472	Axiom Inf	zfinf2 4621
[BellMachover] p. 473	Theorem 2.8	limom 4646
[Bobzien] p. 116	Statement T3	stoic3 1442
[Bobzien] p. 117	Statement T2	stoic2a 1440
[Bobzien] p. 117	Statement T4	stoic4a 1443
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1438
[BourbakiAlg1] p. 1	Definition 1	df-mgm 12939
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 12985
[BourbakiAlg1] p. 12	Definition 2	df-mnd 12998
[BourbakiAlg1] p. 92	Definition 1	df-ring 13494
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 13429
[BourbakiEns] p.	Proposition 8	fcof1 5826  fcofo 5827
[BourbakiTop1] p.	Remark	xnegmnf 9895  xnegpnf 9894
[BourbakiTop1] p.	Remark	rexneg 9896
[BourbakiTop1] p.	Proposition	ishmeo 14472
[BourbakiTop1] p.	Property V_i	ssnei2 14325
[BourbakiTop1] p.	Property V_ii	innei 14331
[BourbakiTop1] p.	Property V_iv	neissex 14333
[BourbakiTop1] p.	Proposition 1	neipsm 14322  neiss 14318
[BourbakiTop1] p.	Proposition 2	cnptopco 14390
[BourbakiTop1] p.	Proposition 4	imasnopn 14467
[BourbakiTop1] p.	Property V_iii	elnei 14320
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14166
[Bruck] p. 1	Section I.1	df-mgm 12939
[Bruck] p. 23	Section II.1	df-sgrp 12985
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13171
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4092
[Cohen] p. 301	Remark	relogoprlem 15003
[Cohen] p. 301	Property 2	relogmul 15004  relogmuld 15019
[Cohen] p. 301	Property 3	relogdiv 15005  relogdivd 15020
[Cohen] p. 301	Property 4	relogexp 15007
[Cohen] p. 301	Property 1a	log1 15001
[Cohen] p. 301	Property 1b	loge 15002
[Cohen4] p. 348	Observation	relogbcxpbap 15097
[Cohen4] p. 352	Definition	rpelogb 15081
[Cohen4] p. 361	Property 2	rprelogbmul 15087
[Cohen4] p. 361	Property 3	logbrec 15092  rprelogbdiv 15089
[Cohen4] p. 361	Property 4	rplogbreexp 15085
[Cohen4] p. 361	Property 6	relogbexpap 15090
[Cohen4] p. 361	Property 1(a)	rplogbid1 15079
[Cohen4] p. 361	Property 1(b)	rplogb1 15080
[Cohen4] p. 367	Property	rplogbchbase 15082
[Cohen4] p. 377	Property 2	logblt 15094
[Crosilla] p.	Axiom 1	ax-ext 2175
[Crosilla] p.	Axiom 2	ax-pr 4238
[Crosilla] p.	Axiom 3	ax-un 4464
[Crosilla] p.	Axiom 4	ax-nul 4155
[Crosilla] p.	Axiom 5	ax-iinf 4620
[Crosilla] p.	Axiom 6	ru 2984
[Crosilla] p.	Axiom 8	ax-pow 4203
[Crosilla] p.	Axiom 9	ax-setind 4569
[Crosilla], p.	Axiom 6	ax-sep 4147
[Crosilla], p.	Axiom 7	ax-coll 4144
[Crosilla], p.	Axiom 7'	repizf 4145
[Crosilla], p.	Theorem is stated	ordtriexmid 4553
[Crosilla], p.	Axiom of choice implies instances	acexmid 5917
[Crosilla], p.	Definition of ordinal	df-iord 4397
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4567
[Eisenberg] p. 67	Definition 5.3	df-dif 3155
[Eisenberg] p. 82	Definition 6.3	df-iom 4623
[Eisenberg] p. 125	Definition 8.21	df-map 6704
[Enderton] p. 18	Axiom of Empty Set	axnul 4154
[Enderton] p. 19	Definition	df-tp 3626
[Enderton] p. 26	Exercise 5	unissb 3865
[Enderton] p. 26	Exercise 10	pwel 4247
[Enderton] p. 28	Exercise 7(b)	pwunim 4317
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3982  iinin2m 3981  iunin1 3977  iunin2 3976
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3980  iundif2ss 3978
[Enderton] p. 33	Exercise 23	iinuniss 3995
[Enderton] p. 33	Exercise 25	iununir 3996
[Enderton] p. 33	Exercise 24(a)	iinpw 4003
[Enderton] p. 33	Exercise 24(b)	iunpw 4511  iunpwss 4004
[Enderton] p. 38	Exercise 6(a)	unipw 4246
[Enderton] p. 38	Exercise 6(b)	pwuni 4221
[Enderton] p. 41	Lemma 3D	opeluu 4481  rnex 4929  rnexg 4927
[Enderton] p. 41	Exercise 8	dmuni 4872  rnuni 5077
[Enderton] p. 42	Definition of a function	dffun7 5281  dffun8 5282
[Enderton] p. 43	Definition of function value	funfvdm2 5621
[Enderton] p. 43	Definition of single-rooted	funcnv 5315
[Enderton] p. 44	Definition (d)	dfima2 5007  dfima3 5008
[Enderton] p. 47	Theorem 3H	fvco2 5626
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7266
[Enderton] p. 50	Theorem 3K(a)	imauni 5804
[Enderton] p. 52	Definition	df-map 6704
[Enderton] p. 53	Exercise 21	coass 5184
[Enderton] p. 53	Exercise 27	dmco 5174
[Enderton] p. 53	Exercise 14(a)	funin 5325
[Enderton] p. 53	Exercise 22(a)	imass2 5041
[Enderton] p. 54	Remark	ixpf 6774  ixpssmap 6786
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6753
[Enderton] p. 56	Theorem 3M	erref 6607
[Enderton] p. 57	Lemma 3N	erthi 6635
[Enderton] p. 57	Definition	df-ec 6589
[Enderton] p. 58	Definition	df-qs 6593
[Enderton] p. 60	Theorem 3Q	th3q 6694  th3qcor 6693  th3qlem1 6691  th3qlem2 6692
[Enderton] p. 61	Exercise 35	df-ec 6589
[Enderton] p. 65	Exercise 56(a)	dmun 4869
[Enderton] p. 68	Definition of successor	df-suc 4402
[Enderton] p. 71	Definition	df-tr 4128  dftr4 4132
[Enderton] p. 72	Theorem 4E	unisuc 4444  unisucg 4445
[Enderton] p. 73	Exercise 6	unisuc 4444  unisucg 4445
[Enderton] p. 73	Exercise 5(a)	truni 4141
[Enderton] p. 73	Exercise 5(b)	trint 4142
[Enderton] p. 79	Theorem 4I(A1)	nna0 6527
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6529  onasuc 6519
[Enderton] p. 79	Definition of operation value	df-ov 5921
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6528
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6530  onmsuc 6526
[Enderton] p. 81	Theorem 4K(1)	nnaass 6538
[Enderton] p. 81	Theorem 4K(2)	nna0r 6531  nnacom 6537
[Enderton] p. 81	Theorem 4K(3)	nndi 6539
[Enderton] p. 81	Theorem 4K(4)	nnmass 6540
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6542
[Enderton] p. 82	Exercise 16	nnm0r 6532  nnmsucr 6541
[Enderton] p. 88	Exercise 23	nnaordex 6581
[Enderton] p. 129	Definition	df-en 6795
[Enderton] p. 132	Theorem 6B(b)	canth 5871
[Enderton] p. 133	Exercise 1	xpomen 12552
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6921
[Enderton] p. 136	Corollary 6E	nneneq 6913
[Enderton] p. 139	Theorem 6H(c)	mapen 6902
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7278
[Enderton] p. 143	Theorem 6J	dju0en 7274  dju1en 7273
[Enderton] p. 144	Corollary 6K	undif2ss 3522
[Enderton] p. 145	Figure 38	ffoss 5532
[Enderton] p. 145	Definition	df-dom 6796
[Enderton] p. 146	Example 1	domen 6805  domeng 6806
[Enderton] p. 146	Example 3	nndomo 6920
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6889  xpdom1g 6887  xpdom2g 6886
[Enderton] p. 168	Definition	df-po 4327
[Enderton] p. 192	Theorem 7M(a)	oneli 4459
[Enderton] p. 192	Theorem 7M(b)	ontr1 4420
[Enderton] p. 192	Theorem 7M(c)	onirri 4575
[Enderton] p. 193	Corollary 7N(b)	0elon 4423
[Enderton] p. 193	Corollary 7N(c)	onsuci 4548
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4521
[Enderton] p. 194	Remark	onprc 4584
[Enderton] p. 194	Exercise 16	suc11 4590
[Enderton] p. 197	Definition	df-card 7240
[Enderton] p. 200	Exercise 25	tfis 4615
[Enderton] p. 206	Theorem 7X(b)	en2lp 4586
[Enderton] p. 207	Exercise 34	opthreg 4588
[Enderton] p. 208	Exercise 35	suc11g 4589
[Geuvers], p. 1	Remark	expap0 10640
[Geuvers], p. 6	Lemma 2.13	mulap0r 8634
[Geuvers], p. 6	Lemma 2.15	mulap0 8673
[Geuvers], p. 9	Lemma 2.35	msqge0 8635
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7991
[Geuvers], p. 10	Lemma 3.9	maxcom 11347
[Geuvers], p. 10	Lemma 3.10	maxle1 11355  maxle2 11356
[Geuvers], p. 10	Lemma 3.11	maxleast 11357
[Geuvers], p. 10	Lemma 3.12	maxleb 11360
[Geuvers], p. 11	Definition 3.13	dfabsmax 11361
[Geuvers], p. 17	Definition 6.1	df-ap 8601
[Gleason] p. 117	Proposition 9-2.1	df-enq 7407  enqer 7418
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7411  df-nqqs 7408
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7404  df-plqqs 7409
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7405  df-mqqs 7410
[Gleason] p. 119	Proposition 9-2.5	df-rq 7412
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7468
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7471  ltbtwnnq 7476  ltbtwnnqq 7475
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7460
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7461
[Gleason] p. 123	Proposition 9-3.5	addclpr 7597
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7639
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7638
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7657
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7673
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7679  ltaprlem 7678
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7676
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7632
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7652
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7641
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7640
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7648
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7698
[Gleason] p. 126	Proposition 9-4.1	df-enr 7786  enrer 7795
[Gleason] p. 126	Proposition 9-4.2	df-0r 7791  df-1r 7792  df-nr 7787
[Gleason] p. 126	Proposition 9-4.3	df-mr 7789  df-plr 7788  negexsr 7832  recexsrlem 7834
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7790
[Gleason] p. 130	Proposition 10-1.3	creui 8979  creur 8978  cru 8621
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7983  axcnre 7941
[Gleason] p. 132	Definition 10-3.1	crim 11002  crimd 11121  crimi 11081  crre 11001  crred 11120  crrei 11080
[Gleason] p. 132	Definition 10-3.2	remim 11004  remimd 11086
[Gleason] p. 133	Definition 10.36	absval2 11201  absval2d 11329  absval2i 11288
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11028  cjaddd 11109  cjaddi 11076
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11029  cjmuld 11110  cjmuli 11077
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11027  cjcjd 11087  cjcji 11059
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11026  cjreb 11010  cjrebd 11090  cjrebi 11062  cjred 11115  rere 11009  rereb 11007  rerebd 11089  rerebi 11061  rered 11113
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11035  addcjd 11101  addcji 11071
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11145
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11196  abscjd 11334  abscji 11292
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11208  abs00d 11330  abs00i 11289  absne0d 11331
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11240  releabsd 11335  releabsi 11293
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11213  absmuld 11338  absmuli 11295
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11199  sqabsaddi 11296
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11248  abstrid 11340  abstrii 11299
[Gleason] p. 134	Definition 10-4.1	df-exp 10610  exp0 10614  expp1 10617  expp1d 10745
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10652  expaddd 10746
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15047  cxpmuld 15070  expmul 10655  expmuld 10747
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10649  mulexpd 10759  rpmulcxp 15044
[Gleason] p. 141	Definition 11-2.1	fzval 10076
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11469
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11471
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11470
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11474
[Gleason] p. 172	Corollary 12-2.5	climrecl 11467
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11463  climcj 11464  climim 11466  climre 11465
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8059  df-xr 8058  ltxr 9841
[Gleason] p. 180	Theorem 12-5.3	climcau 11490
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10369
[Gleason] p. 223	Definition 14-1.1	df-met 14041
[Gleason] p. 223	Definition 14-1.1(a)	met0 14532  xmet0 14531
[Gleason] p. 223	Definition 14-1.1(c)	metsym 14539
[Gleason] p. 223	Definition 14-1.1(d)	mettri 14541  mstri 14641  xmettri 14540  xmstri 14640
[Gleason] p. 230	Proposition 14-2.6	txlm 14447
[Gleason] p. 240	Proposition 14-4.2	metcnp3 14679
[Gleason] p. 243	Proposition 14-4.16	addcn2 11453  addcncntop 14720  mulcn2 11455  mulcncntop 14722  subcn2 11454  subcncntop 14721
[Gleason] p. 295	Remark	bcval3 10822  bcval4 10823
[Gleason] p. 295	Equation 2	bcpasc 10837
[Gleason] p. 295	Definition of binomial coefficient	bcval 10820  df-bc 10819
[Gleason] p. 296	Remark	bcn0 10826  bcnn 10828
[Gleason] p. 296	Theorem 15-2.8	binom 11627
[Gleason] p. 308	Equation 2	ef0 11815
[Gleason] p. 308	Equation 3	efcj 11816
[Gleason] p. 309	Corollary 15-4.3	efne0 11821
[Gleason] p. 309	Corollary 15-4.4	efexp 11825
[Gleason] p. 310	Equation 14	sinadd 11879
[Gleason] p. 310	Equation 15	cosadd 11880
[Gleason] p. 311	Equation 17	sincossq 11891
[Gleason] p. 311	Equation 18	cosbnd 11896  sinbnd 11895
[Gleason] p. 311	Definition of ` `	df-pi 11796
[Golan] p. 1	Remark	srgisid 13482
[Golan] p. 1	Definition	df-srg 13460
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1460
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13083  mndideu 13007
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13110
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13139
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13150
[Herstein] p. 57	Exercise 1	dfgrp3me 13172
[Heyting] p. 127	Axiom #1	ax1hfs 15564
[Hitchcock] p. 5	Rule A3	mptnan 1434
[Hitchcock] p. 5	Rule A4	mptxor 1435
[Hitchcock] p. 5	Rule A5	mtpxor 1437
[HoTT], p.	Lemma 10.4.1	exmidontriim 7285
[HoTT], p.	Theorem 7.2.6	nndceq 6552
[HoTT], p.	Exercise 11.10	neapmkv 15558
[HoTT], p.	Exercise 11.11	mulap0bd 8676
[HoTT], p.	Section 11.2.1	df-iltp 7530  df-imp 7529  df-iplp 7528  df-reap 8594
[HoTT], p.	Theorem 11.2.4	recapb 8690  rerecapb 8862
[HoTT], p.	Corollary 3.9.2	uchoice 6190
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7722
[HoTT], p.	Corollary 11.4.3	conventions 15213
[HoTT], p.	Exercise 11.6(i)	dcapnconst 15551  dceqnconst 15550
[HoTT], p.	Corollary 11.2.13	axcaucvg 7960  caucvgpr 7742  caucvgprpr 7772  caucvgsr 7862
[HoTT], p.	Definition 11.2.1	df-inp 7526
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 15556
[HoTT], p.	Proposition 11.2.3	df-iso 4328  ltpopr 7655  ltsopr 7656
[HoTT], p.	Definition 11.2.7(v)	apsym 8625  reapcotr 8617  reapirr 8596
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8146  gt0add 8592  leadd1 8449  lelttr 8108  lemul1a 8877  lenlt 8095  ltadd1 8448  ltletr 8109  ltmul1 8611  reaplt 8607
[Jech] p. 4	Definition of class	cv 1363  cvjust 2188
[Jech] p. 78	Note	opthprc 4710
[KalishMontague] p. 81	Note 1	ax-i9 1541
[Kreyszig] p. 3	Property M1	metcl 14521  xmetcl 14520
[Kreyszig] p. 4	Property M2	meteq0 14528
[Kreyszig] p. 12	Equation 5	muleqadd 8687
[Kreyszig] p. 18	Definition 1.3-2	mopnval 14610
[Kreyszig] p. 19	Remark	mopntopon 14611
[Kreyszig] p. 19	Theorem T1	mopn0 14656  mopnm 14616
[Kreyszig] p. 19	Theorem T2	unimopn 14654
[Kreyszig] p. 19	Definition of neighborhood	neibl 14659
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 14681
[Kreyszig] p. 25	Definition 1.4-1	lmbr 14381
[Kreyszig] p. 51	Equation 2	lmodvneg1 13826
[Kreyszig] p. 51	Equation 1a	lmod0vs 13817
[Kreyszig] p. 51	Equation 1b	lmodvs0 13818
[Kunen] p. 10	Axiom 0	a9e 1707
[Kunen] p. 12	Axiom 6	zfrep6 4146
[Kunen] p. 24	Definition 10.24	mapval 6714  mapvalg 6712
[Kunen] p. 31	Definition 10.24	mapex 6708
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3922
[Lang] p. 3	Statement	lidrideqd 12964  mndbn0 13012
[Lang] p. 3	Definition	df-mnd 12998
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 12981
[Lang] p. 5	Equation	gsumfzreidx 13407
[Lang] p. 6	Definition	mulgnn0gsum 13198
[Lang] p. 7	Definition	dfgrp2e 13100
[Levy] p. 338	Axiom	df-clab 2180  df-clel 2189  df-cleq 2186
[Lopez-Astorga] p. 12	Rule 1	mptnan 1434
[Lopez-Astorga] p. 12	Rule 2	mptxor 1435
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1437
[Margaris] p. 40	Rule C	exlimiv 1609
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 854
[Margaris] p. 49	Definition	dfbi2 388  dfordc 893  exalim 1513
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 652
[Margaris] p. 89	Theorem 19.2	19.2 1649  r19.2m 3533
[Margaris] p. 89	Theorem 19.3	19.3 1565  19.3h 1564  rr19.3v 2899
[Margaris] p. 89	Theorem 19.5	alcom 1489
[Margaris] p. 89	Theorem 19.6	alexdc 1630  alexim 1656
[Margaris] p. 89	Theorem 19.7	alnex 1510
[Margaris] p. 89	Theorem 19.8	19.8a 1601  spsbe 1853
[Margaris] p. 89	Theorem 19.9	19.9 1655  19.9h 1654  19.9v 1882  exlimd 1608
[Margaris] p. 89	Theorem 19.11	excom 1675  excomim 1674
[Margaris] p. 89	Theorem 19.12	19.12 1676  r19.12 2600
[Margaris] p. 90	Theorem 19.14	exnalim 1657
[Margaris] p. 90	Theorem 19.15	albi 1479  ralbi 2626
[Margaris] p. 90	Theorem 19.16	19.16 1566
[Margaris] p. 90	Theorem 19.17	19.17 1567
[Margaris] p. 90	Theorem 19.18	exbi 1615  rexbi 2627
[Margaris] p. 90	Theorem 19.19	19.19 1677
[Margaris] p. 90	Theorem 19.20	alim 1468  alimd 1532  alimdh 1478  alimdv 1890  ralimdaa 2560  ralimdv 2562  ralimdva 2561  ralimdvva 2563  sbcimdv 3051
[Margaris] p. 90	Theorem 19.21	19.21-2 1678  19.21 1594  19.21bi 1569  19.21h 1568  19.21ht 1592  19.21t 1593  19.21v 1884  alrimd 1621  alrimdd 1620  alrimdh 1490  alrimdv 1887  alrimi 1533  alrimih 1480  alrimiv 1885  alrimivv 1886  r19.21 2570  r19.21be 2585  r19.21bi 2582  r19.21t 2569  r19.21v 2571  ralrimd 2572  ralrimdv 2573  ralrimdva 2574  ralrimdvv 2578  ralrimdvva 2579  ralrimi 2565  ralrimiv 2566  ralrimiva 2567  ralrimivv 2575  ralrimivva 2576  ralrimivvva 2577  ralrimivw 2568  rexlimi 2604
[Margaris] p. 90	Theorem 19.22	2alimdv 1892  2eximdv 1893  exim 1610  eximd 1623  eximdh 1622  eximdv 1891  rexim 2588  reximdai 2592  reximddv 2597  reximddv2 2599  reximdv 2595  reximdv2 2593  reximdva 2596  reximdvai 2594  reximi2 2590
[Margaris] p. 90	Theorem 19.23	19.23 1689  19.23bi 1603  19.23h 1509  19.23ht 1508  19.23t 1688  19.23v 1894  19.23vv 1895  exlimd2 1606  exlimdh 1607  exlimdv 1830  exlimdvv 1909  exlimi 1605  exlimih 1604  exlimiv 1609  exlimivv 1908  r19.23 2602  r19.23v 2603  rexlimd 2608  rexlimdv 2610  rexlimdv3a 2613  rexlimdva 2611  rexlimdva2 2614  rexlimdvaa 2612  rexlimdvv 2618  rexlimdvva 2619  rexlimdvw 2615  rexlimiv 2605  rexlimiva 2606  rexlimivv 2617
[Margaris] p. 90	Theorem 19.24	i19.24 1650
[Margaris] p. 90	Theorem 19.25	19.25 1637
[Margaris] p. 90	Theorem 19.26	19.26-2 1493  19.26-3an 1494  19.26 1492  r19.26-2 2623  r19.26-3 2624  r19.26 2620  r19.26m 2625
[Margaris] p. 90	Theorem 19.27	19.27 1572  19.27h 1571  19.27v 1911  r19.27av 2629  r19.27m 3542  r19.27mv 3543
[Margaris] p. 90	Theorem 19.28	19.28 1574  19.28h 1573  19.28v 1912  r19.28av 2630  r19.28m 3536  r19.28mv 3539  rr19.28v 2900
[Margaris] p. 90	Theorem 19.29	19.29 1631  19.29r 1632  19.29r2 1633  19.29x 1634  r19.29 2631  r19.29d2r 2638  r19.29r 2632
[Margaris] p. 90	Theorem 19.30	19.30dc 1638
[Margaris] p. 90	Theorem 19.31	19.31r 1692
[Margaris] p. 90	Theorem 19.32	19.32dc 1690  19.32r 1691  r19.32r 2640  r19.32vdc 2643  r19.32vr 2642
[Margaris] p. 90	Theorem 19.33	19.33 1495  19.33b2 1640  19.33bdc 1641
[Margaris] p. 90	Theorem 19.34	19.34 1695
[Margaris] p. 90	Theorem 19.35	19.35-1 1635  19.35i 1636
[Margaris] p. 90	Theorem 19.36	19.36-1 1684  19.36aiv 1913  19.36i 1683  r19.36av 2645
[Margaris] p. 90	Theorem 19.37	19.37-1 1685  19.37aiv 1686  r19.37 2646  r19.37av 2647
[Margaris] p. 90	Theorem 19.38	19.38 1687
[Margaris] p. 90	Theorem 19.39	i19.39 1651
[Margaris] p. 90	Theorem 19.40	19.40-2 1643  19.40 1642  r19.40 2648
[Margaris] p. 90	Theorem 19.41	19.41 1697  19.41h 1696  19.41v 1914  19.41vv 1915  19.41vvv 1916  19.41vvvv 1917  r19.41 2649  r19.41v 2650
[Margaris] p. 90	Theorem 19.42	19.42 1699  19.42h 1698  19.42v 1918  19.42vv 1923  19.42vvv 1924  19.42vvvv 1925  r19.42v 2651
[Margaris] p. 90	Theorem 19.43	19.43 1639  r19.43 2652
[Margaris] p. 90	Theorem 19.44	19.44 1693  r19.44av 2653  r19.44mv 3541
[Margaris] p. 90	Theorem 19.45	19.45 1694  r19.45av 2654  r19.45mv 3540
[Margaris] p. 110	Exercise 2(b)	eu1 2067
[Megill] p. 444	Axiom C5	ax-17 1537
[Megill] p. 445	Lemma L12	alequcom 1526  ax-10 1516
[Megill] p. 446	Lemma L17	equtrr 1721
[Megill] p. 446	Lemma L19	hbnae 1732
[Megill] p. 447	Remark 9.1	df-sb 1774  sbid 1785
[Megill] p. 448	Scheme C5'	ax-4 1521
[Megill] p. 448	Scheme C6'	ax-7 1459
[Megill] p. 448	Scheme C8'	ax-8 1515
[Megill] p. 448	Scheme C9'	ax-i12 1518
[Megill] p. 448	Scheme C11'	ax-10o 1727
[Megill] p. 448	Scheme C12'	ax-13 2166
[Megill] p. 448	Scheme C13'	ax-14 2167
[Megill] p. 448	Scheme C15'	ax-11o 1834
[Megill] p. 448	Scheme C16'	ax-16 1825
[Megill] p. 448	Theorem 9.4	dral1 1741  dral2 1742  drex1 1809  drex2 1743  drsb1 1810  drsb2 1852
[Megill] p. 449	Theorem 9.7	sbcom2 2003  sbequ 1851  sbid2v 2012
[Megill] p. 450	Example in Appendix	hba1 1551
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3068  rspsbca 3069  stdpc4 1786
[Mendelson] p. 69	Axiom 5	ra5 3074  stdpc5 1595
[Mendelson] p. 81	Rule C	exlimiv 1609
[Mendelson] p. 95	Axiom 6	stdpc6 1714
[Mendelson] p. 95	Axiom 7	stdpc7 1781
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3483
[Mendelson] p. 231	Exercise 4.10(l)	unv 3484
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3399
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3447
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3400
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3290
[Mendelson] p. 231	Definition of union	unssin 3398
[Mendelson] p. 235	Exercise 4.12(c)	univ 4507
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3834
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4313
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4314
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4315
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3855
[Mendelson] p. 235	Exercise 4.12(p)	reli 4791
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5186
[Mendelson] p. 246	Definition of successor	df-suc 4402
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6901
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6875  xpsneng 6876
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6881  xpcomeng 6882
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6884
[Mendelson] p. 255	Exercise 4.39	endisj 6878
[Mendelson] p. 255	Exercise 4.41	mapprc 6706
[Mendelson] p. 255	Exercise 4.43	mapsnen 6865
[Mendelson] p. 255	Exercise 4.47	xpmapen 6906
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6740
[Mendelson] p. 255	Exercise 4.42(b)	map1 6866
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7277  djucomen 7276
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7275
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6520
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3381
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4747
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4748
[Monk1] p. 34	Definition 3.3	df-opab 4091
[Monk1] p. 36	Theorem 3.7(i)	coi1 5181  coi2 5182
[Monk1] p. 36	Theorem 3.8(v)	dm0 4876  rn0 4918
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5070
[Monk1] p. 37	Theorem 3.13(i)	relxp 4768
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4882  rnxpm 5095
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4739  xp0 5085
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5024
[Monk1] p. 38	Theorem 3.16(viii)	imai 5021
[Monk1] p. 39	Theorem 3.17	imaex 5020  imaexg 5019
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5016
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5688  funfvop 5670
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5600
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5608
[Monk1] p. 43	Theorem 4.6	funun 5298
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5811  dff13f 5813
[Monk1] p. 46	Theorem 4.15(v)	funex 5781  funrnex 6166
[Monk1] p. 50	Definition 5.4	fniunfv 5805
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5149
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3886
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6208  df-1st 6193
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6209  df-2nd 6194
[Monk2] p. 105	Axiom C4	ax-5 1458
[Monk2] p. 105	Axiom C7	ax-8 1515
[Monk2] p. 105	Axiom C8	ax-11 1517  ax-11o 1834
[Monk2] p. 105	Axiom (C8)	ax11v 1838
[Monk2] p. 109	Lemma 12	ax-7 1459
[Monk2] p. 109	Lemma 15	equvin 1874  equvini 1769  eqvinop 4272
[Monk2] p. 113	Axiom C5-1	ax-17 1537
[Monk2] p. 113	Axiom C5-2	ax6b 1662
[Monk2] p. 113	Axiom C5-3	ax-7 1459
[Monk2] p. 114	Lemma 22	hba1 1551
[Monk2] p. 114	Lemma 23	hbia1 1563  nfia1 1591
[Monk2] p. 114	Lemma 24	hba2 1562  nfa2 1590
[Moschovakis] p. 2	Chapter 2	df-stab 832  dftest 15565
[Munkres] p. 77	Example 2	distop 14253
[Munkres] p. 78	Definition of basis	df-bases 14211  isbasis3g 14214
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12871  tgval2 14219
[Munkres] p. 79	Remark	tgcl 14232
[Munkres] p. 80	Lemma 2.1	tgval3 14226
[Munkres] p. 80	Lemma 2.2	tgss2 14247  tgss3 14246
[Munkres] p. 81	Lemma 2.3	basgen 14248  basgen2 14249
[Munkres] p. 89	Definition of subspace topology	resttop 14338
[Munkres] p. 93	Theorem 6.1(1)	0cld 14280  topcld 14277
[Munkres] p. 93	Theorem 6.1(3)	uncld 14281
[Munkres] p. 94	Definition of closure	clsval 14279
[Munkres] p. 94	Definition of interior	ntrval 14278
[Munkres] p. 102	Definition of continuous function	df-cn 14356  iscn 14365  iscn2 14368
[Munkres] p. 107	Theorem 7.2(g)	cncnp 14398  cncnp2m 14399  cncnpi 14396  df-cnp 14357  iscnp 14367
[Munkres] p. 127	Theorem 10.1	metcn 14682
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6959
[Pierik], p. 9	Definition 2.4	df-womni 7223
[Pierik], p. 9	Definition 2.5	df-markov 7211  omniwomnimkv 7226
[Pierik], p. 10	Section 2.3	dfdif3 3269
[Pierik], p. 14	Definition 3.1	df-omni 7194  exmidomniim 7200  finomni 7199
[Pierik], p. 15	Section 3.1	df-nninf 7179
[Pradic2025], p. 2	Section 1.1	nnnninfen 15511
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 15513
[PradicBrown2022], p. 2	Remark	exmidpw 6964
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7261
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7262  exmidfodomrlemrALT 7263
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7208
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 15497  peano4nninf 15496
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 15499
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 15507
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 15509
[PradicBrown2022], p. 5	Definition 3.3	nnsf 15495
[Quine] p. 16	Definition 2.1	df-clab 2180  rabid 2670
[Quine] p. 17	Definition 2.1''	dfsb7 2007
[Quine] p. 18	Definition 2.7	df-cleq 2186
[Quine] p. 19	Definition 2.9	df-v 2762
[Quine] p. 34	Theorem 5.1	abeq2 2302
[Quine] p. 35	Theorem 5.2	abid2 2314  abid2f 2362
[Quine] p. 40	Theorem 6.1	sb5 1899
[Quine] p. 40	Theorem 6.2	sb56 1897  sb6 1898
[Quine] p. 41	Theorem 6.3	df-clel 2189
[Quine] p. 41	Theorem 6.4	eqid 2193
[Quine] p. 41	Theorem 6.5	eqcom 2195
[Quine] p. 42	Theorem 6.6	df-sbc 2986
[Quine] p. 42	Theorem 6.7	dfsbcq 2987  dfsbcq2 2988
[Quine] p. 43	Theorem 6.8	vex 2763
[Quine] p. 43	Theorem 6.9	isset 2766
[Quine] p. 44	Theorem 7.3	spcgf 2842  spcgv 2847  spcimgf 2840
[Quine] p. 44	Theorem 6.11	spsbc 2997  spsbcd 2998
[Quine] p. 44	Theorem 6.12	elex 2771
[Quine] p. 44	Theorem 6.13	elab 2904  elabg 2906  elabgf 2902
[Quine] p. 44	Theorem 6.14	noel 3450
[Quine] p. 48	Theorem 7.2	snprc 3683
[Quine] p. 48	Definition 7.1	df-pr 3625  df-sn 3624
[Quine] p. 49	Theorem 7.4	snss 3753  snssg 3752
[Quine] p. 49	Theorem 7.5	prss 3774  prssg 3775
[Quine] p. 49	Theorem 7.6	prid1 3724  prid1g 3722  prid2 3725  prid2g 3723  snid 3649  snidg 3647
[Quine] p. 51	Theorem 7.12	snexg 4213  snexprc 4215
[Quine] p. 51	Theorem 7.13	prexg 4240
[Quine] p. 53	Theorem 8.2	unisn 3851  unisng 3852
[Quine] p. 53	Theorem 8.3	uniun 3854
[Quine] p. 54	Theorem 8.6	elssuni 3863
[Quine] p. 54	Theorem 8.7	uni0 3862
[Quine] p. 56	Theorem 8.17	uniabio 5225
[Quine] p. 56	Definition 8.18	dfiota2 5216
[Quine] p. 57	Theorem 8.19	iotaval 5226
[Quine] p. 57	Theorem 8.22	iotanul 5230
[Quine] p. 58	Theorem 8.23	euiotaex 5231
[Quine] p. 58	Definition 9.1	df-op 3627
[Quine] p. 61	Theorem 9.5	opabid 4286  opabidw 4287  opelopab 4302  opelopaba 4296  opelopabaf 4304  opelopabf 4305  opelopabg 4298  opelopabga 4293  opelopabgf 4300  oprabid 5950
[Quine] p. 64	Definition 9.11	df-xp 4665
[Quine] p. 64	Definition 9.12	df-cnv 4667
[Quine] p. 64	Definition 9.15	df-id 4324
[Quine] p. 65	Theorem 10.3	fun0 5312
[Quine] p. 65	Theorem 10.4	funi 5286
[Quine] p. 65	Theorem 10.5	funsn 5302  funsng 5300
[Quine] p. 65	Definition 10.1	df-fun 5256
[Quine] p. 65	Definition 10.2	args 5034  dffv4g 5551
[Quine] p. 68	Definition 10.11	df-fv 5262  fv2 5549
[Quine] p. 124	Theorem 17.3	nn0opth2 10795  nn0opth2d 10794  nn0opthd 10793
[Quine] p. 284	Axiom 39(vi)	funimaex 5339  funimaexg 5338
[Roman] p. 18	Part Preliminaries	df-rng 13429
[Roman] p. 19	Part Preliminaries	df-ring 13494
[Rudin] p. 164	Equation 27	efcan 11819
[Rudin] p. 164	Equation 30	efzval 11826
[Rudin] p. 167	Equation 48	absefi 11912
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1437
[Sanford] p. 39	Rule 4	mptxor 1435
[Sanford] p. 40	Rule 1	mptnan 1434
[Schechter] p. 51	Definition of antisymmetry	intasym 5050
[Schechter] p. 51	Definition of irreflexivity	intirr 5052
[Schechter] p. 51	Definition of symmetry	cnvsym 5049
[Schechter] p. 51	Definition of transitivity	cotr 5047
[Schechter] p. 187	Definition of "ring with unit"	isring 13496
[Schechter] p. 428	Definition 15.35	bastop1 14251
[Stoll] p. 13	Definition of symmetric difference	symdif1 3424
[Stoll] p. 16	Exercise 4.4	0dif 3518  dif0 3517
[Stoll] p. 16	Exercise 4.8	difdifdirss 3531
[Stoll] p. 19	Theorem 5.2(13)	undm 3417
[Stoll] p. 19	Theorem 5.2(13')	indmss 3418
[Stoll] p. 20	Remark	invdif 3401
[Stoll] p. 25	Definition of ordered triple	df-ot 3628
[Stoll] p. 43	Definition	uniiun 3966
[Stoll] p. 44	Definition	intiin 3967
[Stoll] p. 45	Definition	df-iin 3915
[Stoll] p. 45	Definition indexed union	df-iun 3914
[Stoll] p. 176	Theorem 3.4(27)	imandc 890  imanst 889
[Stoll] p. 262	Example 4.1	symdif1 3424
[Suppes] p. 22	Theorem 2	eq0 3465
[Suppes] p. 22	Theorem 4	eqss 3194  eqssd 3196  eqssi 3195
[Suppes] p. 23	Theorem 5	ss0 3487  ss0b 3486
[Suppes] p. 23	Theorem 6	sstr 3187
[Suppes] p. 25	Theorem 12	elin 3342  elun 3300
[Suppes] p. 26	Theorem 15	inidm 3368
[Suppes] p. 26	Theorem 16	in0 3481
[Suppes] p. 27	Theorem 23	unidm 3302
[Suppes] p. 27	Theorem 24	un0 3480
[Suppes] p. 27	Theorem 25	ssun1 3322
[Suppes] p. 27	Theorem 26	ssequn1 3329
[Suppes] p. 27	Theorem 27	unss 3333
[Suppes] p. 27	Theorem 28	indir 3408
[Suppes] p. 27	Theorem 29	undir 3409
[Suppes] p. 28	Theorem 32	difid 3515  difidALT 3516
[Suppes] p. 29	Theorem 33	difin 3396
[Suppes] p. 29	Theorem 34	indif 3402
[Suppes] p. 29	Theorem 35	undif1ss 3521
[Suppes] p. 29	Theorem 36	difun2 3526
[Suppes] p. 29	Theorem 37	difin0 3520
[Suppes] p. 29	Theorem 38	disjdif 3519
[Suppes] p. 29	Theorem 39	difundi 3411
[Suppes] p. 29	Theorem 40	difindiss 3413
[Suppes] p. 30	Theorem 41	nalset 4159
[Suppes] p. 39	Theorem 61	uniss 3856
[Suppes] p. 39	Theorem 65	uniop 4284
[Suppes] p. 41	Theorem 70	intsn 3905
[Suppes] p. 42	Theorem 71	intpr 3902  intprg 3903
[Suppes] p. 42	Theorem 73	op1stb 4509  op1stbg 4510
[Suppes] p. 42	Theorem 78	intun 3901
[Suppes] p. 44	Definition 15(a)	dfiun2 3946  dfiun2g 3944
[Suppes] p. 44	Definition 15(b)	dfiin2 3947
[Suppes] p. 47	Theorem 86	elpw 3607  elpw2 4186  elpw2g 4185  elpwg 3609
[Suppes] p. 47	Theorem 87	pwid 3616
[Suppes] p. 47	Theorem 89	pw0 3765
[Suppes] p. 48	Theorem 90	pwpw0ss 3830
[Suppes] p. 52	Theorem 101	xpss12 4766
[Suppes] p. 52	Theorem 102	xpindi 4797  xpindir 4798
[Suppes] p. 52	Theorem 103	xpundi 4715  xpundir 4716
[Suppes] p. 54	Theorem 105	elirrv 4580
[Suppes] p. 58	Theorem 2	relss 4746
[Suppes] p. 59	Theorem 4	eldm 4859  eldm2 4860  eldm2g 4858  eldmg 4857
[Suppes] p. 59	Definition 3	df-dm 4669
[Suppes] p. 60	Theorem 6	dmin 4870
[Suppes] p. 60	Theorem 8	rnun 5074
[Suppes] p. 60	Theorem 9	rnin 5075
[Suppes] p. 60	Definition 4	dfrn2 4850
[Suppes] p. 61	Theorem 11	brcnv 4845  brcnvg 4843
[Suppes] p. 62	Equation 5	elcnv 4839  elcnv2 4840
[Suppes] p. 62	Theorem 12	relcnv 5043
[Suppes] p. 62	Theorem 15	cnvin 5073
[Suppes] p. 62	Theorem 16	cnvun 5071
[Suppes] p. 63	Theorem 20	co02 5179
[Suppes] p. 63	Theorem 21	dmcoss 4931
[Suppes] p. 63	Definition 7	df-co 4668
[Suppes] p. 64	Theorem 26	cnvco 4847
[Suppes] p. 64	Theorem 27	coass 5184
[Suppes] p. 65	Theorem 31	resundi 4955
[Suppes] p. 65	Theorem 34	elima 5010  elima2 5011  elima3 5012  elimag 5009
[Suppes] p. 65	Theorem 35	imaundi 5078
[Suppes] p. 66	Theorem 40	dminss 5080
[Suppes] p. 66	Theorem 41	imainss 5081
[Suppes] p. 67	Exercise 11	cnvxp 5084
[Suppes] p. 81	Definition 34	dfec2 6590
[Suppes] p. 82	Theorem 72	elec 6628  elecg 6627
[Suppes] p. 82	Theorem 73	erth 6633  erth2 6634
[Suppes] p. 89	Theorem 96	map0b 6741
[Suppes] p. 89	Theorem 97	map0 6743  map0g 6742
[Suppes] p. 89	Theorem 98	mapsn 6744
[Suppes] p. 89	Theorem 99	mapss 6745
[Suppes] p. 92	Theorem 1	enref 6819  enrefg 6818
[Suppes] p. 92	Theorem 2	ensym 6835  ensymb 6834  ensymi 6836
[Suppes] p. 92	Theorem 3	entr 6838
[Suppes] p. 92	Theorem 4	unen 6870
[Suppes] p. 94	Theorem 15	endom 6817
[Suppes] p. 94	Theorem 16	ssdomg 6832
[Suppes] p. 94	Theorem 17	domtr 6839
[Suppes] p. 95	Theorem 18	isbth 7026
[Suppes] p. 98	Exercise 4	fundmen 6860  fundmeng 6861
[Suppes] p. 98	Exercise 6	xpdom3m 6888
[Suppes] p. 130	Definition 3	df-tr 4128
[Suppes] p. 132	Theorem 9	ssonuni 4520
[Suppes] p. 134	Definition 6	df-suc 4402
[Suppes] p. 136	Theorem Schema 22	findes 4635  finds 4632  finds1 4634  finds2 4633
[Suppes] p. 162	Definition 5	df-ltnqqs 7413  df-ltpq 7406
[Suppes] p. 228	Theorem Schema 61	onintss 4421
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2175
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2186
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2189
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2188
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2211
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5922
[TakeutiZaring] p. 14	Proposition 4.14	ru 2984
[TakeutiZaring] p. 15	Exercise 1	elpr 3639  elpr2 3640  elprg 3638
[TakeutiZaring] p. 15	Exercise 2	elsn 3634  elsn2 3652  elsn2g 3651  elsng 3633  velsn 3635
[TakeutiZaring] p. 15	Exercise 3	elop 4260
[TakeutiZaring] p. 15	Exercise 4	sneq 3629  sneqr 3786
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3637  dfsn2 3632
[TakeutiZaring] p. 16	Axiom 3	uniex 4468
[TakeutiZaring] p. 16	Exercise 6	opth 4266
[TakeutiZaring] p. 16	Exercise 8	rext 4244
[TakeutiZaring] p. 16	Corollary 5.8	unex 4472  unexg 4474
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3667
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3836
[TakeutiZaring] p. 16	Definition 5.6	df-in 3159  df-un 3157
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3849  uniprg 3850
[TakeutiZaring] p. 17	Axiom 4	vpwex 4208
[TakeutiZaring] p. 17	Exercise 1	eltp 3666
[TakeutiZaring] p. 17	Exercise 5	elsuc 4437  elsucg 4435  sstr2 3186
[TakeutiZaring] p. 17	Exercise 6	uncom 3303
[TakeutiZaring] p. 17	Exercise 7	incom 3351
[TakeutiZaring] p. 17	Exercise 8	unass 3316
[TakeutiZaring] p. 17	Exercise 9	inass 3369
[TakeutiZaring] p. 17	Exercise 10	indi 3406
[TakeutiZaring] p. 17	Exercise 11	undi 3407
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3168
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3603
[TakeutiZaring] p. 18	Exercise 7	unss2 3330
[TakeutiZaring] p. 18	Exercise 9	df-ss 3166  sseqin2 3378
[TakeutiZaring] p. 18	Exercise 10	ssid 3199
[TakeutiZaring] p. 18	Exercise 12	inss1 3379  inss2 3380
[TakeutiZaring] p. 18	Exercise 13	nssr 3239
[TakeutiZaring] p. 18	Exercise 15	unieq 3844
[TakeutiZaring] p. 18	Exercise 18	sspwb 4245
[TakeutiZaring] p. 18	Exercise 19	pweqb 4252
[TakeutiZaring] p. 20	Definition	df-rab 2481
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4156
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3155
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3448
[TakeutiZaring] p. 20	Proposition 5.15	difid 3515  difidALT 3516
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3459
[TakeutiZaring] p. 21	Theorem 5.22	setind 4571
[TakeutiZaring] p. 21	Definition 5.20	df-v 2762
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4161
[TakeutiZaring] p. 22	Exercise 1	0ss 3485
[TakeutiZaring] p. 22	Exercise 3	ssex 4166  ssexg 4168
[TakeutiZaring] p. 22	Exercise 4	inex1 4163
[TakeutiZaring] p. 22	Exercise 5	ruv 4582
[TakeutiZaring] p. 22	Exercise 6	elirr 4573
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3511
[TakeutiZaring] p. 22	Exercise 11	difdif 3284
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3420
[TakeutiZaring] p. 22	Exercise 14	difss 3285
[TakeutiZaring] p. 22	Exercise 15	sscon 3293
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2477
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2478
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4774  xpexg 4773  xpexgALT 6185
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4666
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5318
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5470  fun11 5321
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5265  svrelfun 5319
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4849
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4851
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4671
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4672
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4668
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5120  dfrel2 5116
[TakeutiZaring] p. 25	Exercise 3	xpss 4767
[TakeutiZaring] p. 25	Exercise 5	relun 4776
[TakeutiZaring] p. 25	Exercise 6	reluni 4782
[TakeutiZaring] p. 25	Exercise 9	inxp 4796
[TakeutiZaring] p. 25	Exercise 12	relres 4970
[TakeutiZaring] p. 25	Exercise 13	opelres 4947  opelresg 4949
[TakeutiZaring] p. 25	Exercise 14	dmres 4963
[TakeutiZaring] p. 25	Exercise 15	resss 4966
[TakeutiZaring] p. 25	Exercise 17	resabs1 4971
[TakeutiZaring] p. 25	Exercise 18	funres 5295
[TakeutiZaring] p. 25	Exercise 24	relco 5164
[TakeutiZaring] p. 25	Exercise 29	funco 5294
[TakeutiZaring] p. 25	Exercise 30	f1co 5471
[TakeutiZaring] p. 26	Definition 6.10	eu2 2086
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5262  fv3 5577
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5204  cnvexg 5203
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4928  dmexg 4926
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4929  rnexg 4927
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5571
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5581  tz6.12 5582  tz6.12c 5584
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5545
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5257
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5258
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5260  wfo 5252
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5259  wf1 5251
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5261  wf1o 5253
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5655  eqfnfv2 5656  eqfnfv2f 5659
[TakeutiZaring] p. 28	Exercise 5	fvco 5627
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5780  fnexALT 6163
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5779  resfunexgALT 6160
[TakeutiZaring] p. 29	Exercise 9	funimaex 5339  funimaexg 5338
[TakeutiZaring] p. 29	Definition 6.18	df-br 4030
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5035  iniseg 5037
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4320
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5263
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5853
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5854
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5859
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5861
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5869
[TakeutiZaring] p. 35	Notation	wtr 4127
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4385
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4131
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4608
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4412
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4416
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4524
[TakeutiZaring] p. 38	Definition 7.11	df-on 4399
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4518
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4584
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4614
[TakeutiZaring] p. 40	Exercise 7	dftr2 4129
[TakeutiZaring] p. 40	Exercise 11	unon 4543
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4519
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3863
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4402
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4446  sucidg 4447
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4533
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4400
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4538  ordelsuc 4537
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4626
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4627
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4628
[TakeutiZaring] p. 43	Axiom 7	omex 4625
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4639
[TakeutiZaring] p. 43	Corollary 7.31	find 4631
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4629
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4630
[TakeutiZaring] p. 44	Exercise 2	int0 3884
[TakeutiZaring] p. 44	Exercise 3	trintssm 4143
[TakeutiZaring] p. 44	Exercise 4	intss1 3885
[TakeutiZaring] p. 44	Exercise 6	onintonm 4549
[TakeutiZaring] p. 44	Definition 7.35	df-int 3871
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6361
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6418  tfri1d 6388
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6419  tfri2d 6389
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6420
[TakeutiZaring] p. 50	Exercise 3	smoiso 6355
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6339
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6517
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6513
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6510
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6514
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6562  nnaordi 6561
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3957  uniss2 3866
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6523
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6533
[TakeutiZaring] p. 62	Exercise 5	oaword1 6524
[TakeutiZaring] p. 62	Definition 8.15	om0 6511  omsuc 6525
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6534
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6570  nnmordi 6569
[TakeutiZaring] p. 67	Definition 8.30	oei0 6512
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7247
[TakeutiZaring] p. 88	Exercise 1	en0 6849
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6913
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6914
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6797  isfi 6815
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6885
[TakeutiZaring] p. 95	Definition 10.42	df-map 6704
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 6891
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6904
[Tarski] p. 67	Axiom B5	ax-4 1521
[Tarski] p. 68	Lemma 6	equid 1712
[Tarski] p. 69	Lemma 7	equcomi 1715
[Tarski] p. 70	Lemma 14	spim 1749  spime 1752  spimeh 1750  spimh 1748
[Tarski] p. 70	Lemma 16	ax-11 1517  ax-11o 1834  ax11i 1725
[Tarski] p. 70	Lemmas 16 and 17	sb6 1898
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1537
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2166  ax-14 2167
[WhiteheadRussell] p. 96	Axiom *1.3	olc 712
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 728
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 757
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 766
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 790
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 617
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 644
[WhiteheadRussell] p. 100	Theorem *2.04	pm2.04 82
[WhiteheadRussell] p. 100	Theorem *2.05	imim2 55
[WhiteheadRussell] p. 100	Theorem *2.06	imim1 76
[WhiteheadRussell] p. 101	Theorem *2.1	pm2.1dc 838
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2140  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 738
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 837
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 630
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 886
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 844
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 857
[WhiteheadRussell] p. 103	Theorem *2.16	con3 643
[WhiteheadRussell] p. 103	Theorem *2.17	condc 854
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 856
[WhiteheadRussell] p. 104	Theorem *2.2	orc 713
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 776
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 618
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 622
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 894
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 908
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 769
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 770
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 805
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 806
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 804
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 981
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 779
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 777
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 778
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 739
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 740
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 868  pm2.5gdc 867
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 863
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 741
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 742
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 743
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 656
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 657
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 723
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 892
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 726
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 727
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 866
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 749
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 801
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 802
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 660
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 714  pm2.67 744
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 870  pm2.521gdc 869
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 748
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 811
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 895
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 916
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 807
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 808
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 810
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 809
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 812
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 813
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 906
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 755
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 959
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 960
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 961
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 754
[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 694
[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 861
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 860
[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 690
[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 756  pm3.44 716
[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 786
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 872
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 873
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 891
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 695
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 954  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 758  pm4.25 759
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 819
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 729
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 768
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 793
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 605
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 823
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 982
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 817
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 973
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 951
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 780
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 815  pm4.45 785  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1492
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 958
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 898  imorr 722
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 900
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 751
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 752
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 903
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 940
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 753  pm4.56 781
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 941  oranim 782
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 687
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 899
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 887
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 901
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 688
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 902
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 888
[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 828
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 745
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 603  pm4.76 604
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 711  pm4.77 800
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 783
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 904
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 708
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 909
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 952
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 953
[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 910
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 911
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 913
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 912
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1400
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 829
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 905
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1405  pm5.18dc 884
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 707
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 696
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1403
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1408
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1409
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 896
[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 927  pm5.6r 928
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 956
[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 918
[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 926
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 803
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 919
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 914
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 795
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 947
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 948
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 963
[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 964
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1646
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1496
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1643
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1907
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2045
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2445
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2446
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2898
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3042
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5234
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5235
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2121  eupickbi 2124
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5262
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7250