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 7245  fidcenum 7086
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7086
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7245
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 12957
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7057
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 7043
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 12972
[AczelRathjen], p. 75	Corollary 8.1.20	unct 12974
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 12963  znnen 12930
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 12975
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 12976
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10960
[AczelRathjen], p. 183	Chapter 20	ax-setind 4604
[AhoHopUll] p. 318	Section 9.1	df-concat 11087  df-pfx 11166  df-substr 11139  df-word 11034  lencl 11037  wrd0 11058
[Apostol] p. 18	Theorem I.1	addcan 8289  addcan2d 8294  addcan2i 8292  addcand 8293  addcani 8291
[Apostol] p. 18	Theorem I.2	negeu 8300
[Apostol] p. 18	Theorem I.3	negsub 8357  negsubd 8426  negsubi 8387
[Apostol] p. 18	Theorem I.4	negneg 8359  negnegd 8411  negnegi 8379
[Apostol] p. 18	Theorem I.5	subdi 8494  subdid 8523  subdii 8516  subdir 8495  subdird 8524  subdiri 8517
[Apostol] p. 18	Theorem I.6	mul01 8498  mul01d 8502  mul01i 8500  mul02 8496  mul02d 8501  mul02i 8499
[Apostol] p. 18	Theorem I.9	divrecapd 8903
[Apostol] p. 18	Theorem I.10	recrecapi 8854
[Apostol] p. 18	Theorem I.12	mul2neg 8507  mul2negd 8522  mul2negi 8515  mulneg1 8504  mulneg1d 8520  mulneg1i 8513
[Apostol] p. 18	Theorem I.14	rdivmuldivd 14067
[Apostol] p. 18	Theorem I.15	divdivdivap 8823
[Apostol] p. 20	Axiom 7	rpaddcl 9836  rpaddcld 9871  rpmulcl 9837  rpmulcld 9872
[Apostol] p. 20	Axiom 9	0nrp 9848
[Apostol] p. 20	Theorem I.17	lttri 8214
[Apostol] p. 20	Theorem I.18	ltadd1d 8648  ltadd1dd 8666  ltadd1i 8612
[Apostol] p. 20	Theorem I.19	ltmul1 8702  ltmul1a 8701  ltmul1i 9030  ltmul1ii 9038  ltmul2 8966  ltmul2d 9898  ltmul2dd 9912  ltmul2i 9033
[Apostol] p. 20	Theorem I.21	0lt1 8236
[Apostol] p. 20	Theorem I.23	lt0neg1 8578  lt0neg1d 8625  ltneg 8572  ltnegd 8633  ltnegi 8603
[Apostol] p. 20	Theorem I.25	lt2add 8555  lt2addd 8677  lt2addi 8620
[Apostol] p. 20	Definition of positive numbers	df-rp 9813
[Apostol] p. 21	Exercise 4	recgt0 8960  recgt0d 9044  recgt0i 9016  recgt0ii 9017
[Apostol] p. 22	Definition of integers	df-z 9410
[Apostol] p. 22	Definition of rationals	df-q 9778
[Apostol] p. 24	Theorem I.26	supeuti 7124
[Apostol] p. 26	Theorem I.29	arch 9329
[Apostol] p. 28	Exercise 2	btwnz 9529
[Apostol] p. 28	Exercise 3	nnrecl 9330
[Apostol] p. 28	Exercise 6	qbtwnre 10438
[Apostol] p. 28	Exercise 10(a)	zeneo 12343  zneo 9511
[Apostol] p. 29	Theorem I.35	resqrtth 11503  sqrtthi 11591
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9076
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12518
[Apostol] p. 363	Remark	absgt0api 11618
[Apostol] p. 363	Example	abssubd 11665  abssubi 11622
[ApostolNT] p. 14	Definition	df-dvds 12260
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 12276
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12300
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12296
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12290
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12292
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 12277
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 12278
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 12283
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12317
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12319
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12321
[ApostolNT] p. 15	Definition	dfgcd2 12496
[ApostolNT] p. 16	Definition	isprm2 12600
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12575
[ApostolNT] p. 16	Theorem 1.7	prminf 12987
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12455
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12497
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12499
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12469
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12462
[ApostolNT] p. 17	Theorem 1.8	coprm 12627
[ApostolNT] p. 17	Theorem 1.9	euclemma 12629
[ApostolNT] p. 17	Theorem 1.10	1arith2 12852
[ApostolNT] p. 19	Theorem 1.14	divalg 12396
[ApostolNT] p. 20	Theorem 1.15	eucalg 12542
[ApostolNT] p. 25	Definition	df-phi 12694
[ApostolNT] p. 26	Theorem 2.2	phisum 12724
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12705
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12709
[ApostolNT] p. 38	Remark	df-sgm 15615
[ApostolNT] p. 38	Definition	df-sgm 15615
[ApostolNT] p. 104	Definition	congr 12583
[ApostolNT] p. 106	Remark	dvdsval3 12263
[ApostolNT] p. 106	Definition	moddvds 12271
[ApostolNT] p. 107	Example 2	mod2eq0even 12350
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12351
[ApostolNT] p. 107	Example 4	zmod1congr 10525
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10562
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 10850
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12295
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12586
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 12905
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12588
[ApostolNT] p. 113	Theorem 5.17	eulerth 12716
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12735
[ApostolNT] p. 114	Theorem 5.19	fermltl 12717
[ApostolNT] p. 179	Definition	df-lgs 15636  lgsprme0 15680
[ApostolNT] p. 180	Example 1	1lgs 15681
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 15657
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 15672
[ApostolNT] p. 181	Theorem 9.4	m1lgs 15723
[ApostolNT] p. 181	Theorem 9.5	2lgs 15742  2lgsoddprm 15751
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 15707
[ApostolNT] p. 185	Theorem 9.8	lgsquad 15718
[ApostolNT] p. 188	Definition	df-lgs 15636  lgs1 15682
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 15673
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 15675
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 15683
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 15684
[Bauer] p. 482	Section 1.2	pm2.01 617  pm2.65 661
[Bauer] p. 483	Theorem 1.3	acexmid 5968  onsucelsucexmidlem 4596
[Bauer], p. 481	Section 1.1	pwtrufal 16244
[Bauer], p. 483	Definition	n0rf 3482
[Bauer], p. 483	Theorem 1.2	2irrexpq 15609  2irrexpqap 15611
[Bauer], p. 485	Theorem 2.1	ssfiexmid 7001
[Bauer], p. 493	Section 5.1	ivthdich 15286
[Bauer], p. 494	Theorem 5.5	ivthinc 15276
[BauerHanson], p. 27	Proposition 5.2	cnstab 8755
[BauerSwan], p. 14	Remark	0ct 7237  ctm 7239
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 16247
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 7245
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7651
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7564
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7653
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7687  addlocpr 7686
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7713
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7716
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7721
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2058
[BellMachover] p. 460	Notation	df-mo 2059
[BellMachover] p. 460	Definition	mo3 2110  mo3h 2109
[BellMachover] p. 462	Theorem 1.1	bm1.1 2192
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4182
[BellMachover] p. 466	Axiom Pow	axpow3 4238
[BellMachover] p. 466	Axiom Union	axun2 4501
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4609
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4450
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4612
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4563
[BellMachover] p. 471	Definition of Lim	df-ilim 4435
[BellMachover] p. 472	Axiom Inf	zfinf2 4656
[BellMachover] p. 473	Theorem 2.8	limom 4681
[Bobzien] p. 116	Statement T3	stoic3 1451
[Bobzien] p. 117	Statement T2	stoic2a 1449
[Bobzien] p. 117	Statement T4	stoic4a 1452
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1447
[Bollobas] p. 1	Section I.1	df-edg 15816  isuhgropm 15838  isusgropen 15920  isuspgropen 15919
[Bollobas] p. 7	Section I.1	df-ushgrm 15827
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13349
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13395
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13410
[BourbakiAlg1] p. 92	Definition 1	df-ring 13921
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 13856
[BourbakiEns] p.	Proposition 8	fcof1 5877  fcofo 5878
[BourbakiTop1] p.	Remark	xnegmnf 9988  xnegpnf 9987
[BourbakiTop1] p.	Remark	rexneg 9989
[BourbakiTop1] p.	Proposition	ishmeo 14937
[BourbakiTop1] p.	Property V_i	ssnei2 14790
[BourbakiTop1] p.	Property V_ii	innei 14796
[BourbakiTop1] p.	Property V_iv	neissex 14798
[BourbakiTop1] p.	Proposition 1	neipsm 14787  neiss 14783
[BourbakiTop1] p.	Proposition 2	cnptopco 14855
[BourbakiTop1] p.	Proposition 4	imasnopn 14932
[BourbakiTop1] p.	Property V_iii	elnei 14785
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14631
[Bruck] p. 1	Section I.1	df-mgm 13349
[Bruck] p. 23	Section II.1	df-sgrp 13395
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13592
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4124
[Cohen] p. 301	Remark	relogoprlem 15501
[Cohen] p. 301	Property 2	relogmul 15502  relogmuld 15517
[Cohen] p. 301	Property 3	relogdiv 15503  relogdivd 15518
[Cohen] p. 301	Property 4	relogexp 15505
[Cohen] p. 301	Property 1a	log1 15499
[Cohen] p. 301	Property 1b	loge 15500
[Cohen4] p. 348	Observation	relogbcxpbap 15598
[Cohen4] p. 352	Definition	rpelogb 15582
[Cohen4] p. 361	Property 2	rprelogbmul 15588
[Cohen4] p. 361	Property 3	logbrec 15593  rprelogbdiv 15590
[Cohen4] p. 361	Property 4	rplogbreexp 15586
[Cohen4] p. 361	Property 6	relogbexpap 15591
[Cohen4] p. 361	Property 1(a)	rplogbid1 15580
[Cohen4] p. 361	Property 1(b)	rplogb1 15581
[Cohen4] p. 367	Property	rplogbchbase 15583
[Cohen4] p. 377	Property 2	logblt 15595
[Crosilla] p.	Axiom 1	ax-ext 2189
[Crosilla] p.	Axiom 2	ax-pr 4270
[Crosilla] p.	Axiom 3	ax-un 4499
[Crosilla] p.	Axiom 4	ax-nul 4187
[Crosilla] p.	Axiom 5	ax-iinf 4655
[Crosilla] p.	Axiom 6	ru 3005
[Crosilla] p.	Axiom 8	ax-pow 4235
[Crosilla] p.	Axiom 9	ax-setind 4604
[Crosilla], p.	Axiom 6	ax-sep 4179
[Crosilla], p.	Axiom 7	ax-coll 4176
[Crosilla], p.	Axiom 7'	repizf 4177
[Crosilla], p.	Theorem is stated	ordtriexmid 4588
[Crosilla], p.	Axiom of choice implies instances	acexmid 5968
[Crosilla], p.	Definition of ordinal	df-iord 4432
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4602
[Diestel] p. 27	Section 1.10	df-ushgrm 15827
[Eisenberg] p. 67	Definition 5.3	df-dif 3177
[Eisenberg] p. 82	Definition 6.3	df-iom 4658
[Eisenberg] p. 125	Definition 8.21	df-map 6762
[Enderton] p. 18	Axiom of Empty Set	axnul 4186
[Enderton] p. 19	Definition	df-tp 3652
[Enderton] p. 26	Exercise 5	unissb 3895
[Enderton] p. 26	Exercise 10	pwel 4281
[Enderton] p. 28	Exercise 7(b)	pwunim 4352
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 4012  iinin2m 4011  iunin1 4007  iunin2 4006
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 4010  iundif2ss 4008
[Enderton] p. 33	Exercise 23	iinuniss 4025
[Enderton] p. 33	Exercise 25	iununir 4026
[Enderton] p. 33	Exercise 24(a)	iinpw 4033
[Enderton] p. 33	Exercise 24(b)	iunpw 4546  iunpwss 4034
[Enderton] p. 38	Exercise 6(a)	unipw 4280
[Enderton] p. 38	Exercise 6(b)	pwuni 4253
[Enderton] p. 41	Lemma 3D	opeluu 4516  rnex 4966  rnexg 4963
[Enderton] p. 41	Exercise 8	dmuni 4908  rnuni 5114
[Enderton] p. 42	Definition of a function	dffun7 5318  dffun8 5319
[Enderton] p. 43	Definition of function value	funfvdm2 5668
[Enderton] p. 43	Definition of single-rooted	funcnv 5355
[Enderton] p. 44	Definition (d)	dfima2 5044  dfima3 5045
[Enderton] p. 47	Theorem 3H	fvco2 5673
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7351
[Enderton] p. 50	Theorem 3K(a)	imauni 5855
[Enderton] p. 52	Definition	df-map 6762
[Enderton] p. 53	Exercise 21	coass 5221
[Enderton] p. 53	Exercise 27	dmco 5211
[Enderton] p. 53	Exercise 14(a)	funin 5365
[Enderton] p. 53	Exercise 22(a)	imass2 5078
[Enderton] p. 54	Remark	ixpf 6832  ixpssmap 6844
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6811
[Enderton] p. 56	Theorem 3M	erref 6665
[Enderton] p. 57	Lemma 3N	erthi 6693
[Enderton] p. 57	Definition	df-ec 6647
[Enderton] p. 58	Definition	df-qs 6651
[Enderton] p. 60	Theorem 3Q	th3q 6752  th3qcor 6751  th3qlem1 6749  th3qlem2 6750
[Enderton] p. 61	Exercise 35	df-ec 6647
[Enderton] p. 65	Exercise 56(a)	dmun 4905
[Enderton] p. 68	Definition of successor	df-suc 4437
[Enderton] p. 71	Definition	df-tr 4160  dftr4 4164
[Enderton] p. 72	Theorem 4E	unisuc 4479  unisucg 4480
[Enderton] p. 73	Exercise 6	unisuc 4479  unisucg 4480
[Enderton] p. 73	Exercise 5(a)	truni 4173
[Enderton] p. 73	Exercise 5(b)	trint 4174
[Enderton] p. 79	Theorem 4I(A1)	nna0 6585
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6587  onasuc 6577
[Enderton] p. 79	Definition of operation value	df-ov 5972
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6586
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6588  onmsuc 6584
[Enderton] p. 81	Theorem 4K(1)	nnaass 6596
[Enderton] p. 81	Theorem 4K(2)	nna0r 6589  nnacom 6595
[Enderton] p. 81	Theorem 4K(3)	nndi 6597
[Enderton] p. 81	Theorem 4K(4)	nnmass 6598
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6600
[Enderton] p. 82	Exercise 16	nnm0r 6590  nnmsucr 6599
[Enderton] p. 88	Exercise 23	nnaordex 6639
[Enderton] p. 129	Definition	df-en 6853
[Enderton] p. 132	Theorem 6B(b)	canth 5922
[Enderton] p. 133	Exercise 1	xpomen 12927
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6990
[Enderton] p. 136	Corollary 6E	nneneq 6981
[Enderton] p. 139	Theorem 6H(c)	mapen 6970
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7363
[Enderton] p. 143	Theorem 6J	dju0en 7359  dju1en 7358
[Enderton] p. 144	Corollary 6K	undif2ss 3545
[Enderton] p. 145	Figure 38	ffoss 5577
[Enderton] p. 145	Definition	df-dom 6854
[Enderton] p. 146	Example 1	domen 6865  domeng 6866
[Enderton] p. 146	Example 3	nndomo 6988
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6957  xpdom1g 6955  xpdom2g 6954
[Enderton] p. 168	Definition	df-po 4362
[Enderton] p. 192	Theorem 7M(a)	oneli 4494
[Enderton] p. 192	Theorem 7M(b)	ontr1 4455
[Enderton] p. 192	Theorem 7M(c)	onirri 4610
[Enderton] p. 193	Corollary 7N(b)	0elon 4458
[Enderton] p. 193	Corollary 7N(c)	onsuci 4583
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4556
[Enderton] p. 194	Remark	onprc 4619
[Enderton] p. 194	Exercise 16	suc11 4625
[Enderton] p. 197	Definition	df-card 7314
[Enderton] p. 200	Exercise 25	tfis 4650
[Enderton] p. 206	Theorem 7X(b)	en2lp 4621
[Enderton] p. 207	Exercise 34	opthreg 4623
[Enderton] p. 208	Exercise 35	suc11g 4624
[Geuvers], p. 1	Remark	expap0 10753
[Geuvers], p. 6	Lemma 2.13	mulap0r 8725
[Geuvers], p. 6	Lemma 2.15	mulap0 8764
[Geuvers], p. 9	Lemma 2.35	msqge0 8726
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8081
[Geuvers], p. 10	Lemma 3.9	maxcom 11675
[Geuvers], p. 10	Lemma 3.10	maxle1 11683  maxle2 11684
[Geuvers], p. 10	Lemma 3.11	maxleast 11685
[Geuvers], p. 10	Lemma 3.12	maxleb 11688
[Geuvers], p. 11	Definition 3.13	dfabsmax 11689
[Geuvers], p. 17	Definition 6.1	df-ap 8692
[Gleason] p. 117	Proposition 9-2.1	df-enq 7497  enqer 7508
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7501  df-nqqs 7498
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7494  df-plqqs 7499
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7495  df-mqqs 7500
[Gleason] p. 119	Proposition 9-2.5	df-rq 7502
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7558
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7561  ltbtwnnq 7566  ltbtwnnqq 7565
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7550
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7551
[Gleason] p. 123	Proposition 9-3.5	addclpr 7687
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7729
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7728
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7747
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7763
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7769  ltaprlem 7768
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7766
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7722
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7742
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7731
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7730
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7738
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7788
[Gleason] p. 126	Proposition 9-4.1	df-enr 7876  enrer 7885
[Gleason] p. 126	Proposition 9-4.2	df-0r 7881  df-1r 7882  df-nr 7877
[Gleason] p. 126	Proposition 9-4.3	df-mr 7879  df-plr 7878  negexsr 7922  recexsrlem 7924
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7880
[Gleason] p. 130	Proposition 10-1.3	creui 9070  creur 9069  cru 8712
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8073  axcnre 8031
[Gleason] p. 132	Definition 10-3.1	crim 11330  crimd 11449  crimi 11409  crre 11329  crred 11448  crrei 11408
[Gleason] p. 132	Definition 10-3.2	remim 11332  remimd 11414
[Gleason] p. 133	Definition 10.36	absval2 11529  absval2d 11657  absval2i 11616
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11356  cjaddd 11437  cjaddi 11404
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11357  cjmuld 11438  cjmuli 11405
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11355  cjcjd 11415  cjcji 11387
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11354  cjreb 11338  cjrebd 11418  cjrebi 11390  cjred 11443  rere 11337  rereb 11335  rerebd 11417  rerebi 11389  rered 11441
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11363  addcjd 11429  addcji 11399
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11473
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11524  abscjd 11662  abscji 11620
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11536  abs00d 11658  abs00i 11617  absne0d 11659
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11568  releabsd 11663  releabsi 11621
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11541  absmuld 11666  absmuli 11623
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11527  sqabsaddi 11624
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11576  abstrid 11668  abstrii 11627
[Gleason] p. 134	Definition 10-4.1	df-exp 10723  exp0 10727  expp1 10730  expp1d 10858
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10765  expaddd 10859
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15545  cxpmuld 15570  expmul 10768  expmuld 10860
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10762  mulexpd 10872  rpmulcxp 15542
[Gleason] p. 141	Definition 11-2.1	fzval 10169
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11798
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11800
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11799
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11803
[Gleason] p. 172	Corollary 12-2.5	climrecl 11796
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11792  climcj 11793  climim 11795  climre 11794
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8149  df-xr 8148  ltxr 9934
[Gleason] p. 180	Theorem 12-5.3	climcau 11819
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10482
[Gleason] p. 223	Definition 14-1.1	df-met 14468
[Gleason] p. 223	Definition 14-1.1(a)	met0 14997  xmet0 14996
[Gleason] p. 223	Definition 14-1.1(c)	metsym 15004
[Gleason] p. 223	Definition 14-1.1(d)	mettri 15006  mstri 15106  xmettri 15005  xmstri 15105
[Gleason] p. 230	Proposition 14-2.6	txlm 14912
[Gleason] p. 240	Proposition 14-4.2	metcnp3 15144
[Gleason] p. 243	Proposition 14-4.16	addcn2 11782  addcncntop 15195  mulcn2 11784  mulcncntop 15197  subcn2 11783  subcncntop 15196
[Gleason] p. 295	Remark	bcval3 10935  bcval4 10936
[Gleason] p. 295	Equation 2	bcpasc 10950
[Gleason] p. 295	Definition of binomial coefficient	bcval 10933  df-bc 10932
[Gleason] p. 296	Remark	bcn0 10939  bcnn 10941
[Gleason] p. 296	Theorem 15-2.8	binom 11956
[Gleason] p. 308	Equation 2	ef0 12144
[Gleason] p. 308	Equation 3	efcj 12145
[Gleason] p. 309	Corollary 15-4.3	efne0 12150
[Gleason] p. 309	Corollary 15-4.4	efexp 12154
[Gleason] p. 310	Equation 14	sinadd 12208
[Gleason] p. 310	Equation 15	cosadd 12209
[Gleason] p. 311	Equation 17	sincossq 12220
[Gleason] p. 311	Equation 18	cosbnd 12225  sinbnd 12224
[Gleason] p. 311	Definition of ` `	df-pi 12125
[Golan] p. 1	Remark	srgisid 13909
[Golan] p. 1	Definition	df-srg 13887
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1473
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13504  mndideu 13419
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13531
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13560
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13571
[Herstein] p. 57	Exercise 1	dfgrp3me 13593
[Heyting] p. 127	Axiom #1	ax1hfs 16323
[Hitchcock] p. 5	Rule A3	mptnan 1443
[Hitchcock] p. 5	Rule A4	mptxor 1444
[Hitchcock] p. 5	Rule A5	mtpxor 1446
[HoTT], p.	Lemma 10.4.1	exmidontriim 7370
[HoTT], p.	Theorem 7.2.6	nndceq 6610
[HoTT], p.	Exercise 11.10	neapmkv 16317
[HoTT], p.	Exercise 11.11	mulap0bd 8767
[HoTT], p.	Section 11.2.1	df-iltp 7620  df-imp 7619  df-iplp 7618  df-reap 8685
[HoTT], p.	Theorem 11.2.4	recapb 8781  rerecapb 8953
[HoTT], p.	Corollary 3.9.2	uchoice 6248
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7812
[HoTT], p.	Corollary 11.4.3	conventions 15965
[HoTT], p.	Exercise 11.6(i)	dcapnconst 16310  dceqnconst 16309
[HoTT], p.	Corollary 11.2.13	axcaucvg 8050  caucvgpr 7832  caucvgprpr 7862  caucvgsr 7952
[HoTT], p.	Definition 11.2.1	df-inp 7616
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 16315
[HoTT], p.	Proposition 11.2.3	df-iso 4363  ltpopr 7745  ltsopr 7746
[HoTT], p.	Definition 11.2.7(v)	apsym 8716  reapcotr 8708  reapirr 8687
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8236  gt0add 8683  leadd1 8540  lelttr 8198  lemul1a 8968  lenlt 8185  ltadd1 8539  ltletr 8199  ltmul1 8702  reaplt 8698
[Jech] p. 4	Definition of class	cv 1372  cvjust 2202
[Jech] p. 78	Note	opthprc 4745
[KalishMontague] p. 81	Note 1	ax-i9 1554
[Kreyszig] p. 3	Property M1	metcl 14986  xmetcl 14985
[Kreyszig] p. 4	Property M2	meteq0 14993
[Kreyszig] p. 12	Equation 5	muleqadd 8778
[Kreyszig] p. 18	Definition 1.3-2	mopnval 15075
[Kreyszig] p. 19	Remark	mopntopon 15076
[Kreyszig] p. 19	Theorem T1	mopn0 15121  mopnm 15081
[Kreyszig] p. 19	Theorem T2	unimopn 15119
[Kreyszig] p. 19	Definition of neighborhood	neibl 15124
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 15146
[Kreyszig] p. 25	Definition 1.4-1	lmbr 14846
[Kreyszig] p. 51	Equation 2	lmodvneg1 14253
[Kreyszig] p. 51	Equation 1a	lmod0vs 14244
[Kreyszig] p. 51	Equation 1b	lmodvs0 14245
[Kunen] p. 10	Axiom 0	a9e 1720
[Kunen] p. 12	Axiom 6	zfrep6 4178
[Kunen] p. 24	Definition 10.24	mapval 6772  mapvalg 6770
[Kunen] p. 31	Definition 10.24	mapex 6766
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3952
[Lang] p. 3	Statement	lidrideqd 13374  mndbn0 13424
[Lang] p. 3	Definition	df-mnd 13410
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 13391
[Lang] p. 5	Equation	gsumfzreidx 13834
[Lang] p. 6	Definition	mulgnn0gsum 13625
[Lang] p. 7	Definition	dfgrp2e 13521
[Levy] p. 338	Axiom	df-clab 2194  df-clel 2203  df-cleq 2200
[Lopez-Astorga] p. 12	Rule 1	mptnan 1443
[Lopez-Astorga] p. 12	Rule 2	mptxor 1444
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1446
[Margaris] p. 40	Rule C	exlimiv 1622
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 855
[Margaris] p. 49	Definition	dfbi2 388  dfordc 894  exalim 1526
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 653
[Margaris] p. 89	Theorem 19.2	19.2 1662  r19.2m 3556
[Margaris] p. 89	Theorem 19.3	19.3 1578  19.3h 1577  rr19.3v 2920
[Margaris] p. 89	Theorem 19.5	alcom 1502
[Margaris] p. 89	Theorem 19.6	alexdc 1643  alexim 1669
[Margaris] p. 89	Theorem 19.7	alnex 1523
[Margaris] p. 89	Theorem 19.8	19.8a 1614  spsbe 1866
[Margaris] p. 89	Theorem 19.9	19.9 1668  19.9h 1667  19.9v 1895  exlimd 1621
[Margaris] p. 89	Theorem 19.11	excom 1688  excomim 1687
[Margaris] p. 89	Theorem 19.12	19.12 1689  r19.12 2615
[Margaris] p. 90	Theorem 19.14	exnalim 1670
[Margaris] p. 90	Theorem 19.15	albi 1492  ralbi 2641
[Margaris] p. 90	Theorem 19.16	19.16 1579
[Margaris] p. 90	Theorem 19.17	19.17 1580
[Margaris] p. 90	Theorem 19.18	exbi 1628  rexbi 2642
[Margaris] p. 90	Theorem 19.19	19.19 1690
[Margaris] p. 90	Theorem 19.20	alim 1481  alimd 1545  alimdh 1491  alimdv 1903  ralimdaa 2574  ralimdv 2576  ralimdva 2575  ralimdvva 2577  sbcimdv 3072
[Margaris] p. 90	Theorem 19.21	19.21-2 1691  19.21 1607  19.21bi 1582  19.21h 1581  19.21ht 1605  19.21t 1606  19.21v 1897  alrimd 1634  alrimdd 1633  alrimdh 1503  alrimdv 1900  alrimi 1546  alrimih 1493  alrimiv 1898  alrimivv 1899  r19.21 2584  r19.21be 2599  r19.21bi 2596  r19.21t 2583  r19.21v 2585  ralrimd 2586  ralrimdv 2587  ralrimdva 2588  ralrimdvv 2592  ralrimdvva 2593  ralrimi 2579  ralrimiv 2580  ralrimiva 2581  ralrimivv 2589  ralrimivva 2590  ralrimivvva 2591  ralrimivw 2582  rexlimi 2619
[Margaris] p. 90	Theorem 19.22	2alimdv 1905  2eximdv 1906  exim 1623  eximd 1636  eximdh 1635  eximdv 1904  rexim 2602  reximdai 2606  reximddv 2611  reximddv2 2613  reximdv 2609  reximdv2 2607  reximdva 2610  reximdvai 2608  reximi2 2604
[Margaris] p. 90	Theorem 19.23	19.23 1702  19.23bi 1616  19.23h 1522  19.23ht 1521  19.23t 1701  19.23v 1907  19.23vv 1908  exlimd2 1619  exlimdh 1620  exlimdv 1843  exlimdvv 1922  exlimi 1618  exlimih 1617  exlimiv 1622  exlimivv 1921  r19.23 2617  r19.23v 2618  rexlimd 2623  rexlimdv 2625  rexlimdv3a 2628  rexlimdva 2626  rexlimdva2 2629  rexlimdvaa 2627  rexlimdvv 2633  rexlimdvva 2634  rexlimdvw 2630  rexlimiv 2620  rexlimiva 2621  rexlimivv 2632
[Margaris] p. 90	Theorem 19.24	i19.24 1663
[Margaris] p. 90	Theorem 19.25	19.25 1650
[Margaris] p. 90	Theorem 19.26	19.26-2 1506  19.26-3an 1507  19.26 1505  r19.26-2 2638  r19.26-3 2639  r19.26 2635  r19.26m 2640
[Margaris] p. 90	Theorem 19.27	19.27 1585  19.27h 1584  19.27v 1924  r19.27av 2644  r19.27m 3565  r19.27mv 3566
[Margaris] p. 90	Theorem 19.28	19.28 1587  19.28h 1586  19.28v 1925  r19.28av 2645  r19.28m 3559  r19.28mv 3562  rr19.28v 2921
[Margaris] p. 90	Theorem 19.29	19.29 1644  19.29r 1645  19.29r2 1646  19.29x 1647  r19.29 2646  r19.29d2r 2653  r19.29r 2647
[Margaris] p. 90	Theorem 19.30	19.30dc 1651
[Margaris] p. 90	Theorem 19.31	19.31r 1705
[Margaris] p. 90	Theorem 19.32	19.32dc 1703  19.32r 1704  r19.32r 2655  r19.32vdc 2658  r19.32vr 2657
[Margaris] p. 90	Theorem 19.33	19.33 1508  19.33b2 1653  19.33bdc 1654
[Margaris] p. 90	Theorem 19.34	19.34 1708
[Margaris] p. 90	Theorem 19.35	19.35-1 1648  19.35i 1649
[Margaris] p. 90	Theorem 19.36	19.36-1 1697  19.36aiv 1926  19.36i 1696  r19.36av 2660
[Margaris] p. 90	Theorem 19.37	19.37-1 1698  19.37aiv 1699  r19.37 2661  r19.37av 2662
[Margaris] p. 90	Theorem 19.38	19.38 1700
[Margaris] p. 90	Theorem 19.39	i19.39 1664
[Margaris] p. 90	Theorem 19.40	19.40-2 1656  19.40 1655  r19.40 2663
[Margaris] p. 90	Theorem 19.41	19.41 1710  19.41h 1709  19.41v 1927  19.41vv 1928  19.41vvv 1929  19.41vvvv 1930  r19.41 2664  r19.41v 2665
[Margaris] p. 90	Theorem 19.42	19.42 1712  19.42h 1711  19.42v 1931  19.42vv 1936  19.42vvv 1937  19.42vvvv 1938  r19.42v 2666
[Margaris] p. 90	Theorem 19.43	19.43 1652  r19.43 2667
[Margaris] p. 90	Theorem 19.44	19.44 1706  r19.44av 2668  r19.44mv 3564
[Margaris] p. 90	Theorem 19.45	19.45 1707  r19.45av 2669  r19.45mv 3563
[Margaris] p. 110	Exercise 2(b)	eu1 2080
[Megill] p. 444	Axiom C5	ax-17 1550
[Megill] p. 445	Lemma L12	alequcom 1539  ax-10 1529
[Megill] p. 446	Lemma L17	equtrr 1734
[Megill] p. 446	Lemma L19	hbnae 1745
[Megill] p. 447	Remark 9.1	df-sb 1787  sbid 1798
[Megill] p. 448	Scheme C5'	ax-4 1534
[Megill] p. 448	Scheme C6'	ax-7 1472
[Megill] p. 448	Scheme C8'	ax-8 1528
[Megill] p. 448	Scheme C9'	ax-i12 1531
[Megill] p. 448	Scheme C11'	ax-10o 1740
[Megill] p. 448	Scheme C12'	ax-13 2180
[Megill] p. 448	Scheme C13'	ax-14 2181
[Megill] p. 448	Scheme C15'	ax-11o 1847
[Megill] p. 448	Scheme C16'	ax-16 1838
[Megill] p. 448	Theorem 9.4	dral1 1754  dral2 1755  drex1 1822  drex2 1756  drsb1 1823  drsb2 1865
[Megill] p. 449	Theorem 9.7	sbcom2 2016  sbequ 1864  sbid2v 2025
[Megill] p. 450	Example in Appendix	hba1 1564
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3090  rspsbca 3091  stdpc4 1799
[Mendelson] p. 69	Axiom 5	ra5 3096  stdpc5 1608
[Mendelson] p. 81	Rule C	exlimiv 1622
[Mendelson] p. 95	Axiom 6	stdpc6 1727
[Mendelson] p. 95	Axiom 7	stdpc7 1794
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3506
[Mendelson] p. 231	Exercise 4.10(l)	unv 3507
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3422
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3470
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3423
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3313
[Mendelson] p. 231	Definition of union	unssin 3421
[Mendelson] p. 235	Exercise 4.12(c)	univ 4542
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3864
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4348
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4349
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4350
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3885
[Mendelson] p. 235	Exercise 4.12(p)	reli 4826
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5223
[Mendelson] p. 246	Definition of successor	df-suc 4437
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6969
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6943  xpsneng 6944
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6949  xpcomeng 6950
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6952
[Mendelson] p. 255	Exercise 4.39	endisj 6946
[Mendelson] p. 255	Exercise 4.41	mapprc 6764
[Mendelson] p. 255	Exercise 4.43	mapsnen 6929
[Mendelson] p. 255	Exercise 4.47	xpmapen 6974
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6798
[Mendelson] p. 255	Exercise 4.42(b)	map1 6930
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7362  djucomen 7361
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7360
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6578
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3404
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4782
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4783
[Monk1] p. 34	Definition 3.3	df-opab 4123
[Monk1] p. 36	Theorem 3.7(i)	coi1 5218  coi2 5219
[Monk1] p. 36	Theorem 3.8(v)	dm0 4912  rn0 4954
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5107
[Monk1] p. 37	Theorem 3.13(i)	relxp 4803
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4918  rnxpm 5132
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4774  xp0 5122
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5061
[Monk1] p. 38	Theorem 3.16(viii)	imai 5058
[Monk1] p. 39	Theorem 3.17	imaex 5057  imaexg 5056
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5053
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5735  funfvop 5717
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5646
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5655
[Monk1] p. 43	Theorem 4.6	funun 5335
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5862  dff13f 5864
[Monk1] p. 46	Theorem 4.15(v)	funex 5832  funrnex 6224
[Monk1] p. 50	Definition 5.4	fniunfv 5856
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5186
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3916
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6266  df-1st 6251
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6267  df-2nd 6252
[Monk2] p. 105	Axiom C4	ax-5 1471
[Monk2] p. 105	Axiom C7	ax-8 1528
[Monk2] p. 105	Axiom C8	ax-11 1530  ax-11o 1847
[Monk2] p. 105	Axiom (C8)	ax11v 1851
[Monk2] p. 109	Lemma 12	ax-7 1472
[Monk2] p. 109	Lemma 15	equvin 1887  equvini 1782  eqvinop 4306
[Monk2] p. 113	Axiom C5-1	ax-17 1550
[Monk2] p. 113	Axiom C5-2	ax6b 1675
[Monk2] p. 113	Axiom C5-3	ax-7 1472
[Monk2] p. 114	Lemma 22	hba1 1564
[Monk2] p. 114	Lemma 23	hbia1 1576  nfia1 1604
[Monk2] p. 114	Lemma 24	hba2 1575  nfa2 1603
[Moschovakis] p. 2	Chapter 2	df-stab 833  dftest 16324
[Munkres] p. 77	Example 2	distop 14718
[Munkres] p. 78	Definition of basis	df-bases 14676  isbasis3g 14679
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 13253  tgval2 14684
[Munkres] p. 79	Remark	tgcl 14697
[Munkres] p. 80	Lemma 2.1	tgval3 14691
[Munkres] p. 80	Lemma 2.2	tgss2 14712  tgss3 14711
[Munkres] p. 81	Lemma 2.3	basgen 14713  basgen2 14714
[Munkres] p. 89	Definition of subspace topology	resttop 14803
[Munkres] p. 93	Theorem 6.1(1)	0cld 14745  topcld 14742
[Munkres] p. 93	Theorem 6.1(3)	uncld 14746
[Munkres] p. 94	Definition of closure	clsval 14744
[Munkres] p. 94	Definition of interior	ntrval 14743
[Munkres] p. 102	Definition of continuous function	df-cn 14821  iscn 14830  iscn2 14833
[Munkres] p. 107	Theorem 7.2(g)	cncnp 14863  cncnp2m 14864  cncnpi 14861  df-cnp 14822  iscnp 14832
[Munkres] p. 127	Theorem 10.1	metcn 15147
[Pierik], p. 8	Section 2.2.1	dfrex2fin 7028
[Pierik], p. 9	Definition 2.4	df-womni 7294
[Pierik], p. 9	Definition 2.5	df-markov 7282  omniwomnimkv 7297
[Pierik], p. 10	Section 2.3	dfdif3 3292
[Pierik], p. 14	Definition 3.1	df-omni 7265  exmidomniim 7271  finomni 7270
[Pierik], p. 15	Section 3.1	df-nninf 7250
[Pradic2025], p. 2	Section 1.1	nnnninfen 16268
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 16272
[PradicBrown2022], p. 2	Remark	exmidpw 7033
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7342
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7343  exmidfodomrlemrALT 7344
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7279
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 16254  peano4nninf 16253
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 16256
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 16264
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 16266
[PradicBrown2022], p. 5	Definition 3.3	nnsf 16252
[Quine] p. 16	Definition 2.1	df-clab 2194  rabid 2685
[Quine] p. 17	Definition 2.1''	dfsb7 2020
[Quine] p. 18	Definition 2.7	df-cleq 2200
[Quine] p. 19	Definition 2.9	df-v 2779
[Quine] p. 34	Theorem 5.1	abeq2 2316
[Quine] p. 35	Theorem 5.2	abid2 2328  abid2f 2376
[Quine] p. 40	Theorem 6.1	sb5 1912
[Quine] p. 40	Theorem 6.2	sb56 1910  sb6 1911
[Quine] p. 41	Theorem 6.3	df-clel 2203
[Quine] p. 41	Theorem 6.4	eqid 2207
[Quine] p. 41	Theorem 6.5	eqcom 2209
[Quine] p. 42	Theorem 6.6	df-sbc 3007
[Quine] p. 42	Theorem 6.7	dfsbcq 3008  dfsbcq2 3009
[Quine] p. 43	Theorem 6.8	vex 2780
[Quine] p. 43	Theorem 6.9	isset 2784
[Quine] p. 44	Theorem 7.3	spcgf 2863  spcgv 2868  spcimgf 2861
[Quine] p. 44	Theorem 6.11	spsbc 3018  spsbcd 3019
[Quine] p. 44	Theorem 6.12	elex 2789
[Quine] p. 44	Theorem 6.13	elab 2925  elabg 2927  elabgf 2923
[Quine] p. 44	Theorem 6.14	noel 3473
[Quine] p. 48	Theorem 7.2	snprc 3709
[Quine] p. 48	Definition 7.1	df-pr 3651  df-sn 3650
[Quine] p. 49	Theorem 7.4	snss 3780  snssg 3779
[Quine] p. 49	Theorem 7.5	prss 3801  prssg 3802
[Quine] p. 49	Theorem 7.6	prid1 3750  prid1g 3748  prid2 3751  prid2g 3749  snid 3675  snidg 3673
[Quine] p. 51	Theorem 7.12	snexg 4245  snexprc 4247
[Quine] p. 51	Theorem 7.13	prexg 4272
[Quine] p. 53	Theorem 8.2	unisn 3881  unisng 3882
[Quine] p. 53	Theorem 8.3	uniun 3884
[Quine] p. 54	Theorem 8.6	elssuni 3893
[Quine] p. 54	Theorem 8.7	uni0 3892
[Quine] p. 56	Theorem 8.17	uniabio 5262
[Quine] p. 56	Definition 8.18	dfiota2 5253
[Quine] p. 57	Theorem 8.19	iotaval 5263
[Quine] p. 57	Theorem 8.22	iotanul 5267
[Quine] p. 58	Theorem 8.23	euiotaex 5268
[Quine] p. 58	Definition 9.1	df-op 3653
[Quine] p. 61	Theorem 9.5	opabid 4321  opabidw 4322  opelopab 4337  opelopaba 4331  opelopabaf 4339  opelopabf 4340  opelopabg 4333  opelopabga 4328  opelopabgf 4335  oprabid 6001
[Quine] p. 64	Definition 9.11	df-xp 4700
[Quine] p. 64	Definition 9.12	df-cnv 4702
[Quine] p. 64	Definition 9.15	df-id 4359
[Quine] p. 65	Theorem 10.3	fun0 5352
[Quine] p. 65	Theorem 10.4	funi 5323
[Quine] p. 65	Theorem 10.5	funsn 5342  funsng 5340
[Quine] p. 65	Definition 10.1	df-fun 5293
[Quine] p. 65	Definition 10.2	args 5071  dffv4g 5597
[Quine] p. 68	Definition 10.11	df-fv 5299  fv2 5595
[Quine] p. 124	Theorem 17.3	nn0opth2 10908  nn0opth2d 10907  nn0opthd 10906
[Quine] p. 284	Axiom 39(vi)	funimaex 5379  funimaexg 5378
[Roman] p. 18	Part Preliminaries	df-rng 13856
[Roman] p. 19	Part Preliminaries	df-ring 13921
[Rudin] p. 164	Equation 27	efcan 12148
[Rudin] p. 164	Equation 30	efzval 12155
[Rudin] p. 167	Equation 48	absefi 12241
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1446
[Sanford] p. 39	Rule 4	mptxor 1444
[Sanford] p. 40	Rule 1	mptnan 1443
[Schechter] p. 51	Definition of antisymmetry	intasym 5087
[Schechter] p. 51	Definition of irreflexivity	intirr 5089
[Schechter] p. 51	Definition of symmetry	cnvsym 5086
[Schechter] p. 51	Definition of transitivity	cotr 5084
[Schechter] p. 187	Definition of "ring with unit"	isring 13923
[Schechter] p. 428	Definition 15.35	bastop1 14716
[Stoll] p. 13	Definition of symmetric difference	symdif1 3447
[Stoll] p. 16	Exercise 4.4	0dif 3541  dif0 3540
[Stoll] p. 16	Exercise 4.8	difdifdirss 3554
[Stoll] p. 19	Theorem 5.2(13)	undm 3440
[Stoll] p. 19	Theorem 5.2(13')	indmss 3441
[Stoll] p. 20	Remark	invdif 3424
[Stoll] p. 25	Definition of ordered triple	df-ot 3654
[Stoll] p. 43	Definition	uniiun 3996
[Stoll] p. 44	Definition	intiin 3997
[Stoll] p. 45	Definition	df-iin 3945
[Stoll] p. 45	Definition indexed union	df-iun 3944
[Stoll] p. 176	Theorem 3.4(27)	imandc 891  imanst 890
[Stoll] p. 262	Example 4.1	symdif1 3447
[Suppes] p. 22	Theorem 2	eq0 3488
[Suppes] p. 22	Theorem 4	eqss 3217  eqssd 3219  eqssi 3218
[Suppes] p. 23	Theorem 5	ss0 3510  ss0b 3509
[Suppes] p. 23	Theorem 6	sstr 3210
[Suppes] p. 25	Theorem 12	elin 3365  elun 3323
[Suppes] p. 26	Theorem 15	inidm 3391
[Suppes] p. 26	Theorem 16	in0 3504
[Suppes] p. 27	Theorem 23	unidm 3325
[Suppes] p. 27	Theorem 24	un0 3503
[Suppes] p. 27	Theorem 25	ssun1 3345
[Suppes] p. 27	Theorem 26	ssequn1 3352
[Suppes] p. 27	Theorem 27	unss 3356
[Suppes] p. 27	Theorem 28	indir 3431
[Suppes] p. 27	Theorem 29	undir 3432
[Suppes] p. 28	Theorem 32	difid 3538  difidALT 3539
[Suppes] p. 29	Theorem 33	difin 3419
[Suppes] p. 29	Theorem 34	indif 3425
[Suppes] p. 29	Theorem 35	undif1ss 3544
[Suppes] p. 29	Theorem 36	difun2 3549
[Suppes] p. 29	Theorem 37	difin0 3543
[Suppes] p. 29	Theorem 38	disjdif 3542
[Suppes] p. 29	Theorem 39	difundi 3434
[Suppes] p. 29	Theorem 40	difindiss 3436
[Suppes] p. 30	Theorem 41	nalset 4191
[Suppes] p. 39	Theorem 61	uniss 3886
[Suppes] p. 39	Theorem 65	uniop 4319
[Suppes] p. 41	Theorem 70	intsn 3935
[Suppes] p. 42	Theorem 71	intpr 3932  intprg 3933
[Suppes] p. 42	Theorem 73	op1stb 4544  op1stbg 4545
[Suppes] p. 42	Theorem 78	intun 3931
[Suppes] p. 44	Definition 15(a)	dfiun2 3976  dfiun2g 3974
[Suppes] p. 44	Definition 15(b)	dfiin2 3977
[Suppes] p. 47	Theorem 86	elpw 3633  elpw2 4218  elpw2g 4217  elpwg 3635
[Suppes] p. 47	Theorem 87	pwid 3642
[Suppes] p. 47	Theorem 89	pw0 3792
[Suppes] p. 48	Theorem 90	pwpw0ss 3860
[Suppes] p. 52	Theorem 101	xpss12 4801
[Suppes] p. 52	Theorem 102	xpindi 4832  xpindir 4833
[Suppes] p. 52	Theorem 103	xpundi 4750  xpundir 4751
[Suppes] p. 54	Theorem 105	elirrv 4615
[Suppes] p. 58	Theorem 2	relss 4781
[Suppes] p. 59	Theorem 4	eldm 4895  eldm2 4896  eldm2g 4894  eldmg 4893
[Suppes] p. 59	Definition 3	df-dm 4704
[Suppes] p. 60	Theorem 6	dmin 4906
[Suppes] p. 60	Theorem 8	rnun 5111
[Suppes] p. 60	Theorem 9	rnin 5112
[Suppes] p. 60	Definition 4	dfrn2 4885
[Suppes] p. 61	Theorem 11	brcnv 4880  brcnvg 4878
[Suppes] p. 62	Equation 5	elcnv 4874  elcnv2 4875
[Suppes] p. 62	Theorem 12	relcnv 5080
[Suppes] p. 62	Theorem 15	cnvin 5110
[Suppes] p. 62	Theorem 16	cnvun 5108
[Suppes] p. 63	Theorem 20	co02 5216
[Suppes] p. 63	Theorem 21	dmcoss 4968
[Suppes] p. 63	Definition 7	df-co 4703
[Suppes] p. 64	Theorem 26	cnvco 4882
[Suppes] p. 64	Theorem 27	coass 5221
[Suppes] p. 65	Theorem 31	resundi 4992
[Suppes] p. 65	Theorem 34	elima 5047  elima2 5048  elima3 5049  elimag 5046
[Suppes] p. 65	Theorem 35	imaundi 5115
[Suppes] p. 66	Theorem 40	dminss 5117
[Suppes] p. 66	Theorem 41	imainss 5118
[Suppes] p. 67	Exercise 11	cnvxp 5121
[Suppes] p. 81	Definition 34	dfec2 6648
[Suppes] p. 82	Theorem 72	elec 6686  elecg 6685
[Suppes] p. 82	Theorem 73	erth 6691  erth2 6692
[Suppes] p. 89	Theorem 96	map0b 6799
[Suppes] p. 89	Theorem 97	map0 6801  map0g 6800
[Suppes] p. 89	Theorem 98	mapsn 6802
[Suppes] p. 89	Theorem 99	mapss 6803
[Suppes] p. 92	Theorem 1	enref 6881  enrefg 6880
[Suppes] p. 92	Theorem 2	ensym 6898  ensymb 6897  ensymi 6899
[Suppes] p. 92	Theorem 3	entr 6901
[Suppes] p. 92	Theorem 4	unen 6934
[Suppes] p. 94	Theorem 15	endom 6879
[Suppes] p. 94	Theorem 16	ssdomg 6895
[Suppes] p. 94	Theorem 17	domtr 6902
[Suppes] p. 95	Theorem 18	isbth 7097
[Suppes] p. 98	Exercise 4	fundmen 6924  fundmeng 6925
[Suppes] p. 98	Exercise 6	xpdom3m 6956
[Suppes] p. 130	Definition 3	df-tr 4160
[Suppes] p. 132	Theorem 9	ssonuni 4555
[Suppes] p. 134	Definition 6	df-suc 4437
[Suppes] p. 136	Theorem Schema 22	findes 4670  finds 4667  finds1 4669  finds2 4668
[Suppes] p. 162	Definition 5	df-ltnqqs 7503  df-ltpq 7496
[Suppes] p. 228	Theorem Schema 61	onintss 4456
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2189
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2200
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2203
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2202
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2225
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5973
[TakeutiZaring] p. 14	Proposition 4.14	ru 3005
[TakeutiZaring] p. 15	Exercise 1	elpr 3665  elpr2 3666  elprg 3664
[TakeutiZaring] p. 15	Exercise 2	elsn 3660  elsn2 3678  elsn2g 3677  elsng 3659  velsn 3661
[TakeutiZaring] p. 15	Exercise 3	elop 4294
[TakeutiZaring] p. 15	Exercise 4	sneq 3655  sneqr 3815
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3663  dfsn2 3658
[TakeutiZaring] p. 16	Axiom 3	uniex 4503
[TakeutiZaring] p. 16	Exercise 6	opth 4300
[TakeutiZaring] p. 16	Exercise 8	rext 4278
[TakeutiZaring] p. 16	Corollary 5.8	unex 4507  unexg 4509
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3693
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3866
[TakeutiZaring] p. 16	Definition 5.6	df-in 3181  df-un 3179
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3879  uniprg 3880
[TakeutiZaring] p. 17	Axiom 4	vpwex 4240
[TakeutiZaring] p. 17	Exercise 1	eltp 3692
[TakeutiZaring] p. 17	Exercise 5	elsuc 4472  elsucg 4470  sstr2 3209
[TakeutiZaring] p. 17	Exercise 6	uncom 3326
[TakeutiZaring] p. 17	Exercise 7	incom 3374
[TakeutiZaring] p. 17	Exercise 8	unass 3339
[TakeutiZaring] p. 17	Exercise 9	inass 3392
[TakeutiZaring] p. 17	Exercise 10	indi 3429
[TakeutiZaring] p. 17	Exercise 11	undi 3430
[TakeutiZaring] p. 17	Definition 5.9	ssalel 3190
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3629
[TakeutiZaring] p. 18	Exercise 7	unss2 3353
[TakeutiZaring] p. 18	Exercise 9	df-ss 3188  dfss2 3192  sseqin2 3401
[TakeutiZaring] p. 18	Exercise 10	ssid 3222
[TakeutiZaring] p. 18	Exercise 12	inss1 3402  inss2 3403
[TakeutiZaring] p. 18	Exercise 13	nssr 3262
[TakeutiZaring] p. 18	Exercise 15	unieq 3874
[TakeutiZaring] p. 18	Exercise 18	sspwb 4279
[TakeutiZaring] p. 18	Exercise 19	pweqb 4286
[TakeutiZaring] p. 20	Definition	df-rab 2495
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4188
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3177
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3471
[TakeutiZaring] p. 20	Proposition 5.15	difid 3538  difidALT 3539
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3482
[TakeutiZaring] p. 21	Theorem 5.22	setind 4606
[TakeutiZaring] p. 21	Definition 5.20	df-v 2779
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4193
[TakeutiZaring] p. 22	Exercise 1	0ss 3508
[TakeutiZaring] p. 22	Exercise 3	ssex 4198  ssexg 4200
[TakeutiZaring] p. 22	Exercise 4	inex1 4195
[TakeutiZaring] p. 22	Exercise 5	ruv 4617
[TakeutiZaring] p. 22	Exercise 6	elirr 4608
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3534
[TakeutiZaring] p. 22	Exercise 11	difdif 3307
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3443
[TakeutiZaring] p. 22	Exercise 14	difss 3308
[TakeutiZaring] p. 22	Exercise 15	sscon 3316
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2491
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2492
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4809  xpexg 4808  xpexgALT 6243
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4701
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5358
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5515  fun11 5361
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5302  svrelfun 5359
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4884
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4886
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4706
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4707
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4703
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5157  dfrel2 5153
[TakeutiZaring] p. 25	Exercise 3	xpss 4802
[TakeutiZaring] p. 25	Exercise 5	relun 4811
[TakeutiZaring] p. 25	Exercise 6	reluni 4817
[TakeutiZaring] p. 25	Exercise 9	inxp 4831
[TakeutiZaring] p. 25	Exercise 12	relres 5007
[TakeutiZaring] p. 25	Exercise 13	opelres 4984  opelresg 4986
[TakeutiZaring] p. 25	Exercise 14	dmres 5000
[TakeutiZaring] p. 25	Exercise 15	resss 5003
[TakeutiZaring] p. 25	Exercise 17	resabs1 5008
[TakeutiZaring] p. 25	Exercise 18	funres 5332
[TakeutiZaring] p. 25	Exercise 24	relco 5201
[TakeutiZaring] p. 25	Exercise 29	funco 5331
[TakeutiZaring] p. 25	Exercise 30	f1co 5516
[TakeutiZaring] p. 26	Definition 6.10	eu2 2100
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5299  fv3 5623
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5241  cnvexg 5240
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4965  dmexg 4962
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4966  rnexg 4963
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5617
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5627  tz6.12 5628  tz6.12c 5630
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5591
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5294
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5295
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5297  wfo 5289
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5296  wf1 5288
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5298  wf1o 5290
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5702  eqfnfv2 5703  eqfnfv2f 5706
[TakeutiZaring] p. 28	Exercise 5	fvco 5674
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5831  fnexALT 6221
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5830  resfunexgALT 6218
[TakeutiZaring] p. 29	Exercise 9	funimaex 5379  funimaexg 5378
[TakeutiZaring] p. 29	Definition 6.18	df-br 4061
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5072  iniseg 5074
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4355
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5300
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5904
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5905
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5910
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5912
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5920
[TakeutiZaring] p. 35	Notation	wtr 4159
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4420
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4163
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4643
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4447
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4451
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4559
[TakeutiZaring] p. 38	Definition 7.11	df-on 4434
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4553
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4619
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4649
[TakeutiZaring] p. 40	Exercise 7	dftr2 4161
[TakeutiZaring] p. 40	Exercise 11	unon 4578
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4554
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3893
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4437
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4481  sucidg 4482
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4568
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4435
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4573  ordelsuc 4572
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4661
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4662
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4663
[TakeutiZaring] p. 43	Axiom 7	omex 4660
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4674
[TakeutiZaring] p. 43	Corollary 7.31	find 4666
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4664
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4665
[TakeutiZaring] p. 44	Exercise 2	int0 3914
[TakeutiZaring] p. 44	Exercise 3	trintssm 4175
[TakeutiZaring] p. 44	Exercise 4	intss1 3915
[TakeutiZaring] p. 44	Exercise 6	onintonm 4584
[TakeutiZaring] p. 44	Definition 7.35	df-int 3901
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6419
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6476  tfri1d 6446
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6477  tfri2d 6447
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6478
[TakeutiZaring] p. 50	Exercise 3	smoiso 6413
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6397
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6575
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6571
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6568
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6572
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6620  nnaordi 6619
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3987  uniss2 3896
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6581
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6591
[TakeutiZaring] p. 62	Exercise 5	oaword1 6582
[TakeutiZaring] p. 62	Definition 8.15	om0 6569  omsuc 6583
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6592
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6628  nnmordi 6627
[TakeutiZaring] p. 67	Definition 8.30	oei0 6570
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7322
[TakeutiZaring] p. 88	Exercise 1	en0 6912
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6981
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6982
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6855  isfi 6877
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6953
[TakeutiZaring] p. 95	Definition 10.42	df-map 6762
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 6959
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6972
[Tarski] p. 67	Axiom B5	ax-4 1534
[Tarski] p. 68	Lemma 6	equid 1725
[Tarski] p. 69	Lemma 7	equcomi 1728
[Tarski] p. 70	Lemma 14	spim 1762  spime 1765  spimeh 1763  spimh 1761
[Tarski] p. 70	Lemma 16	ax-11 1530  ax-11o 1847  ax11i 1738
[Tarski] p. 70	Lemmas 16 and 17	sb6 1911
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1550
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2180  ax-14 2181
[WhiteheadRussell] p. 96	Axiom *1.3	olc 713
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 729
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 758
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 767
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 791
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 617
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 644
[WhiteheadRussell] p. 100	Theorem *2.04	pm2.04 82
[WhiteheadRussell] p. 100	Theorem *2.05	imim2 55
[WhiteheadRussell] p. 100	Theorem *2.06	imim1 76
[WhiteheadRussell] p. 101	Theorem *2.1	pm2.1dc 839
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2154  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 739
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 838
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 630
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 887
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 845
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 858
[WhiteheadRussell] p. 103	Theorem *2.16	con3 643
[WhiteheadRussell] p. 103	Theorem *2.17	condc 855
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 857
[WhiteheadRussell] p. 104	Theorem *2.2	orc 714
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 777
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 618
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 622
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 895
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 909
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 770
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 771
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 806
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 807
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 805
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 982
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 780
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 778
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 779
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 740
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 741
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 869  pm2.5gdc 868
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 864
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 742
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 743
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 744
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 657
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 658
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 724
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 893
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 727
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 728
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 867
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 750
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 802
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 803
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 661
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 715  pm2.67 745
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 871  pm2.521gdc 870
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 749
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 812
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 896
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 917
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 808
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 809
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 811
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 810
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 813
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 814
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 907
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 756
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 960
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 961
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 962
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 755
[WhiteheadRussell] p. 111	Theorem *3.21	pm3.21 264
[WhiteheadRussell] p. 111	Theorem *3.22	pm3.22 265
[WhiteheadRussell] p. 111	Theorem *3.24	pm3.24 695
[WhiteheadRussell] p. 112	Theorem *3.35	pm3.35 347
[WhiteheadRussell] p. 112	Theorem *3.3 (Exp)	pm3.3 261
[WhiteheadRussell] p. 112	Theorem *3.31 (Imp)	pm3.31 262
[WhiteheadRussell] p. 112	Theorem *3.26 (Simp)	simpl 109  simplimdc 862
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 861
[WhiteheadRussell] p. 112	Theorem *3.33 (Syll)	pm3.33 345
[WhiteheadRussell] p. 112	Theorem *3.34 (Syll)	pm3.34 346
[WhiteheadRussell] p. 112	Theorem *3.37 (Transp)	pm3.37 691
[WhiteheadRussell] p. 113	Fact)	pm3.45 597
[WhiteheadRussell] p. 113	Theorem *3.4	pm3.4 333
[WhiteheadRussell] p. 113	Theorem *3.41	pm3.41 331
[WhiteheadRussell] p. 113	Theorem *3.42	pm3.42 332
[WhiteheadRussell] p. 113	Theorem *3.44	jao 757  pm3.44 717
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 344
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 602
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 787
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 873
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 874
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 892
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 696
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 955  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 759  pm4.25 760
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 820
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 730
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 769
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 794
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 605
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 824
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 983
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 818
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 974
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 952
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 781
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 816  pm4.45 786  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1505
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 959
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 899  imorr 723
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 901
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 752
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 753
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 904
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 941
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 754  pm4.56 782
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 942  oranim 783
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 688
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 900
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 888
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 902
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 689
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 903
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 889
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 389  pm4.71d 393  pm4.71i 391  pm4.71r 390  pm4.71rd 394  pm4.71ri 392
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 829
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 746
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 603  pm4.76 604
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 712  pm4.77 801
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 784
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 905
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 709
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 910
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 953
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 954
[WhiteheadRussell] p. 122	Theorem *4.84	imbi1 236
[WhiteheadRussell] p. 122	Theorem *4.85	imbi2 237
[WhiteheadRussell] p. 122	Theorem *4.86	bibi1 240
[WhiteheadRussell] p. 122	Theorem *4.87	bi2.04 248  impexp 263  pm4.87 557
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 601
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 911
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 912
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 914
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 913
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1409
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 830
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 906
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1414  pm5.18dc 885
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 708
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 697
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1412
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1417
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1418
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 897
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 475
[WhiteheadRussell] p. 125	Theorem *5.4	pm5.4 249
[WhiteheadRussell] p. 125	Theorem *5.5	pm5.5 242
[WhiteheadRussell] p. 125	Theorem *5.6	pm5.6dc 928  pm5.6r 929
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 957
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 348
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 453
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 609
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 919
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 610
[WhiteheadRussell] p. 125	Theorem *5.41	imdi 250  pm5.41 251
[WhiteheadRussell] p. 125	Theorem *5.42	pm5.42 320
[WhiteheadRussell] p. 125	Theorem *5.44	pm5.44 927
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 804
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 920
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 915
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 796
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 948
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 949
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 964
[WhiteheadRussell] p. 125	Theorem *5.501	pm5.501 244
[WhiteheadRussell] p. 126	Theorem *5.74	pm5.74 179
[WhiteheadRussell] p. 126	Theorem *5.75	pm5.75 965
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1659
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1509
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1656
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1920
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2058
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2459
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2460
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2919
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3063
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5271
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5272
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2135  eupickbi 2138
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5299
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7326