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 7076  fidcenum 6917
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6917
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7076
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12354
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6891
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6879
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12369
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12371
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12360  znnen 12327
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12372
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12373
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10685
[AczelRathjen], p. 183	Chapter 20	ax-setind 4513
[Apostol] p. 18	Theorem I.1	addcan 8074  addcan2d 8079  addcan2i 8077  addcand 8078  addcani 8076
[Apostol] p. 18	Theorem I.2	negeu 8085
[Apostol] p. 18	Theorem I.3	negsub 8142  negsubd 8211  negsubi 8172
[Apostol] p. 18	Theorem I.4	negneg 8144  negnegd 8196  negnegi 8164
[Apostol] p. 18	Theorem I.5	subdi 8279  subdid 8308  subdii 8301  subdir 8280  subdird 8309  subdiri 8302
[Apostol] p. 18	Theorem I.6	mul01 8283  mul01d 8287  mul01i 8285  mul02 8281  mul02d 8286  mul02i 8284
[Apostol] p. 18	Theorem I.9	divrecapd 8685
[Apostol] p. 18	Theorem I.10	recrecapi 8636
[Apostol] p. 18	Theorem I.12	mul2neg 8292  mul2negd 8307  mul2negi 8300  mulneg1 8289  mulneg1d 8305  mulneg1i 8298
[Apostol] p. 18	Theorem I.15	divdivdivap 8605
[Apostol] p. 20	Axiom 7	rpaddcl 9609  rpaddcld 9644  rpmulcl 9610  rpmulcld 9645
[Apostol] p. 20	Axiom 9	0nrp 9621
[Apostol] p. 20	Theorem I.17	lttri 7999
[Apostol] p. 20	Theorem I.18	ltadd1d 8432  ltadd1dd 8450  ltadd1i 8396
[Apostol] p. 20	Theorem I.19	ltmul1 8486  ltmul1a 8485  ltmul1i 8811  ltmul1ii 8819  ltmul2 8747  ltmul2d 9671  ltmul2dd 9685  ltmul2i 8814
[Apostol] p. 20	Theorem I.21	0lt1 8021
[Apostol] p. 20	Theorem I.23	lt0neg1 8362  lt0neg1d 8409  ltneg 8356  ltnegd 8417  ltnegi 8387
[Apostol] p. 20	Theorem I.25	lt2add 8339  lt2addd 8461  lt2addi 8404
[Apostol] p. 20	Definition of positive numbers	df-rp 9586
[Apostol] p. 21	Exercise 4	recgt0 8741  recgt0d 8825  recgt0i 8797  recgt0ii 8798
[Apostol] p. 22	Definition of integers	df-z 9188
[Apostol] p. 22	Definition of rationals	df-q 9554
[Apostol] p. 24	Theorem I.26	supeuti 6955
[Apostol] p. 26	Theorem I.29	arch 9107
[Apostol] p. 28	Exercise 2	btwnz 9306
[Apostol] p. 28	Exercise 3	nnrecl 9108
[Apostol] p. 28	Exercise 6	qbtwnre 10188
[Apostol] p. 28	Exercise 10(a)	zeneo 11804  zneo 9288
[Apostol] p. 29	Theorem I.35	resqrtth 10969  sqrtthi 11057
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8856
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 11965
[Apostol] p. 363	Remark	absgt0api 11084
[Apostol] p. 363	Example	abssubd 11131  abssubi 11088
[ApostolNT] p. 14	Definition	df-dvds 11724
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11740
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11764
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11760
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11754
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11756
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11741
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11742
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11747
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11779
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11781
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11783
[ApostolNT] p. 15	Definition	dfgcd2 11943
[ApostolNT] p. 16	Definition	isprm2 12045
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12020
[ApostolNT] p. 16	Theorem 1.7	prminf 12384
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11902
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11944
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 11946
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11916
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11909
[ApostolNT] p. 17	Theorem 1.8	coprm 12072
[ApostolNT] p. 17	Theorem 1.9	euclemma 12074
[ApostolNT] p. 17	Theorem 1.10	1arith2 12294
[ApostolNT] p. 19	Theorem 1.14	divalg 11857
[ApostolNT] p. 20	Theorem 1.15	eucalg 11987
[ApostolNT] p. 25	Definition	df-phi 12139
[ApostolNT] p. 26	Theorem 2.2	phisum 12168
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12150
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12154
[ApostolNT] p. 104	Definition	congr 12028
[ApostolNT] p. 106	Remark	dvdsval3 11727
[ApostolNT] p. 106	Definition	moddvds 11735
[ApostolNT] p. 107	Example 2	mod2eq0even 11811
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11812
[ApostolNT] p. 107	Example 4	zmod1congr 10272
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10309
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10577
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11759
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12031
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12033
[ApostolNT] p. 113	Theorem 5.17	eulerth 12161
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12179
[ApostolNT] p. 114	Theorem 5.19	fermltl 12162
[ApostolNT] p. 179	Definition	df-lgs 13499  lgsprme0 13543
[ApostolNT] p. 180	Example 1	1lgs 13544
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 13520
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 13535
[ApostolNT] p. 188	Definition	df-lgs 13499  lgs1 13545
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 13536
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 13538
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 13546
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 13547
[Bauer] p. 482	Section 1.2	pm2.01 606  pm2.65 649
[Bauer] p. 483	Theorem 1.3	acexmid 5840  onsucelsucexmidlem 4505
[Bauer], p. 481	Section 1.1	pwtrufal 13837
[Bauer], p. 483	Definition	n0rf 3420
[Bauer], p. 483	Theorem 1.2	2irrexpq 13494  2irrexpqap 13496
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6838
[Bauer], p. 494	Theorem 5.5	ivthinc 13221
[BauerHanson], p. 27	Proposition 5.2	cnstab 8539
[BauerSwan], p. 14	Remark	0ct 7068  ctm 7070
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 13841
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7076
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7438
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7351
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7440
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7474  addlocpr 7473
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7500
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7503
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7508
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2017
[BellMachover] p. 460	Notation	df-mo 2018
[BellMachover] p. 460	Definition	mo3 2068  mo3h 2067
[BellMachover] p. 462	Theorem 1.1	bm1.1 2150
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4102
[BellMachover] p. 466	Axiom Pow	axpow3 4155
[BellMachover] p. 466	Axiom Union	axun2 4412
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4518
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4361
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4521
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4472
[BellMachover] p. 471	Definition of Lim	df-ilim 4346
[BellMachover] p. 472	Axiom Inf	zfinf2 4565
[BellMachover] p. 473	Theorem 2.8	limom 4590
[Bobzien] p. 116	Statement T3	stoic3 1419
[Bobzien] p. 117	Statement T2	stoic2a 1417
[Bobzien] p. 117	Statement T4	stoic4a 1420
[BourbakiEns] p.	Proposition 8	fcof1 5750  fcofo 5751
[BourbakiTop1] p.	Remark	xnegmnf 9761  xnegpnf 9760
[BourbakiTop1] p.	Remark	rexneg 9762
[BourbakiTop1] p.	Proposition	ishmeo 12904
[BourbakiTop1] p.	Property V_i	ssnei2 12757
[BourbakiTop1] p.	Property V_ii	innei 12763
[BourbakiTop1] p.	Property V_iv	neissex 12765
[BourbakiTop1] p.	Proposition 1	neipsm 12754  neiss 12750
[BourbakiTop1] p.	Proposition 2	cnptopco 12822
[BourbakiTop1] p.	Proposition 4	imasnopn 12899
[BourbakiTop1] p.	Property V_iii	elnei 12752
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 12596
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4044
[Cohen] p. 301	Remark	relogoprlem 13389
[Cohen] p. 301	Property 2	relogmul 13390  relogmuld 13405
[Cohen] p. 301	Property 3	relogdiv 13391  relogdivd 13406
[Cohen] p. 301	Property 4	relogexp 13393
[Cohen] p. 301	Property 1a	log1 13387
[Cohen] p. 301	Property 1b	loge 13388
[Cohen4] p. 348	Observation	relogbcxpbap 13483
[Cohen4] p. 352	Definition	rpelogb 13467
[Cohen4] p. 361	Property 2	rprelogbmul 13473
[Cohen4] p. 361	Property 3	logbrec 13478  rprelogbdiv 13475
[Cohen4] p. 361	Property 4	rplogbreexp 13471
[Cohen4] p. 361	Property 6	relogbexpap 13476
[Cohen4] p. 361	Property 1(a)	rplogbid1 13465
[Cohen4] p. 361	Property 1(b)	rplogb1 13466
[Cohen4] p. 367	Property	rplogbchbase 13468
[Cohen4] p. 377	Property 2	logblt 13480
[Crosilla] p.	Axiom 1	ax-ext 2147
[Crosilla] p.	Axiom 2	ax-pr 4186
[Crosilla] p.	Axiom 3	ax-un 4410
[Crosilla] p.	Axiom 4	ax-nul 4107
[Crosilla] p.	Axiom 5	ax-iinf 4564
[Crosilla] p.	Axiom 6	ru 2949
[Crosilla] p.	Axiom 8	ax-pow 4152
[Crosilla] p.	Axiom 9	ax-setind 4513
[Crosilla], p.	Axiom 6	ax-sep 4099
[Crosilla], p.	Axiom 7	ax-coll 4096
[Crosilla], p.	Axiom 7'	repizf 4097
[Crosilla], p.	Theorem is stated	ordtriexmid 4497
[Crosilla], p.	Axiom of choice implies instances	acexmid 5840
[Crosilla], p.	Definition of ordinal	df-iord 4343
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4511
[Eisenberg] p. 67	Definition 5.3	df-dif 3117
[Eisenberg] p. 82	Definition 6.3	df-iom 4567
[Eisenberg] p. 125	Definition 8.21	df-map 6612
[Enderton] p. 18	Axiom of Empty Set	axnul 4106
[Enderton] p. 19	Definition	df-tp 3583
[Enderton] p. 26	Exercise 5	unissb 3818
[Enderton] p. 26	Exercise 10	pwel 4195
[Enderton] p. 28	Exercise 7(b)	pwunim 4263
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3934  iinin2m 3933  iunin1 3929  iunin2 3928
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3932  iundif2ss 3930
[Enderton] p. 33	Exercise 23	iinuniss 3947
[Enderton] p. 33	Exercise 25	iununir 3948
[Enderton] p. 33	Exercise 24(a)	iinpw 3955
[Enderton] p. 33	Exercise 24(b)	iunpw 4457  iunpwss 3956
[Enderton] p. 38	Exercise 6(a)	unipw 4194
[Enderton] p. 38	Exercise 6(b)	pwuni 4170
[Enderton] p. 41	Lemma 3D	opeluu 4427  rnex 4870  rnexg 4868
[Enderton] p. 41	Exercise 8	dmuni 4813  rnuni 5014
[Enderton] p. 42	Definition of a function	dffun7 5214  dffun8 5215
[Enderton] p. 43	Definition of function value	funfvdm2 5549
[Enderton] p. 43	Definition of single-rooted	funcnv 5248
[Enderton] p. 44	Definition (d)	dfima2 4947  dfima3 4948
[Enderton] p. 47	Theorem 3H	fvco2 5554
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7158
[Enderton] p. 50	Theorem 3K(a)	imauni 5728
[Enderton] p. 52	Definition	df-map 6612
[Enderton] p. 53	Exercise 21	coass 5121
[Enderton] p. 53	Exercise 27	dmco 5111
[Enderton] p. 53	Exercise 14(a)	funin 5258
[Enderton] p. 53	Exercise 22(a)	imass2 4979
[Enderton] p. 54	Remark	ixpf 6682  ixpssmap 6694
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6661
[Enderton] p. 56	Theorem 3M	erref 6517
[Enderton] p. 57	Lemma 3N	erthi 6543
[Enderton] p. 57	Definition	df-ec 6499
[Enderton] p. 58	Definition	df-qs 6503
[Enderton] p. 60	Theorem 3Q	th3q 6602  th3qcor 6601  th3qlem1 6599  th3qlem2 6600
[Enderton] p. 61	Exercise 35	df-ec 6499
[Enderton] p. 65	Exercise 56(a)	dmun 4810
[Enderton] p. 68	Definition of successor	df-suc 4348
[Enderton] p. 71	Definition	df-tr 4080  dftr4 4084
[Enderton] p. 72	Theorem 4E	unisuc 4390  unisucg 4391
[Enderton] p. 73	Exercise 6	unisuc 4390  unisucg 4391
[Enderton] p. 73	Exercise 5(a)	truni 4093
[Enderton] p. 73	Exercise 5(b)	trint 4094
[Enderton] p. 79	Theorem 4I(A1)	nna0 6438
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6440  onasuc 6430
[Enderton] p. 79	Definition of operation value	df-ov 5844
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6439
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6441  onmsuc 6437
[Enderton] p. 81	Theorem 4K(1)	nnaass 6449
[Enderton] p. 81	Theorem 4K(2)	nna0r 6442  nnacom 6448
[Enderton] p. 81	Theorem 4K(3)	nndi 6450
[Enderton] p. 81	Theorem 4K(4)	nnmass 6451
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6453
[Enderton] p. 82	Exercise 16	nnm0r 6443  nnmsucr 6452
[Enderton] p. 88	Exercise 23	nnaordex 6491
[Enderton] p. 129	Definition	df-en 6703
[Enderton] p. 132	Theorem 6B(b)	canth 5795
[Enderton] p. 133	Exercise 1	xpomen 12324
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6827
[Enderton] p. 136	Corollary 6E	nneneq 6819
[Enderton] p. 139	Theorem 6H(c)	mapen 6808
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7170
[Enderton] p. 143	Theorem 6J	dju0en 7166  dju1en 7165
[Enderton] p. 144	Corollary 6K	undif2ss 3483
[Enderton] p. 145	Figure 38	ffoss 5463
[Enderton] p. 145	Definition	df-dom 6704
[Enderton] p. 146	Example 1	domen 6713  domeng 6714
[Enderton] p. 146	Example 3	nndomo 6826
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6797  xpdom1g 6795  xpdom2g 6794
[Enderton] p. 168	Definition	df-po 4273
[Enderton] p. 192	Theorem 7M(a)	oneli 4405
[Enderton] p. 192	Theorem 7M(b)	ontr1 4366
[Enderton] p. 192	Theorem 7M(c)	onirri 4519
[Enderton] p. 193	Corollary 7N(b)	0elon 4369
[Enderton] p. 193	Corollary 7N(c)	onsuci 4492
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4465
[Enderton] p. 194	Remark	onprc 4528
[Enderton] p. 194	Exercise 16	suc11 4534
[Enderton] p. 197	Definition	df-card 7132
[Enderton] p. 200	Exercise 25	tfis 4559
[Enderton] p. 206	Theorem 7X(b)	en2lp 4530
[Enderton] p. 207	Exercise 34	opthreg 4532
[Enderton] p. 208	Exercise 35	suc11g 4533
[Geuvers], p. 1	Remark	expap0 10481
[Geuvers], p. 6	Lemma 2.13	mulap0r 8509
[Geuvers], p. 6	Lemma 2.15	mulap0 8547
[Geuvers], p. 9	Lemma 2.35	msqge0 8510
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7868
[Geuvers], p. 10	Lemma 3.9	maxcom 11141
[Geuvers], p. 10	Lemma 3.10	maxle1 11149  maxle2 11150
[Geuvers], p. 10	Lemma 3.11	maxleast 11151
[Geuvers], p. 10	Lemma 3.12	maxleb 11154
[Geuvers], p. 11	Definition 3.13	dfabsmax 11155
[Geuvers], p. 17	Definition 6.1	df-ap 8476
[Gleason] p. 117	Proposition 9-2.1	df-enq 7284  enqer 7295
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7288  df-nqqs 7285
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7281  df-plqqs 7286
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7282  df-mqqs 7287
[Gleason] p. 119	Proposition 9-2.5	df-rq 7289
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7345
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7348  ltbtwnnq 7353  ltbtwnnqq 7352
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7337
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7338
[Gleason] p. 123	Proposition 9-3.5	addclpr 7474
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7516
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7515
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7534
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7550
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7556  ltaprlem 7555
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7553
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7509
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7529
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7518
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7517
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7525
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7575
[Gleason] p. 126	Proposition 9-4.1	df-enr 7663  enrer 7672
[Gleason] p. 126	Proposition 9-4.2	df-0r 7668  df-1r 7669  df-nr 7664
[Gleason] p. 126	Proposition 9-4.3	df-mr 7666  df-plr 7665  negexsr 7709  recexsrlem 7711
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7667
[Gleason] p. 130	Proposition 10-1.3	creui 8851  creur 8850  cru 8496
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7860  axcnre 7818
[Gleason] p. 132	Definition 10-3.1	crim 10796  crimd 10915  crimi 10875  crre 10795  crred 10914  crrei 10874
[Gleason] p. 132	Definition 10-3.2	remim 10798  remimd 10880
[Gleason] p. 133	Definition 10.36	absval2 10995  absval2d 11123  absval2i 11082
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10822  cjaddd 10903  cjaddi 10870
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10823  cjmuld 10904  cjmuli 10871
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10821  cjcjd 10881  cjcji 10853
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10820  cjreb 10804  cjrebd 10884  cjrebi 10856  cjred 10909  rere 10803  rereb 10801  rerebd 10883  rerebi 10855  rered 10907
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10829  addcjd 10895  addcji 10865
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10939
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 10990  abscjd 11128  abscji 11086
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11002  abs00d 11124  abs00i 11083  absne0d 11125
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11034  releabsd 11129  releabsi 11087
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11007  absmuld 11132  absmuli 11089
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 10993  sqabsaddi 11090
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11042  abstrid 11134  abstrii 11093
[Gleason] p. 134	Definition 10-4.1	df-exp 10451  exp0 10455  expp1 10458  expp1d 10585
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10493  expaddd 10586
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 13433  cxpmuld 13456  expmul 10496  expmuld 10587
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10490  mulexpd 10599  rpmulcxp 13430
[Gleason] p. 141	Definition 11-2.1	fzval 9942
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11263
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11265
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11264
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11268
[Gleason] p. 172	Corollary 12-2.5	climrecl 11261
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11257  climcj 11258  climim 11260  climre 11259
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7934  df-xr 7933  ltxr 9707
[Gleason] p. 180	Theorem 12-5.3	climcau 11284
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10231
[Gleason] p. 223	Definition 14-1.1	df-met 12589
[Gleason] p. 223	Definition 14-1.1(a)	met0 12964  xmet0 12963
[Gleason] p. 223	Definition 14-1.1(c)	metsym 12971
[Gleason] p. 223	Definition 14-1.1(d)	mettri 12973  mstri 13073  xmettri 12972  xmstri 13072
[Gleason] p. 230	Proposition 14-2.6	txlm 12879
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13111
[Gleason] p. 243	Proposition 14-4.16	addcn2 11247  addcncntop 13152  mulcn2 11249  mulcncntop 13154  subcn2 11248  subcncntop 13153
[Gleason] p. 295	Remark	bcval3 10660  bcval4 10661
[Gleason] p. 295	Equation 2	bcpasc 10675
[Gleason] p. 295	Definition of binomial coefficient	bcval 10658  df-bc 10657
[Gleason] p. 296	Remark	bcn0 10664  bcnn 10666
[Gleason] p. 296	Theorem 15-2.8	binom 11421
[Gleason] p. 308	Equation 2	ef0 11609
[Gleason] p. 308	Equation 3	efcj 11610
[Gleason] p. 309	Corollary 15-4.3	efne0 11615
[Gleason] p. 309	Corollary 15-4.4	efexp 11619
[Gleason] p. 310	Equation 14	sinadd 11673
[Gleason] p. 310	Equation 15	cosadd 11674
[Gleason] p. 311	Equation 17	sincossq 11685
[Gleason] p. 311	Equation 18	cosbnd 11690  sinbnd 11689
[Gleason] p. 311	Definition of ` `	df-pi 11590
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1437
[Heyting] p. 127	Axiom #1	ax1hfs 13910
[Hitchcock] p. 5	Rule A3	mptnan 1413
[Hitchcock] p. 5	Rule A4	mptxor 1414
[Hitchcock] p. 5	Rule A5	mtpxor 1416
[HoTT], p.	Lemma 10.4.1	exmidontriim 7177
[HoTT], p.	Theorem 7.2.6	nndceq 6463
[HoTT], p.	Exercise 11.10	neapmkv 13906
[HoTT], p.	Exercise 11.11	mulap0bd 8550
[HoTT], p.	Section 11.2.1	df-iltp 7407  df-imp 7406  df-iplp 7405  df-reap 8469
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7599
[HoTT], p.	Corollary 11.4.3	conventions 13562
[HoTT], p.	Exercise 11.6(i)	dcapnconst 13899  dceqnconst 13898
[HoTT], p.	Corollary 11.2.13	axcaucvg 7837  caucvgpr 7619  caucvgprpr 7649  caucvgsr 7739
[HoTT], p.	Definition 11.2.1	df-inp 7403
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 13904
[HoTT], p.	Proposition 11.2.3	df-iso 4274  ltpopr 7532  ltsopr 7533
[HoTT], p.	Definition 11.2.7(v)	apsym 8500  reapcotr 8492  reapirr 8471
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8021  gt0add 8467  leadd1 8324  lelttr 7983  lemul1a 8749  lenlt 7970  ltadd1 8323  ltletr 7984  ltmul1 8486  reaplt 8482
[Jech] p. 4	Definition of class	cv 1342  cvjust 2160
[Jech] p. 78	Note	opthprc 4654
[KalishMontague] p. 81	Note 1	ax-i9 1518
[Kreyszig] p. 3	Property M1	metcl 12953  xmetcl 12952
[Kreyszig] p. 4	Property M2	meteq0 12960
[Kreyszig] p. 12	Equation 5	muleqadd 8561
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13042
[Kreyszig] p. 19	Remark	mopntopon 13043
[Kreyszig] p. 19	Theorem T1	mopn0 13088  mopnm 13048
[Kreyszig] p. 19	Theorem T2	unimopn 13086
[Kreyszig] p. 19	Definition of neighborhood	neibl 13091
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13113
[Kreyszig] p. 25	Definition 1.4-1	lmbr 12813
[Kunen] p. 10	Axiom 0	a9e 1684
[Kunen] p. 12	Axiom 6	zfrep6 4098
[Kunen] p. 24	Definition 10.24	mapval 6622  mapvalg 6620
[Kunen] p. 31	Definition 10.24	mapex 6616
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3875
[Levy] p. 338	Axiom	df-clab 2152  df-clel 2161  df-cleq 2158
[Lopez-Astorga] p. 12	Rule 1	mptnan 1413
[Lopez-Astorga] p. 12	Rule 2	mptxor 1414
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1416
[Margaris] p. 40	Rule C	exlimiv 1586
[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 1490
[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 1626  r19.2m 3494
[Margaris] p. 89	Theorem 19.3	19.3 1542  19.3h 1541  rr19.3v 2864
[Margaris] p. 89	Theorem 19.5	alcom 1466
[Margaris] p. 89	Theorem 19.6	alexdc 1607  alexim 1633
[Margaris] p. 89	Theorem 19.7	alnex 1487
[Margaris] p. 89	Theorem 19.8	19.8a 1578  spsbe 1830
[Margaris] p. 89	Theorem 19.9	19.9 1632  19.9h 1631  19.9v 1859  exlimd 1585
[Margaris] p. 89	Theorem 19.11	excom 1652  excomim 1651
[Margaris] p. 89	Theorem 19.12	19.12 1653  r19.12 2571
[Margaris] p. 90	Theorem 19.14	exnalim 1634
[Margaris] p. 90	Theorem 19.15	albi 1456  ralbi 2597
[Margaris] p. 90	Theorem 19.16	19.16 1543
[Margaris] p. 90	Theorem 19.17	19.17 1544
[Margaris] p. 90	Theorem 19.18	exbi 1592  rexbi 2598
[Margaris] p. 90	Theorem 19.19	19.19 1654
[Margaris] p. 90	Theorem 19.20	alim 1445  alimd 1509  alimdh 1455  alimdv 1867  ralimdaa 2531  ralimdv 2533  ralimdva 2532  ralimdvva 2534  sbcimdv 3015
[Margaris] p. 90	Theorem 19.21	19.21-2 1655  19.21 1571  19.21bi 1546  19.21h 1545  19.21ht 1569  19.21t 1570  19.21v 1861  alrimd 1598  alrimdd 1597  alrimdh 1467  alrimdv 1864  alrimi 1510  alrimih 1457  alrimiv 1862  alrimivv 1863  r19.21 2541  r19.21be 2556  r19.21bi 2553  r19.21t 2540  r19.21v 2542  ralrimd 2543  ralrimdv 2544  ralrimdva 2545  ralrimdvv 2549  ralrimdvva 2550  ralrimi 2536  ralrimiv 2537  ralrimiva 2538  ralrimivv 2546  ralrimivva 2547  ralrimivvva 2548  ralrimivw 2539  rexlimi 2575
[Margaris] p. 90	Theorem 19.22	2alimdv 1869  2eximdv 1870  exim 1587  eximd 1600  eximdh 1599  eximdv 1868  rexim 2559  reximdai 2563  reximddv 2568  reximddv2 2570  reximdv 2566  reximdv2 2564  reximdva 2567  reximdvai 2565  reximi2 2561
[Margaris] p. 90	Theorem 19.23	19.23 1666  19.23bi 1580  19.23h 1486  19.23ht 1485  19.23t 1665  19.23v 1871  19.23vv 1872  exlimd2 1583  exlimdh 1584  exlimdv 1807  exlimdvv 1885  exlimi 1582  exlimih 1581  exlimiv 1586  exlimivv 1884  r19.23 2573  r19.23v 2574  rexlimd 2579  rexlimdv 2581  rexlimdv3a 2584  rexlimdva 2582  rexlimdva2 2585  rexlimdvaa 2583  rexlimdvv 2589  rexlimdvva 2590  rexlimdvw 2586  rexlimiv 2576  rexlimiva 2577  rexlimivv 2588
[Margaris] p. 90	Theorem 19.24	i19.24 1627
[Margaris] p. 90	Theorem 19.25	19.25 1614
[Margaris] p. 90	Theorem 19.26	19.26-2 1470  19.26-3an 1471  19.26 1469  r19.26-2 2594  r19.26-3 2595  r19.26 2591  r19.26m 2596
[Margaris] p. 90	Theorem 19.27	19.27 1549  19.27h 1548  19.27v 1887  r19.27av 2600  r19.27m 3503  r19.27mv 3504
[Margaris] p. 90	Theorem 19.28	19.28 1551  19.28h 1550  19.28v 1888  r19.28av 2601  r19.28m 3497  r19.28mv 3500  rr19.28v 2865
[Margaris] p. 90	Theorem 19.29	19.29 1608  19.29r 1609  19.29r2 1610  19.29x 1611  r19.29 2602  r19.29d2r 2609  r19.29r 2603
[Margaris] p. 90	Theorem 19.30	19.30dc 1615
[Margaris] p. 90	Theorem 19.31	19.31r 1669
[Margaris] p. 90	Theorem 19.32	19.32dc 1667  19.32r 1668  r19.32r 2611  r19.32vdc 2614  r19.32vr 2613
[Margaris] p. 90	Theorem 19.33	19.33 1472  19.33b2 1617  19.33bdc 1618
[Margaris] p. 90	Theorem 19.34	19.34 1672
[Margaris] p. 90	Theorem 19.35	19.35-1 1612  19.35i 1613
[Margaris] p. 90	Theorem 19.36	19.36-1 1661  19.36aiv 1889  19.36i 1660  r19.36av 2616
[Margaris] p. 90	Theorem 19.37	19.37-1 1662  19.37aiv 1663  r19.37 2617  r19.37av 2618
[Margaris] p. 90	Theorem 19.38	19.38 1664
[Margaris] p. 90	Theorem 19.39	i19.39 1628
[Margaris] p. 90	Theorem 19.40	19.40-2 1620  19.40 1619  r19.40 2619
[Margaris] p. 90	Theorem 19.41	19.41 1674  19.41h 1673  19.41v 1890  19.41vv 1891  19.41vvv 1892  19.41vvvv 1893  r19.41 2620  r19.41v 2621
[Margaris] p. 90	Theorem 19.42	19.42 1676  19.42h 1675  19.42v 1894  19.42vv 1899  19.42vvv 1900  19.42vvvv 1901  r19.42v 2622
[Margaris] p. 90	Theorem 19.43	19.43 1616  r19.43 2623
[Margaris] p. 90	Theorem 19.44	19.44 1670  r19.44av 2624  r19.44mv 3502
[Margaris] p. 90	Theorem 19.45	19.45 1671  r19.45av 2625  r19.45mv 3501
[Margaris] p. 110	Exercise 2(b)	eu1 2039
[Megill] p. 444	Axiom C5	ax-17 1514
[Megill] p. 445	Lemma L12	alequcom 1503  ax-10 1493
[Megill] p. 446	Lemma L17	equtrr 1698
[Megill] p. 446	Lemma L19	hbnae 1709
[Megill] p. 447	Remark 9.1	df-sb 1751  sbid 1762
[Megill] p. 448	Scheme C5'	ax-4 1498
[Megill] p. 448	Scheme C6'	ax-7 1436
[Megill] p. 448	Scheme C8'	ax-8 1492
[Megill] p. 448	Scheme C9'	ax-i12 1495
[Megill] p. 448	Scheme C11'	ax-10o 1704
[Megill] p. 448	Scheme C12'	ax-13 2138
[Megill] p. 448	Scheme C13'	ax-14 2139
[Megill] p. 448	Scheme C15'	ax-11o 1811
[Megill] p. 448	Scheme C16'	ax-16 1802
[Megill] p. 448	Theorem 9.4	dral1 1718  dral2 1719  drex1 1786  drex2 1720  drsb1 1787  drsb2 1829
[Megill] p. 449	Theorem 9.7	sbcom2 1975  sbequ 1828  sbid2v 1984
[Megill] p. 450	Example in Appendix	hba1 1528
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3032  rspsbca 3033  stdpc4 1763
[Mendelson] p. 69	Axiom 5	ra5 3038  stdpc5 1572
[Mendelson] p. 81	Rule C	exlimiv 1586
[Mendelson] p. 95	Axiom 6	stdpc6 1691
[Mendelson] p. 95	Axiom 7	stdpc7 1758
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3444
[Mendelson] p. 231	Exercise 4.10(l)	unv 3445
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3361
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3409
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3362
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3252
[Mendelson] p. 231	Definition of union	unssin 3360
[Mendelson] p. 235	Exercise 4.12(c)	univ 4453
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3787
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4259
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4260
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4261
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3808
[Mendelson] p. 235	Exercise 4.12(p)	reli 4732
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5123
[Mendelson] p. 246	Definition of successor	df-suc 4348
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6807
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6783  xpsneng 6784
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6789  xpcomeng 6790
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6792
[Mendelson] p. 255	Exercise 4.39	endisj 6786
[Mendelson] p. 255	Exercise 4.41	mapprc 6614
[Mendelson] p. 255	Exercise 4.43	mapsnen 6773
[Mendelson] p. 255	Exercise 4.47	xpmapen 6812
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6648
[Mendelson] p. 255	Exercise 4.42(b)	map1 6774
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7169  djucomen 7168
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7167
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6431
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3343
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4691
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4692
[Monk1] p. 34	Definition 3.3	df-opab 4043
[Monk1] p. 36	Theorem 3.7(i)	coi1 5118  coi2 5119
[Monk1] p. 36	Theorem 3.8(v)	dm0 4817  rn0 4859
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5007
[Monk1] p. 37	Theorem 3.13(i)	relxp 4712
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4823  rnxpm 5032
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4683  xp0 5022
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4962
[Monk1] p. 38	Theorem 3.16(viii)	imai 4959
[Monk1] p. 39	Theorem 3.17	imaex 4958  imaexg 4957
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4956
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5614  funfvop 5596
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5529
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5537
[Monk1] p. 43	Theorem 4.6	funun 5231
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5735  dff13f 5737
[Monk1] p. 46	Theorem 4.15(v)	funex 5707  funrnex 6079
[Monk1] p. 50	Definition 5.4	fniunfv 5729
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5086
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3839
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6120  df-1st 6105
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6121  df-2nd 6106
[Monk2] p. 105	Axiom C4	ax-5 1435
[Monk2] p. 105	Axiom C7	ax-8 1492
[Monk2] p. 105	Axiom C8	ax-11 1494  ax-11o 1811
[Monk2] p. 105	Axiom (C8)	ax11v 1815
[Monk2] p. 109	Lemma 12	ax-7 1436
[Monk2] p. 109	Lemma 15	equvin 1851  equvini 1746  eqvinop 4220
[Monk2] p. 113	Axiom C5-1	ax-17 1514
[Monk2] p. 113	Axiom C5-2	ax6b 1639
[Monk2] p. 113	Axiom C5-3	ax-7 1436
[Monk2] p. 114	Lemma 22	hba1 1528
[Monk2] p. 114	Lemma 23	hbia1 1540  nfia1 1568
[Monk2] p. 114	Lemma 24	hba2 1539  nfa2 1567
[Moschovakis] p. 2	Chapter 2	df-stab 821  dftest 13911
[Munkres] p. 77	Example 2	distop 12685
[Munkres] p. 78	Definition of basis	df-bases 12641  isbasis3g 12644
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12572  tgval2 12651
[Munkres] p. 79	Remark	tgcl 12664
[Munkres] p. 80	Lemma 2.1	tgval3 12658
[Munkres] p. 80	Lemma 2.2	tgss2 12679  tgss3 12678
[Munkres] p. 81	Lemma 2.3	basgen 12680  basgen2 12681
[Munkres] p. 89	Definition of subspace topology	resttop 12770
[Munkres] p. 93	Theorem 6.1(1)	0cld 12712  topcld 12709
[Munkres] p. 93	Theorem 6.1(3)	uncld 12713
[Munkres] p. 94	Definition of closure	clsval 12711
[Munkres] p. 94	Definition of interior	ntrval 12710
[Munkres] p. 102	Definition of continuous function	df-cn 12788  iscn 12797  iscn2 12800
[Munkres] p. 107	Theorem 7.2(g)	cncnp 12830  cncnp2m 12831  cncnpi 12828  df-cnp 12789  iscnp 12799
[Munkres] p. 127	Theorem 10.1	metcn 13114
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6865
[Pierik], p. 9	Definition 2.4	df-womni 7124
[Pierik], p. 9	Definition 2.5	df-markov 7112  omniwomnimkv 7127
[Pierik], p. 10	Section 2.3	dfdif3 3231
[Pierik], p. 14	Definition 3.1	df-omni 7095  exmidomniim 7101  finomni 7100
[Pierik], p. 15	Section 3.1	df-nninf 7081
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 13862
[PradicBrown2022], p. 2	Remark	exmidpw 6870
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7153
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7154  exmidfodomrlemrALT 7155
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7109
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 13847  peano4nninf 13846
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 13849
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 13857
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 13859
[PradicBrown2022], p. 5	Definition 3.3	nnsf 13845
[Quine] p. 16	Definition 2.1	df-clab 2152  rabid 2640
[Quine] p. 17	Definition 2.1''	dfsb7 1979
[Quine] p. 18	Definition 2.7	df-cleq 2158
[Quine] p. 19	Definition 2.9	df-v 2727
[Quine] p. 34	Theorem 5.1	abeq2 2274
[Quine] p. 35	Theorem 5.2	abid2 2286  abid2f 2333
[Quine] p. 40	Theorem 6.1	sb5 1875
[Quine] p. 40	Theorem 6.2	sb56 1873  sb6 1874
[Quine] p. 41	Theorem 6.3	df-clel 2161
[Quine] p. 41	Theorem 6.4	eqid 2165
[Quine] p. 41	Theorem 6.5	eqcom 2167
[Quine] p. 42	Theorem 6.6	df-sbc 2951
[Quine] p. 42	Theorem 6.7	dfsbcq 2952  dfsbcq2 2953
[Quine] p. 43	Theorem 6.8	vex 2728
[Quine] p. 43	Theorem 6.9	isset 2731
[Quine] p. 44	Theorem 7.3	spcgf 2807  spcgv 2812  spcimgf 2805
[Quine] p. 44	Theorem 6.11	spsbc 2961  spsbcd 2962
[Quine] p. 44	Theorem 6.12	elex 2736
[Quine] p. 44	Theorem 6.13	elab 2869  elabg 2871  elabgf 2867
[Quine] p. 44	Theorem 6.14	noel 3412
[Quine] p. 48	Theorem 7.2	snprc 3640
[Quine] p. 48	Definition 7.1	df-pr 3582  df-sn 3581
[Quine] p. 49	Theorem 7.4	snss 3701  snssg 3708
[Quine] p. 49	Theorem 7.5	prss 3728  prssg 3729
[Quine] p. 49	Theorem 7.6	prid1 3681  prid1g 3679  prid2 3682  prid2g 3680  snid 3606  snidg 3604
[Quine] p. 51	Theorem 7.12	snexg 4162  snexprc 4164
[Quine] p. 51	Theorem 7.13	prexg 4188
[Quine] p. 53	Theorem 8.2	unisn 3804  unisng 3805
[Quine] p. 53	Theorem 8.3	uniun 3807
[Quine] p. 54	Theorem 8.6	elssuni 3816
[Quine] p. 54	Theorem 8.7	uni0 3815
[Quine] p. 56	Theorem 8.17	uniabio 5162
[Quine] p. 56	Definition 8.18	dfiota2 5153
[Quine] p. 57	Theorem 8.19	iotaval 5163
[Quine] p. 57	Theorem 8.22	iotanul 5167
[Quine] p. 58	Theorem 8.23	euiotaex 5168
[Quine] p. 58	Definition 9.1	df-op 3584
[Quine] p. 61	Theorem 9.5	opabid 4234  opelopab 4248  opelopaba 4243  opelopabaf 4250  opelopabf 4251  opelopabg 4245  opelopabga 4240  oprabid 5870
[Quine] p. 64	Definition 9.11	df-xp 4609
[Quine] p. 64	Definition 9.12	df-cnv 4611
[Quine] p. 64	Definition 9.15	df-id 4270
[Quine] p. 65	Theorem 10.3	fun0 5245
[Quine] p. 65	Theorem 10.4	funi 5219
[Quine] p. 65	Theorem 10.5	funsn 5235  funsng 5233
[Quine] p. 65	Definition 10.1	df-fun 5189
[Quine] p. 65	Definition 10.2	args 4972  dffv4g 5482
[Quine] p. 68	Definition 10.11	df-fv 5195  fv2 5480
[Quine] p. 124	Theorem 17.3	nn0opth2 10633  nn0opth2d 10632  nn0opthd 10631
[Quine] p. 284	Axiom 39(vi)	funimaex 5272  funimaexg 5271
[Rudin] p. 164	Equation 27	efcan 11613
[Rudin] p. 164	Equation 30	efzval 11620
[Rudin] p. 167	Equation 48	absefi 11705
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1416
[Sanford] p. 39	Rule 4	mptxor 1414
[Sanford] p. 40	Rule 1	mptnan 1413
[Schechter] p. 51	Definition of antisymmetry	intasym 4987
[Schechter] p. 51	Definition of irreflexivity	intirr 4989
[Schechter] p. 51	Definition of symmetry	cnvsym 4986
[Schechter] p. 51	Definition of transitivity	cotr 4984
[Schechter] p. 428	Definition 15.35	bastop1 12683
[Stoll] p. 13	Definition of symmetric difference	symdif1 3386
[Stoll] p. 16	Exercise 4.4	0dif 3479  dif0 3478
[Stoll] p. 16	Exercise 4.8	difdifdirss 3492
[Stoll] p. 19	Theorem 5.2(13)	undm 3379
[Stoll] p. 19	Theorem 5.2(13')	indmss 3380
[Stoll] p. 20	Remark	invdif 3363
[Stoll] p. 25	Definition of ordered triple	df-ot 3585
[Stoll] p. 43	Definition	uniiun 3918
[Stoll] p. 44	Definition	intiin 3919
[Stoll] p. 45	Definition	df-iin 3868
[Stoll] p. 45	Definition indexed union	df-iun 3867
[Stoll] p. 176	Theorem 3.4(27)	imandc 879  imanst 878
[Stoll] p. 262	Example 4.1	symdif1 3386
[Suppes] p. 22	Theorem 2	eq0 3426
[Suppes] p. 22	Theorem 4	eqss 3156  eqssd 3158  eqssi 3157
[Suppes] p. 23	Theorem 5	ss0 3448  ss0b 3447
[Suppes] p. 23	Theorem 6	sstr 3149
[Suppes] p. 25	Theorem 12	elin 3304  elun 3262
[Suppes] p. 26	Theorem 15	inidm 3330
[Suppes] p. 26	Theorem 16	in0 3442
[Suppes] p. 27	Theorem 23	unidm 3264
[Suppes] p. 27	Theorem 24	un0 3441
[Suppes] p. 27	Theorem 25	ssun1 3284
[Suppes] p. 27	Theorem 26	ssequn1 3291
[Suppes] p. 27	Theorem 27	unss 3295
[Suppes] p. 27	Theorem 28	indir 3370
[Suppes] p. 27	Theorem 29	undir 3371
[Suppes] p. 28	Theorem 32	difid 3476  difidALT 3477
[Suppes] p. 29	Theorem 33	difin 3358
[Suppes] p. 29	Theorem 34	indif 3364
[Suppes] p. 29	Theorem 35	undif1ss 3482
[Suppes] p. 29	Theorem 36	difun2 3487
[Suppes] p. 29	Theorem 37	difin0 3481
[Suppes] p. 29	Theorem 38	disjdif 3480
[Suppes] p. 29	Theorem 39	difundi 3373
[Suppes] p. 29	Theorem 40	difindiss 3375
[Suppes] p. 30	Theorem 41	nalset 4111
[Suppes] p. 39	Theorem 61	uniss 3809
[Suppes] p. 39	Theorem 65	uniop 4232
[Suppes] p. 41	Theorem 70	intsn 3858
[Suppes] p. 42	Theorem 71	intpr 3855  intprg 3856
[Suppes] p. 42	Theorem 73	op1stb 4455  op1stbg 4456
[Suppes] p. 42	Theorem 78	intun 3854
[Suppes] p. 44	Definition 15(a)	dfiun2 3899  dfiun2g 3897
[Suppes] p. 44	Definition 15(b)	dfiin2 3900
[Suppes] p. 47	Theorem 86	elpw 3564  elpw2 4135  elpw2g 4134  elpwg 3566
[Suppes] p. 47	Theorem 87	pwid 3573
[Suppes] p. 47	Theorem 89	pw0 3719
[Suppes] p. 48	Theorem 90	pwpw0ss 3783
[Suppes] p. 52	Theorem 101	xpss12 4710
[Suppes] p. 52	Theorem 102	xpindi 4738  xpindir 4739
[Suppes] p. 52	Theorem 103	xpundi 4659  xpundir 4660
[Suppes] p. 54	Theorem 105	elirrv 4524
[Suppes] p. 58	Theorem 2	relss 4690
[Suppes] p. 59	Theorem 4	eldm 4800  eldm2 4801  eldm2g 4799  eldmg 4798
[Suppes] p. 59	Definition 3	df-dm 4613
[Suppes] p. 60	Theorem 6	dmin 4811
[Suppes] p. 60	Theorem 8	rnun 5011
[Suppes] p. 60	Theorem 9	rnin 5012
[Suppes] p. 60	Definition 4	dfrn2 4791
[Suppes] p. 61	Theorem 11	brcnv 4786  brcnvg 4784
[Suppes] p. 62	Equation 5	elcnv 4780  elcnv2 4781
[Suppes] p. 62	Theorem 12	relcnv 4981
[Suppes] p. 62	Theorem 15	cnvin 5010
[Suppes] p. 62	Theorem 16	cnvun 5008
[Suppes] p. 63	Theorem 20	co02 5116
[Suppes] p. 63	Theorem 21	dmcoss 4872
[Suppes] p. 63	Definition 7	df-co 4612
[Suppes] p. 64	Theorem 26	cnvco 4788
[Suppes] p. 64	Theorem 27	coass 5121
[Suppes] p. 65	Theorem 31	resundi 4896
[Suppes] p. 65	Theorem 34	elima 4950  elima2 4951  elima3 4952  elimag 4949
[Suppes] p. 65	Theorem 35	imaundi 5015
[Suppes] p. 66	Theorem 40	dminss 5017
[Suppes] p. 66	Theorem 41	imainss 5018
[Suppes] p. 67	Exercise 11	cnvxp 5021
[Suppes] p. 81	Definition 34	dfec2 6500
[Suppes] p. 82	Theorem 72	elec 6536  elecg 6535
[Suppes] p. 82	Theorem 73	erth 6541  erth2 6542
[Suppes] p. 89	Theorem 96	map0b 6649
[Suppes] p. 89	Theorem 97	map0 6651  map0g 6650
[Suppes] p. 89	Theorem 98	mapsn 6652
[Suppes] p. 89	Theorem 99	mapss 6653
[Suppes] p. 92	Theorem 1	enref 6727  enrefg 6726
[Suppes] p. 92	Theorem 2	ensym 6743  ensymb 6742  ensymi 6744
[Suppes] p. 92	Theorem 3	entr 6746
[Suppes] p. 92	Theorem 4	unen 6778
[Suppes] p. 94	Theorem 15	endom 6725
[Suppes] p. 94	Theorem 16	ssdomg 6740
[Suppes] p. 94	Theorem 17	domtr 6747
[Suppes] p. 95	Theorem 18	isbth 6928
[Suppes] p. 98	Exercise 4	fundmen 6768  fundmeng 6769
[Suppes] p. 98	Exercise 6	xpdom3m 6796
[Suppes] p. 130	Definition 3	df-tr 4080
[Suppes] p. 132	Theorem 9	ssonuni 4464
[Suppes] p. 134	Definition 6	df-suc 4348
[Suppes] p. 136	Theorem Schema 22	findes 4579  finds 4576  finds1 4578  finds2 4577
[Suppes] p. 162	Definition 5	df-ltnqqs 7290  df-ltpq 7283
[Suppes] p. 228	Theorem Schema 61	onintss 4367
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2147
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2158
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2161
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2160
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2183
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5845
[TakeutiZaring] p. 14	Proposition 4.14	ru 2949
[TakeutiZaring] p. 15	Exercise 1	elpr 3596  elpr2 3597  elprg 3595
[TakeutiZaring] p. 15	Exercise 2	elsn 3591  elsn2 3609  elsn2g 3608  elsng 3590  velsn 3592
[TakeutiZaring] p. 15	Exercise 3	elop 4208
[TakeutiZaring] p. 15	Exercise 4	sneq 3586  sneqr 3739
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3594  dfsn2 3589
[TakeutiZaring] p. 16	Axiom 3	uniex 4414
[TakeutiZaring] p. 16	Exercise 6	opth 4214
[TakeutiZaring] p. 16	Exercise 8	rext 4192
[TakeutiZaring] p. 16	Corollary 5.8	unex 4418  unexg 4420
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3624
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3789
[TakeutiZaring] p. 16	Definition 5.6	df-in 3121  df-un 3119
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3802  uniprg 3803
[TakeutiZaring] p. 17	Axiom 4	vpwex 4157
[TakeutiZaring] p. 17	Exercise 1	eltp 3623
[TakeutiZaring] p. 17	Exercise 5	elsuc 4383  elsucg 4381  sstr2 3148
[TakeutiZaring] p. 17	Exercise 6	uncom 3265
[TakeutiZaring] p. 17	Exercise 7	incom 3313
[TakeutiZaring] p. 17	Exercise 8	unass 3278
[TakeutiZaring] p. 17	Exercise 9	inass 3331
[TakeutiZaring] p. 17	Exercise 10	indi 3368
[TakeutiZaring] p. 17	Exercise 11	undi 3369
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3130
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3560
[TakeutiZaring] p. 18	Exercise 7	unss2 3292
[TakeutiZaring] p. 18	Exercise 9	df-ss 3128  sseqin2 3340
[TakeutiZaring] p. 18	Exercise 10	ssid 3161
[TakeutiZaring] p. 18	Exercise 12	inss1 3341  inss2 3342
[TakeutiZaring] p. 18	Exercise 13	nssr 3201
[TakeutiZaring] p. 18	Exercise 15	unieq 3797
[TakeutiZaring] p. 18	Exercise 18	sspwb 4193
[TakeutiZaring] p. 18	Exercise 19	pweqb 4200
[TakeutiZaring] p. 20	Definition	df-rab 2452
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4108
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3117
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3410
[TakeutiZaring] p. 20	Proposition 5.15	difid 3476  difidALT 3477
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3420
[TakeutiZaring] p. 21	Theorem 5.22	setind 4515
[TakeutiZaring] p. 21	Definition 5.20	df-v 2727
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4113
[TakeutiZaring] p. 22	Exercise 1	0ss 3446
[TakeutiZaring] p. 22	Exercise 3	ssex 4118  ssexg 4120
[TakeutiZaring] p. 22	Exercise 4	inex1 4115
[TakeutiZaring] p. 22	Exercise 5	ruv 4526
[TakeutiZaring] p. 22	Exercise 6	elirr 4517
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3472
[TakeutiZaring] p. 22	Exercise 11	difdif 3246
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3382
[TakeutiZaring] p. 22	Exercise 14	difss 3247
[TakeutiZaring] p. 22	Exercise 15	sscon 3255
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2448
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2449
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4718  xpexg 4717  xpexgALT 6098
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4610
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5251
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5403  fun11 5254
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5198  svrelfun 5252
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4790
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4792
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4615
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4616
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4612
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5057  dfrel2 5053
[TakeutiZaring] p. 25	Exercise 3	xpss 4711
[TakeutiZaring] p. 25	Exercise 5	relun 4720
[TakeutiZaring] p. 25	Exercise 6	reluni 4726
[TakeutiZaring] p. 25	Exercise 9	inxp 4737
[TakeutiZaring] p. 25	Exercise 12	relres 4911
[TakeutiZaring] p. 25	Exercise 13	opelres 4888  opelresg 4890
[TakeutiZaring] p. 25	Exercise 14	dmres 4904
[TakeutiZaring] p. 25	Exercise 15	resss 4907
[TakeutiZaring] p. 25	Exercise 17	resabs1 4912
[TakeutiZaring] p. 25	Exercise 18	funres 5228
[TakeutiZaring] p. 25	Exercise 24	relco 5101
[TakeutiZaring] p. 25	Exercise 29	funco 5227
[TakeutiZaring] p. 25	Exercise 30	f1co 5404
[TakeutiZaring] p. 26	Definition 6.10	eu2 2058
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5195  fv3 5508
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5141  cnvexg 5140
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4869  dmexg 4867
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4870  rnexg 4868
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5502
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5512  tz6.12 5513  tz6.12c 5515
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5476
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5190
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5191
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5193  wfo 5185
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5192  wf1 5184
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5194  wf1o 5186
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5582  eqfnfv2 5583  eqfnfv2f 5586
[TakeutiZaring] p. 28	Exercise 5	fvco 5555
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5706  fnexALT 6078
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5705  resfunexgALT 6075
[TakeutiZaring] p. 29	Exercise 9	funimaex 5272  funimaexg 5271
[TakeutiZaring] p. 29	Definition 6.18	df-br 3982
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4973  iniseg 4975
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4266
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5196
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5777
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5778
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5783
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5785
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5793
[TakeutiZaring] p. 35	Notation	wtr 4079
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4331
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4083
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4552
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4358
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4362
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4468
[TakeutiZaring] p. 38	Definition 7.11	df-on 4345
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4462
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4528
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4558
[TakeutiZaring] p. 40	Exercise 7	dftr2 4081
[TakeutiZaring] p. 40	Exercise 11	unon 4487
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4463
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3816
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4348
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4392  sucidg 4393
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 4477
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4346
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4482  ordelsuc 4481
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4570
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4571
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4572
[TakeutiZaring] p. 43	Axiom 7	omex 4569
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4583
[TakeutiZaring] p. 43	Corollary 7.31	find 4575
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4573
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4574
[TakeutiZaring] p. 44	Exercise 2	int0 3837
[TakeutiZaring] p. 44	Exercise 3	trintssm 4095
[TakeutiZaring] p. 44	Exercise 4	intss1 3838
[TakeutiZaring] p. 44	Exercise 6	onintonm 4493
[TakeutiZaring] p. 44	Definition 7.35	df-int 3824
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6272
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6329  tfri1d 6299
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6330  tfri2d 6300
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6331
[TakeutiZaring] p. 50	Exercise 3	smoiso 6266
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6250
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6428
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6424
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6421
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6425
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6473  nnaordi 6472
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3910  uniss2 3819
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6434
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6444
[TakeutiZaring] p. 62	Exercise 5	oaword1 6435
[TakeutiZaring] p. 62	Definition 8.15	om0 6422  omsuc 6436
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6445
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6481  nnmordi 6480
[TakeutiZaring] p. 67	Definition 8.30	oei0 6423
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7139
[TakeutiZaring] p. 88	Exercise 1	en0 6757
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6819
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6820
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6705  isfi 6723
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6793
[TakeutiZaring] p. 95	Definition 10.42	df-map 6612
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6810
[Tarski] p. 67	Axiom B5	ax-4 1498
[Tarski] p. 68	Lemma 6	equid 1689
[Tarski] p. 69	Lemma 7	equcomi 1692
[Tarski] p. 70	Lemma 14	spim 1726  spime 1729  spimeh 1727  spimh 1725
[Tarski] p. 70	Lemma 16	ax-11 1494  ax-11o 1811  ax11i 1702
[Tarski] p. 70	Lemmas 16 and 17	sb6 1874
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1514
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2138  ax-14 2139
[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 2112  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 969
[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 947
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 948
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 949
[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 942  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 970
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 806
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 961
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 939
[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 1469
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 946
[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 928
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 742  pm4.56 770
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 929  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 940
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 941
[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 1379
[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 1384  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 1382
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1387
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1388
[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 944
[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 935
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 936
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 951
[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 952
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1623
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1473
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1620
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1883
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2017
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2416
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2417
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2863
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3006
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5170
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5171
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2093  eupickbi 2096
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5195
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7142