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 7080  fidcenum 6921
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6921
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7080
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12358
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6895
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6883
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12373
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12375
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12364  znnen 12331
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12376
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12377
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10689
[AczelRathjen], p. 183	Chapter 20	ax-setind 4514
[Apostol] p. 18	Theorem I.1	addcan 8078  addcan2d 8083  addcan2i 8081  addcand 8082  addcani 8080
[Apostol] p. 18	Theorem I.2	negeu 8089
[Apostol] p. 18	Theorem I.3	negsub 8146  negsubd 8215  negsubi 8176
[Apostol] p. 18	Theorem I.4	negneg 8148  negnegd 8200  negnegi 8168
[Apostol] p. 18	Theorem I.5	subdi 8283  subdid 8312  subdii 8305  subdir 8284  subdird 8313  subdiri 8306
[Apostol] p. 18	Theorem I.6	mul01 8287  mul01d 8291  mul01i 8289  mul02 8285  mul02d 8290  mul02i 8288
[Apostol] p. 18	Theorem I.9	divrecapd 8689
[Apostol] p. 18	Theorem I.10	recrecapi 8640
[Apostol] p. 18	Theorem I.12	mul2neg 8296  mul2negd 8311  mul2negi 8304  mulneg1 8293  mulneg1d 8309  mulneg1i 8302
[Apostol] p. 18	Theorem I.15	divdivdivap 8609
[Apostol] p. 20	Axiom 7	rpaddcl 9613  rpaddcld 9648  rpmulcl 9614  rpmulcld 9649
[Apostol] p. 20	Axiom 9	0nrp 9625
[Apostol] p. 20	Theorem I.17	lttri 8003
[Apostol] p. 20	Theorem I.18	ltadd1d 8436  ltadd1dd 8454  ltadd1i 8400
[Apostol] p. 20	Theorem I.19	ltmul1 8490  ltmul1a 8489  ltmul1i 8815  ltmul1ii 8823  ltmul2 8751  ltmul2d 9675  ltmul2dd 9689  ltmul2i 8818
[Apostol] p. 20	Theorem I.21	0lt1 8025
[Apostol] p. 20	Theorem I.23	lt0neg1 8366  lt0neg1d 8413  ltneg 8360  ltnegd 8421  ltnegi 8391
[Apostol] p. 20	Theorem I.25	lt2add 8343  lt2addd 8465  lt2addi 8408
[Apostol] p. 20	Definition of positive numbers	df-rp 9590
[Apostol] p. 21	Exercise 4	recgt0 8745  recgt0d 8829  recgt0i 8801  recgt0ii 8802
[Apostol] p. 22	Definition of integers	df-z 9192
[Apostol] p. 22	Definition of rationals	df-q 9558
[Apostol] p. 24	Theorem I.26	supeuti 6959
[Apostol] p. 26	Theorem I.29	arch 9111
[Apostol] p. 28	Exercise 2	btwnz 9310
[Apostol] p. 28	Exercise 3	nnrecl 9112
[Apostol] p. 28	Exercise 6	qbtwnre 10192
[Apostol] p. 28	Exercise 10(a)	zeneo 11808  zneo 9292
[Apostol] p. 29	Theorem I.35	resqrtth 10973  sqrtthi 11061
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8860
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 11969
[Apostol] p. 363	Remark	absgt0api 11088
[Apostol] p. 363	Example	abssubd 11135  abssubi 11092
[ApostolNT] p. 14	Definition	df-dvds 11728
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11744
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11768
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11764
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11758
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11760
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11745
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11746
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11751
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11783
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11785
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11787
[ApostolNT] p. 15	Definition	dfgcd2 11947
[ApostolNT] p. 16	Definition	isprm2 12049
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12024
[ApostolNT] p. 16	Theorem 1.7	prminf 12388
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11906
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11948
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 11950
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11920
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11913
[ApostolNT] p. 17	Theorem 1.8	coprm 12076
[ApostolNT] p. 17	Theorem 1.9	euclemma 12078
[ApostolNT] p. 17	Theorem 1.10	1arith2 12298
[ApostolNT] p. 19	Theorem 1.14	divalg 11861
[ApostolNT] p. 20	Theorem 1.15	eucalg 11991
[ApostolNT] p. 25	Definition	df-phi 12143
[ApostolNT] p. 26	Theorem 2.2	phisum 12172
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12154
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12158
[ApostolNT] p. 104	Definition	congr 12032
[ApostolNT] p. 106	Remark	dvdsval3 11731
[ApostolNT] p. 106	Definition	moddvds 11739
[ApostolNT] p. 107	Example 2	mod2eq0even 11815
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11816
[ApostolNT] p. 107	Example 4	zmod1congr 10276
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10313
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10581
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11763
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12035
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12037
[ApostolNT] p. 113	Theorem 5.17	eulerth 12165
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12183
[ApostolNT] p. 114	Theorem 5.19	fermltl 12166
[ApostolNT] p. 179	Definition	df-lgs 13539  lgsprme0 13583
[ApostolNT] p. 180	Example 1	1lgs 13584
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 13560
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 13575
[ApostolNT] p. 188	Definition	df-lgs 13539  lgs1 13585
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 13576
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 13578
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 13586
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 13587
[Bauer] p. 482	Section 1.2	pm2.01 606  pm2.65 649
[Bauer] p. 483	Theorem 1.3	acexmid 5841  onsucelsucexmidlem 4506
[Bauer], p. 481	Section 1.1	pwtrufal 13877
[Bauer], p. 483	Definition	n0rf 3421
[Bauer], p. 483	Theorem 1.2	2irrexpq 13534  2irrexpqap 13536
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6842
[Bauer], p. 494	Theorem 5.5	ivthinc 13261
[BauerHanson], p. 27	Proposition 5.2	cnstab 8543
[BauerSwan], p. 14	Remark	0ct 7072  ctm 7074
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 13881
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7080
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7442
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7355
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7444
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7478  addlocpr 7477
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7504
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7507
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7512
[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 4103
[BellMachover] p. 466	Axiom Pow	axpow3 4156
[BellMachover] p. 466	Axiom Union	axun2 4413
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4519
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4362
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4522
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4473
[BellMachover] p. 471	Definition of Lim	df-ilim 4347
[BellMachover] p. 472	Axiom Inf	zfinf2 4566
[BellMachover] p. 473	Theorem 2.8	limom 4591
[Bobzien] p. 116	Statement T3	stoic3 1419
[Bobzien] p. 117	Statement T2	stoic2a 1417
[Bobzien] p. 117	Statement T4	stoic4a 1420
[BourbakiAlg1] p. 1	Definition 1	df-mgm 12587
[BourbakiEns] p.	Proposition 8	fcof1 5751  fcofo 5752
[BourbakiTop1] p.	Remark	xnegmnf 9765  xnegpnf 9764
[BourbakiTop1] p.	Remark	rexneg 9766
[BourbakiTop1] p.	Proposition	ishmeo 12944
[BourbakiTop1] p.	Property V_i	ssnei2 12797
[BourbakiTop1] p.	Property V_ii	innei 12803
[BourbakiTop1] p.	Property V_iv	neissex 12805
[BourbakiTop1] p.	Proposition 1	neipsm 12794  neiss 12790
[BourbakiTop1] p.	Proposition 2	cnptopco 12862
[BourbakiTop1] p.	Proposition 4	imasnopn 12939
[BourbakiTop1] p.	Property V_iii	elnei 12792
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 12636
[Bruck] p. 1	Section I.1	df-mgm 12587
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4045
[Cohen] p. 301	Remark	relogoprlem 13429
[Cohen] p. 301	Property 2	relogmul 13430  relogmuld 13445
[Cohen] p. 301	Property 3	relogdiv 13431  relogdivd 13446
[Cohen] p. 301	Property 4	relogexp 13433
[Cohen] p. 301	Property 1a	log1 13427
[Cohen] p. 301	Property 1b	loge 13428
[Cohen4] p. 348	Observation	relogbcxpbap 13523
[Cohen4] p. 352	Definition	rpelogb 13507
[Cohen4] p. 361	Property 2	rprelogbmul 13513
[Cohen4] p. 361	Property 3	logbrec 13518  rprelogbdiv 13515
[Cohen4] p. 361	Property 4	rplogbreexp 13511
[Cohen4] p. 361	Property 6	relogbexpap 13516
[Cohen4] p. 361	Property 1(a)	rplogbid1 13505
[Cohen4] p. 361	Property 1(b)	rplogb1 13506
[Cohen4] p. 367	Property	rplogbchbase 13508
[Cohen4] p. 377	Property 2	logblt 13520
[Crosilla] p.	Axiom 1	ax-ext 2147
[Crosilla] p.	Axiom 2	ax-pr 4187
[Crosilla] p.	Axiom 3	ax-un 4411
[Crosilla] p.	Axiom 4	ax-nul 4108
[Crosilla] p.	Axiom 5	ax-iinf 4565
[Crosilla] p.	Axiom 6	ru 2950
[Crosilla] p.	Axiom 8	ax-pow 4153
[Crosilla] p.	Axiom 9	ax-setind 4514
[Crosilla], p.	Axiom 6	ax-sep 4100
[Crosilla], p.	Axiom 7	ax-coll 4097
[Crosilla], p.	Axiom 7'	repizf 4098
[Crosilla], p.	Theorem is stated	ordtriexmid 4498
[Crosilla], p.	Axiom of choice implies instances	acexmid 5841
[Crosilla], p.	Definition of ordinal	df-iord 4344
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4512
[Eisenberg] p. 67	Definition 5.3	df-dif 3118
[Eisenberg] p. 82	Definition 6.3	df-iom 4568
[Eisenberg] p. 125	Definition 8.21	df-map 6616
[Enderton] p. 18	Axiom of Empty Set	axnul 4107
[Enderton] p. 19	Definition	df-tp 3584
[Enderton] p. 26	Exercise 5	unissb 3819
[Enderton] p. 26	Exercise 10	pwel 4196
[Enderton] p. 28	Exercise 7(b)	pwunim 4264
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3935  iinin2m 3934  iunin1 3930  iunin2 3929
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3933  iundif2ss 3931
[Enderton] p. 33	Exercise 23	iinuniss 3948
[Enderton] p. 33	Exercise 25	iununir 3949
[Enderton] p. 33	Exercise 24(a)	iinpw 3956
[Enderton] p. 33	Exercise 24(b)	iunpw 4458  iunpwss 3957
[Enderton] p. 38	Exercise 6(a)	unipw 4195
[Enderton] p. 38	Exercise 6(b)	pwuni 4171
[Enderton] p. 41	Lemma 3D	opeluu 4428  rnex 4871  rnexg 4869
[Enderton] p. 41	Exercise 8	dmuni 4814  rnuni 5015
[Enderton] p. 42	Definition of a function	dffun7 5215  dffun8 5216
[Enderton] p. 43	Definition of function value	funfvdm2 5550
[Enderton] p. 43	Definition of single-rooted	funcnv 5249
[Enderton] p. 44	Definition (d)	dfima2 4948  dfima3 4949
[Enderton] p. 47	Theorem 3H	fvco2 5555
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7162
[Enderton] p. 50	Theorem 3K(a)	imauni 5729
[Enderton] p. 52	Definition	df-map 6616
[Enderton] p. 53	Exercise 21	coass 5122
[Enderton] p. 53	Exercise 27	dmco 5112
[Enderton] p. 53	Exercise 14(a)	funin 5259
[Enderton] p. 53	Exercise 22(a)	imass2 4980
[Enderton] p. 54	Remark	ixpf 6686  ixpssmap 6698
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6665
[Enderton] p. 56	Theorem 3M	erref 6521
[Enderton] p. 57	Lemma 3N	erthi 6547
[Enderton] p. 57	Definition	df-ec 6503
[Enderton] p. 58	Definition	df-qs 6507
[Enderton] p. 60	Theorem 3Q	th3q 6606  th3qcor 6605  th3qlem1 6603  th3qlem2 6604
[Enderton] p. 61	Exercise 35	df-ec 6503
[Enderton] p. 65	Exercise 56(a)	dmun 4811
[Enderton] p. 68	Definition of successor	df-suc 4349
[Enderton] p. 71	Definition	df-tr 4081  dftr4 4085
[Enderton] p. 72	Theorem 4E	unisuc 4391  unisucg 4392
[Enderton] p. 73	Exercise 6	unisuc 4391  unisucg 4392
[Enderton] p. 73	Exercise 5(a)	truni 4094
[Enderton] p. 73	Exercise 5(b)	trint 4095
[Enderton] p. 79	Theorem 4I(A1)	nna0 6442
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6444  onasuc 6434
[Enderton] p. 79	Definition of operation value	df-ov 5845
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6443
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6445  onmsuc 6441
[Enderton] p. 81	Theorem 4K(1)	nnaass 6453
[Enderton] p. 81	Theorem 4K(2)	nna0r 6446  nnacom 6452
[Enderton] p. 81	Theorem 4K(3)	nndi 6454
[Enderton] p. 81	Theorem 4K(4)	nnmass 6455
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6457
[Enderton] p. 82	Exercise 16	nnm0r 6447  nnmsucr 6456
[Enderton] p. 88	Exercise 23	nnaordex 6495
[Enderton] p. 129	Definition	df-en 6707
[Enderton] p. 132	Theorem 6B(b)	canth 5796
[Enderton] p. 133	Exercise 1	xpomen 12328
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6831
[Enderton] p. 136	Corollary 6E	nneneq 6823
[Enderton] p. 139	Theorem 6H(c)	mapen 6812
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7174
[Enderton] p. 143	Theorem 6J	dju0en 7170  dju1en 7169
[Enderton] p. 144	Corollary 6K	undif2ss 3484
[Enderton] p. 145	Figure 38	ffoss 5464
[Enderton] p. 145	Definition	df-dom 6708
[Enderton] p. 146	Example 1	domen 6717  domeng 6718
[Enderton] p. 146	Example 3	nndomo 6830
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6801  xpdom1g 6799  xpdom2g 6798
[Enderton] p. 168	Definition	df-po 4274
[Enderton] p. 192	Theorem 7M(a)	oneli 4406
[Enderton] p. 192	Theorem 7M(b)	ontr1 4367
[Enderton] p. 192	Theorem 7M(c)	onirri 4520
[Enderton] p. 193	Corollary 7N(b)	0elon 4370
[Enderton] p. 193	Corollary 7N(c)	onsuci 4493
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4466
[Enderton] p. 194	Remark	onprc 4529
[Enderton] p. 194	Exercise 16	suc11 4535
[Enderton] p. 197	Definition	df-card 7136
[Enderton] p. 200	Exercise 25	tfis 4560
[Enderton] p. 206	Theorem 7X(b)	en2lp 4531
[Enderton] p. 207	Exercise 34	opthreg 4533
[Enderton] p. 208	Exercise 35	suc11g 4534
[Geuvers], p. 1	Remark	expap0 10485
[Geuvers], p. 6	Lemma 2.13	mulap0r 8513
[Geuvers], p. 6	Lemma 2.15	mulap0 8551
[Geuvers], p. 9	Lemma 2.35	msqge0 8514
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7872
[Geuvers], p. 10	Lemma 3.9	maxcom 11145
[Geuvers], p. 10	Lemma 3.10	maxle1 11153  maxle2 11154
[Geuvers], p. 10	Lemma 3.11	maxleast 11155
[Geuvers], p. 10	Lemma 3.12	maxleb 11158
[Geuvers], p. 11	Definition 3.13	dfabsmax 11159
[Geuvers], p. 17	Definition 6.1	df-ap 8480
[Gleason] p. 117	Proposition 9-2.1	df-enq 7288  enqer 7299
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7292  df-nqqs 7289
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7285  df-plqqs 7290
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7286  df-mqqs 7291
[Gleason] p. 119	Proposition 9-2.5	df-rq 7293
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7349
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7352  ltbtwnnq 7357  ltbtwnnqq 7356
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7341
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7342
[Gleason] p. 123	Proposition 9-3.5	addclpr 7478
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7520
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7519
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7538
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7554
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7560  ltaprlem 7559
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7557
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7513
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7533
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7522
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7521
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7529
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7579
[Gleason] p. 126	Proposition 9-4.1	df-enr 7667  enrer 7676
[Gleason] p. 126	Proposition 9-4.2	df-0r 7672  df-1r 7673  df-nr 7668
[Gleason] p. 126	Proposition 9-4.3	df-mr 7670  df-plr 7669  negexsr 7713  recexsrlem 7715
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7671
[Gleason] p. 130	Proposition 10-1.3	creui 8855  creur 8854  cru 8500
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7864  axcnre 7822
[Gleason] p. 132	Definition 10-3.1	crim 10800  crimd 10919  crimi 10879  crre 10799  crred 10918  crrei 10878
[Gleason] p. 132	Definition 10-3.2	remim 10802  remimd 10884
[Gleason] p. 133	Definition 10.36	absval2 10999  absval2d 11127  absval2i 11086
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10826  cjaddd 10907  cjaddi 10874
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10827  cjmuld 10908  cjmuli 10875
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10825  cjcjd 10885  cjcji 10857
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10824  cjreb 10808  cjrebd 10888  cjrebi 10860  cjred 10913  rere 10807  rereb 10805  rerebd 10887  rerebi 10859  rered 10911
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10833  addcjd 10899  addcji 10869
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10943
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 10994  abscjd 11132  abscji 11090
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11006  abs00d 11128  abs00i 11087  absne0d 11129
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11038  releabsd 11133  releabsi 11091
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11011  absmuld 11136  absmuli 11093
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 10997  sqabsaddi 11094
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11046  abstrid 11138  abstrii 11097
[Gleason] p. 134	Definition 10-4.1	df-exp 10455  exp0 10459  expp1 10462  expp1d 10589
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10497  expaddd 10590
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 13473  cxpmuld 13496  expmul 10500  expmuld 10591
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10494  mulexpd 10603  rpmulcxp 13470
[Gleason] p. 141	Definition 11-2.1	fzval 9946
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11267
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11269
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11268
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11272
[Gleason] p. 172	Corollary 12-2.5	climrecl 11265
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11261  climcj 11262  climim 11264  climre 11263
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7938  df-xr 7937  ltxr 9711
[Gleason] p. 180	Theorem 12-5.3	climcau 11288
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10235
[Gleason] p. 223	Definition 14-1.1	df-met 12629
[Gleason] p. 223	Definition 14-1.1(a)	met0 13004  xmet0 13003
[Gleason] p. 223	Definition 14-1.1(c)	metsym 13011
[Gleason] p. 223	Definition 14-1.1(d)	mettri 13013  mstri 13113  xmettri 13012  xmstri 13112
[Gleason] p. 230	Proposition 14-2.6	txlm 12919
[Gleason] p. 240	Proposition 14-4.2	metcnp3 13151
[Gleason] p. 243	Proposition 14-4.16	addcn2 11251  addcncntop 13192  mulcn2 11253  mulcncntop 13194  subcn2 11252  subcncntop 13193
[Gleason] p. 295	Remark	bcval3 10664  bcval4 10665
[Gleason] p. 295	Equation 2	bcpasc 10679
[Gleason] p. 295	Definition of binomial coefficient	bcval 10662  df-bc 10661
[Gleason] p. 296	Remark	bcn0 10668  bcnn 10670
[Gleason] p. 296	Theorem 15-2.8	binom 11425
[Gleason] p. 308	Equation 2	ef0 11613
[Gleason] p. 308	Equation 3	efcj 11614
[Gleason] p. 309	Corollary 15-4.3	efne0 11619
[Gleason] p. 309	Corollary 15-4.4	efexp 11623
[Gleason] p. 310	Equation 14	sinadd 11677
[Gleason] p. 310	Equation 15	cosadd 11678
[Gleason] p. 311	Equation 17	sincossq 11689
[Gleason] p. 311	Equation 18	cosbnd 11694  sinbnd 11693
[Gleason] p. 311	Definition of ` `	df-pi 11594
[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 13950
[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 7181
[HoTT], p.	Theorem 7.2.6	nndceq 6467
[HoTT], p.	Exercise 11.10	neapmkv 13946
[HoTT], p.	Exercise 11.11	mulap0bd 8554
[HoTT], p.	Section 11.2.1	df-iltp 7411  df-imp 7410  df-iplp 7409  df-reap 8473
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7603
[HoTT], p.	Corollary 11.4.3	conventions 13602
[HoTT], p.	Exercise 11.6(i)	dcapnconst 13939  dceqnconst 13938
[HoTT], p.	Corollary 11.2.13	axcaucvg 7841  caucvgpr 7623  caucvgprpr 7653  caucvgsr 7743
[HoTT], p.	Definition 11.2.1	df-inp 7407
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 13944
[HoTT], p.	Proposition 11.2.3	df-iso 4275  ltpopr 7536  ltsopr 7537
[HoTT], p.	Definition 11.2.7(v)	apsym 8504  reapcotr 8496  reapirr 8475
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8025  gt0add 8471  leadd1 8328  lelttr 7987  lemul1a 8753  lenlt 7974  ltadd1 8327  ltletr 7988  ltmul1 8490  reaplt 8486
[Jech] p. 4	Definition of class	cv 1342  cvjust 2160
[Jech] p. 78	Note	opthprc 4655
[KalishMontague] p. 81	Note 1	ax-i9 1518
[Kreyszig] p. 3	Property M1	metcl 12993  xmetcl 12992
[Kreyszig] p. 4	Property M2	meteq0 13000
[Kreyszig] p. 12	Equation 5	muleqadd 8565
[Kreyszig] p. 18	Definition 1.3-2	mopnval 13082
[Kreyszig] p. 19	Remark	mopntopon 13083
[Kreyszig] p. 19	Theorem T1	mopn0 13128  mopnm 13088
[Kreyszig] p. 19	Theorem T2	unimopn 13126
[Kreyszig] p. 19	Definition of neighborhood	neibl 13131
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 13153
[Kreyszig] p. 25	Definition 1.4-1	lmbr 12853
[Kunen] p. 10	Axiom 0	a9e 1684
[Kunen] p. 12	Axiom 6	zfrep6 4099
[Kunen] p. 24	Definition 10.24	mapval 6626  mapvalg 6624
[Kunen] p. 31	Definition 10.24	mapex 6620
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3876
[Lang] p. 3	Statement	lidrideqd 12612
[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 3495
[Margaris] p. 89	Theorem 19.3	19.3 1542  19.3h 1541  rr19.3v 2865
[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 2572
[Margaris] p. 90	Theorem 19.14	exnalim 1634
[Margaris] p. 90	Theorem 19.15	albi 1456  ralbi 2598
[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 2599
[Margaris] p. 90	Theorem 19.19	19.19 1654
[Margaris] p. 90	Theorem 19.20	alim 1445  alimd 1509  alimdh 1455  alimdv 1867  ralimdaa 2532  ralimdv 2534  ralimdva 2533  ralimdvva 2535  sbcimdv 3016
[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 2542  r19.21be 2557  r19.21bi 2554  r19.21t 2541  r19.21v 2543  ralrimd 2544  ralrimdv 2545  ralrimdva 2546  ralrimdvv 2550  ralrimdvva 2551  ralrimi 2537  ralrimiv 2538  ralrimiva 2539  ralrimivv 2547  ralrimivva 2548  ralrimivvva 2549  ralrimivw 2540  rexlimi 2576
[Margaris] p. 90	Theorem 19.22	2alimdv 1869  2eximdv 1870  exim 1587  eximd 1600  eximdh 1599  eximdv 1868  rexim 2560  reximdai 2564  reximddv 2569  reximddv2 2571  reximdv 2567  reximdv2 2565  reximdva 2568  reximdvai 2566  reximi2 2562
[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 2574  r19.23v 2575  rexlimd 2580  rexlimdv 2582  rexlimdv3a 2585  rexlimdva 2583  rexlimdva2 2586  rexlimdvaa 2584  rexlimdvv 2590  rexlimdvva 2591  rexlimdvw 2587  rexlimiv 2577  rexlimiva 2578  rexlimivv 2589
[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 2595  r19.26-3 2596  r19.26 2592  r19.26m 2597
[Margaris] p. 90	Theorem 19.27	19.27 1549  19.27h 1548  19.27v 1887  r19.27av 2601  r19.27m 3504  r19.27mv 3505
[Margaris] p. 90	Theorem 19.28	19.28 1551  19.28h 1550  19.28v 1888  r19.28av 2602  r19.28m 3498  r19.28mv 3501  rr19.28v 2866
[Margaris] p. 90	Theorem 19.29	19.29 1608  19.29r 1609  19.29r2 1610  19.29x 1611  r19.29 2603  r19.29d2r 2610  r19.29r 2604
[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 2612  r19.32vdc 2615  r19.32vr 2614
[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 2617
[Margaris] p. 90	Theorem 19.37	19.37-1 1662  19.37aiv 1663  r19.37 2618  r19.37av 2619
[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 2620
[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 2621  r19.41v 2622
[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 2623
[Margaris] p. 90	Theorem 19.43	19.43 1616  r19.43 2624
[Margaris] p. 90	Theorem 19.44	19.44 1670  r19.44av 2625  r19.44mv 3503
[Margaris] p. 90	Theorem 19.45	19.45 1671  r19.45av 2626  r19.45mv 3502
[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 3033  rspsbca 3034  stdpc4 1763
[Mendelson] p. 69	Axiom 5	ra5 3039  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 3445
[Mendelson] p. 231	Exercise 4.10(l)	unv 3446
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3362
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3410
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3363
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3253
[Mendelson] p. 231	Definition of union	unssin 3361
[Mendelson] p. 235	Exercise 4.12(c)	univ 4454
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3788
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4260
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4261
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4262
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3809
[Mendelson] p. 235	Exercise 4.12(p)	reli 4733
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5124
[Mendelson] p. 246	Definition of successor	df-suc 4349
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6811
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6787  xpsneng 6788
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6793  xpcomeng 6794
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6796
[Mendelson] p. 255	Exercise 4.39	endisj 6790
[Mendelson] p. 255	Exercise 4.41	mapprc 6618
[Mendelson] p. 255	Exercise 4.43	mapsnen 6777
[Mendelson] p. 255	Exercise 4.47	xpmapen 6816
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6652
[Mendelson] p. 255	Exercise 4.42(b)	map1 6778
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7173  djucomen 7172
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7171
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6435
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3344
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4692
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4693
[Monk1] p. 34	Definition 3.3	df-opab 4044
[Monk1] p. 36	Theorem 3.7(i)	coi1 5119  coi2 5120
[Monk1] p. 36	Theorem 3.8(v)	dm0 4818  rn0 4860
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5008
[Monk1] p. 37	Theorem 3.13(i)	relxp 4713
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4824  rnxpm 5033
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4684  xp0 5023
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4963
[Monk1] p. 38	Theorem 3.16(viii)	imai 4960
[Monk1] p. 39	Theorem 3.17	imaex 4959  imaexg 4958
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4957
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5615  funfvop 5597
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5530
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5538
[Monk1] p. 43	Theorem 4.6	funun 5232
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5736  dff13f 5738
[Monk1] p. 46	Theorem 4.15(v)	funex 5708  funrnex 6082
[Monk1] p. 50	Definition 5.4	fniunfv 5730
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5087
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3840
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6123  df-1st 6108
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6124  df-2nd 6109
[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 4221
[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 13951
[Munkres] p. 77	Example 2	distop 12725
[Munkres] p. 78	Definition of basis	df-bases 12681  isbasis3g 12684
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12577  tgval2 12691
[Munkres] p. 79	Remark	tgcl 12704
[Munkres] p. 80	Lemma 2.1	tgval3 12698
[Munkres] p. 80	Lemma 2.2	tgss2 12719  tgss3 12718
[Munkres] p. 81	Lemma 2.3	basgen 12720  basgen2 12721
[Munkres] p. 89	Definition of subspace topology	resttop 12810
[Munkres] p. 93	Theorem 6.1(1)	0cld 12752  topcld 12749
[Munkres] p. 93	Theorem 6.1(3)	uncld 12753
[Munkres] p. 94	Definition of closure	clsval 12751
[Munkres] p. 94	Definition of interior	ntrval 12750
[Munkres] p. 102	Definition of continuous function	df-cn 12828  iscn 12837  iscn2 12840
[Munkres] p. 107	Theorem 7.2(g)	cncnp 12870  cncnp2m 12871  cncnpi 12868  df-cnp 12829  iscnp 12839
[Munkres] p. 127	Theorem 10.1	metcn 13154
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6869
[Pierik], p. 9	Definition 2.4	df-womni 7128
[Pierik], p. 9	Definition 2.5	df-markov 7116  omniwomnimkv 7131
[Pierik], p. 10	Section 2.3	dfdif3 3232
[Pierik], p. 14	Definition 3.1	df-omni 7099  exmidomniim 7105  finomni 7104
[Pierik], p. 15	Section 3.1	df-nninf 7085
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 13902
[PradicBrown2022], p. 2	Remark	exmidpw 6874
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7157
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7158  exmidfodomrlemrALT 7159
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7113
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 13887  peano4nninf 13886
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 13889
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 13897
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 13899
[PradicBrown2022], p. 5	Definition 3.3	nnsf 13885
[Quine] p. 16	Definition 2.1	df-clab 2152  rabid 2641
[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 2728
[Quine] p. 34	Theorem 5.1	abeq2 2275
[Quine] p. 35	Theorem 5.2	abid2 2287  abid2f 2334
[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 2952
[Quine] p. 42	Theorem 6.7	dfsbcq 2953  dfsbcq2 2954
[Quine] p. 43	Theorem 6.8	vex 2729
[Quine] p. 43	Theorem 6.9	isset 2732
[Quine] p. 44	Theorem 7.3	spcgf 2808  spcgv 2813  spcimgf 2806
[Quine] p. 44	Theorem 6.11	spsbc 2962  spsbcd 2963
[Quine] p. 44	Theorem 6.12	elex 2737
[Quine] p. 44	Theorem 6.13	elab 2870  elabg 2872  elabgf 2868
[Quine] p. 44	Theorem 6.14	noel 3413
[Quine] p. 48	Theorem 7.2	snprc 3641
[Quine] p. 48	Definition 7.1	df-pr 3583  df-sn 3582
[Quine] p. 49	Theorem 7.4	snss 3702  snssg 3709
[Quine] p. 49	Theorem 7.5	prss 3729  prssg 3730
[Quine] p. 49	Theorem 7.6	prid1 3682  prid1g 3680  prid2 3683  prid2g 3681  snid 3607  snidg 3605
[Quine] p. 51	Theorem 7.12	snexg 4163  snexprc 4165
[Quine] p. 51	Theorem 7.13	prexg 4189
[Quine] p. 53	Theorem 8.2	unisn 3805  unisng 3806
[Quine] p. 53	Theorem 8.3	uniun 3808
[Quine] p. 54	Theorem 8.6	elssuni 3817
[Quine] p. 54	Theorem 8.7	uni0 3816
[Quine] p. 56	Theorem 8.17	uniabio 5163
[Quine] p. 56	Definition 8.18	dfiota2 5154
[Quine] p. 57	Theorem 8.19	iotaval 5164
[Quine] p. 57	Theorem 8.22	iotanul 5168
[Quine] p. 58	Theorem 8.23	euiotaex 5169
[Quine] p. 58	Definition 9.1	df-op 3585
[Quine] p. 61	Theorem 9.5	opabid 4235  opelopab 4249  opelopaba 4244  opelopabaf 4251  opelopabf 4252  opelopabg 4246  opelopabga 4241  oprabid 5874
[Quine] p. 64	Definition 9.11	df-xp 4610
[Quine] p. 64	Definition 9.12	df-cnv 4612
[Quine] p. 64	Definition 9.15	df-id 4271
[Quine] p. 65	Theorem 10.3	fun0 5246
[Quine] p. 65	Theorem 10.4	funi 5220
[Quine] p. 65	Theorem 10.5	funsn 5236  funsng 5234
[Quine] p. 65	Definition 10.1	df-fun 5190
[Quine] p. 65	Definition 10.2	args 4973  dffv4g 5483
[Quine] p. 68	Definition 10.11	df-fv 5196  fv2 5481
[Quine] p. 124	Theorem 17.3	nn0opth2 10637  nn0opth2d 10636  nn0opthd 10635
[Quine] p. 284	Axiom 39(vi)	funimaex 5273  funimaexg 5272
[Rudin] p. 164	Equation 27	efcan 11617
[Rudin] p. 164	Equation 30	efzval 11624
[Rudin] p. 167	Equation 48	absefi 11709
[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 4988
[Schechter] p. 51	Definition of irreflexivity	intirr 4990
[Schechter] p. 51	Definition of symmetry	cnvsym 4987
[Schechter] p. 51	Definition of transitivity	cotr 4985
[Schechter] p. 428	Definition 15.35	bastop1 12723
[Stoll] p. 13	Definition of symmetric difference	symdif1 3387
[Stoll] p. 16	Exercise 4.4	0dif 3480  dif0 3479
[Stoll] p. 16	Exercise 4.8	difdifdirss 3493
[Stoll] p. 19	Theorem 5.2(13)	undm 3380
[Stoll] p. 19	Theorem 5.2(13')	indmss 3381
[Stoll] p. 20	Remark	invdif 3364
[Stoll] p. 25	Definition of ordered triple	df-ot 3586
[Stoll] p. 43	Definition	uniiun 3919
[Stoll] p. 44	Definition	intiin 3920
[Stoll] p. 45	Definition	df-iin 3869
[Stoll] p. 45	Definition indexed union	df-iun 3868
[Stoll] p. 176	Theorem 3.4(27)	imandc 879  imanst 878
[Stoll] p. 262	Example 4.1	symdif1 3387
[Suppes] p. 22	Theorem 2	eq0 3427
[Suppes] p. 22	Theorem 4	eqss 3157  eqssd 3159  eqssi 3158
[Suppes] p. 23	Theorem 5	ss0 3449  ss0b 3448
[Suppes] p. 23	Theorem 6	sstr 3150
[Suppes] p. 25	Theorem 12	elin 3305  elun 3263
[Suppes] p. 26	Theorem 15	inidm 3331
[Suppes] p. 26	Theorem 16	in0 3443
[Suppes] p. 27	Theorem 23	unidm 3265
[Suppes] p. 27	Theorem 24	un0 3442
[Suppes] p. 27	Theorem 25	ssun1 3285
[Suppes] p. 27	Theorem 26	ssequn1 3292
[Suppes] p. 27	Theorem 27	unss 3296
[Suppes] p. 27	Theorem 28	indir 3371
[Suppes] p. 27	Theorem 29	undir 3372
[Suppes] p. 28	Theorem 32	difid 3477  difidALT 3478
[Suppes] p. 29	Theorem 33	difin 3359
[Suppes] p. 29	Theorem 34	indif 3365
[Suppes] p. 29	Theorem 35	undif1ss 3483
[Suppes] p. 29	Theorem 36	difun2 3488
[Suppes] p. 29	Theorem 37	difin0 3482
[Suppes] p. 29	Theorem 38	disjdif 3481
[Suppes] p. 29	Theorem 39	difundi 3374
[Suppes] p. 29	Theorem 40	difindiss 3376
[Suppes] p. 30	Theorem 41	nalset 4112
[Suppes] p. 39	Theorem 61	uniss 3810
[Suppes] p. 39	Theorem 65	uniop 4233
[Suppes] p. 41	Theorem 70	intsn 3859
[Suppes] p. 42	Theorem 71	intpr 3856  intprg 3857
[Suppes] p. 42	Theorem 73	op1stb 4456  op1stbg 4457
[Suppes] p. 42	Theorem 78	intun 3855
[Suppes] p. 44	Definition 15(a)	dfiun2 3900  dfiun2g 3898
[Suppes] p. 44	Definition 15(b)	dfiin2 3901
[Suppes] p. 47	Theorem 86	elpw 3565  elpw2 4136  elpw2g 4135  elpwg 3567
[Suppes] p. 47	Theorem 87	pwid 3574
[Suppes] p. 47	Theorem 89	pw0 3720
[Suppes] p. 48	Theorem 90	pwpw0ss 3784
[Suppes] p. 52	Theorem 101	xpss12 4711
[Suppes] p. 52	Theorem 102	xpindi 4739  xpindir 4740
[Suppes] p. 52	Theorem 103	xpundi 4660  xpundir 4661
[Suppes] p. 54	Theorem 105	elirrv 4525
[Suppes] p. 58	Theorem 2	relss 4691
[Suppes] p. 59	Theorem 4	eldm 4801  eldm2 4802  eldm2g 4800  eldmg 4799
[Suppes] p. 59	Definition 3	df-dm 4614
[Suppes] p. 60	Theorem 6	dmin 4812
[Suppes] p. 60	Theorem 8	rnun 5012
[Suppes] p. 60	Theorem 9	rnin 5013
[Suppes] p. 60	Definition 4	dfrn2 4792
[Suppes] p. 61	Theorem 11	brcnv 4787  brcnvg 4785
[Suppes] p. 62	Equation 5	elcnv 4781  elcnv2 4782
[Suppes] p. 62	Theorem 12	relcnv 4982
[Suppes] p. 62	Theorem 15	cnvin 5011
[Suppes] p. 62	Theorem 16	cnvun 5009
[Suppes] p. 63	Theorem 20	co02 5117
[Suppes] p. 63	Theorem 21	dmcoss 4873
[Suppes] p. 63	Definition 7	df-co 4613
[Suppes] p. 64	Theorem 26	cnvco 4789
[Suppes] p. 64	Theorem 27	coass 5122
[Suppes] p. 65	Theorem 31	resundi 4897
[Suppes] p. 65	Theorem 34	elima 4951  elima2 4952  elima3 4953  elimag 4950
[Suppes] p. 65	Theorem 35	imaundi 5016
[Suppes] p. 66	Theorem 40	dminss 5018
[Suppes] p. 66	Theorem 41	imainss 5019
[Suppes] p. 67	Exercise 11	cnvxp 5022
[Suppes] p. 81	Definition 34	dfec2 6504
[Suppes] p. 82	Theorem 72	elec 6540  elecg 6539
[Suppes] p. 82	Theorem 73	erth 6545  erth2 6546
[Suppes] p. 89	Theorem 96	map0b 6653
[Suppes] p. 89	Theorem 97	map0 6655  map0g 6654
[Suppes] p. 89	Theorem 98	mapsn 6656
[Suppes] p. 89	Theorem 99	mapss 6657
[Suppes] p. 92	Theorem 1	enref 6731  enrefg 6730
[Suppes] p. 92	Theorem 2	ensym 6747  ensymb 6746  ensymi 6748
[Suppes] p. 92	Theorem 3	entr 6750
[Suppes] p. 92	Theorem 4	unen 6782
[Suppes] p. 94	Theorem 15	endom 6729
[Suppes] p. 94	Theorem 16	ssdomg 6744
[Suppes] p. 94	Theorem 17	domtr 6751
[Suppes] p. 95	Theorem 18	isbth 6932
[Suppes] p. 98	Exercise 4	fundmen 6772  fundmeng 6773
[Suppes] p. 98	Exercise 6	xpdom3m 6800
[Suppes] p. 130	Definition 3	df-tr 4081
[Suppes] p. 132	Theorem 9	ssonuni 4465
[Suppes] p. 134	Definition 6	df-suc 4349
[Suppes] p. 136	Theorem Schema 22	findes 4580  finds 4577  finds1 4579  finds2 4578
[Suppes] p. 162	Definition 5	df-ltnqqs 7294  df-ltpq 7287
[Suppes] p. 228	Theorem Schema 61	onintss 4368
[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 5846
[TakeutiZaring] p. 14	Proposition 4.14	ru 2950
[TakeutiZaring] p. 15	Exercise 1	elpr 3597  elpr2 3598  elprg 3596
[TakeutiZaring] p. 15	Exercise 2	elsn 3592  elsn2 3610  elsn2g 3609  elsng 3591  velsn 3593
[TakeutiZaring] p. 15	Exercise 3	elop 4209
[TakeutiZaring] p. 15	Exercise 4	sneq 3587  sneqr 3740
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3595  dfsn2 3590
[TakeutiZaring] p. 16	Axiom 3	uniex 4415
[TakeutiZaring] p. 16	Exercise 6	opth 4215
[TakeutiZaring] p. 16	Exercise 8	rext 4193
[TakeutiZaring] p. 16	Corollary 5.8	unex 4419  unexg 4421
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3625
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3790
[TakeutiZaring] p. 16	Definition 5.6	df-in 3122  df-un 3120
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3803  uniprg 3804
[TakeutiZaring] p. 17	Axiom 4	vpwex 4158
[TakeutiZaring] p. 17	Exercise 1	eltp 3624
[TakeutiZaring] p. 17	Exercise 5	elsuc 4384  elsucg 4382  sstr2 3149
[TakeutiZaring] p. 17	Exercise 6	uncom 3266
[TakeutiZaring] p. 17	Exercise 7	incom 3314
[TakeutiZaring] p. 17	Exercise 8	unass 3279
[TakeutiZaring] p. 17	Exercise 9	inass 3332
[TakeutiZaring] p. 17	Exercise 10	indi 3369
[TakeutiZaring] p. 17	Exercise 11	undi 3370
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3131
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3561
[TakeutiZaring] p. 18	Exercise 7	unss2 3293
[TakeutiZaring] p. 18	Exercise 9	df-ss 3129  sseqin2 3341
[TakeutiZaring] p. 18	Exercise 10	ssid 3162
[TakeutiZaring] p. 18	Exercise 12	inss1 3342  inss2 3343
[TakeutiZaring] p. 18	Exercise 13	nssr 3202
[TakeutiZaring] p. 18	Exercise 15	unieq 3798
[TakeutiZaring] p. 18	Exercise 18	sspwb 4194
[TakeutiZaring] p. 18	Exercise 19	pweqb 4201
[TakeutiZaring] p. 20	Definition	df-rab 2453
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4109
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3118
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3411
[TakeutiZaring] p. 20	Proposition 5.15	difid 3477  difidALT 3478
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3421
[TakeutiZaring] p. 21	Theorem 5.22	setind 4516
[TakeutiZaring] p. 21	Definition 5.20	df-v 2728
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4114
[TakeutiZaring] p. 22	Exercise 1	0ss 3447
[TakeutiZaring] p. 22	Exercise 3	ssex 4119  ssexg 4121
[TakeutiZaring] p. 22	Exercise 4	inex1 4116
[TakeutiZaring] p. 22	Exercise 5	ruv 4527
[TakeutiZaring] p. 22	Exercise 6	elirr 4518
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3473
[TakeutiZaring] p. 22	Exercise 11	difdif 3247
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3383
[TakeutiZaring] p. 22	Exercise 14	difss 3248
[TakeutiZaring] p. 22	Exercise 15	sscon 3256
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2449
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2450
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4719  xpexg 4718  xpexgALT 6101
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4611
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5252
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5404  fun11 5255
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5199  svrelfun 5253
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4791
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4793
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4616
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4617
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4613
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5058  dfrel2 5054
[TakeutiZaring] p. 25	Exercise 3	xpss 4712
[TakeutiZaring] p. 25	Exercise 5	relun 4721
[TakeutiZaring] p. 25	Exercise 6	reluni 4727
[TakeutiZaring] p. 25	Exercise 9	inxp 4738
[TakeutiZaring] p. 25	Exercise 12	relres 4912
[TakeutiZaring] p. 25	Exercise 13	opelres 4889  opelresg 4891
[TakeutiZaring] p. 25	Exercise 14	dmres 4905
[TakeutiZaring] p. 25	Exercise 15	resss 4908
[TakeutiZaring] p. 25	Exercise 17	resabs1 4913
[TakeutiZaring] p. 25	Exercise 18	funres 5229
[TakeutiZaring] p. 25	Exercise 24	relco 5102
[TakeutiZaring] p. 25	Exercise 29	funco 5228
[TakeutiZaring] p. 25	Exercise 30	f1co 5405
[TakeutiZaring] p. 26	Definition 6.10	eu2 2058
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5196  fv3 5509
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5142  cnvexg 5141
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4870  dmexg 4868
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4871  rnexg 4869
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5503
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5513  tz6.12 5514  tz6.12c 5516
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5477
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5191
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5192
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5194  wfo 5186
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5193  wf1 5185
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5195  wf1o 5187
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5583  eqfnfv2 5584  eqfnfv2f 5587
[TakeutiZaring] p. 28	Exercise 5	fvco 5556
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5707  fnexALT 6079
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5706  resfunexgALT 6076
[TakeutiZaring] p. 29	Exercise 9	funimaex 5273  funimaexg 5272
[TakeutiZaring] p. 29	Definition 6.18	df-br 3983
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4974  iniseg 4976
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4267
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5197
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5778
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5779
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5784
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5786
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5794
[TakeutiZaring] p. 35	Notation	wtr 4080
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4332
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4084
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4553
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4359
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4363
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4469
[TakeutiZaring] p. 38	Definition 7.11	df-on 4346
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4463
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4529
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4559
[TakeutiZaring] p. 40	Exercise 7	dftr2 4082
[TakeutiZaring] p. 40	Exercise 11	unon 4488
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4464
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3817
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4349
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4393  sucidg 4394
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 4478
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4347
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4483  ordelsuc 4482
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4571
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4572
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4573
[TakeutiZaring] p. 43	Axiom 7	omex 4570
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4584
[TakeutiZaring] p. 43	Corollary 7.31	find 4576
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4574
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4575
[TakeutiZaring] p. 44	Exercise 2	int0 3838
[TakeutiZaring] p. 44	Exercise 3	trintssm 4096
[TakeutiZaring] p. 44	Exercise 4	intss1 3839
[TakeutiZaring] p. 44	Exercise 6	onintonm 4494
[TakeutiZaring] p. 44	Definition 7.35	df-int 3825
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6276
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6333  tfri1d 6303
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6334  tfri2d 6304
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6335
[TakeutiZaring] p. 50	Exercise 3	smoiso 6270
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6254
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6432
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6428
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6425
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6429
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6477  nnaordi 6476
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3911  uniss2 3820
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6438
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6448
[TakeutiZaring] p. 62	Exercise 5	oaword1 6439
[TakeutiZaring] p. 62	Definition 8.15	om0 6426  omsuc 6440
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6449
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6485  nnmordi 6484
[TakeutiZaring] p. 67	Definition 8.30	oei0 6427
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7143
[TakeutiZaring] p. 88	Exercise 1	en0 6761
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6823
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6824
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6709  isfi 6727
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6797
[TakeutiZaring] p. 95	Definition 10.42	df-map 6616
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6814
[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 2417
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2418
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2864
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3007
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5171
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5172
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2093  eupickbi 2096
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5196
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7146