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 7092  fidcenum 6933
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6933
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7092
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12380
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6907
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6895
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12395
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12397
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12386  znnen 12353
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12398
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12399
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10710
[AczelRathjen], p. 183	Chapter 20	ax-setind 4521
[Apostol] p. 18	Theorem I.1	addcan 8099  addcan2d 8104  addcan2i 8102  addcand 8103  addcani 8101
[Apostol] p. 18	Theorem I.2	negeu 8110
[Apostol] p. 18	Theorem I.3	negsub 8167  negsubd 8236  negsubi 8197
[Apostol] p. 18	Theorem I.4	negneg 8169  negnegd 8221  negnegi 8189
[Apostol] p. 18	Theorem I.5	subdi 8304  subdid 8333  subdii 8326  subdir 8305  subdird 8334  subdiri 8327
[Apostol] p. 18	Theorem I.6	mul01 8308  mul01d 8312  mul01i 8310  mul02 8306  mul02d 8311  mul02i 8309
[Apostol] p. 18	Theorem I.9	divrecapd 8710
[Apostol] p. 18	Theorem I.10	recrecapi 8661
[Apostol] p. 18	Theorem I.12	mul2neg 8317  mul2negd 8332  mul2negi 8325  mulneg1 8314  mulneg1d 8330  mulneg1i 8323
[Apostol] p. 18	Theorem I.15	divdivdivap 8630
[Apostol] p. 20	Axiom 7	rpaddcl 9634  rpaddcld 9669  rpmulcl 9635  rpmulcld 9670
[Apostol] p. 20	Axiom 9	0nrp 9646
[Apostol] p. 20	Theorem I.17	lttri 8024
[Apostol] p. 20	Theorem I.18	ltadd1d 8457  ltadd1dd 8475  ltadd1i 8421
[Apostol] p. 20	Theorem I.19	ltmul1 8511  ltmul1a 8510  ltmul1i 8836  ltmul1ii 8844  ltmul2 8772  ltmul2d 9696  ltmul2dd 9710  ltmul2i 8839
[Apostol] p. 20	Theorem I.21	0lt1 8046
[Apostol] p. 20	Theorem I.23	lt0neg1 8387  lt0neg1d 8434  ltneg 8381  ltnegd 8442  ltnegi 8412
[Apostol] p. 20	Theorem I.25	lt2add 8364  lt2addd 8486  lt2addi 8429
[Apostol] p. 20	Definition of positive numbers	df-rp 9611
[Apostol] p. 21	Exercise 4	recgt0 8766  recgt0d 8850  recgt0i 8822  recgt0ii 8823
[Apostol] p. 22	Definition of integers	df-z 9213
[Apostol] p. 22	Definition of rationals	df-q 9579
[Apostol] p. 24	Theorem I.26	supeuti 6971
[Apostol] p. 26	Theorem I.29	arch 9132
[Apostol] p. 28	Exercise 2	btwnz 9331
[Apostol] p. 28	Exercise 3	nnrecl 9133
[Apostol] p. 28	Exercise 6	qbtwnre 10213
[Apostol] p. 28	Exercise 10(a)	zeneo 11830  zneo 9313
[Apostol] p. 29	Theorem I.35	resqrtth 10995  sqrtthi 11083
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8881
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 11991
[Apostol] p. 363	Remark	absgt0api 11110
[Apostol] p. 363	Example	abssubd 11157  abssubi 11114
[ApostolNT] p. 14	Definition	df-dvds 11750
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11766
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11790
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11786
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11780
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11782
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11767
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11768
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11773
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11805
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11807
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11809
[ApostolNT] p. 15	Definition	dfgcd2 11969
[ApostolNT] p. 16	Definition	isprm2 12071
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12046
[ApostolNT] p. 16	Theorem 1.7	prminf 12410
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11928
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11970
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 11972
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11942
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11935
[ApostolNT] p. 17	Theorem 1.8	coprm 12098
[ApostolNT] p. 17	Theorem 1.9	euclemma 12100
[ApostolNT] p. 17	Theorem 1.10	1arith2 12320
[ApostolNT] p. 19	Theorem 1.14	divalg 11883
[ApostolNT] p. 20	Theorem 1.15	eucalg 12013
[ApostolNT] p. 25	Definition	df-phi 12165
[ApostolNT] p. 26	Theorem 2.2	phisum 12194
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12176
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12180
[ApostolNT] p. 104	Definition	congr 12054
[ApostolNT] p. 106	Remark	dvdsval3 11753
[ApostolNT] p. 106	Definition	moddvds 11761
[ApostolNT] p. 107	Example 2	mod2eq0even 11837
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11838
[ApostolNT] p. 107	Example 4	zmod1congr 10297
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10334
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10602
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11785
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12057
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12059
[ApostolNT] p. 113	Theorem 5.17	eulerth 12187
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12205
[ApostolNT] p. 114	Theorem 5.19	fermltl 12188
[ApostolNT] p. 179	Definition	df-lgs 13693  lgsprme0 13737
[ApostolNT] p. 180	Example 1	1lgs 13738
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 13714
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 13729
[ApostolNT] p. 188	Definition	df-lgs 13693  lgs1 13739
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 13730
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 13732
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 13740
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 13741
[Bauer] p. 482	Section 1.2	pm2.01 611  pm2.65 654
[Bauer] p. 483	Theorem 1.3	acexmid 5852  onsucelsucexmidlem 4513
[Bauer], p. 481	Section 1.1	pwtrufal 14030
[Bauer], p. 483	Definition	n0rf 3427
[Bauer], p. 483	Theorem 1.2	2irrexpq 13688  2irrexpqap 13690
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6854
[Bauer], p. 494	Theorem 5.5	ivthinc 13415
[BauerHanson], p. 27	Proposition 5.2	cnstab 8564
[BauerSwan], p. 14	Remark	0ct 7084  ctm 7086
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 14034
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7092
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7463
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7376
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7465
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7499  addlocpr 7498
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7525
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7528
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7533
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2022
[BellMachover] p. 460	Notation	df-mo 2023
[BellMachover] p. 460	Definition	mo3 2073  mo3h 2072
[BellMachover] p. 462	Theorem 1.1	bm1.1 2155
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4110
[BellMachover] p. 466	Axiom Pow	axpow3 4163
[BellMachover] p. 466	Axiom Union	axun2 4420
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4526
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4369
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4529
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4480
[BellMachover] p. 471	Definition of Lim	df-ilim 4354
[BellMachover] p. 472	Axiom Inf	zfinf2 4573
[BellMachover] p. 473	Theorem 2.8	limom 4598
[Bobzien] p. 116	Statement T3	stoic3 1424
[Bobzien] p. 117	Statement T2	stoic2a 1422
[Bobzien] p. 117	Statement T4	stoic4a 1425
[BourbakiAlg1] p. 1	Definition 1	df-mgm 12610
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 12643
[BourbakiAlg1] p. 12	Definition 2	df-mnd 12653
[BourbakiEns] p.	Proposition 8	fcof1 5762  fcofo 5763
[BourbakiTop1] p.	Remark	xnegmnf 9786  xnegpnf 9785
[BourbakiTop1] p.	Remark	rexneg 9787
[BourbakiTop1] p.	Proposition	ishmeo 13098
[BourbakiTop1] p.	Property V_i	ssnei2 12951
[BourbakiTop1] p.	Property V_ii	innei 12957
[BourbakiTop1] p.	Property V_iv	neissex 12959
[BourbakiTop1] p.	Proposition 1	neipsm 12948  neiss 12944
[BourbakiTop1] p.	Proposition 2	cnptopco 13016
[BourbakiTop1] p.	Proposition 4	imasnopn 13093
[BourbakiTop1] p.	Property V_iii	elnei 12946
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 12790
[Bruck] p. 1	Section I.1	df-mgm 12610
[Bruck] p. 23	Section II.1	df-sgrp 12643
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4052
[Cohen] p. 301	Remark	relogoprlem 13583
[Cohen] p. 301	Property 2	relogmul 13584  relogmuld 13599
[Cohen] p. 301	Property 3	relogdiv 13585  relogdivd 13600
[Cohen] p. 301	Property 4	relogexp 13587
[Cohen] p. 301	Property 1a	log1 13581
[Cohen] p. 301	Property 1b	loge 13582
[Cohen4] p. 348	Observation	relogbcxpbap 13677
[Cohen4] p. 352	Definition	rpelogb 13661
[Cohen4] p. 361	Property 2	rprelogbmul 13667
[Cohen4] p. 361	Property 3	logbrec 13672  rprelogbdiv 13669
[Cohen4] p. 361	Property 4	rplogbreexp 13665
[Cohen4] p. 361	Property 6	relogbexpap 13670
[Cohen4] p. 361	Property 1(a)	rplogbid1 13659
[Cohen4] p. 361	Property 1(b)	rplogb1 13660
[Cohen4] p. 367	Property	rplogbchbase 13662
[Cohen4] p. 377	Property 2	logblt 13674
[Crosilla] p.	Axiom 1	ax-ext 2152
[Crosilla] p.	Axiom 2	ax-pr 4194
[Crosilla] p.	Axiom 3	ax-un 4418
[Crosilla] p.	Axiom 4	ax-nul 4115
[Crosilla] p.	Axiom 5	ax-iinf 4572
[Crosilla] p.	Axiom 6	ru 2954
[Crosilla] p.	Axiom 8	ax-pow 4160
[Crosilla] p.	Axiom 9	ax-setind 4521
[Crosilla], p.	Axiom 6	ax-sep 4107
[Crosilla], p.	Axiom 7	ax-coll 4104
[Crosilla], p.	Axiom 7'	repizf 4105
[Crosilla], p.	Theorem is stated	ordtriexmid 4505
[Crosilla], p.	Axiom of choice implies instances	acexmid 5852
[Crosilla], p.	Definition of ordinal	df-iord 4351
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4519
[Eisenberg] p. 67	Definition 5.3	df-dif 3123
[Eisenberg] p. 82	Definition 6.3	df-iom 4575
[Eisenberg] p. 125	Definition 8.21	df-map 6628
[Enderton] p. 18	Axiom of Empty Set	axnul 4114
[Enderton] p. 19	Definition	df-tp 3591
[Enderton] p. 26	Exercise 5	unissb 3826
[Enderton] p. 26	Exercise 10	pwel 4203
[Enderton] p. 28	Exercise 7(b)	pwunim 4271
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3942  iinin2m 3941  iunin1 3937  iunin2 3936
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3940  iundif2ss 3938
[Enderton] p. 33	Exercise 23	iinuniss 3955
[Enderton] p. 33	Exercise 25	iununir 3956
[Enderton] p. 33	Exercise 24(a)	iinpw 3963
[Enderton] p. 33	Exercise 24(b)	iunpw 4465  iunpwss 3964
[Enderton] p. 38	Exercise 6(a)	unipw 4202
[Enderton] p. 38	Exercise 6(b)	pwuni 4178
[Enderton] p. 41	Lemma 3D	opeluu 4435  rnex 4878  rnexg 4876
[Enderton] p. 41	Exercise 8	dmuni 4821  rnuni 5022
[Enderton] p. 42	Definition of a function	dffun7 5225  dffun8 5226
[Enderton] p. 43	Definition of function value	funfvdm2 5560
[Enderton] p. 43	Definition of single-rooted	funcnv 5259
[Enderton] p. 44	Definition (d)	dfima2 4955  dfima3 4956
[Enderton] p. 47	Theorem 3H	fvco2 5565
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7183
[Enderton] p. 50	Theorem 3K(a)	imauni 5740
[Enderton] p. 52	Definition	df-map 6628
[Enderton] p. 53	Exercise 21	coass 5129
[Enderton] p. 53	Exercise 27	dmco 5119
[Enderton] p. 53	Exercise 14(a)	funin 5269
[Enderton] p. 53	Exercise 22(a)	imass2 4987
[Enderton] p. 54	Remark	ixpf 6698  ixpssmap 6710
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6677
[Enderton] p. 56	Theorem 3M	erref 6533
[Enderton] p. 57	Lemma 3N	erthi 6559
[Enderton] p. 57	Definition	df-ec 6515
[Enderton] p. 58	Definition	df-qs 6519
[Enderton] p. 60	Theorem 3Q	th3q 6618  th3qcor 6617  th3qlem1 6615  th3qlem2 6616
[Enderton] p. 61	Exercise 35	df-ec 6515
[Enderton] p. 65	Exercise 56(a)	dmun 4818
[Enderton] p. 68	Definition of successor	df-suc 4356
[Enderton] p. 71	Definition	df-tr 4088  dftr4 4092
[Enderton] p. 72	Theorem 4E	unisuc 4398  unisucg 4399
[Enderton] p. 73	Exercise 6	unisuc 4398  unisucg 4399
[Enderton] p. 73	Exercise 5(a)	truni 4101
[Enderton] p. 73	Exercise 5(b)	trint 4102
[Enderton] p. 79	Theorem 4I(A1)	nna0 6453
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6455  onasuc 6445
[Enderton] p. 79	Definition of operation value	df-ov 5856
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6454
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6456  onmsuc 6452
[Enderton] p. 81	Theorem 4K(1)	nnaass 6464
[Enderton] p. 81	Theorem 4K(2)	nna0r 6457  nnacom 6463
[Enderton] p. 81	Theorem 4K(3)	nndi 6465
[Enderton] p. 81	Theorem 4K(4)	nnmass 6466
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6468
[Enderton] p. 82	Exercise 16	nnm0r 6458  nnmsucr 6467
[Enderton] p. 88	Exercise 23	nnaordex 6507
[Enderton] p. 129	Definition	df-en 6719
[Enderton] p. 132	Theorem 6B(b)	canth 5807
[Enderton] p. 133	Exercise 1	xpomen 12350
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6843
[Enderton] p. 136	Corollary 6E	nneneq 6835
[Enderton] p. 139	Theorem 6H(c)	mapen 6824
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7195
[Enderton] p. 143	Theorem 6J	dju0en 7191  dju1en 7190
[Enderton] p. 144	Corollary 6K	undif2ss 3490
[Enderton] p. 145	Figure 38	ffoss 5474
[Enderton] p. 145	Definition	df-dom 6720
[Enderton] p. 146	Example 1	domen 6729  domeng 6730
[Enderton] p. 146	Example 3	nndomo 6842
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6813  xpdom1g 6811  xpdom2g 6810
[Enderton] p. 168	Definition	df-po 4281
[Enderton] p. 192	Theorem 7M(a)	oneli 4413
[Enderton] p. 192	Theorem 7M(b)	ontr1 4374
[Enderton] p. 192	Theorem 7M(c)	onirri 4527
[Enderton] p. 193	Corollary 7N(b)	0elon 4377
[Enderton] p. 193	Corollary 7N(c)	onsuci 4500
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4473
[Enderton] p. 194	Remark	onprc 4536
[Enderton] p. 194	Exercise 16	suc11 4542
[Enderton] p. 197	Definition	df-card 7157
[Enderton] p. 200	Exercise 25	tfis 4567
[Enderton] p. 206	Theorem 7X(b)	en2lp 4538
[Enderton] p. 207	Exercise 34	opthreg 4540
[Enderton] p. 208	Exercise 35	suc11g 4541
[Geuvers], p. 1	Remark	expap0 10506
[Geuvers], p. 6	Lemma 2.13	mulap0r 8534
[Geuvers], p. 6	Lemma 2.15	mulap0 8572
[Geuvers], p. 9	Lemma 2.35	msqge0 8535
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7893
[Geuvers], p. 10	Lemma 3.9	maxcom 11167
[Geuvers], p. 10	Lemma 3.10	maxle1 11175  maxle2 11176
[Geuvers], p. 10	Lemma 3.11	maxleast 11177
[Geuvers], p. 10	Lemma 3.12	maxleb 11180
[Geuvers], p. 11	Definition 3.13	dfabsmax 11181
[Geuvers], p. 17	Definition 6.1	df-ap 8501
[Gleason] p. 117	Proposition 9-2.1	df-enq 7309  enqer 7320
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7313  df-nqqs 7310
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7306  df-plqqs 7311
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7307  df-mqqs 7312
[Gleason] p. 119	Proposition 9-2.5	df-rq 7314
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7370
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7373  ltbtwnnq 7378  ltbtwnnqq 7377
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7362
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7363
[Gleason] p. 123	Proposition 9-3.5	addclpr 7499
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7541
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7540
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7559
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7575
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7581  ltaprlem 7580
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7578
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7534
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7554
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7543
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7542
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7550
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7600
[Gleason] p. 126	Proposition 9-4.1	df-enr 7688  enrer 7697
[Gleason] p. 126	Proposition 9-4.2	df-0r 7693  df-1r 7694  df-nr 7689
[Gleason] p. 126	Proposition 9-4.3	df-mr 7691  df-plr 7690  negexsr 7734  recexsrlem 7736
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7692
[Gleason] p. 130	Proposition 10-1.3	creui 8876  creur 8875  cru 8521
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7885  axcnre 7843
[Gleason] p. 132	Definition 10-3.1	crim 10822  crimd 10941  crimi 10901  crre 10821  crred 10940  crrei 10900
[Gleason] p. 132	Definition 10-3.2	remim 10824  remimd 10906
[Gleason] p. 133	Definition 10.36	absval2 11021  absval2d 11149  absval2i 11108
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10848  cjaddd 10929  cjaddi 10896
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10849  cjmuld 10930  cjmuli 10897
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10847  cjcjd 10907  cjcji 10879
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10846  cjreb 10830  cjrebd 10910  cjrebi 10882  cjred 10935  rere 10829  rereb 10827  rerebd 10909  rerebi 10881  rered 10933
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10855  addcjd 10921  addcji 10891
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10965
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11016  abscjd 11154  abscji 11112
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11028  abs00d 11150  abs00i 11109  absne0d 11151
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11060  releabsd 11155  releabsi 11113
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11033  absmuld 11158  absmuli 11115
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11019  sqabsaddi 11116
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11068  abstrid 11160  abstrii 11119
[Gleason] p. 134	Definition 10-4.1	df-exp 10476  exp0 10480  expp1 10483  expp1d 10610
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10518  expaddd 10611
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 13627  cxpmuld 13650  expmul 10521  expmuld 10612
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10515  mulexpd 10624  rpmulcxp 13624
[Gleason] p. 141	Definition 11-2.1	fzval 9967
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11289
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11291
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11290
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11294
[Gleason] p. 172	Corollary 12-2.5	climrecl 11287
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11283  climcj 11284  climim 11286  climre 11285
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7959  df-xr 7958  ltxr 9732
[Gleason] p. 180	Theorem 12-5.3	climcau 11310
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10256
[Gleason] p. 223	Definition 14-1.1	df-met 12783
[Gleason] p. 223	Definition 14-1.1(a)	met0 13158  xmet0 13157
[Gleason] p. 223	Definition 14-1.1(c)	metsym 13165
[Gleason] p. 223	Definition 14-1.1(d)	mettri 13167  mstri 13267  xmettri 13166  xmstri 13266
[Gleason] p. 230	Proposition 14-2.6	txlm 13073
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13305
[Gleason] p. 243	Proposition 14-4.16	addcn2 11273  addcncntop 13346  mulcn2 11275  mulcncntop 13348  subcn2 11274  subcncntop 13347
[Gleason] p. 295	Remark	bcval3 10685  bcval4 10686
[Gleason] p. 295	Equation 2	bcpasc 10700
[Gleason] p. 295	Definition of binomial coefficient	bcval 10683  df-bc 10682
[Gleason] p. 296	Remark	bcn0 10689  bcnn 10691
[Gleason] p. 296	Theorem 15-2.8	binom 11447
[Gleason] p. 308	Equation 2	ef0 11635
[Gleason] p. 308	Equation 3	efcj 11636
[Gleason] p. 309	Corollary 15-4.3	efne0 11641
[Gleason] p. 309	Corollary 15-4.4	efexp 11645
[Gleason] p. 310	Equation 14	sinadd 11699
[Gleason] p. 310	Equation 15	cosadd 11700
[Gleason] p. 311	Equation 17	sincossq 11711
[Gleason] p. 311	Equation 18	cosbnd 11716  sinbnd 11715
[Gleason] p. 311	Definition of ` `	df-pi 11616
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1442
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 12719  mndideu 12662
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 12741
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 12766
[Heyting] p. 127	Axiom #1	ax1hfs 14103
[Hitchcock] p. 5	Rule A3	mptnan 1418
[Hitchcock] p. 5	Rule A4	mptxor 1419
[Hitchcock] p. 5	Rule A5	mtpxor 1421
[HoTT], p.	Lemma 10.4.1	exmidontriim 7202
[HoTT], p.	Theorem 7.2.6	nndceq 6478
[HoTT], p.	Exercise 11.10	neapmkv 14099
[HoTT], p.	Exercise 11.11	mulap0bd 8575
[HoTT], p.	Section 11.2.1	df-iltp 7432  df-imp 7431  df-iplp 7430  df-reap 8494
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7624
[HoTT], p.	Corollary 11.4.3	conventions 13756
[HoTT], p.	Exercise 11.6(i)	dcapnconst 14092  dceqnconst 14091
[HoTT], p.	Corollary 11.2.13	axcaucvg 7862  caucvgpr 7644  caucvgprpr 7674  caucvgsr 7764
[HoTT], p.	Definition 11.2.1	df-inp 7428
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 14097
[HoTT], p.	Proposition 11.2.3	df-iso 4282  ltpopr 7557  ltsopr 7558
[HoTT], p.	Definition 11.2.7(v)	apsym 8525  reapcotr 8517  reapirr 8496
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8046  gt0add 8492  leadd1 8349  lelttr 8008  lemul1a 8774  lenlt 7995  ltadd1 8348  ltletr 8009  ltmul1 8511  reaplt 8507
[Jech] p. 4	Definition of class	cv 1347  cvjust 2165
[Jech] p. 78	Note	opthprc 4662
[KalishMontague] p. 81	Note 1	ax-i9 1523
[Kreyszig] p. 3	Property M1	metcl 13147  xmetcl 13146
[Kreyszig] p. 4	Property M2	meteq0 13154
[Kreyszig] p. 12	Equation 5	muleqadd 8586
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13236
[Kreyszig] p. 19	Remark	mopntopon 13237
[Kreyszig] p. 19	Theorem T1	mopn0 13282  mopnm 13242
[Kreyszig] p. 19	Theorem T2	unimopn 13280
[Kreyszig] p. 19	Definition of neighborhood	neibl 13285
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13307
[Kreyszig] p. 25	Definition 1.4-1	lmbr 13007
[Kunen] p. 10	Axiom 0	a9e 1689
[Kunen] p. 12	Axiom 6	zfrep6 4106
[Kunen] p. 24	Definition 10.24	mapval 6638  mapvalg 6636
[Kunen] p. 31	Definition 10.24	mapex 6632
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3883
[Lang] p. 3	Statement	lidrideqd 12635  mndbn0 12667
[Lang] p. 3	Definition	df-mnd 12653
[Lang] p. 7	Definition	dfgrp2e 12733
[Levy] p. 338	Axiom	df-clab 2157  df-clel 2166  df-cleq 2163
[Lopez-Astorga] p. 12	Rule 1	mptnan 1418
[Lopez-Astorga] p. 12	Rule 2	mptxor 1419
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1421
[Margaris] p. 40	Rule C	exlimiv 1591
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 848
[Margaris] p. 49	Definition	dfbi2 386  dfordc 887  exalim 1495
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 646
[Margaris] p. 89	Theorem 19.2	19.2 1631  r19.2m 3501
[Margaris] p. 89	Theorem 19.3	19.3 1547  19.3h 1546  rr19.3v 2869
[Margaris] p. 89	Theorem 19.5	alcom 1471
[Margaris] p. 89	Theorem 19.6	alexdc 1612  alexim 1638
[Margaris] p. 89	Theorem 19.7	alnex 1492
[Margaris] p. 89	Theorem 19.8	19.8a 1583  spsbe 1835
[Margaris] p. 89	Theorem 19.9	19.9 1637  19.9h 1636  19.9v 1864  exlimd 1590
[Margaris] p. 89	Theorem 19.11	excom 1657  excomim 1656
[Margaris] p. 89	Theorem 19.12	19.12 1658  r19.12 2576
[Margaris] p. 90	Theorem 19.14	exnalim 1639
[Margaris] p. 90	Theorem 19.15	albi 1461  ralbi 2602
[Margaris] p. 90	Theorem 19.16	19.16 1548
[Margaris] p. 90	Theorem 19.17	19.17 1549
[Margaris] p. 90	Theorem 19.18	exbi 1597  rexbi 2603
[Margaris] p. 90	Theorem 19.19	19.19 1659
[Margaris] p. 90	Theorem 19.20	alim 1450  alimd 1514  alimdh 1460  alimdv 1872  ralimdaa 2536  ralimdv 2538  ralimdva 2537  ralimdvva 2539  sbcimdv 3020
[Margaris] p. 90	Theorem 19.21	19.21-2 1660  19.21 1576  19.21bi 1551  19.21h 1550  19.21ht 1574  19.21t 1575  19.21v 1866  alrimd 1603  alrimdd 1602  alrimdh 1472  alrimdv 1869  alrimi 1515  alrimih 1462  alrimiv 1867  alrimivv 1868  r19.21 2546  r19.21be 2561  r19.21bi 2558  r19.21t 2545  r19.21v 2547  ralrimd 2548  ralrimdv 2549  ralrimdva 2550  ralrimdvv 2554  ralrimdvva 2555  ralrimi 2541  ralrimiv 2542  ralrimiva 2543  ralrimivv 2551  ralrimivva 2552  ralrimivvva 2553  ralrimivw 2544  rexlimi 2580
[Margaris] p. 90	Theorem 19.22	2alimdv 1874  2eximdv 1875  exim 1592  eximd 1605  eximdh 1604  eximdv 1873  rexim 2564  reximdai 2568  reximddv 2573  reximddv2 2575  reximdv 2571  reximdv2 2569  reximdva 2572  reximdvai 2570  reximi2 2566
[Margaris] p. 90	Theorem 19.23	19.23 1671  19.23bi 1585  19.23h 1491  19.23ht 1490  19.23t 1670  19.23v 1876  19.23vv 1877  exlimd2 1588  exlimdh 1589  exlimdv 1812  exlimdvv 1890  exlimi 1587  exlimih 1586  exlimiv 1591  exlimivv 1889  r19.23 2578  r19.23v 2579  rexlimd 2584  rexlimdv 2586  rexlimdv3a 2589  rexlimdva 2587  rexlimdva2 2590  rexlimdvaa 2588  rexlimdvv 2594  rexlimdvva 2595  rexlimdvw 2591  rexlimiv 2581  rexlimiva 2582  rexlimivv 2593
[Margaris] p. 90	Theorem 19.24	i19.24 1632
[Margaris] p. 90	Theorem 19.25	19.25 1619
[Margaris] p. 90	Theorem 19.26	19.26-2 1475  19.26-3an 1476  19.26 1474  r19.26-2 2599  r19.26-3 2600  r19.26 2596  r19.26m 2601
[Margaris] p. 90	Theorem 19.27	19.27 1554  19.27h 1553  19.27v 1892  r19.27av 2605  r19.27m 3510  r19.27mv 3511
[Margaris] p. 90	Theorem 19.28	19.28 1556  19.28h 1555  19.28v 1893  r19.28av 2606  r19.28m 3504  r19.28mv 3507  rr19.28v 2870
[Margaris] p. 90	Theorem 19.29	19.29 1613  19.29r 1614  19.29r2 1615  19.29x 1616  r19.29 2607  r19.29d2r 2614  r19.29r 2608
[Margaris] p. 90	Theorem 19.30	19.30dc 1620
[Margaris] p. 90	Theorem 19.31	19.31r 1674
[Margaris] p. 90	Theorem 19.32	19.32dc 1672  19.32r 1673  r19.32r 2616  r19.32vdc 2619  r19.32vr 2618
[Margaris] p. 90	Theorem 19.33	19.33 1477  19.33b2 1622  19.33bdc 1623
[Margaris] p. 90	Theorem 19.34	19.34 1677
[Margaris] p. 90	Theorem 19.35	19.35-1 1617  19.35i 1618
[Margaris] p. 90	Theorem 19.36	19.36-1 1666  19.36aiv 1894  19.36i 1665  r19.36av 2621
[Margaris] p. 90	Theorem 19.37	19.37-1 1667  19.37aiv 1668  r19.37 2622  r19.37av 2623
[Margaris] p. 90	Theorem 19.38	19.38 1669
[Margaris] p. 90	Theorem 19.39	i19.39 1633
[Margaris] p. 90	Theorem 19.40	19.40-2 1625  19.40 1624  r19.40 2624
[Margaris] p. 90	Theorem 19.41	19.41 1679  19.41h 1678  19.41v 1895  19.41vv 1896  19.41vvv 1897  19.41vvvv 1898  r19.41 2625  r19.41v 2626
[Margaris] p. 90	Theorem 19.42	19.42 1681  19.42h 1680  19.42v 1899  19.42vv 1904  19.42vvv 1905  19.42vvvv 1906  r19.42v 2627
[Margaris] p. 90	Theorem 19.43	19.43 1621  r19.43 2628
[Margaris] p. 90	Theorem 19.44	19.44 1675  r19.44av 2629  r19.44mv 3509
[Margaris] p. 90	Theorem 19.45	19.45 1676  r19.45av 2630  r19.45mv 3508
[Margaris] p. 110	Exercise 2(b)	eu1 2044
[Megill] p. 444	Axiom C5	ax-17 1519
[Megill] p. 445	Lemma L12	alequcom 1508  ax-10 1498
[Megill] p. 446	Lemma L17	equtrr 1703
[Megill] p. 446	Lemma L19	hbnae 1714
[Megill] p. 447	Remark 9.1	df-sb 1756  sbid 1767
[Megill] p. 448	Scheme C5'	ax-4 1503
[Megill] p. 448	Scheme C6'	ax-7 1441
[Megill] p. 448	Scheme C8'	ax-8 1497
[Megill] p. 448	Scheme C9'	ax-i12 1500
[Megill] p. 448	Scheme C11'	ax-10o 1709
[Megill] p. 448	Scheme C12'	ax-13 2143
[Megill] p. 448	Scheme C13'	ax-14 2144
[Megill] p. 448	Scheme C15'	ax-11o 1816
[Megill] p. 448	Scheme C16'	ax-16 1807
[Megill] p. 448	Theorem 9.4	dral1 1723  dral2 1724  drex1 1791  drex2 1725  drsb1 1792  drsb2 1834
[Megill] p. 449	Theorem 9.7	sbcom2 1980  sbequ 1833  sbid2v 1989
[Megill] p. 450	Example in Appendix	hba1 1533
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3037  rspsbca 3038  stdpc4 1768
[Mendelson] p. 69	Axiom 5	ra5 3043  stdpc5 1577
[Mendelson] p. 81	Rule C	exlimiv 1591
[Mendelson] p. 95	Axiom 6	stdpc6 1696
[Mendelson] p. 95	Axiom 7	stdpc7 1763
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3451
[Mendelson] p. 231	Exercise 4.10(l)	unv 3452
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3367
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3415
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3368
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3258
[Mendelson] p. 231	Definition of union	unssin 3366
[Mendelson] p. 235	Exercise 4.12(c)	univ 4461
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3795
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4267
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4268
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4269
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3816
[Mendelson] p. 235	Exercise 4.12(p)	reli 4740
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5131
[Mendelson] p. 246	Definition of successor	df-suc 4356
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6823
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6799  xpsneng 6800
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6805  xpcomeng 6806
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6808
[Mendelson] p. 255	Exercise 4.39	endisj 6802
[Mendelson] p. 255	Exercise 4.41	mapprc 6630
[Mendelson] p. 255	Exercise 4.43	mapsnen 6789
[Mendelson] p. 255	Exercise 4.47	xpmapen 6828
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6664
[Mendelson] p. 255	Exercise 4.42(b)	map1 6790
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7194  djucomen 7193
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7192
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6446
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3349
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4699
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4700
[Monk1] p. 34	Definition 3.3	df-opab 4051
[Monk1] p. 36	Theorem 3.7(i)	coi1 5126  coi2 5127
[Monk1] p. 36	Theorem 3.8(v)	dm0 4825  rn0 4867
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5015
[Monk1] p. 37	Theorem 3.13(i)	relxp 4720
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4831  rnxpm 5040
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4691  xp0 5030
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4970
[Monk1] p. 38	Theorem 3.16(viii)	imai 4967
[Monk1] p. 39	Theorem 3.17	imaex 4966  imaexg 4965
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4964
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5626  funfvop 5608
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5540
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5548
[Monk1] p. 43	Theorem 4.6	funun 5242
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5747  dff13f 5749
[Monk1] p. 46	Theorem 4.15(v)	funex 5719  funrnex 6093
[Monk1] p. 50	Definition 5.4	fniunfv 5741
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5094
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3847
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6134  df-1st 6119
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6135  df-2nd 6120
[Monk2] p. 105	Axiom C4	ax-5 1440
[Monk2] p. 105	Axiom C7	ax-8 1497
[Monk2] p. 105	Axiom C8	ax-11 1499  ax-11o 1816
[Monk2] p. 105	Axiom (C8)	ax11v 1820
[Monk2] p. 109	Lemma 12	ax-7 1441
[Monk2] p. 109	Lemma 15	equvin 1856  equvini 1751  eqvinop 4228
[Monk2] p. 113	Axiom C5-1	ax-17 1519
[Monk2] p. 113	Axiom C5-2	ax6b 1644
[Monk2] p. 113	Axiom C5-3	ax-7 1441
[Monk2] p. 114	Lemma 22	hba1 1533
[Monk2] p. 114	Lemma 23	hbia1 1545  nfia1 1573
[Monk2] p. 114	Lemma 24	hba2 1544  nfa2 1572
[Moschovakis] p. 2	Chapter 2	df-stab 826  dftest 14104
[Munkres] p. 77	Example 2	distop 12879
[Munkres] p. 78	Definition of basis	df-bases 12835  isbasis3g 12838
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12600  tgval2 12845
[Munkres] p. 79	Remark	tgcl 12858
[Munkres] p. 80	Lemma 2.1	tgval3 12852
[Munkres] p. 80	Lemma 2.2	tgss2 12873  tgss3 12872
[Munkres] p. 81	Lemma 2.3	basgen 12874  basgen2 12875
[Munkres] p. 89	Definition of subspace topology	resttop 12964
[Munkres] p. 93	Theorem 6.1(1)	0cld 12906  topcld 12903
[Munkres] p. 93	Theorem 6.1(3)	uncld 12907
[Munkres] p. 94	Definition of closure	clsval 12905
[Munkres] p. 94	Definition of interior	ntrval 12904
[Munkres] p. 102	Definition of continuous function	df-cn 12982  iscn 12991  iscn2 12994
[Munkres] p. 107	Theorem 7.2(g)	cncnp 13024  cncnp2m 13025  cncnpi 13022  df-cnp 12983  iscnp 12993
[Munkres] p. 127	Theorem 10.1	metcn 13308
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6881
[Pierik], p. 9	Definition 2.4	df-womni 7140
[Pierik], p. 9	Definition 2.5	df-markov 7128  omniwomnimkv 7143
[Pierik], p. 10	Section 2.3	dfdif3 3237
[Pierik], p. 14	Definition 3.1	df-omni 7111  exmidomniim 7117  finomni 7116
[Pierik], p. 15	Section 3.1	df-nninf 7097
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 14055
[PradicBrown2022], p. 2	Remark	exmidpw 6886
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7178
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7179  exmidfodomrlemrALT 7180
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7125
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 14040  peano4nninf 14039
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 14042
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 14050
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 14052
[PradicBrown2022], p. 5	Definition 3.3	nnsf 14038
[Quine] p. 16	Definition 2.1	df-clab 2157  rabid 2645
[Quine] p. 17	Definition 2.1''	dfsb7 1984
[Quine] p. 18	Definition 2.7	df-cleq 2163
[Quine] p. 19	Definition 2.9	df-v 2732
[Quine] p. 34	Theorem 5.1	abeq2 2279
[Quine] p. 35	Theorem 5.2	abid2 2291  abid2f 2338
[Quine] p. 40	Theorem 6.1	sb5 1880
[Quine] p. 40	Theorem 6.2	sb56 1878  sb6 1879
[Quine] p. 41	Theorem 6.3	df-clel 2166
[Quine] p. 41	Theorem 6.4	eqid 2170
[Quine] p. 41	Theorem 6.5	eqcom 2172
[Quine] p. 42	Theorem 6.6	df-sbc 2956
[Quine] p. 42	Theorem 6.7	dfsbcq 2957  dfsbcq2 2958
[Quine] p. 43	Theorem 6.8	vex 2733
[Quine] p. 43	Theorem 6.9	isset 2736
[Quine] p. 44	Theorem 7.3	spcgf 2812  spcgv 2817  spcimgf 2810
[Quine] p. 44	Theorem 6.11	spsbc 2966  spsbcd 2967
[Quine] p. 44	Theorem 6.12	elex 2741
[Quine] p. 44	Theorem 6.13	elab 2874  elabg 2876  elabgf 2872
[Quine] p. 44	Theorem 6.14	noel 3418
[Quine] p. 48	Theorem 7.2	snprc 3648
[Quine] p. 48	Definition 7.1	df-pr 3590  df-sn 3589
[Quine] p. 49	Theorem 7.4	snss 3709  snssg 3716
[Quine] p. 49	Theorem 7.5	prss 3736  prssg 3737
[Quine] p. 49	Theorem 7.6	prid1 3689  prid1g 3687  prid2 3690  prid2g 3688  snid 3614  snidg 3612
[Quine] p. 51	Theorem 7.12	snexg 4170  snexprc 4172
[Quine] p. 51	Theorem 7.13	prexg 4196
[Quine] p. 53	Theorem 8.2	unisn 3812  unisng 3813
[Quine] p. 53	Theorem 8.3	uniun 3815
[Quine] p. 54	Theorem 8.6	elssuni 3824
[Quine] p. 54	Theorem 8.7	uni0 3823
[Quine] p. 56	Theorem 8.17	uniabio 5170
[Quine] p. 56	Definition 8.18	dfiota2 5161
[Quine] p. 57	Theorem 8.19	iotaval 5171
[Quine] p. 57	Theorem 8.22	iotanul 5175
[Quine] p. 58	Theorem 8.23	euiotaex 5176
[Quine] p. 58	Definition 9.1	df-op 3592
[Quine] p. 61	Theorem 9.5	opabid 4242  opelopab 4256  opelopaba 4251  opelopabaf 4258  opelopabf 4259  opelopabg 4253  opelopabga 4248  oprabid 5885
[Quine] p. 64	Definition 9.11	df-xp 4617
[Quine] p. 64	Definition 9.12	df-cnv 4619
[Quine] p. 64	Definition 9.15	df-id 4278
[Quine] p. 65	Theorem 10.3	fun0 5256
[Quine] p. 65	Theorem 10.4	funi 5230
[Quine] p. 65	Theorem 10.5	funsn 5246  funsng 5244
[Quine] p. 65	Definition 10.1	df-fun 5200
[Quine] p. 65	Definition 10.2	args 4980  dffv4g 5493
[Quine] p. 68	Definition 10.11	df-fv 5206  fv2 5491
[Quine] p. 124	Theorem 17.3	nn0opth2 10658  nn0opth2d 10657  nn0opthd 10656
[Quine] p. 284	Axiom 39(vi)	funimaex 5283  funimaexg 5282
[Rudin] p. 164	Equation 27	efcan 11639
[Rudin] p. 164	Equation 30	efzval 11646
[Rudin] p. 167	Equation 48	absefi 11731
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1421
[Sanford] p. 39	Rule 4	mptxor 1419
[Sanford] p. 40	Rule 1	mptnan 1418
[Schechter] p. 51	Definition of antisymmetry	intasym 4995
[Schechter] p. 51	Definition of irreflexivity	intirr 4997
[Schechter] p. 51	Definition of symmetry	cnvsym 4994
[Schechter] p. 51	Definition of transitivity	cotr 4992
[Schechter] p. 428	Definition 15.35	bastop1 12877
[Stoll] p. 13	Definition of symmetric difference	symdif1 3392
[Stoll] p. 16	Exercise 4.4	0dif 3486  dif0 3485
[Stoll] p. 16	Exercise 4.8	difdifdirss 3499
[Stoll] p. 19	Theorem 5.2(13)	undm 3385
[Stoll] p. 19	Theorem 5.2(13')	indmss 3386
[Stoll] p. 20	Remark	invdif 3369
[Stoll] p. 25	Definition of ordered triple	df-ot 3593
[Stoll] p. 43	Definition	uniiun 3926
[Stoll] p. 44	Definition	intiin 3927
[Stoll] p. 45	Definition	df-iin 3876
[Stoll] p. 45	Definition indexed union	df-iun 3875
[Stoll] p. 176	Theorem 3.4(27)	imandc 884  imanst 883
[Stoll] p. 262	Example 4.1	symdif1 3392
[Suppes] p. 22	Theorem 2	eq0 3433
[Suppes] p. 22	Theorem 4	eqss 3162  eqssd 3164  eqssi 3163
[Suppes] p. 23	Theorem 5	ss0 3455  ss0b 3454
[Suppes] p. 23	Theorem 6	sstr 3155
[Suppes] p. 25	Theorem 12	elin 3310  elun 3268
[Suppes] p. 26	Theorem 15	inidm 3336
[Suppes] p. 26	Theorem 16	in0 3449
[Suppes] p. 27	Theorem 23	unidm 3270
[Suppes] p. 27	Theorem 24	un0 3448
[Suppes] p. 27	Theorem 25	ssun1 3290
[Suppes] p. 27	Theorem 26	ssequn1 3297
[Suppes] p. 27	Theorem 27	unss 3301
[Suppes] p. 27	Theorem 28	indir 3376
[Suppes] p. 27	Theorem 29	undir 3377
[Suppes] p. 28	Theorem 32	difid 3483  difidALT 3484
[Suppes] p. 29	Theorem 33	difin 3364
[Suppes] p. 29	Theorem 34	indif 3370
[Suppes] p. 29	Theorem 35	undif1ss 3489
[Suppes] p. 29	Theorem 36	difun2 3494
[Suppes] p. 29	Theorem 37	difin0 3488
[Suppes] p. 29	Theorem 38	disjdif 3487
[Suppes] p. 29	Theorem 39	difundi 3379
[Suppes] p. 29	Theorem 40	difindiss 3381
[Suppes] p. 30	Theorem 41	nalset 4119
[Suppes] p. 39	Theorem 61	uniss 3817
[Suppes] p. 39	Theorem 65	uniop 4240
[Suppes] p. 41	Theorem 70	intsn 3866
[Suppes] p. 42	Theorem 71	intpr 3863  intprg 3864
[Suppes] p. 42	Theorem 73	op1stb 4463  op1stbg 4464
[Suppes] p. 42	Theorem 78	intun 3862
[Suppes] p. 44	Definition 15(a)	dfiun2 3907  dfiun2g 3905
[Suppes] p. 44	Definition 15(b)	dfiin2 3908
[Suppes] p. 47	Theorem 86	elpw 3572  elpw2 4143  elpw2g 4142  elpwg 3574
[Suppes] p. 47	Theorem 87	pwid 3581
[Suppes] p. 47	Theorem 89	pw0 3727
[Suppes] p. 48	Theorem 90	pwpw0ss 3791
[Suppes] p. 52	Theorem 101	xpss12 4718
[Suppes] p. 52	Theorem 102	xpindi 4746  xpindir 4747
[Suppes] p. 52	Theorem 103	xpundi 4667  xpundir 4668
[Suppes] p. 54	Theorem 105	elirrv 4532
[Suppes] p. 58	Theorem 2	relss 4698
[Suppes] p. 59	Theorem 4	eldm 4808  eldm2 4809  eldm2g 4807  eldmg 4806
[Suppes] p. 59	Definition 3	df-dm 4621
[Suppes] p. 60	Theorem 6	dmin 4819
[Suppes] p. 60	Theorem 8	rnun 5019
[Suppes] p. 60	Theorem 9	rnin 5020
[Suppes] p. 60	Definition 4	dfrn2 4799
[Suppes] p. 61	Theorem 11	brcnv 4794  brcnvg 4792
[Suppes] p. 62	Equation 5	elcnv 4788  elcnv2 4789
[Suppes] p. 62	Theorem 12	relcnv 4989
[Suppes] p. 62	Theorem 15	cnvin 5018
[Suppes] p. 62	Theorem 16	cnvun 5016
[Suppes] p. 63	Theorem 20	co02 5124
[Suppes] p. 63	Theorem 21	dmcoss 4880
[Suppes] p. 63	Definition 7	df-co 4620
[Suppes] p. 64	Theorem 26	cnvco 4796
[Suppes] p. 64	Theorem 27	coass 5129
[Suppes] p. 65	Theorem 31	resundi 4904
[Suppes] p. 65	Theorem 34	elima 4958  elima2 4959  elima3 4960  elimag 4957
[Suppes] p. 65	Theorem 35	imaundi 5023
[Suppes] p. 66	Theorem 40	dminss 5025
[Suppes] p. 66	Theorem 41	imainss 5026
[Suppes] p. 67	Exercise 11	cnvxp 5029
[Suppes] p. 81	Definition 34	dfec2 6516
[Suppes] p. 82	Theorem 72	elec 6552  elecg 6551
[Suppes] p. 82	Theorem 73	erth 6557  erth2 6558
[Suppes] p. 89	Theorem 96	map0b 6665
[Suppes] p. 89	Theorem 97	map0 6667  map0g 6666
[Suppes] p. 89	Theorem 98	mapsn 6668
[Suppes] p. 89	Theorem 99	mapss 6669
[Suppes] p. 92	Theorem 1	enref 6743  enrefg 6742
[Suppes] p. 92	Theorem 2	ensym 6759  ensymb 6758  ensymi 6760
[Suppes] p. 92	Theorem 3	entr 6762
[Suppes] p. 92	Theorem 4	unen 6794
[Suppes] p. 94	Theorem 15	endom 6741
[Suppes] p. 94	Theorem 16	ssdomg 6756
[Suppes] p. 94	Theorem 17	domtr 6763
[Suppes] p. 95	Theorem 18	isbth 6944
[Suppes] p. 98	Exercise 4	fundmen 6784  fundmeng 6785
[Suppes] p. 98	Exercise 6	xpdom3m 6812
[Suppes] p. 130	Definition 3	df-tr 4088
[Suppes] p. 132	Theorem 9	ssonuni 4472
[Suppes] p. 134	Definition 6	df-suc 4356
[Suppes] p. 136	Theorem Schema 22	findes 4587  finds 4584  finds1 4586  finds2 4585
[Suppes] p. 162	Definition 5	df-ltnqqs 7315  df-ltpq 7308
[Suppes] p. 228	Theorem Schema 61	onintss 4375
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2152
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2163
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2166
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2165
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2188
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5857
[TakeutiZaring] p. 14	Proposition 4.14	ru 2954
[TakeutiZaring] p. 15	Exercise 1	elpr 3604  elpr2 3605  elprg 3603
[TakeutiZaring] p. 15	Exercise 2	elsn 3599  elsn2 3617  elsn2g 3616  elsng 3598  velsn 3600
[TakeutiZaring] p. 15	Exercise 3	elop 4216
[TakeutiZaring] p. 15	Exercise 4	sneq 3594  sneqr 3747
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3602  dfsn2 3597
[TakeutiZaring] p. 16	Axiom 3	uniex 4422
[TakeutiZaring] p. 16	Exercise 6	opth 4222
[TakeutiZaring] p. 16	Exercise 8	rext 4200
[TakeutiZaring] p. 16	Corollary 5.8	unex 4426  unexg 4428
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3632
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3797
[TakeutiZaring] p. 16	Definition 5.6	df-in 3127  df-un 3125
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3810  uniprg 3811
[TakeutiZaring] p. 17	Axiom 4	vpwex 4165
[TakeutiZaring] p. 17	Exercise 1	eltp 3631
[TakeutiZaring] p. 17	Exercise 5	elsuc 4391  elsucg 4389  sstr2 3154
[TakeutiZaring] p. 17	Exercise 6	uncom 3271
[TakeutiZaring] p. 17	Exercise 7	incom 3319
[TakeutiZaring] p. 17	Exercise 8	unass 3284
[TakeutiZaring] p. 17	Exercise 9	inass 3337
[TakeutiZaring] p. 17	Exercise 10	indi 3374
[TakeutiZaring] p. 17	Exercise 11	undi 3375
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3136
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3568
[TakeutiZaring] p. 18	Exercise 7	unss2 3298
[TakeutiZaring] p. 18	Exercise 9	df-ss 3134  sseqin2 3346
[TakeutiZaring] p. 18	Exercise 10	ssid 3167
[TakeutiZaring] p. 18	Exercise 12	inss1 3347  inss2 3348
[TakeutiZaring] p. 18	Exercise 13	nssr 3207
[TakeutiZaring] p. 18	Exercise 15	unieq 3805
[TakeutiZaring] p. 18	Exercise 18	sspwb 4201
[TakeutiZaring] p. 18	Exercise 19	pweqb 4208
[TakeutiZaring] p. 20	Definition	df-rab 2457
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4116
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3123
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3416
[TakeutiZaring] p. 20	Proposition 5.15	difid 3483  difidALT 3484
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3427
[TakeutiZaring] p. 21	Theorem 5.22	setind 4523
[TakeutiZaring] p. 21	Definition 5.20	df-v 2732
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4121
[TakeutiZaring] p. 22	Exercise 1	0ss 3453
[TakeutiZaring] p. 22	Exercise 3	ssex 4126  ssexg 4128
[TakeutiZaring] p. 22	Exercise 4	inex1 4123
[TakeutiZaring] p. 22	Exercise 5	ruv 4534
[TakeutiZaring] p. 22	Exercise 6	elirr 4525
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3479
[TakeutiZaring] p. 22	Exercise 11	difdif 3252
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3388
[TakeutiZaring] p. 22	Exercise 14	difss 3253
[TakeutiZaring] p. 22	Exercise 15	sscon 3261
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2453
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2454
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4726  xpexg 4725  xpexgALT 6112
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4618
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5262
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5414  fun11 5265
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5209  svrelfun 5263
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4798
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4800
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4623
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4624
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4620
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5065  dfrel2 5061
[TakeutiZaring] p. 25	Exercise 3	xpss 4719
[TakeutiZaring] p. 25	Exercise 5	relun 4728
[TakeutiZaring] p. 25	Exercise 6	reluni 4734
[TakeutiZaring] p. 25	Exercise 9	inxp 4745
[TakeutiZaring] p. 25	Exercise 12	relres 4919
[TakeutiZaring] p. 25	Exercise 13	opelres 4896  opelresg 4898
[TakeutiZaring] p. 25	Exercise 14	dmres 4912
[TakeutiZaring] p. 25	Exercise 15	resss 4915
[TakeutiZaring] p. 25	Exercise 17	resabs1 4920
[TakeutiZaring] p. 25	Exercise 18	funres 5239
[TakeutiZaring] p. 25	Exercise 24	relco 5109
[TakeutiZaring] p. 25	Exercise 29	funco 5238
[TakeutiZaring] p. 25	Exercise 30	f1co 5415
[TakeutiZaring] p. 26	Definition 6.10	eu2 2063
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5206  fv3 5519
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5149  cnvexg 5148
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4877  dmexg 4875
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4878  rnexg 4876
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5513
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5523  tz6.12 5524  tz6.12c 5526
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5487
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5201
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5202
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5204  wfo 5196
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5203  wf1 5195
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5205  wf1o 5197
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5593  eqfnfv2 5594  eqfnfv2f 5597
[TakeutiZaring] p. 28	Exercise 5	fvco 5566
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5718  fnexALT 6090
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5717  resfunexgALT 6087
[TakeutiZaring] p. 29	Exercise 9	funimaex 5283  funimaexg 5282
[TakeutiZaring] p. 29	Definition 6.18	df-br 3990
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4981  iniseg 4983
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4274
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5207
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5789
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5790
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5795
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5797
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5805
[TakeutiZaring] p. 35	Notation	wtr 4087
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4339
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4091
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4560
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4366
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4370
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4476
[TakeutiZaring] p. 38	Definition 7.11	df-on 4353
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4470
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4536
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4566
[TakeutiZaring] p. 40	Exercise 7	dftr2 4089
[TakeutiZaring] p. 40	Exercise 11	unon 4495
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4471
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3824
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4356
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4400  sucidg 4401
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 4485
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4354
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4490  ordelsuc 4489
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4578
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4579
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4580
[TakeutiZaring] p. 43	Axiom 7	omex 4577
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4591
[TakeutiZaring] p. 43	Corollary 7.31	find 4583
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4581
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4582
[TakeutiZaring] p. 44	Exercise 2	int0 3845
[TakeutiZaring] p. 44	Exercise 3	trintssm 4103
[TakeutiZaring] p. 44	Exercise 4	intss1 3846
[TakeutiZaring] p. 44	Exercise 6	onintonm 4501
[TakeutiZaring] p. 44	Definition 7.35	df-int 3832
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6287
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6344  tfri1d 6314
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6345  tfri2d 6315
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6346
[TakeutiZaring] p. 50	Exercise 3	smoiso 6281
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6265
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6443
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6439
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6436
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6440
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6488  nnaordi 6487
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3918  uniss2 3827
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6449
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6459
[TakeutiZaring] p. 62	Exercise 5	oaword1 6450
[TakeutiZaring] p. 62	Definition 8.15	om0 6437  omsuc 6451
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6460
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6496  nnmordi 6495
[TakeutiZaring] p. 67	Definition 8.30	oei0 6438
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7164
[TakeutiZaring] p. 88	Exercise 1	en0 6773
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6835
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6836
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6721  isfi 6739
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6809
[TakeutiZaring] p. 95	Definition 10.42	df-map 6628
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6826
[Tarski] p. 67	Axiom B5	ax-4 1503
[Tarski] p. 68	Lemma 6	equid 1694
[Tarski] p. 69	Lemma 7	equcomi 1697
[Tarski] p. 70	Lemma 14	spim 1731  spime 1734  spimeh 1732  spimh 1730
[Tarski] p. 70	Lemma 16	ax-11 1499  ax-11o 1816  ax11i 1707
[Tarski] p. 70	Lemmas 16 and 17	sb6 1879
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1519
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2143  ax-14 2144
[WhiteheadRussell] p. 96	Axiom *1.3	olc 706
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 722
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 751
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 760
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 784
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 611
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 638
[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 832
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2117  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 732
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 831
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 624
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 880
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 838
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 851
[WhiteheadRussell] p. 103	Theorem *2.16	con3 637
[WhiteheadRussell] p. 103	Theorem *2.17	condc 848
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 850
[WhiteheadRussell] p. 104	Theorem *2.2	orc 707
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 770
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 612
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 616
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 888
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 902
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 763
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 764
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 799
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 800
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 798
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 974
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 773
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 771
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 772
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 733
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 734
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 862  pm2.5gdc 861
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 857
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 735
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 736
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 737
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 650
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 651
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 717
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 886
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 720
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 721
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 860
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 743
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 795
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 796
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 654
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 708  pm2.67 738
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 864  pm2.521gdc 863
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 742
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 805
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 889
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 910
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 801
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 802
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 804
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 803
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 806
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 807
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 900
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 100
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 749
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 138
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 952
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 953
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 954
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 748
[WhiteheadRussell] p. 111	Theorem *3.21	pm3.21 262
[WhiteheadRussell] p. 111	Theorem *3.22	pm3.22 263
[WhiteheadRussell] p. 111	Theorem *3.24	pm3.24 688
[WhiteheadRussell] p. 112	Theorem *3.35	pm3.35 345
[WhiteheadRussell] p. 112	Theorem *3.3 (Exp)	pm3.3 259
[WhiteheadRussell] p. 112	Theorem *3.31 (Imp)	pm3.31 260
[WhiteheadRussell] p. 112	Theorem *3.26 (Simp)	simpl 108  simplimdc 855
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 109  simprimdc 854
[WhiteheadRussell] p. 112	Theorem *3.33 (Syll)	pm3.33 343
[WhiteheadRussell] p. 112	Theorem *3.34 (Syll)	pm3.34 344
[WhiteheadRussell] p. 112	Theorem *3.37 (Transp)	pm3.37 684
[WhiteheadRussell] p. 113	Fact)	pm3.45 592
[WhiteheadRussell] p. 113	Theorem *3.4	pm3.4 331
[WhiteheadRussell] p. 113	Theorem *3.41	pm3.41 329
[WhiteheadRussell] p. 113	Theorem *3.42	pm3.42 330
[WhiteheadRussell] p. 113	Theorem *3.44	jao 750  pm3.44 710
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 342
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 597
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 780
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 866
[WhiteheadRussell] p. 117	Theorem *4.2	biid 170
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 867
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 885
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 689
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 139
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 947  bitr 469
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 393
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 752  pm4.25 753
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 264
[WhiteheadRussell] p. 118	Theorem *4.4	andi 813
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 723
[WhiteheadRussell] p. 118	Theorem *4.32	anass 399
[WhiteheadRussell] p. 118	Theorem *4.33	orass 762
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 463
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 787
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 600
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 817
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 975
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 811
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 966
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 944
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 774
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 809  pm4.45 779  pm4.45im 332
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1474
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 951
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 892  imorr 716
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 317
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 894
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 745
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 746
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 897
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 933
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 747  pm4.56 775
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 934  oranim 776
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 681
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 893
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 881
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 895
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 682
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 896
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 882
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 387  pm4.71d 391  pm4.71i 389  pm4.71r 388  pm4.71rd 392  pm4.71ri 390
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 822
[WhiteheadRussell] p. 121	Theorem *4.73	iba 298
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 739
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 598  pm4.76 599
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 705  pm4.77 794
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 777
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 898
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 702
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 903
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 945
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 946
[WhiteheadRussell] p. 122	Theorem *4.84	imbi1 235
[WhiteheadRussell] p. 122	Theorem *4.85	imbi2 236
[WhiteheadRussell] p. 122	Theorem *4.86	bibi1 239
[WhiteheadRussell] p. 122	Theorem *4.87	bi2.04 247  impexp 261  pm4.87 552
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 596
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 904
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 905
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 907
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 906
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1384
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 823
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 899
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1389  pm5.18dc 878
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 701
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 690
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1387
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1392
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1393
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 890
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 472
[WhiteheadRussell] p. 125	Theorem *5.4	pm5.4 248
[WhiteheadRussell] p. 125	Theorem *5.5	pm5.5 241
[WhiteheadRussell] p. 125	Theorem *5.6	pm5.6dc 921  pm5.6r 922
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 949
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 346
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 450
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 604
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 912
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 605
[WhiteheadRussell] p. 125	Theorem *5.41	imdi 249  pm5.41 250
[WhiteheadRussell] p. 125	Theorem *5.42	pm5.42 318
[WhiteheadRussell] p. 125	Theorem *5.44	pm5.44 920
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 797
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 913
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 908
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 789
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 940
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 941
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 956
[WhiteheadRussell] p. 125	Theorem *5.501	pm5.501 243
[WhiteheadRussell] p. 126	Theorem *5.74	pm5.74 178
[WhiteheadRussell] p. 126	Theorem *5.75	pm5.75 957
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1628
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1478
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1625
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1888
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2022
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2421
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2422
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2868
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3011
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5178
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5179
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2098  eupickbi 2101
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5206
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7167