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 7071  fidcenum 6912
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6912
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7071
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12295
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6886
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6874
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12310
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12312
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12301  znnen 12268
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12313
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12314
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10678
[AczelRathjen], p. 183	Chapter 20	ax-setind 4508
[Apostol] p. 18	Theorem I.1	addcan 8069  addcan2d 8074  addcan2i 8072  addcand 8073  addcani 8071
[Apostol] p. 18	Theorem I.2	negeu 8080
[Apostol] p. 18	Theorem I.3	negsub 8137  negsubd 8206  negsubi 8167
[Apostol] p. 18	Theorem I.4	negneg 8139  negnegd 8191  negnegi 8159
[Apostol] p. 18	Theorem I.5	subdi 8274  subdid 8303  subdii 8296  subdir 8275  subdird 8304  subdiri 8297
[Apostol] p. 18	Theorem I.6	mul01 8278  mul01d 8282  mul01i 8280  mul02 8276  mul02d 8281  mul02i 8279
[Apostol] p. 18	Theorem I.9	divrecapd 8680
[Apostol] p. 18	Theorem I.10	recrecapi 8631
[Apostol] p. 18	Theorem I.12	mul2neg 8287  mul2negd 8302  mul2negi 8295  mulneg1 8284  mulneg1d 8300  mulneg1i 8293
[Apostol] p. 18	Theorem I.15	divdivdivap 8600
[Apostol] p. 20	Axiom 7	rpaddcl 9604  rpaddcld 9639  rpmulcl 9605  rpmulcld 9640
[Apostol] p. 20	Axiom 9	0nrp 9616
[Apostol] p. 20	Theorem I.17	lttri 7994
[Apostol] p. 20	Theorem I.18	ltadd1d 8427  ltadd1dd 8445  ltadd1i 8391
[Apostol] p. 20	Theorem I.19	ltmul1 8481  ltmul1a 8480  ltmul1i 8806  ltmul1ii 8814  ltmul2 8742  ltmul2d 9666  ltmul2dd 9680  ltmul2i 8809
[Apostol] p. 20	Theorem I.21	0lt1 8016
[Apostol] p. 20	Theorem I.23	lt0neg1 8357  lt0neg1d 8404  ltneg 8351  ltnegd 8412  ltnegi 8382
[Apostol] p. 20	Theorem I.25	lt2add 8334  lt2addd 8456  lt2addi 8399
[Apostol] p. 20	Definition of positive numbers	df-rp 9581
[Apostol] p. 21	Exercise 4	recgt0 8736  recgt0d 8820  recgt0i 8792  recgt0ii 8793
[Apostol] p. 22	Definition of integers	df-z 9183
[Apostol] p. 22	Definition of rationals	df-q 9549
[Apostol] p. 24	Theorem I.26	supeuti 6950
[Apostol] p. 26	Theorem I.29	arch 9102
[Apostol] p. 28	Exercise 2	btwnz 9301
[Apostol] p. 28	Exercise 3	nnrecl 9103
[Apostol] p. 28	Exercise 6	qbtwnre 10182
[Apostol] p. 28	Exercise 10(a)	zeneo 11793  zneo 9283
[Apostol] p. 29	Theorem I.35	resqrtth 10959  sqrtthi 11047
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8851
[Apostol] p. 363	Remark	absgt0api 11074
[Apostol] p. 363	Example	abssubd 11121  abssubi 11078
[ApostolNT] p. 14	Definition	df-dvds 11714
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11730
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11754
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11750
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11744
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11746
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11731
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11732
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11737
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11768
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11770
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11772
[ApostolNT] p. 15	Definition	dfgcd2 11932
[ApostolNT] p. 16	Definition	isprm2 12028
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12003
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11891
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11933
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 11935
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11905
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11898
[ApostolNT] p. 17	Theorem 1.8	coprm 12053
[ApostolNT] p. 17	Theorem 1.9	euclemma 12055
[ApostolNT] p. 19	Theorem 1.14	divalg 11846
[ApostolNT] p. 20	Theorem 1.15	eucalg 11970
[ApostolNT] p. 25	Definition	df-phi 12120
[ApostolNT] p. 26	Theorem 2.2	phisum 12149
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12131
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12135
[ApostolNT] p. 104	Definition	congr 12011
[ApostolNT] p. 106	Remark	dvdsval3 11717
[ApostolNT] p. 106	Definition	moddvds 11725
[ApostolNT] p. 107	Example 2	mod2eq0even 11800
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11801
[ApostolNT] p. 107	Example 4	zmod1congr 10266
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10303
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10570
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11749
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12014
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12016
[ApostolNT] p. 113	Theorem 5.17	eulerth 12142
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12160
[ApostolNT] p. 114	Theorem 5.19	fermltl 12143
[Bauer] p. 482	Section 1.2	pm2.01 606  pm2.65 649
[Bauer] p. 483	Theorem 1.3	acexmid 5835  onsucelsucexmidlem 4500
[Bauer], p. 481	Section 1.1	pwtrufal 13711
[Bauer], p. 483	Definition	n0rf 3416
[Bauer], p. 483	Theorem 1.2	2irrexpq 13435  2irrexpqap 13437
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6833
[Bauer], p. 494	Theorem 5.5	ivthinc 13162
[BauerHanson], p. 27	Proposition 5.2	cnstab 8534
[BauerSwan], p. 14	Remark	0ct 7063  ctm 7065
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 13715
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7071
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7433
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7346
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7435
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7469  addlocpr 7468
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7495
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7498
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7503
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2016
[BellMachover] p. 460	Notation	df-mo 2017
[BellMachover] p. 460	Definition	mo3 2067  mo3h 2066
[BellMachover] p. 462	Theorem 1.1	bm1.1 2149
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4097
[BellMachover] p. 466	Axiom Pow	axpow3 4150
[BellMachover] p. 466	Axiom Union	axun2 4407
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4513
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4356
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4516
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4467
[BellMachover] p. 471	Definition of Lim	df-ilim 4341
[BellMachover] p. 472	Axiom Inf	zfinf2 4560
[BellMachover] p. 473	Theorem 2.8	limom 4585
[Bobzien] p. 116	Statement T3	stoic3 1418
[Bobzien] p. 117	Statement T2	stoic2a 1416
[Bobzien] p. 117	Statement T4	stoic4a 1419
[BourbakiEns] p.	Proposition 8	fcof1 5745  fcofo 5746
[BourbakiTop1] p.	Remark	xnegmnf 9756  xnegpnf 9755
[BourbakiTop1] p.	Remark	rexneg 9757
[BourbakiTop1] p.	Proposition	ishmeo 12845
[BourbakiTop1] p.	Property V_i	ssnei2 12698
[BourbakiTop1] p.	Property V_ii	innei 12704
[BourbakiTop1] p.	Property V_iv	neissex 12706
[BourbakiTop1] p.	Proposition 1	neipsm 12695  neiss 12691
[BourbakiTop1] p.	Proposition 2	cnptopco 12763
[BourbakiTop1] p.	Proposition 4	imasnopn 12840
[BourbakiTop1] p.	Property V_iii	elnei 12693
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 12537
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4039
[Cohen] p. 301	Remark	relogoprlem 13330
[Cohen] p. 301	Property 2	relogmul 13331  relogmuld 13346
[Cohen] p. 301	Property 3	relogdiv 13332  relogdivd 13347
[Cohen] p. 301	Property 4	relogexp 13334
[Cohen] p. 301	Property 1a	log1 13328
[Cohen] p. 301	Property 1b	loge 13329
[Cohen4] p. 348	Observation	relogbcxpbap 13424
[Cohen4] p. 352	Definition	rpelogb 13408
[Cohen4] p. 361	Property 2	rprelogbmul 13414
[Cohen4] p. 361	Property 3	logbrec 13419  rprelogbdiv 13416
[Cohen4] p. 361	Property 4	rplogbreexp 13412
[Cohen4] p. 361	Property 6	relogbexpap 13417
[Cohen4] p. 361	Property 1(a)	rplogbid1 13406
[Cohen4] p. 361	Property 1(b)	rplogb1 13407
[Cohen4] p. 367	Property	rplogbchbase 13409
[Cohen4] p. 377	Property 2	logblt 13421
[Crosilla] p.	Axiom 1	ax-ext 2146
[Crosilla] p.	Axiom 2	ax-pr 4181
[Crosilla] p.	Axiom 3	ax-un 4405
[Crosilla] p.	Axiom 4	ax-nul 4102
[Crosilla] p.	Axiom 5	ax-iinf 4559
[Crosilla] p.	Axiom 6	ru 2945
[Crosilla] p.	Axiom 8	ax-pow 4147
[Crosilla] p.	Axiom 9	ax-setind 4508
[Crosilla], p.	Axiom 6	ax-sep 4094
[Crosilla], p.	Axiom 7	ax-coll 4091
[Crosilla], p.	Axiom 7'	repizf 4092
[Crosilla], p.	Theorem is stated	ordtriexmid 4492
[Crosilla], p.	Axiom of choice implies instances	acexmid 5835
[Crosilla], p.	Definition of ordinal	df-iord 4338
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4506
[Eisenberg] p. 67	Definition 5.3	df-dif 3113
[Eisenberg] p. 82	Definition 6.3	df-iom 4562
[Eisenberg] p. 125	Definition 8.21	df-map 6607
[Enderton] p. 18	Axiom of Empty Set	axnul 4101
[Enderton] p. 19	Definition	df-tp 3578
[Enderton] p. 26	Exercise 5	unissb 3813
[Enderton] p. 26	Exercise 10	pwel 4190
[Enderton] p. 28	Exercise 7(b)	pwunim 4258
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3929  iinin2m 3928  iunin1 3924  iunin2 3923
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3927  iundif2ss 3925
[Enderton] p. 33	Exercise 23	iinuniss 3942
[Enderton] p. 33	Exercise 25	iununir 3943
[Enderton] p. 33	Exercise 24(a)	iinpw 3950
[Enderton] p. 33	Exercise 24(b)	iunpw 4452  iunpwss 3951
[Enderton] p. 38	Exercise 6(a)	unipw 4189
[Enderton] p. 38	Exercise 6(b)	pwuni 4165
[Enderton] p. 41	Lemma 3D	opeluu 4422  rnex 4865  rnexg 4863
[Enderton] p. 41	Exercise 8	dmuni 4808  rnuni 5009
[Enderton] p. 42	Definition of a function	dffun7 5209  dffun8 5210
[Enderton] p. 43	Definition of function value	funfvdm2 5544
[Enderton] p. 43	Definition of single-rooted	funcnv 5243
[Enderton] p. 44	Definition (d)	dfima2 4942  dfima3 4943
[Enderton] p. 47	Theorem 3H	fvco2 5549
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7153
[Enderton] p. 50	Theorem 3K(a)	imauni 5723
[Enderton] p. 52	Definition	df-map 6607
[Enderton] p. 53	Exercise 21	coass 5116
[Enderton] p. 53	Exercise 27	dmco 5106
[Enderton] p. 53	Exercise 14(a)	funin 5253
[Enderton] p. 53	Exercise 22(a)	imass2 4974
[Enderton] p. 54	Remark	ixpf 6677  ixpssmap 6689
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6656
[Enderton] p. 56	Theorem 3M	erref 6512
[Enderton] p. 57	Lemma 3N	erthi 6538
[Enderton] p. 57	Definition	df-ec 6494
[Enderton] p. 58	Definition	df-qs 6498
[Enderton] p. 60	Theorem 3Q	th3q 6597  th3qcor 6596  th3qlem1 6594  th3qlem2 6595
[Enderton] p. 61	Exercise 35	df-ec 6494
[Enderton] p. 65	Exercise 56(a)	dmun 4805
[Enderton] p. 68	Definition of successor	df-suc 4343
[Enderton] p. 71	Definition	df-tr 4075  dftr4 4079
[Enderton] p. 72	Theorem 4E	unisuc 4385  unisucg 4386
[Enderton] p. 73	Exercise 6	unisuc 4385  unisucg 4386
[Enderton] p. 73	Exercise 5(a)	truni 4088
[Enderton] p. 73	Exercise 5(b)	trint 4089
[Enderton] p. 79	Theorem 4I(A1)	nna0 6433
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6435  onasuc 6425
[Enderton] p. 79	Definition of operation value	df-ov 5839
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6434
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6436  onmsuc 6432
[Enderton] p. 81	Theorem 4K(1)	nnaass 6444
[Enderton] p. 81	Theorem 4K(2)	nna0r 6437  nnacom 6443
[Enderton] p. 81	Theorem 4K(3)	nndi 6445
[Enderton] p. 81	Theorem 4K(4)	nnmass 6446
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6448
[Enderton] p. 82	Exercise 16	nnm0r 6438  nnmsucr 6447
[Enderton] p. 88	Exercise 23	nnaordex 6486
[Enderton] p. 129	Definition	df-en 6698
[Enderton] p. 132	Theorem 6B(b)	canth 5790
[Enderton] p. 133	Exercise 1	xpomen 12265
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6822
[Enderton] p. 136	Corollary 6E	nneneq 6814
[Enderton] p. 139	Theorem 6H(c)	mapen 6803
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7165
[Enderton] p. 143	Theorem 6J	dju0en 7161  dju1en 7160
[Enderton] p. 144	Corollary 6K	undif2ss 3479
[Enderton] p. 145	Figure 38	ffoss 5458
[Enderton] p. 145	Definition	df-dom 6699
[Enderton] p. 146	Example 1	domen 6708  domeng 6709
[Enderton] p. 146	Example 3	nndomo 6821
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6792  xpdom1g 6790  xpdom2g 6789
[Enderton] p. 168	Definition	df-po 4268
[Enderton] p. 192	Theorem 7M(a)	oneli 4400
[Enderton] p. 192	Theorem 7M(b)	ontr1 4361
[Enderton] p. 192	Theorem 7M(c)	onirri 4514
[Enderton] p. 193	Corollary 7N(b)	0elon 4364
[Enderton] p. 193	Corollary 7N(c)	onsuci 4487
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4460
[Enderton] p. 194	Remark	onprc 4523
[Enderton] p. 194	Exercise 16	suc11 4529
[Enderton] p. 197	Definition	df-card 7127
[Enderton] p. 200	Exercise 25	tfis 4554
[Enderton] p. 206	Theorem 7X(b)	en2lp 4525
[Enderton] p. 207	Exercise 34	opthreg 4527
[Enderton] p. 208	Exercise 35	suc11g 4528
[Geuvers], p. 1	Remark	expap0 10475
[Geuvers], p. 6	Lemma 2.13	mulap0r 8504
[Geuvers], p. 6	Lemma 2.15	mulap0 8542
[Geuvers], p. 9	Lemma 2.35	msqge0 8505
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7863
[Geuvers], p. 10	Lemma 3.9	maxcom 11131
[Geuvers], p. 10	Lemma 3.10	maxle1 11139  maxle2 11140
[Geuvers], p. 10	Lemma 3.11	maxleast 11141
[Geuvers], p. 10	Lemma 3.12	maxleb 11144
[Geuvers], p. 11	Definition 3.13	dfabsmax 11145
[Geuvers], p. 17	Definition 6.1	df-ap 8471
[Gleason] p. 117	Proposition 9-2.1	df-enq 7279  enqer 7290
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7283  df-nqqs 7280
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7276  df-plqqs 7281
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7277  df-mqqs 7282
[Gleason] p. 119	Proposition 9-2.5	df-rq 7284
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7340
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7343  ltbtwnnq 7348  ltbtwnnqq 7347
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7332
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7333
[Gleason] p. 123	Proposition 9-3.5	addclpr 7469
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7511
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7510
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7529
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7545
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7551  ltaprlem 7550
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7548
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7504
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7524
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7513
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7512
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7520
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7570
[Gleason] p. 126	Proposition 9-4.1	df-enr 7658  enrer 7667
[Gleason] p. 126	Proposition 9-4.2	df-0r 7663  df-1r 7664  df-nr 7659
[Gleason] p. 126	Proposition 9-4.3	df-mr 7661  df-plr 7660  negexsr 7704  recexsrlem 7706
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7662
[Gleason] p. 130	Proposition 10-1.3	creui 8846  creur 8845  cru 8491
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7855  axcnre 7813
[Gleason] p. 132	Definition 10-3.1	crim 10786  crimd 10905  crimi 10865  crre 10785  crred 10904  crrei 10864
[Gleason] p. 132	Definition 10-3.2	remim 10788  remimd 10870
[Gleason] p. 133	Definition 10.36	absval2 10985  absval2d 11113  absval2i 11072
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10812  cjaddd 10893  cjaddi 10860
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10813  cjmuld 10894  cjmuli 10861
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10811  cjcjd 10871  cjcji 10843
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10810  cjreb 10794  cjrebd 10874  cjrebi 10846  cjred 10899  rere 10793  rereb 10791  rerebd 10873  rerebi 10845  rered 10897
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10819  addcjd 10885  addcji 10855
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10929
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 10980  abscjd 11118  abscji 11076
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 10992  abs00d 11114  abs00i 11073  absne0d 11115
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11024  releabsd 11119  releabsi 11077
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 10997  absmuld 11122  absmuli 11079
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 10983  sqabsaddi 11080
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11032  abstrid 11124  abstrii 11083
[Gleason] p. 134	Definition 10-4.1	df-exp 10445  exp0 10449  expp1 10452  expp1d 10578
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10487  expaddd 10579
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 13374  cxpmuld 13397  expmul 10490  expmuld 10580
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10484  mulexpd 10592  rpmulcxp 13371
[Gleason] p. 141	Definition 11-2.1	fzval 9937
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11253
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11255
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11254
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11258
[Gleason] p. 172	Corollary 12-2.5	climrecl 11251
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11247  climcj 11248  climim 11250  climre 11249
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7929  df-xr 7928  ltxr 9702
[Gleason] p. 180	Theorem 12-5.3	climcau 11274
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10225
[Gleason] p. 223	Definition 14-1.1	df-met 12530
[Gleason] p. 223	Definition 14-1.1(a)	met0 12905  xmet0 12904
[Gleason] p. 223	Definition 14-1.1(c)	metsym 12912
[Gleason] p. 223	Definition 14-1.1(d)	mettri 12914  mstri 13014  xmettri 12913  xmstri 13013
[Gleason] p. 230	Proposition 14-2.6	txlm 12820
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13052
[Gleason] p. 243	Proposition 14-4.16	addcn2 11237  addcncntop 13093  mulcn2 11239  mulcncntop 13095  subcn2 11238  subcncntop 13094
[Gleason] p. 295	Remark	bcval3 10653  bcval4 10654
[Gleason] p. 295	Equation 2	bcpasc 10668
[Gleason] p. 295	Definition of binomial coefficient	bcval 10651  df-bc 10650
[Gleason] p. 296	Remark	bcn0 10657  bcnn 10659
[Gleason] p. 296	Theorem 15-2.8	binom 11411
[Gleason] p. 308	Equation 2	ef0 11599
[Gleason] p. 308	Equation 3	efcj 11600
[Gleason] p. 309	Corollary 15-4.3	efne0 11605
[Gleason] p. 309	Corollary 15-4.4	efexp 11609
[Gleason] p. 310	Equation 14	sinadd 11663
[Gleason] p. 310	Equation 15	cosadd 11664
[Gleason] p. 311	Equation 17	sincossq 11675
[Gleason] p. 311	Equation 18	cosbnd 11680  sinbnd 11679
[Gleason] p. 311	Definition of ` `	df-pi 11580
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1436
[Heyting] p. 127	Axiom #1	ax1hfs 13784
[Hitchcock] p. 5	Rule A3	mptnan 1412
[Hitchcock] p. 5	Rule A4	mptxor 1413
[Hitchcock] p. 5	Rule A5	mtpxor 1415
[HoTT], p.	Lemma 10.4.1	exmidontriim 7172
[HoTT], p.	Theorem 7.2.6	nndceq 6458
[HoTT], p.	Exercise 11.10	neapmkv 13780
[HoTT], p.	Exercise 11.11	mulap0bd 8545
[HoTT], p.	Section 11.2.1	df-iltp 7402  df-imp 7401  df-iplp 7400  df-reap 8464
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7594
[HoTT], p.	Corollary 11.4.3	conventions 13439
[HoTT], p.	Exercise 11.6(i)	dcapnconst 13773  dceqnconst 13772
[HoTT], p.	Corollary 11.2.13	axcaucvg 7832  caucvgpr 7614  caucvgprpr 7644  caucvgsr 7734
[HoTT], p.	Definition 11.2.1	df-inp 7398
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 13778
[HoTT], p.	Proposition 11.2.3	df-iso 4269  ltpopr 7527  ltsopr 7528
[HoTT], p.	Definition 11.2.7(v)	apsym 8495  reapcotr 8487  reapirr 8466
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8016  gt0add 8462  leadd1 8319  lelttr 7978  lemul1a 8744  lenlt 7965  ltadd1 8318  ltletr 7979  ltmul1 8481  reaplt 8477
[Jech] p. 4	Definition of class	cv 1341  cvjust 2159
[Jech] p. 78	Note	opthprc 4649
[KalishMontague] p. 81	Note 1	ax-i9 1517
[Kreyszig] p. 3	Property M1	metcl 12894  xmetcl 12893
[Kreyszig] p. 4	Property M2	meteq0 12901
[Kreyszig] p. 12	Equation 5	muleqadd 8556
[Kreyszig] p. 18	Definition 1.3-2	mopnval 12983
[Kreyszig] p. 19	Remark	mopntopon 12984
[Kreyszig] p. 19	Theorem T1	mopn0 13029  mopnm 12989
[Kreyszig] p. 19	Theorem T2	unimopn 13027
[Kreyszig] p. 19	Definition of neighborhood	neibl 13032
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13054
[Kreyszig] p. 25	Definition 1.4-1	lmbr 12754
[Kunen] p. 10	Axiom 0	a9e 1683
[Kunen] p. 12	Axiom 6	zfrep6 4093
[Kunen] p. 24	Definition 10.24	mapval 6617  mapvalg 6615
[Kunen] p. 31	Definition 10.24	mapex 6611
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3870
[Levy] p. 338	Axiom	df-clab 2151  df-clel 2160  df-cleq 2157
[Lopez-Astorga] p. 12	Rule 1	mptnan 1412
[Lopez-Astorga] p. 12	Rule 2	mptxor 1413
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1415
[Margaris] p. 40	Rule C	exlimiv 1585
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 843
[Margaris] p. 49	Definition	dfbi2 386  dfordc 882  exalim 1489
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 641
[Margaris] p. 89	Theorem 19.2	19.2 1625  r19.2m 3490
[Margaris] p. 89	Theorem 19.3	19.3 1541  19.3h 1540  rr19.3v 2860
[Margaris] p. 89	Theorem 19.5	alcom 1465
[Margaris] p. 89	Theorem 19.6	alexdc 1606  alexim 1632
[Margaris] p. 89	Theorem 19.7	alnex 1486
[Margaris] p. 89	Theorem 19.8	19.8a 1577  spsbe 1829
[Margaris] p. 89	Theorem 19.9	19.9 1631  19.9h 1630  19.9v 1858  exlimd 1584
[Margaris] p. 89	Theorem 19.11	excom 1651  excomim 1650
[Margaris] p. 89	Theorem 19.12	19.12 1652  r19.12 2570
[Margaris] p. 90	Theorem 19.14	exnalim 1633
[Margaris] p. 90	Theorem 19.15	albi 1455  ralbi 2596
[Margaris] p. 90	Theorem 19.16	19.16 1542
[Margaris] p. 90	Theorem 19.17	19.17 1543
[Margaris] p. 90	Theorem 19.18	exbi 1591  rexbi 2597
[Margaris] p. 90	Theorem 19.19	19.19 1653
[Margaris] p. 90	Theorem 19.20	alim 1444  alimd 1508  alimdh 1454  alimdv 1866  ralimdaa 2530  ralimdv 2532  ralimdva 2531  ralimdvva 2533  sbcimdv 3011
[Margaris] p. 90	Theorem 19.21	19.21-2 1654  19.21 1570  19.21bi 1545  19.21h 1544  19.21ht 1568  19.21t 1569  19.21v 1860  alrimd 1597  alrimdd 1596  alrimdh 1466  alrimdv 1863  alrimi 1509  alrimih 1456  alrimiv 1861  alrimivv 1862  r19.21 2540  r19.21be 2555  r19.21bi 2552  r19.21t 2539  r19.21v 2541  ralrimd 2542  ralrimdv 2543  ralrimdva 2544  ralrimdvv 2548  ralrimdvva 2549  ralrimi 2535  ralrimiv 2536  ralrimiva 2537  ralrimivv 2545  ralrimivva 2546  ralrimivvva 2547  ralrimivw 2538  rexlimi 2574
[Margaris] p. 90	Theorem 19.22	2alimdv 1868  2eximdv 1869  exim 1586  eximd 1599  eximdh 1598  eximdv 1867  rexim 2558  reximdai 2562  reximddv 2567  reximddv2 2569  reximdv 2565  reximdv2 2563  reximdva 2566  reximdvai 2564  reximi2 2560
[Margaris] p. 90	Theorem 19.23	19.23 1665  19.23bi 1579  19.23h 1485  19.23ht 1484  19.23t 1664  19.23v 1870  19.23vv 1871  exlimd2 1582  exlimdh 1583  exlimdv 1806  exlimdvv 1884  exlimi 1581  exlimih 1580  exlimiv 1585  exlimivv 1883  r19.23 2572  r19.23v 2573  rexlimd 2578  rexlimdv 2580  rexlimdv3a 2583  rexlimdva 2581  rexlimdva2 2584  rexlimdvaa 2582  rexlimdvv 2588  rexlimdvva 2589  rexlimdvw 2585  rexlimiv 2575  rexlimiva 2576  rexlimivv 2587
[Margaris] p. 90	Theorem 19.24	i19.24 1626
[Margaris] p. 90	Theorem 19.25	19.25 1613
[Margaris] p. 90	Theorem 19.26	19.26-2 1469  19.26-3an 1470  19.26 1468  r19.26-2 2593  r19.26-3 2594  r19.26 2590  r19.26m 2595
[Margaris] p. 90	Theorem 19.27	19.27 1548  19.27h 1547  19.27v 1886  r19.27av 2599  r19.27m 3499  r19.27mv 3500
[Margaris] p. 90	Theorem 19.28	19.28 1550  19.28h 1549  19.28v 1887  r19.28av 2600  r19.28m 3493  r19.28mv 3496  rr19.28v 2861
[Margaris] p. 90	Theorem 19.29	19.29 1607  19.29r 1608  19.29r2 1609  19.29x 1610  r19.29 2601  r19.29d2r 2608  r19.29r 2602
[Margaris] p. 90	Theorem 19.30	19.30dc 1614
[Margaris] p. 90	Theorem 19.31	19.31r 1668
[Margaris] p. 90	Theorem 19.32	19.32dc 1666  19.32r 1667  r19.32r 2610  r19.32vdc 2613  r19.32vr 2612
[Margaris] p. 90	Theorem 19.33	19.33 1471  19.33b2 1616  19.33bdc 1617
[Margaris] p. 90	Theorem 19.34	19.34 1671
[Margaris] p. 90	Theorem 19.35	19.35-1 1611  19.35i 1612
[Margaris] p. 90	Theorem 19.36	19.36-1 1660  19.36aiv 1888  19.36i 1659  r19.36av 2615
[Margaris] p. 90	Theorem 19.37	19.37-1 1661  19.37aiv 1662  r19.37 2616  r19.37av 2617
[Margaris] p. 90	Theorem 19.38	19.38 1663
[Margaris] p. 90	Theorem 19.39	i19.39 1627
[Margaris] p. 90	Theorem 19.40	19.40-2 1619  19.40 1618  r19.40 2618
[Margaris] p. 90	Theorem 19.41	19.41 1673  19.41h 1672  19.41v 1889  19.41vv 1890  19.41vvv 1891  19.41vvvv 1892  r19.41 2619  r19.41v 2620
[Margaris] p. 90	Theorem 19.42	19.42 1675  19.42h 1674  19.42v 1893  19.42vv 1898  19.42vvv 1899  19.42vvvv 1900  r19.42v 2621
[Margaris] p. 90	Theorem 19.43	19.43 1615  r19.43 2622
[Margaris] p. 90	Theorem 19.44	19.44 1669  r19.44av 2623  r19.44mv 3498
[Margaris] p. 90	Theorem 19.45	19.45 1670  r19.45av 2624  r19.45mv 3497
[Margaris] p. 110	Exercise 2(b)	eu1 2038
[Megill] p. 444	Axiom C5	ax-17 1513
[Megill] p. 445	Lemma L12	alequcom 1502  ax-10 1492
[Megill] p. 446	Lemma L17	equtrr 1697
[Megill] p. 446	Lemma L19	hbnae 1708
[Megill] p. 447	Remark 9.1	df-sb 1750  sbid 1761
[Megill] p. 448	Scheme C5'	ax-4 1497
[Megill] p. 448	Scheme C6'	ax-7 1435
[Megill] p. 448	Scheme C8'	ax-8 1491
[Megill] p. 448	Scheme C9'	ax-i12 1494
[Megill] p. 448	Scheme C11'	ax-10o 1703
[Megill] p. 448	Scheme C12'	ax-13 2137
[Megill] p. 448	Scheme C13'	ax-14 2138
[Megill] p. 448	Scheme C15'	ax-11o 1810
[Megill] p. 448	Scheme C16'	ax-16 1801
[Megill] p. 448	Theorem 9.4	dral1 1717  dral2 1718  drex1 1785  drex2 1719  drsb1 1786  drsb2 1828
[Megill] p. 449	Theorem 9.7	sbcom2 1974  sbequ 1827  sbid2v 1983
[Megill] p. 450	Example in Appendix	hba1 1527
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3028  rspsbca 3029  stdpc4 1762
[Mendelson] p. 69	Axiom 5	ra5 3034  stdpc5 1571
[Mendelson] p. 81	Rule C	exlimiv 1585
[Mendelson] p. 95	Axiom 6	stdpc6 1690
[Mendelson] p. 95	Axiom 7	stdpc7 1757
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3440
[Mendelson] p. 231	Exercise 4.10(l)	unv 3441
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3357
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3405
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3358
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3248
[Mendelson] p. 231	Definition of union	unssin 3356
[Mendelson] p. 235	Exercise 4.12(c)	univ 4448
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3782
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4254
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4255
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4256
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3803
[Mendelson] p. 235	Exercise 4.12(p)	reli 4727
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5118
[Mendelson] p. 246	Definition of successor	df-suc 4343
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6802
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6778  xpsneng 6779
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6784  xpcomeng 6785
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6787
[Mendelson] p. 255	Exercise 4.39	endisj 6781
[Mendelson] p. 255	Exercise 4.41	mapprc 6609
[Mendelson] p. 255	Exercise 4.43	mapsnen 6768
[Mendelson] p. 255	Exercise 4.47	xpmapen 6807
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6643
[Mendelson] p. 255	Exercise 4.42(b)	map1 6769
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7164  djucomen 7163
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7162
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6426
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3339
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4686
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4687
[Monk1] p. 34	Definition 3.3	df-opab 4038
[Monk1] p. 36	Theorem 3.7(i)	coi1 5113  coi2 5114
[Monk1] p. 36	Theorem 3.8(v)	dm0 4812  rn0 4854
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5002
[Monk1] p. 37	Theorem 3.13(i)	relxp 4707
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4818  rnxpm 5027
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4678  xp0 5017
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4957
[Monk1] p. 38	Theorem 3.16(viii)	imai 4954
[Monk1] p. 39	Theorem 3.17	imaex 4953  imaexg 4952
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4951
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5609  funfvop 5591
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5524
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5532
[Monk1] p. 43	Theorem 4.6	funun 5226
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5730  dff13f 5732
[Monk1] p. 46	Theorem 4.15(v)	funex 5702  funrnex 6074
[Monk1] p. 50	Definition 5.4	fniunfv 5724
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5081
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3834
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6115  df-1st 6100
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6116  df-2nd 6101
[Monk2] p. 105	Axiom C4	ax-5 1434
[Monk2] p. 105	Axiom C7	ax-8 1491
[Monk2] p. 105	Axiom C8	ax-11 1493  ax-11o 1810
[Monk2] p. 105	Axiom (C8)	ax11v 1814
[Monk2] p. 109	Lemma 12	ax-7 1435
[Monk2] p. 109	Lemma 15	equvin 1850  equvini 1745  eqvinop 4215
[Monk2] p. 113	Axiom C5-1	ax-17 1513
[Monk2] p. 113	Axiom C5-2	ax6b 1638
[Monk2] p. 113	Axiom C5-3	ax-7 1435
[Monk2] p. 114	Lemma 22	hba1 1527
[Monk2] p. 114	Lemma 23	hbia1 1539  nfia1 1567
[Monk2] p. 114	Lemma 24	hba2 1538  nfa2 1566
[Moschovakis] p. 2	Chapter 2	df-stab 821  dftest 13785
[Munkres] p. 77	Example 2	distop 12626
[Munkres] p. 78	Definition of basis	df-bases 12582  isbasis3g 12585
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12513  tgval2 12592
[Munkres] p. 79	Remark	tgcl 12605
[Munkres] p. 80	Lemma 2.1	tgval3 12599
[Munkres] p. 80	Lemma 2.2	tgss2 12620  tgss3 12619
[Munkres] p. 81	Lemma 2.3	basgen 12621  basgen2 12622
[Munkres] p. 89	Definition of subspace topology	resttop 12711
[Munkres] p. 93	Theorem 6.1(1)	0cld 12653  topcld 12650
[Munkres] p. 93	Theorem 6.1(3)	uncld 12654
[Munkres] p. 94	Definition of closure	clsval 12652
[Munkres] p. 94	Definition of interior	ntrval 12651
[Munkres] p. 102	Definition of continuous function	df-cn 12729  iscn 12738  iscn2 12741
[Munkres] p. 107	Theorem 7.2(g)	cncnp 12771  cncnp2m 12772  cncnpi 12769  df-cnp 12730  iscnp 12740
[Munkres] p. 127	Theorem 10.1	metcn 13055
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6860
[Pierik], p. 9	Definition 2.4	df-womni 7119
[Pierik], p. 9	Definition 2.5	df-markov 7107  omniwomnimkv 7122
[Pierik], p. 10	Section 2.3	dfdif3 3227
[Pierik], p. 14	Definition 3.1	df-omni 7090  exmidomniim 7096  finomni 7095
[Pierik], p. 15	Section 3.1	df-nninf 7076
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 13736
[PradicBrown2022], p. 2	Remark	exmidpw 6865
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7148
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7149  exmidfodomrlemrALT 7150
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7104
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 13721  peano4nninf 13720
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 13723
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 13731
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 13733
[PradicBrown2022], p. 5	Definition 3.3	nnsf 13719
[Quine] p. 16	Definition 2.1	df-clab 2151  rabid 2639
[Quine] p. 17	Definition 2.1''	dfsb7 1978
[Quine] p. 18	Definition 2.7	df-cleq 2157
[Quine] p. 19	Definition 2.9	df-v 2723
[Quine] p. 34	Theorem 5.1	abeq2 2273
[Quine] p. 35	Theorem 5.2	abid2 2285  abid2f 2332
[Quine] p. 40	Theorem 6.1	sb5 1874
[Quine] p. 40	Theorem 6.2	sb56 1872  sb6 1873
[Quine] p. 41	Theorem 6.3	df-clel 2160
[Quine] p. 41	Theorem 6.4	eqid 2164
[Quine] p. 41	Theorem 6.5	eqcom 2166
[Quine] p. 42	Theorem 6.6	df-sbc 2947
[Quine] p. 42	Theorem 6.7	dfsbcq 2948  dfsbcq2 2949
[Quine] p. 43	Theorem 6.8	vex 2724
[Quine] p. 43	Theorem 6.9	isset 2727
[Quine] p. 44	Theorem 7.3	spcgf 2803  spcgv 2808  spcimgf 2801
[Quine] p. 44	Theorem 6.11	spsbc 2957  spsbcd 2958
[Quine] p. 44	Theorem 6.12	elex 2732
[Quine] p. 44	Theorem 6.13	elab 2865  elabg 2867  elabgf 2863
[Quine] p. 44	Theorem 6.14	noel 3408
[Quine] p. 48	Theorem 7.2	snprc 3635
[Quine] p. 48	Definition 7.1	df-pr 3577  df-sn 3576
[Quine] p. 49	Theorem 7.4	snss 3696  snssg 3703
[Quine] p. 49	Theorem 7.5	prss 3723  prssg 3724
[Quine] p. 49	Theorem 7.6	prid1 3676  prid1g 3674  prid2 3677  prid2g 3675  snid 3601  snidg 3599
[Quine] p. 51	Theorem 7.12	snexg 4157  snexprc 4159
[Quine] p. 51	Theorem 7.13	prexg 4183
[Quine] p. 53	Theorem 8.2	unisn 3799  unisng 3800
[Quine] p. 53	Theorem 8.3	uniun 3802
[Quine] p. 54	Theorem 8.6	elssuni 3811
[Quine] p. 54	Theorem 8.7	uni0 3810
[Quine] p. 56	Theorem 8.17	uniabio 5157
[Quine] p. 56	Definition 8.18	dfiota2 5148
[Quine] p. 57	Theorem 8.19	iotaval 5158
[Quine] p. 57	Theorem 8.22	iotanul 5162
[Quine] p. 58	Theorem 8.23	euiotaex 5163
[Quine] p. 58	Definition 9.1	df-op 3579
[Quine] p. 61	Theorem 9.5	opabid 4229  opelopab 4243  opelopaba 4238  opelopabaf 4245  opelopabf 4246  opelopabg 4240  opelopabga 4235  oprabid 5865
[Quine] p. 64	Definition 9.11	df-xp 4604
[Quine] p. 64	Definition 9.12	df-cnv 4606
[Quine] p. 64	Definition 9.15	df-id 4265
[Quine] p. 65	Theorem 10.3	fun0 5240
[Quine] p. 65	Theorem 10.4	funi 5214
[Quine] p. 65	Theorem 10.5	funsn 5230  funsng 5228
[Quine] p. 65	Definition 10.1	df-fun 5184
[Quine] p. 65	Definition 10.2	args 4967  dffv4g 5477
[Quine] p. 68	Definition 10.11	df-fv 5190  fv2 5475
[Quine] p. 124	Theorem 17.3	nn0opth2 10626  nn0opth2d 10625  nn0opthd 10624
[Quine] p. 284	Axiom 39(vi)	funimaex 5267  funimaexg 5266
[Rudin] p. 164	Equation 27	efcan 11603
[Rudin] p. 164	Equation 30	efzval 11610
[Rudin] p. 167	Equation 48	absefi 11695
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1415
[Sanford] p. 39	Rule 4	mptxor 1413
[Sanford] p. 40	Rule 1	mptnan 1412
[Schechter] p. 51	Definition of antisymmetry	intasym 4982
[Schechter] p. 51	Definition of irreflexivity	intirr 4984
[Schechter] p. 51	Definition of symmetry	cnvsym 4981
[Schechter] p. 51	Definition of transitivity	cotr 4979
[Schechter] p. 428	Definition 15.35	bastop1 12624
[Stoll] p. 13	Definition of symmetric difference	symdif1 3382
[Stoll] p. 16	Exercise 4.4	0dif 3475  dif0 3474
[Stoll] p. 16	Exercise 4.8	difdifdirss 3488
[Stoll] p. 19	Theorem 5.2(13)	undm 3375
[Stoll] p. 19	Theorem 5.2(13')	indmss 3376
[Stoll] p. 20	Remark	invdif 3359
[Stoll] p. 25	Definition of ordered triple	df-ot 3580
[Stoll] p. 43	Definition	uniiun 3913
[Stoll] p. 44	Definition	intiin 3914
[Stoll] p. 45	Definition	df-iin 3863
[Stoll] p. 45	Definition indexed union	df-iun 3862
[Stoll] p. 176	Theorem 3.4(27)	imandc 879  imanst 878
[Stoll] p. 262	Example 4.1	symdif1 3382
[Suppes] p. 22	Theorem 2	eq0 3422
[Suppes] p. 22	Theorem 4	eqss 3152  eqssd 3154  eqssi 3153
[Suppes] p. 23	Theorem 5	ss0 3444  ss0b 3443
[Suppes] p. 23	Theorem 6	sstr 3145
[Suppes] p. 25	Theorem 12	elin 3300  elun 3258
[Suppes] p. 26	Theorem 15	inidm 3326
[Suppes] p. 26	Theorem 16	in0 3438
[Suppes] p. 27	Theorem 23	unidm 3260
[Suppes] p. 27	Theorem 24	un0 3437
[Suppes] p. 27	Theorem 25	ssun1 3280
[Suppes] p. 27	Theorem 26	ssequn1 3287
[Suppes] p. 27	Theorem 27	unss 3291
[Suppes] p. 27	Theorem 28	indir 3366
[Suppes] p. 27	Theorem 29	undir 3367
[Suppes] p. 28	Theorem 32	difid 3472  difidALT 3473
[Suppes] p. 29	Theorem 33	difin 3354
[Suppes] p. 29	Theorem 34	indif 3360
[Suppes] p. 29	Theorem 35	undif1ss 3478
[Suppes] p. 29	Theorem 36	difun2 3483
[Suppes] p. 29	Theorem 37	difin0 3477
[Suppes] p. 29	Theorem 38	disjdif 3476
[Suppes] p. 29	Theorem 39	difundi 3369
[Suppes] p. 29	Theorem 40	difindiss 3371
[Suppes] p. 30	Theorem 41	nalset 4106
[Suppes] p. 39	Theorem 61	uniss 3804
[Suppes] p. 39	Theorem 65	uniop 4227
[Suppes] p. 41	Theorem 70	intsn 3853
[Suppes] p. 42	Theorem 71	intpr 3850  intprg 3851
[Suppes] p. 42	Theorem 73	op1stb 4450  op1stbg 4451
[Suppes] p. 42	Theorem 78	intun 3849
[Suppes] p. 44	Definition 15(a)	dfiun2 3894  dfiun2g 3892
[Suppes] p. 44	Definition 15(b)	dfiin2 3895
[Suppes] p. 47	Theorem 86	elpw 3559  elpw2 4130  elpw2g 4129  elpwg 3561
[Suppes] p. 47	Theorem 87	pwid 3568
[Suppes] p. 47	Theorem 89	pw0 3714
[Suppes] p. 48	Theorem 90	pwpw0ss 3778
[Suppes] p. 52	Theorem 101	xpss12 4705
[Suppes] p. 52	Theorem 102	xpindi 4733  xpindir 4734
[Suppes] p. 52	Theorem 103	xpundi 4654  xpundir 4655
[Suppes] p. 54	Theorem 105	elirrv 4519
[Suppes] p. 58	Theorem 2	relss 4685
[Suppes] p. 59	Theorem 4	eldm 4795  eldm2 4796  eldm2g 4794  eldmg 4793
[Suppes] p. 59	Definition 3	df-dm 4608
[Suppes] p. 60	Theorem 6	dmin 4806
[Suppes] p. 60	Theorem 8	rnun 5006
[Suppes] p. 60	Theorem 9	rnin 5007
[Suppes] p. 60	Definition 4	dfrn2 4786
[Suppes] p. 61	Theorem 11	brcnv 4781  brcnvg 4779
[Suppes] p. 62	Equation 5	elcnv 4775  elcnv2 4776
[Suppes] p. 62	Theorem 12	relcnv 4976
[Suppes] p. 62	Theorem 15	cnvin 5005
[Suppes] p. 62	Theorem 16	cnvun 5003
[Suppes] p. 63	Theorem 20	co02 5111
[Suppes] p. 63	Theorem 21	dmcoss 4867
[Suppes] p. 63	Definition 7	df-co 4607
[Suppes] p. 64	Theorem 26	cnvco 4783
[Suppes] p. 64	Theorem 27	coass 5116
[Suppes] p. 65	Theorem 31	resundi 4891
[Suppes] p. 65	Theorem 34	elima 4945  elima2 4946  elima3 4947  elimag 4944
[Suppes] p. 65	Theorem 35	imaundi 5010
[Suppes] p. 66	Theorem 40	dminss 5012
[Suppes] p. 66	Theorem 41	imainss 5013
[Suppes] p. 67	Exercise 11	cnvxp 5016
[Suppes] p. 81	Definition 34	dfec2 6495
[Suppes] p. 82	Theorem 72	elec 6531  elecg 6530
[Suppes] p. 82	Theorem 73	erth 6536  erth2 6537
[Suppes] p. 89	Theorem 96	map0b 6644
[Suppes] p. 89	Theorem 97	map0 6646  map0g 6645
[Suppes] p. 89	Theorem 98	mapsn 6647
[Suppes] p. 89	Theorem 99	mapss 6648
[Suppes] p. 92	Theorem 1	enref 6722  enrefg 6721
[Suppes] p. 92	Theorem 2	ensym 6738  ensymb 6737  ensymi 6739
[Suppes] p. 92	Theorem 3	entr 6741
[Suppes] p. 92	Theorem 4	unen 6773
[Suppes] p. 94	Theorem 15	endom 6720
[Suppes] p. 94	Theorem 16	ssdomg 6735
[Suppes] p. 94	Theorem 17	domtr 6742
[Suppes] p. 95	Theorem 18	isbth 6923
[Suppes] p. 98	Exercise 4	fundmen 6763  fundmeng 6764
[Suppes] p. 98	Exercise 6	xpdom3m 6791
[Suppes] p. 130	Definition 3	df-tr 4075
[Suppes] p. 132	Theorem 9	ssonuni 4459
[Suppes] p. 134	Definition 6	df-suc 4343
[Suppes] p. 136	Theorem Schema 22	findes 4574  finds 4571  finds1 4573  finds2 4572
[Suppes] p. 162	Definition 5	df-ltnqqs 7285  df-ltpq 7278
[Suppes] p. 228	Theorem Schema 61	onintss 4362
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2146
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2157
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2160
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2159
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2182
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5840
[TakeutiZaring] p. 14	Proposition 4.14	ru 2945
[TakeutiZaring] p. 15	Exercise 1	elpr 3591  elpr2 3592  elprg 3590
[TakeutiZaring] p. 15	Exercise 2	elsn 3586  elsn2 3604  elsn2g 3603  elsng 3585  velsn 3587
[TakeutiZaring] p. 15	Exercise 3	elop 4203
[TakeutiZaring] p. 15	Exercise 4	sneq 3581  sneqr 3734
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3589  dfsn2 3584
[TakeutiZaring] p. 16	Axiom 3	uniex 4409
[TakeutiZaring] p. 16	Exercise 6	opth 4209
[TakeutiZaring] p. 16	Exercise 8	rext 4187
[TakeutiZaring] p. 16	Corollary 5.8	unex 4413  unexg 4415
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3619
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3784
[TakeutiZaring] p. 16	Definition 5.6	df-in 3117  df-un 3115
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3797  uniprg 3798
[TakeutiZaring] p. 17	Axiom 4	vpwex 4152
[TakeutiZaring] p. 17	Exercise 1	eltp 3618
[TakeutiZaring] p. 17	Exercise 5	elsuc 4378  elsucg 4376  sstr2 3144
[TakeutiZaring] p. 17	Exercise 6	uncom 3261
[TakeutiZaring] p. 17	Exercise 7	incom 3309
[TakeutiZaring] p. 17	Exercise 8	unass 3274
[TakeutiZaring] p. 17	Exercise 9	inass 3327
[TakeutiZaring] p. 17	Exercise 10	indi 3364
[TakeutiZaring] p. 17	Exercise 11	undi 3365
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3126
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3555
[TakeutiZaring] p. 18	Exercise 7	unss2 3288
[TakeutiZaring] p. 18	Exercise 9	df-ss 3124  sseqin2 3336
[TakeutiZaring] p. 18	Exercise 10	ssid 3157
[TakeutiZaring] p. 18	Exercise 12	inss1 3337  inss2 3338
[TakeutiZaring] p. 18	Exercise 13	nssr 3197
[TakeutiZaring] p. 18	Exercise 15	unieq 3792
[TakeutiZaring] p. 18	Exercise 18	sspwb 4188
[TakeutiZaring] p. 18	Exercise 19	pweqb 4195
[TakeutiZaring] p. 20	Definition	df-rab 2451
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4103
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3113
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3406
[TakeutiZaring] p. 20	Proposition 5.15	difid 3472  difidALT 3473
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3416
[TakeutiZaring] p. 21	Theorem 5.22	setind 4510
[TakeutiZaring] p. 21	Definition 5.20	df-v 2723
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4108
[TakeutiZaring] p. 22	Exercise 1	0ss 3442
[TakeutiZaring] p. 22	Exercise 3	ssex 4113  ssexg 4115
[TakeutiZaring] p. 22	Exercise 4	inex1 4110
[TakeutiZaring] p. 22	Exercise 5	ruv 4521
[TakeutiZaring] p. 22	Exercise 6	elirr 4512
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3468
[TakeutiZaring] p. 22	Exercise 11	difdif 3242
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3378
[TakeutiZaring] p. 22	Exercise 14	difss 3243
[TakeutiZaring] p. 22	Exercise 15	sscon 3251
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2447
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2448
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4713  xpexg 4712  xpexgALT 6093
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4605
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5246
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5398  fun11 5249
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5193  svrelfun 5247
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4785
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4787
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4610
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4611
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4607
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5052  dfrel2 5048
[TakeutiZaring] p. 25	Exercise 3	xpss 4706
[TakeutiZaring] p. 25	Exercise 5	relun 4715
[TakeutiZaring] p. 25	Exercise 6	reluni 4721
[TakeutiZaring] p. 25	Exercise 9	inxp 4732
[TakeutiZaring] p. 25	Exercise 12	relres 4906
[TakeutiZaring] p. 25	Exercise 13	opelres 4883  opelresg 4885
[TakeutiZaring] p. 25	Exercise 14	dmres 4899
[TakeutiZaring] p. 25	Exercise 15	resss 4902
[TakeutiZaring] p. 25	Exercise 17	resabs1 4907
[TakeutiZaring] p. 25	Exercise 18	funres 5223
[TakeutiZaring] p. 25	Exercise 24	relco 5096
[TakeutiZaring] p. 25	Exercise 29	funco 5222
[TakeutiZaring] p. 25	Exercise 30	f1co 5399
[TakeutiZaring] p. 26	Definition 6.10	eu2 2057
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5190  fv3 5503
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5136  cnvexg 5135
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4864  dmexg 4862
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4865  rnexg 4863
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5497
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5507  tz6.12 5508  tz6.12c 5510
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5471
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5185
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5186
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5188  wfo 5180
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5187  wf1 5179
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5189  wf1o 5181
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5577  eqfnfv2 5578  eqfnfv2f 5581
[TakeutiZaring] p. 28	Exercise 5	fvco 5550
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5701  fnexALT 6073
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5700  resfunexgALT 6070
[TakeutiZaring] p. 29	Exercise 9	funimaex 5267  funimaexg 5266
[TakeutiZaring] p. 29	Definition 6.18	df-br 3977
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4968  iniseg 4970
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4261
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5191
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5772
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5773
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5778
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5780
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5788
[TakeutiZaring] p. 35	Notation	wtr 4074
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4326
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4078
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4547
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4353
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4357
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4463
[TakeutiZaring] p. 38	Definition 7.11	df-on 4340
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4457
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4523
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4553
[TakeutiZaring] p. 40	Exercise 7	dftr2 4076
[TakeutiZaring] p. 40	Exercise 11	unon 4482
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4458
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3811
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4343
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4387  sucidg 4388
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 4472
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4341
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4477  ordelsuc 4476
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4565
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4566
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4567
[TakeutiZaring] p. 43	Axiom 7	omex 4564
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4578
[TakeutiZaring] p. 43	Corollary 7.31	find 4570
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4568
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4569
[TakeutiZaring] p. 44	Exercise 2	int0 3832
[TakeutiZaring] p. 44	Exercise 3	trintssm 4090
[TakeutiZaring] p. 44	Exercise 4	intss1 3833
[TakeutiZaring] p. 44	Exercise 6	onintonm 4488
[TakeutiZaring] p. 44	Definition 7.35	df-int 3819
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6267
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6324  tfri1d 6294
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6325  tfri2d 6295
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6326
[TakeutiZaring] p. 50	Exercise 3	smoiso 6261
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6245
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6423
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6419
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6416
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6420
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6468  nnaordi 6467
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3905  uniss2 3814
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6429
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6439
[TakeutiZaring] p. 62	Exercise 5	oaword1 6430
[TakeutiZaring] p. 62	Definition 8.15	om0 6417  omsuc 6431
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6440
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6476  nnmordi 6475
[TakeutiZaring] p. 67	Definition 8.30	oei0 6418
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7134
[TakeutiZaring] p. 88	Exercise 1	en0 6752
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6814
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6815
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6700  isfi 6718
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6788
[TakeutiZaring] p. 95	Definition 10.42	df-map 6607
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6805
[Tarski] p. 67	Axiom B5	ax-4 1497
[Tarski] p. 68	Lemma 6	equid 1688
[Tarski] p. 69	Lemma 7	equcomi 1691
[Tarski] p. 70	Lemma 14	spim 1725  spime 1728  spimeh 1726  spimh 1724
[Tarski] p. 70	Lemma 16	ax-11 1493  ax-11o 1810  ax11i 1701
[Tarski] p. 70	Lemmas 16 and 17	sb6 1873
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1513
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2137  ax-14 2138
[WhiteheadRussell] p. 96	Axiom *1.3	olc 701
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 717
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 746
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 755
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 779
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 606
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 633
[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 827
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2111  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 727
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 826
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 619
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 875
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 833
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 846
[WhiteheadRussell] p. 103	Theorem *2.16	con3 632
[WhiteheadRussell] p. 103	Theorem *2.17	condc 843
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 845
[WhiteheadRussell] p. 104	Theorem *2.2	orc 702
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 765
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 607
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 611
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 883
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 897
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 758
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 759
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 794
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 795
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 793
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 968
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 768
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 766
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 767
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 728
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 729
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 857  pm2.5gdc 856
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 852
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 730
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 731
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 732
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 645
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 646
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 712
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 881
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 715
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 716
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 855
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 738
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 790
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 791
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 649
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 703  pm2.67 733
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 859  pm2.521gdc 858
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 737
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 800
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 884
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 905
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 796
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 797
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 799
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 798
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 801
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 802
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 895
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 100
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 744
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 138
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 946
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 947
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 948
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 743
[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 683
[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 850
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 109  simprimdc 849
[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 679
[WhiteheadRussell] p. 113	Fact)	pm3.45 587
[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 745  pm3.44 705
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 342
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 592
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 775
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 861
[WhiteheadRussell] p. 117	Theorem *4.2	biid 170
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 862
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 880
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 684
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 139
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 941  bitr 464
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 393
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 747  pm4.25 748
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 264
[WhiteheadRussell] p. 118	Theorem *4.4	andi 808
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 718
[WhiteheadRussell] p. 118	Theorem *4.32	anass 399
[WhiteheadRussell] p. 118	Theorem *4.33	orass 757
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 462
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 782
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 595
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 812
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 969
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 806
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 960
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 938
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 769
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 804  pm4.45 774  pm4.45im 332
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1468
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 945
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 887  imorr 711
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 317
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 889
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 740
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 741
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 892
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 927
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 742  pm4.56 770
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 928  oranim 771
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 676
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 888
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 876
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 890
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 677
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 891
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 877
[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 817
[WhiteheadRussell] p. 121	Theorem *4.73	iba 298
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 734
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 593  pm4.76 594
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 700  pm4.77 789
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 772
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 893
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 697
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 898
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 939
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 940
[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 547
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 591
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 899
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 900
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 902
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 901
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1378
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 818
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 894
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1383  pm5.18dc 873
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 696
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 685
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1381
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1386
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1387
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 885
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 467
[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 916  pm5.6r 917
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 943
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 346
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 449
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 599
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 907
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 600
[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 915
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 792
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 908
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 903
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 784
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 934
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 935
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 950
[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 951
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1622
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1472
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1619
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1882
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2016
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2415
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2416
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2859
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3002
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5165
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5166
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2092  eupickbi 2095
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5190
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7137