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 7419  fidcenum 7239
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7239
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7419
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 13260
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7205
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 7191
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 13275
[AczelRathjen], p. 75	Corollary 8.1.20	unct 13277
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 13266  znnen 13233
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 13278
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 13279
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 11164
[AczelRathjen], p. 183	Chapter 20	ax-setind 4664
[AhoHopUll] p. 318	Section 9.1	df-concat 11304  df-pfx 11390  df-substr 11363  df-word 11250  lencl 11253  wrd0 11274
[Apostol] p. 18	Theorem I.1	addcan 8469  addcan2d 8474  addcan2i 8472  addcand 8473  addcani 8471
[Apostol] p. 18	Theorem I.2	negeu 8480
[Apostol] p. 18	Theorem I.3	negsub 8537  negsubd 8606  negsubi 8567
[Apostol] p. 18	Theorem I.4	negneg 8539  negnegd 8591  negnegi 8559
[Apostol] p. 18	Theorem I.5	subdi 8675  subdid 8704  subdii 8697  subdir 8676  subdird 8705  subdiri 8698
[Apostol] p. 18	Theorem I.6	mul01 8679  mul01d 8683  mul01i 8681  mul02 8677  mul02d 8682  mul02i 8680
[Apostol] p. 18	Theorem I.9	divrecapd 9084
[Apostol] p. 18	Theorem I.10	recrecapi 9035
[Apostol] p. 18	Theorem I.12	mul2neg 8688  mul2negd 8703  mul2negi 8696  mulneg1 8685  mulneg1d 8701  mulneg1i 8694
[Apostol] p. 18	Theorem I.14	rdivmuldivd 14389
[Apostol] p. 18	Theorem I.15	divdivdivap 9004
[Apostol] p. 20	Axiom 7	rpaddcl 10028  rpaddcld 10063  rpmulcl 10029  rpmulcld 10064
[Apostol] p. 20	Axiom 9	0nrp 10040
[Apostol] p. 20	Theorem I.17	lttri 8394
[Apostol] p. 20	Theorem I.18	ltadd1d 8829  ltadd1dd 8847  ltadd1i 8793
[Apostol] p. 20	Theorem I.19	ltmul1 8883  ltmul1a 8882  ltmul1i 9211  ltmul1ii 9219  ltmul2 9147  ltmul2d 10090  ltmul2dd 10104  ltmul2i 9214
[Apostol] p. 20	Theorem I.21	0lt1 8416
[Apostol] p. 20	Theorem I.23	lt0neg1 8759  lt0neg1d 8806  ltneg 8753  ltnegd 8814  ltnegi 8784
[Apostol] p. 20	Theorem I.25	lt2add 8736  lt2addd 8858  lt2addi 8801
[Apostol] p. 20	Definition of positive numbers	df-rp 10005
[Apostol] p. 21	Exercise 4	recgt0 9141  recgt0d 9225  recgt0i 9197  recgt0ii 9198
[Apostol] p. 22	Definition of integers	df-z 9595
[Apostol] p. 22	Definition of rationals	df-q 9970
[Apostol] p. 24	Theorem I.26	supeuti 7298
[Apostol] p. 26	Theorem I.29	arch 9510
[Apostol] p. 28	Exercise 2	btwnz 9715
[Apostol] p. 28	Exercise 3	nnrecl 9511
[Apostol] p. 28	Exercise 6	qbtwnre 10640
[Apostol] p. 28	Exercise 10(a)	zeneo 12582  zneo 9697
[Apostol] p. 29	Theorem I.35	resqrtth 11741  sqrtthi 11829
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9257
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12757
[Apostol] p. 363	Remark	absgt0api 11856
[Apostol] p. 363	Example	abssubd 11903  abssubi 11860
[ApostolNT] p. 14	Definition	df-dvds 12499
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 12515
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12539
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12535
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12529
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12531
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 12516
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 12517
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 12522
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12556
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12558
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12560
[ApostolNT] p. 15	Definition	dfgcd2 12735
[ApostolNT] p. 16	Definition	isprm2 12839
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12814
[ApostolNT] p. 16	Theorem 1.7	prminf 13290
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12694
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12736
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12738
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12708
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12701
[ApostolNT] p. 17	Theorem 1.8	coprm 12866
[ApostolNT] p. 17	Theorem 1.9	euclemma 12868
[ApostolNT] p. 17	Theorem 1.10	1arith2 13091
[ApostolNT] p. 19	Theorem 1.14	divalg 12635
[ApostolNT] p. 20	Theorem 1.15	eucalg 12781
[ApostolNT] p. 25	Definition	df-phi 12933
[ApostolNT] p. 26	Theorem 2.2	phisum 12963
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 12944
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 12948
[ApostolNT] p. 38	Remark	df-sgm 15976
[ApostolNT] p. 38	Definition	df-sgm 15976
[ApostolNT] p. 104	Definition	congr 12822
[ApostolNT] p. 106	Remark	dvdsval3 12502
[ApostolNT] p. 106	Definition	moddvds 12510
[ApostolNT] p. 107	Example 2	mod2eq0even 12589
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12590
[ApostolNT] p. 107	Example 4	zmod1congr 10727
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10764
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 11053
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12534
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12825
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 13144
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12827
[ApostolNT] p. 113	Theorem 5.17	eulerth 12955
[ApostolNT] p. 113	Theorem 5.18	vfermltl 12974
[ApostolNT] p. 114	Theorem 5.19	fermltl 12956
[ApostolNT] p. 179	Definition	df-lgs 15997  lgsprme0 16041
[ApostolNT] p. 180	Example 1	1lgs 16042
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 16018
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 16033
[ApostolNT] p. 181	Theorem 9.4	m1lgs 16084
[ApostolNT] p. 181	Theorem 9.5	2lgs 16103  2lgsoddprm 16112
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 16068
[ApostolNT] p. 185	Theorem 9.8	lgsquad 16079
[ApostolNT] p. 188	Definition	df-lgs 15997  lgs1 16043
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 16034
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 16036
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 16044
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 16045
[Bauer] p. 482	Section 1.2	pm2.01 621  pm2.65 665
[Bauer] p. 483	Theorem 1.3	acexmid 6057  onsucelsucexmidlem 4656
[Bauer], p. 481	Section 1.1	pwtrufal 16897
[Bauer], p. 483	Definition	n0rf 3525
[Bauer], p. 483	Theorem 1.2	2irrexpq 15967  2irrexpqap 15969
[Bauer], p. 485	Theorem 2.1	exmidssfi 7212  ssfiexmid 7144  ssfiexmidt 7146
[Bauer], p. 493	Section 5.1	ivthdich 15644
[Bauer], p. 494	Theorem 5.5	ivthinc 15634
[BauerHanson], p. 27	Proposition 5.2	cnstab 8936
[BauerSwan], p. 3	Definition on page 14:3	enumct 7419
[BauerSwan], p. 14	Remark	0ct 7411  ctm 7413
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 16900
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7832
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7745
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7834
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7868  addlocpr 7867
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7894
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7897
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7902
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2085
[BellMachover] p. 460	Notation	df-mo 2086
[BellMachover] p. 460	Definition	mo3 2137  mo3h 2136
[BellMachover] p. 462	Theorem 1.1	bm1.1 2219
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4236
[BellMachover] p. 466	Axiom Pow	axpow3 4295
[BellMachover] p. 466	Axiom Union	axun2 4561
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4669
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4510
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4672
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4623
[BellMachover] p. 471	Definition of Lim	df-ilim 4495
[BellMachover] p. 472	Axiom Inf	zfinf2 4716
[BellMachover] p. 473	Theorem 2.8	limom 4741
[Bobzien] p. 116	Statement T3	stoic3 1476
[Bobzien] p. 117	Statement T2	stoic2a 1474
[Bobzien] p. 117	Statement T4	stoic4a 1477
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1472
[Bollobas] p. 1	Section I.1	df-edg 16179  isuhgropm 16202  isusgropen 16286  isuspgropen 16285
[Bollobas] p. 2	Section I.1	df-subgr 16375  uhgrspansubgr 16398
[Bollobas] p. 4	Definition	df-wlks 16439
[Bollobas] p. 5	Definition	df-trls 16502
[Bollobas] p. 7	Section I.1	df-ushgrm 16191
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13619
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13665
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13678
[BourbakiAlg1] p. 92	Definition 1	df-ring 14241
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 14172
[BourbakiEns] p.	Proposition 8	fcof1 5962  fcofo 5963
[BourbakiTop1] p.	Remark	xnegmnf 10181  xnegpnf 10180
[BourbakiTop1] p.	Remark	rexneg 10182
[BourbakiTop1] p.	Proposition	ishmeo 15295
[BourbakiTop1] p.	Property V_i	ssnei2 15148
[BourbakiTop1] p.	Property V_ii	innei 15154
[BourbakiTop1] p.	Property V_iv	neissex 15156
[BourbakiTop1] p.	Proposition 1	neipsm 15145  neiss 15141
[BourbakiTop1] p.	Proposition 2	cnptopco 15213
[BourbakiTop1] p.	Proposition 4	imasnopn 15290
[BourbakiTop1] p.	Property V_iii	elnei 15143
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 14989
[Bruck] p. 1	Section I.1	df-mgm 13619
[Bruck] p. 23	Section II.1	df-sgrp 13665
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13854
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4178
[Church] p. 129	Section II.24	df-ifp 987  dfifp2dc 990
[Cohen] p. 301	Remark	relogoprlem 15859
[Cohen] p. 301	Property 2	relogmul 15860  relogmuld 15875
[Cohen] p. 301	Property 3	relogdiv 15861  relogdivd 15876
[Cohen] p. 301	Property 4	relogexp 15863
[Cohen] p. 301	Property 1a	log1 15857
[Cohen] p. 301	Property 1b	loge 15858
[Cohen4] p. 348	Observation	relogbcxpbap 15956
[Cohen4] p. 352	Definition	rpelogb 15940
[Cohen4] p. 361	Property 2	rprelogbmul 15946
[Cohen4] p. 361	Property 3	logbrec 15951  rprelogbdiv 15948
[Cohen4] p. 361	Property 4	rplogbreexp 15944
[Cohen4] p. 361	Property 6	relogbexpap 15949
[Cohen4] p. 361	Property 1(a)	rplogbid1 15938
[Cohen4] p. 361	Property 1(b)	rplogb1 15939
[Cohen4] p. 367	Property	rplogbchbase 15941
[Cohen4] p. 377	Property 2	logblt 15953
[Crosilla] p.	Axiom 1	ax-ext 2216
[Crosilla] p.	Axiom 2	ax-pr 4327
[Crosilla] p.	Axiom 3	ax-un 4559
[Crosilla] p.	Axiom 4	ax-nul 4241
[Crosilla] p.	Axiom 5	ax-iinf 4715
[Crosilla] p.	Axiom 6	ru 3044
[Crosilla] p.	Axiom 8	ax-pow 4292
[Crosilla] p.	Axiom 9	ax-setind 4664
[Crosilla], p.	Axiom 6	ax-sep 4233
[Crosilla], p.	Axiom 7	ax-coll 4230
[Crosilla], p.	Axiom 7'	repizf 4231
[Crosilla], p.	Theorem is stated	ordtriexmid 4648
[Crosilla], p.	Axiom of choice implies instances	acexmid 6057
[Crosilla], p.	Definition of ordinal	df-iord 4492
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4662
[Diestel] p. 4	Section 1.1	df-subgr 16375  uhgrspansubgr 16398
[Diestel] p. 27	Section 1.10	df-ushgrm 16191
[Eisenberg] p. 67	Definition 5.3	df-dif 3216
[Eisenberg] p. 82	Definition 6.3	df-iom 4718
[Eisenberg] p. 125	Definition 8.21	df-map 6897
[Enderton] p. 18	Axiom of Empty Set	axnul 4240
[Enderton] p. 19	Definition	df-tp 3702
[Enderton] p. 26	Exercise 5	unissb 3949
[Enderton] p. 26	Exercise 10	pwel 4339
[Enderton] p. 28	Exercise 7(b)	pwunim 4412
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 4066  iinin2m 4065  iunin1 4061  iunin2 4060
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 4064  iundif2ss 4062
[Enderton] p. 33	Exercise 23	iinuniss 4079
[Enderton] p. 33	Exercise 25	iununir 4080
[Enderton] p. 33	Exercise 24(a)	iinpw 4087
[Enderton] p. 33	Exercise 24(b)	iunpw 4606  iunpwss 4088
[Enderton] p. 38	Exercise 6(a)	unipw 4338
[Enderton] p. 38	Exercise 6(b)	pwuni 4310
[Enderton] p. 41	Lemma 3D	opeluu 4576  rnex 5030  rnexg 5027
[Enderton] p. 41	Exercise 8	dmuni 4971  rnuni 5179
[Enderton] p. 42	Definition of a function	dffun7 5384  dffun8 5385
[Enderton] p. 43	Definition of function value	funfvdm2 5746
[Enderton] p. 43	Definition of single-rooted	funcnv 5422
[Enderton] p. 44	Definition (d)	dfima2 5108  dfima3 5109
[Enderton] p. 47	Theorem 3H	fvco2 5751
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7526
[Enderton] p. 50	Theorem 3K(a)	imauni 5940
[Enderton] p. 52	Definition	df-map 6897
[Enderton] p. 53	Exercise 21	coass 5286
[Enderton] p. 53	Exercise 27	dmco 5276
[Enderton] p. 53	Exercise 14(a)	funin 5432
[Enderton] p. 53	Exercise 22(a)	imass2 5143
[Enderton] p. 54	Remark	ixpf 6968  ixpssmap 6980
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6947
[Enderton] p. 56	Theorem 3M	erref 6800
[Enderton] p. 57	Lemma 3N	erthi 6828
[Enderton] p. 57	Definition	df-ec 6782
[Enderton] p. 58	Definition	df-qs 6786
[Enderton] p. 60	Theorem 3Q	th3q 6887  th3qcor 6886  th3qlem1 6884  th3qlem2 6885
[Enderton] p. 61	Exercise 35	df-ec 6782
[Enderton] p. 65	Exercise 56(a)	dmun 4968
[Enderton] p. 68	Definition of successor	df-suc 4497
[Enderton] p. 71	Definition	df-tr 4214  dftr4 4218
[Enderton] p. 72	Theorem 4E	unisuc 4539  unisucg 4540
[Enderton] p. 73	Exercise 6	unisuc 4539  unisucg 4540
[Enderton] p. 73	Exercise 5(a)	truni 4227
[Enderton] p. 73	Exercise 5(b)	trint 4228
[Enderton] p. 79	Theorem 4I(A1)	nna0 6720
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6722  onasuc 6712
[Enderton] p. 79	Definition of operation value	df-ov 6061
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6721
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6723  onmsuc 6719
[Enderton] p. 81	Theorem 4K(1)	nnaass 6731
[Enderton] p. 81	Theorem 4K(2)	nna0r 6724  nnacom 6730
[Enderton] p. 81	Theorem 4K(3)	nndi 6732
[Enderton] p. 81	Theorem 4K(4)	nnmass 6733
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6735
[Enderton] p. 82	Exercise 16	nnm0r 6725  nnmsucr 6734
[Enderton] p. 88	Exercise 23	nnaordex 6774
[Enderton] p. 129	Definition	df-en 6989
[Enderton] p. 132	Theorem 6B(b)	canth 6009
[Enderton] p. 133	Exercise 1	xpomen 13230
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 7133
[Enderton] p. 136	Corollary 6E	nneneq 7124
[Enderton] p. 139	Theorem 6H(c)	mapen 7112
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7538
[Enderton] p. 143	Theorem 6J	dju0en 7534  dju1en 7533
[Enderton] p. 144	Corollary 6K	undif2ss 3589
[Enderton] p. 145	Figure 38	ffoss 5652
[Enderton] p. 145	Definition	df-dom 6990
[Enderton] p. 146	Example 1	domen 7001  domeng 7002
[Enderton] p. 146	Example 3	nndomo 7131
[Enderton] p. 149	Theorem 6L(c)	xpdom1 7099  xpdom1g 7097  xpdom2g 7096
[Enderton] p. 168	Definition	df-po 4422
[Enderton] p. 192	Theorem 7M(a)	oneli 4554
[Enderton] p. 192	Theorem 7M(b)	ontr1 4515
[Enderton] p. 192	Theorem 7M(c)	onirri 4670
[Enderton] p. 193	Corollary 7N(b)	0elon 4518
[Enderton] p. 193	Corollary 7N(c)	onsuci 4643
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4616
[Enderton] p. 194	Remark	onprc 4679
[Enderton] p. 194	Exercise 16	suc11 4685
[Enderton] p. 197	Definition	df-card 7488
[Enderton] p. 200	Exercise 25	tfis 4710
[Enderton] p. 206	Theorem 7X(b)	en2lp 4681
[Enderton] p. 207	Exercise 34	opthreg 4683
[Enderton] p. 208	Exercise 35	suc11g 4684
[Geuvers], p. 1	Remark	expap0 10955
[Geuvers], p. 6	Lemma 2.13	mulap0r 8906
[Geuvers], p. 6	Lemma 2.15	mulap0 8945
[Geuvers], p. 9	Lemma 2.35	msqge0 8907
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8262
[Geuvers], p. 10	Lemma 3.9	maxcom 11913
[Geuvers], p. 10	Lemma 3.10	maxle1 11921  maxle2 11922
[Geuvers], p. 10	Lemma 3.11	maxleast 11923
[Geuvers], p. 10	Lemma 3.12	maxleb 11926
[Geuvers], p. 11	Definition 3.13	dfabsmax 11927
[Geuvers], p. 17	Definition 6.1	df-ap 8873
[Gleason] p. 117	Proposition 9-2.1	df-enq 7678  enqer 7689
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7682  df-nqqs 7679
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7675  df-plqqs 7680
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7676  df-mqqs 7681
[Gleason] p. 119	Proposition 9-2.5	df-rq 7683
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7739
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7742  ltbtwnnq 7747  ltbtwnnqq 7746
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7731
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7732
[Gleason] p. 123	Proposition 9-3.5	addclpr 7868
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7910
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7909
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7928
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7944
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7950  ltaprlem 7949
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7947
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7903
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7923
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7912
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7911
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7919
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7969
[Gleason] p. 126	Proposition 9-4.1	df-enr 8057  enrer 8066
[Gleason] p. 126	Proposition 9-4.2	df-0r 8062  df-1r 8063  df-nr 8058
[Gleason] p. 126	Proposition 9-4.3	df-mr 8060  df-plr 8059  negexsr 8103  recexsrlem 8105
[Gleason] p. 127	Proposition 9-4.4	df-ltr 8061
[Gleason] p. 130	Proposition 10-1.3	creui 9251  creur 9250  cru 8893
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8254  axcnre 8212
[Gleason] p. 132	Definition 10-3.1	crim 11568  crimd 11687  crimi 11647  crre 11567  crred 11686  crrei 11646
[Gleason] p. 132	Definition 10-3.2	remim 11570  remimd 11652
[Gleason] p. 133	Definition 10.36	absval2 11767  absval2d 11895  absval2i 11854
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11594  cjaddd 11675  cjaddi 11642
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11595  cjmuld 11676  cjmuli 11643
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11593  cjcjd 11653  cjcji 11625
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11592  cjreb 11576  cjrebd 11656  cjrebi 11628  cjred 11681  rere 11575  rereb 11573  rerebd 11655  rerebi 11627  rered 11679
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11601  addcjd 11667  addcji 11637
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11711
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11762  abscjd 11900  abscji 11858
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11774  abs00d 11896  abs00i 11855  absne0d 11897
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11806  releabsd 11901  releabsi 11859
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11779  absmuld 11904  absmuli 11861
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11765  sqabsaddi 11862
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11814  abstrid 11906  abstrii 11865
[Gleason] p. 134	Definition 10-4.1	df-exp 10925  exp0 10929  expp1 10932  expp1d 11061
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10967  expaddd 11062
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 15903  cxpmuld 15928  expmul 10970  expmuld 11063
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10964  mulexpd 11075  rpmulcxp 15900
[Gleason] p. 141	Definition 11-2.1	fzval 10363
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 12036
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 12038
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 12037
[Gleason] p. 171	Corollary 12-2.2	climmulc2 12041
[Gleason] p. 172	Corollary 12-2.5	climrecl 12034
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 12030  climcj 12031  climim 12033  climre 12032
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8329  df-xr 8328  ltxr 10127
[Gleason] p. 180	Theorem 12-5.3	climcau 12057
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10684
[Gleason] p. 223	Definition 14-1.1	df-met 14819
[Gleason] p. 223	Definition 14-1.1(a)	met0 15355  xmet0 15354
[Gleason] p. 223	Definition 14-1.1(c)	metsym 15362
[Gleason] p. 223	Definition 14-1.1(d)	mettri 15364  mstri 15464  xmettri 15363  xmstri 15463
[Gleason] p. 230	Proposition 14-2.6	txlm 15270
[Gleason] p. 240	Proposition 14-4.2	metcnp3 15502
[Gleason] p. 243	Proposition 14-4.16	addcn2 12020  addcncntop 15553  mulcn2 12022  mulcncntop 15555  subcn2 12021  subcncntop 15554
[Gleason] p. 295	Remark	bcval3 11138  bcval4 11139
[Gleason] p. 295	Equation 2	bcpasc 11153
[Gleason] p. 295	Definition of binomial coefficient	bcval 11136  df-bc 11135
[Gleason] p. 296	Remark	bcn0 11142  bcnn 11144
[Gleason] p. 296	Theorem 15-2.8	binom 12195
[Gleason] p. 308	Equation 2	ef0 12383
[Gleason] p. 308	Equation 3	efcj 12384
[Gleason] p. 309	Corollary 15-4.3	efne0 12389
[Gleason] p. 309	Corollary 15-4.4	efexp 12393
[Gleason] p. 310	Equation 14	sinadd 12447
[Gleason] p. 310	Equation 15	cosadd 12448
[Gleason] p. 311	Equation 17	sincossq 12459
[Gleason] p. 311	Equation 18	cosbnd 12464  sinbnd 12463
[Gleason] p. 311	Definition of ` `	df-pi 12364
[Golan] p. 1	Remark	srgisid 14229
[Golan] p. 1	Definition	df-srg 14207
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1498
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13766  mndideu 13687
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13793
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13822
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13833
[Herstein] p. 57	Exercise 1	dfgrp3me 13855
[Heyting] p. 127	Axiom #1	ax1hfs 16986
[Hitchcock] p. 5	Rule A3	mptnan 1468
[Hitchcock] p. 5	Rule A4	mptxor 1469
[Hitchcock] p. 5	Rule A5	mtpxor 1471
[HoTT], p.	Lemma 10.4.1	exmidontriim 7545
[HoTT], p.	Theorem 7.2.6	nndceq 6745
[HoTT], p.	Exercise 11.10	neapmkv 16980
[HoTT], p.	Exercise 11.11	mulap0bd 8948
[HoTT], p.	Section 11.2.1	df-iltp 7801  df-imp 7800  df-iplp 7799  df-reap 8866
[HoTT], p.	Theorem 11.2.4	recapb 8962  rerecapb 9134
[HoTT], p.	Corollary 3.9.2	uchoice 6344
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7993
[HoTT], p.	Corollary 11.4.3	conventions 16615
[HoTT], p.	Exercise 11.6(i)	dcapnconst 16973  dceqnconst 16972
[HoTT], p.	Corollary 11.2.13	axcaucvg 8231  caucvgpr 8013  caucvgprpr 8043  caucvgsr 8133
[HoTT], p.	Definition 11.2.1	df-inp 7797
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 16978
[HoTT], p.	Proposition 11.2.3	df-iso 4423  ltpopr 7926  ltsopr 7927
[HoTT], p.	Definition 11.2.7(v)	apsym 8897  reapcotr 8889  reapirr 8868
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8416  gt0add 8864  leadd1 8721  lelttr 8378  lemul1a 9149  lenlt 8365  ltadd1 8720  ltletr 8379  ltmul1 8883  reaplt 8879
[Huneke] p. 2	Statement	df-clwwlknon 16548
[Jech] p. 4	Definition of class	cv 1397  cvjust 2229
[Jech] p. 78	Note	opthprc 4806
[KalishMontague] p. 81	Note 1	ax-i9 1579
[Kreyszig] p. 3	Property M1	metcl 15344  xmetcl 15343
[Kreyszig] p. 4	Property M2	meteq0 15351
[Kreyszig] p. 12	Equation 5	muleqadd 8959
[Kreyszig] p. 18	Definition 1.3-2	mopnval 15433
[Kreyszig] p. 19	Remark	mopntopon 15434
[Kreyszig] p. 19	Theorem T1	mopn0 15479  mopnm 15439
[Kreyszig] p. 19	Theorem T2	unimopn 15477
[Kreyszig] p. 19	Definition of neighborhood	neibl 15482
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 15504
[Kreyszig] p. 25	Definition 1.4-1	lmbr 15204
[Kreyszig] p. 51	Equation 2	lmodvneg1 14604
[Kreyszig] p. 51	Equation 1a	lmod0vs 14595
[Kreyszig] p. 51	Equation 1b	lmodvs0 14596
[Kunen] p. 10	Axiom 0	a9e 1744
[Kunen] p. 12	Axiom 6	zfrep6 4232
[Kunen] p. 24	Definition 10.24	mapval 6907  mapvalg 6905
[Kunen] p. 31	Definition 10.24	mapex 6901
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 4006
[Lang] p. 3	Statement	lidrideqd 13644  mndbn0 13692
[Lang] p. 3	Definition	df-mnd 13678
[Lang] p. 4	Definition of a (finite) product	gsumsplit1r 13661
[Lang] p. 5	Equation	gsumfzreidx 14090
[Lang] p. 6	Definition	mulgnn0gsum 13881
[Lang] p. 7	Definition	dfgrp2e 13783
[Levy] p. 338	Axiom	df-clab 2221  df-clel 2230  df-cleq 2227
[Lopez-Astorga] p. 12	Rule 1	mptnan 1468
[Lopez-Astorga] p. 12	Rule 2	mptxor 1469
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1471
[Margaris] p. 40	Rule C	exlimiv 1647
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 861
[Margaris] p. 49	Definition	dfbi2 388  dfordc 900  exalim 1551
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 657
[Margaris] p. 89	Theorem 19.2	19.2 1687  r19.2m 3600
[Margaris] p. 89	Theorem 19.3	19.3 1603  19.3h 1602  rr19.3v 2959
[Margaris] p. 89	Theorem 19.5	alcom 1527
[Margaris] p. 89	Theorem 19.6	alexdc 1668  alexim 1694
[Margaris] p. 89	Theorem 19.7	alnex 1548
[Margaris] p. 89	Theorem 19.8	19.8a 1639  spsbe 1891
[Margaris] p. 89	Theorem 19.9	19.9 1693  19.9h 1692  19.9v 1920  exlimd 1646
[Margaris] p. 89	Theorem 19.11	excom 1712  excomim 1711
[Margaris] p. 89	Theorem 19.12	19.12 1713  r19.12 2651
[Margaris] p. 90	Theorem 19.14	exnalim 1695
[Margaris] p. 90	Theorem 19.15	albi 1517  ralbi 2677
[Margaris] p. 90	Theorem 19.16	19.16 1604
[Margaris] p. 90	Theorem 19.17	19.17 1605
[Margaris] p. 90	Theorem 19.18	exbi 1653  rexbi 2678
[Margaris] p. 90	Theorem 19.19	19.19 1714
[Margaris] p. 90	Theorem 19.20	alim 1506  alimd 1570  alimdh 1516  alimdv 1928  ralimdaa 2610  ralimdv 2612  ralimdva 2611  ralimdvva 2613  sbcimdv 3111
[Margaris] p. 90	Theorem 19.21	19.21-2 1715  19.21 1632  19.21bi 1607  19.21h 1606  19.21ht 1630  19.21t 1631  19.21v 1922  alrimd 1659  alrimdd 1658  alrimdh 1528  alrimdv 1925  alrimi 1571  alrimih 1518  alrimiv 1923  alrimivv 1924  r19.21 2620  r19.21be 2635  r19.21bi 2632  r19.21t 2619  r19.21v 2621  ralrimd 2622  ralrimdv 2623  ralrimdva 2624  ralrimdvv 2628  ralrimdvva 2629  ralrimi 2615  ralrimiv 2616  ralrimiva 2617  ralrimivv 2625  ralrimivva 2626  ralrimivvva 2627  ralrimivw 2618  rexlimi 2655
[Margaris] p. 90	Theorem 19.22	2alimdv 1930  2eximdv 1931  exim 1648  eximd 1661  eximdh 1660  eximdv 1929  rexim 2638  reximdai 2642  reximddv 2647  reximddv2 2649  reximdv 2645  reximdv2 2643  reximdva 2646  reximdvai 2644  reximi2 2640
[Margaris] p. 90	Theorem 19.23	19.23 1726  19.23bi 1641  19.23h 1547  19.23ht 1546  19.23t 1725  19.23v 1932  19.23vv 1933  exlimd2 1644  exlimdh 1645  exlimdv 1868  exlimdvv 1949  exlimi 1643  exlimih 1642  exlimiv 1647  exlimivv 1948  r19.23 2653  r19.23v 2654  rexlimd 2659  rexlimdv 2661  rexlimdv3a 2664  rexlimdva 2662  rexlimdva2 2665  rexlimdvaa 2663  rexlimdvv 2669  rexlimdvva 2670  rexlimdvw 2666  rexlimiv 2656  rexlimiva 2657  rexlimivv 2668
[Margaris] p. 90	Theorem 19.24	i19.24 1688
[Margaris] p. 90	Theorem 19.25	19.25 1675
[Margaris] p. 90	Theorem 19.26	19.26-2 1531  19.26-3an 1532  19.26 1530  r19.26-2 2674  r19.26-3 2675  r19.26 2671  r19.26m 2676
[Margaris] p. 90	Theorem 19.27	19.27 1610  19.27h 1609  19.27v 1951  r19.27av 2680  r19.27m 3609  r19.27mv 3610
[Margaris] p. 90	Theorem 19.28	19.28 1612  19.28h 1611  19.28v 1952  r19.28av 2681  r19.28m 3603  r19.28mv 3606  rr19.28v 2960
[Margaris] p. 90	Theorem 19.29	19.29 1669  19.29r 1670  19.29r2 1671  19.29x 1672  r19.29 2682  r19.29d2r 2689  r19.29r 2683
[Margaris] p. 90	Theorem 19.30	19.30dc 1676
[Margaris] p. 90	Theorem 19.31	19.31r 1729
[Margaris] p. 90	Theorem 19.32	19.32dc 1727  19.32r 1728  r19.32r 2691  r19.32vdc 2694  r19.32vr 2693
[Margaris] p. 90	Theorem 19.33	19.33 1533  19.33b2 1678  19.33bdc 1679
[Margaris] p. 90	Theorem 19.34	19.34 1732
[Margaris] p. 90	Theorem 19.35	19.35-1 1673  19.35i 1674
[Margaris] p. 90	Theorem 19.36	19.36-1 1721  19.36aiv 1953  19.36i 1720  r19.36av 2696
[Margaris] p. 90	Theorem 19.37	19.37-1 1722  19.37aiv 1723  r19.37 2697  r19.37av 2698
[Margaris] p. 90	Theorem 19.38	19.38 1724
[Margaris] p. 90	Theorem 19.39	i19.39 1689
[Margaris] p. 90	Theorem 19.40	19.40-2 1681  19.40 1680  r19.40 2699
[Margaris] p. 90	Theorem 19.41	19.41 1734  19.41h 1733  19.41v 1954  19.41vv 1955  19.41vvv 1956  19.41vvvv 1957  r19.41 2700  r19.41v 2701
[Margaris] p. 90	Theorem 19.42	19.42 1736  19.42h 1735  19.42v 1958  19.42vv 1963  19.42vvv 1964  19.42vvvv 1965  r19.42v 2702
[Margaris] p. 90	Theorem 19.43	19.43 1677  r19.43 2703
[Margaris] p. 90	Theorem 19.44	19.44 1730  r19.44av 2704  r19.44mv 3608
[Margaris] p. 90	Theorem 19.45	19.45 1731  r19.45av 2705  r19.45mv 3607
[Margaris] p. 110	Exercise 2(b)	eu1 2107
[Megill] p. 444	Axiom C5	ax-17 1575
[Megill] p. 445	Lemma L12	alequcom 1564  ax-10 1554
[Megill] p. 446	Lemma L17	equtrr 1758
[Megill] p. 446	Lemma L19	hbnae 1769
[Megill] p. 447	Remark 9.1	df-sb 1812  sbid 1823
[Megill] p. 448	Scheme C5'	ax-4 1559
[Megill] p. 448	Scheme C6'	ax-7 1497
[Megill] p. 448	Scheme C8'	ax-8 1553
[Megill] p. 448	Scheme C9'	ax-i12 1556
[Megill] p. 448	Scheme C11'	ax-10o 1764
[Megill] p. 448	Scheme C12'	ax-13 2207
[Megill] p. 448	Scheme C13'	ax-14 2208
[Megill] p. 448	Scheme C15'	ax-11o 1872
[Megill] p. 448	Scheme C16'	ax-16 1863
[Megill] p. 448	Theorem 9.4	dral1 1779  dral2 1780  drex1 1847  drex2 1781  drsb1 1848  drsb2 1890
[Megill] p. 449	Theorem 9.7	sbcom2 2043  sbequ 1889  sbid2v 2052
[Megill] p. 450	Example in Appendix	hba1 1589
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3129  rspsbca 3130  stdpc4 1824
[Mendelson] p. 69	Axiom 5	ra5 3135  stdpc5 1633
[Mendelson] p. 81	Rule C	exlimiv 1647
[Mendelson] p. 95	Axiom 6	stdpc6 1751
[Mendelson] p. 95	Axiom 7	stdpc7 1819
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3549
[Mendelson] p. 231	Exercise 4.10(l)	unv 3550
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3465
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3513
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3466
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3354
[Mendelson] p. 231	Definition of union	unssin 3464
[Mendelson] p. 235	Exercise 4.12(c)	univ 4602
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3918
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4408
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4409
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4410
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3939
[Mendelson] p. 235	Exercise 4.12(p)	reli 4889
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5288
[Mendelson] p. 246	Definition of successor	df-suc 4497
[Mendelson] p. 254	Proposition 4.22(b)	xpen 7111
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 7085  xpsneng 7086
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 7091  xpcomeng 7092
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 7094
[Mendelson] p. 255	Exercise 4.39	endisj 7088
[Mendelson] p. 255	Exercise 4.41	mapprc 6899
[Mendelson] p. 255	Exercise 4.43	mapsnen 7066  mapsnend 7065
[Mendelson] p. 255	Exercise 4.45	mapunen 7117
[Mendelson] p. 255	Exercise 4.47	xpmapen 7116
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6933
[Mendelson] p. 255	Exercise 4.42(b)	map1 7067
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7537  djucomen 7536
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7535
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6713
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3447
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4843
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4844
[Monk1] p. 34	Definition 3.3	df-opab 4177
[Monk1] p. 36	Theorem 3.7(i)	coi1 5283  coi2 5284
[Monk1] p. 36	Theorem 3.8(v)	dm0 4975  rn0 5018
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5172
[Monk1] p. 37	Theorem 3.13(i)	relxp 4864
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4982  rnxpm 5197
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4835  xp0 5187
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5126
[Monk1] p. 38	Theorem 3.16(viii)	imai 5123
[Monk1] p. 39	Theorem 3.17	imaex 5121  imaexg 5120
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5117
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5812  funfvop 5795
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5723
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5733
[Monk1] p. 43	Theorem 4.6	funun 5402
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5947  dff13f 5949
[Monk1] p. 46	Theorem 4.15(v)	funex 5914  funrnex 6316
[Monk1] p. 50	Definition 5.4	fniunfv 5941
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5251
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3970
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6362  df-1st 6347
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6363  df-2nd 6348
[Monk2] p. 105	Axiom C4	ax-5 1496
[Monk2] p. 105	Axiom C7	ax-8 1553
[Monk2] p. 105	Axiom C8	ax-11 1555  ax-11o 1872
[Monk2] p. 105	Axiom (C8)	ax11v 1876
[Monk2] p. 109	Lemma 12	ax-7 1497
[Monk2] p. 109	Lemma 15	equvin 1912  equvini 1807  eqvinop 4364
[Monk2] p. 113	Axiom C5-1	ax-17 1575
[Monk2] p. 113	Axiom C5-2	hbn1 1700
[Monk2] p. 113	Axiom C5-3	ax-7 1497
[Monk2] p. 114	Lemma 22	hba1 1589
[Monk2] p. 114	Lemma 23	hbia1 1601  nfia1 1629
[Monk2] p. 114	Lemma 24	hba2 1600  nfa2 1628
[Moschovakis] p. 2	Chapter 2	df-stab 839  dftest 16987
[Munkres] p. 77	Example 2	distop 15076
[Munkres] p. 78	Definition of basis	df-bases 15034  isbasis3g 15037
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 13557  tgval2 15042
[Munkres] p. 79	Remark	tgcl 15055
[Munkres] p. 80	Lemma 2.1	tgval3 15049
[Munkres] p. 80	Lemma 2.2	tgss2 15070  tgss3 15069
[Munkres] p. 81	Lemma 2.3	basgen 15071  basgen2 15072
[Munkres] p. 89	Definition of subspace topology	resttop 15161
[Munkres] p. 93	Theorem 6.1(1)	0cld 15103  topcld 15100
[Munkres] p. 93	Theorem 6.1(3)	uncld 15104
[Munkres] p. 94	Definition of closure	clsval 15102
[Munkres] p. 94	Definition of interior	ntrval 15101
[Munkres] p. 102	Definition of continuous function	df-cn 15179  iscn 15188  iscn2 15191
[Munkres] p. 107	Theorem 7.2(g)	cncnp 15221  cncnp2m 15222  cncnpi 15219  df-cnp 15180  iscnp 15190
[Munkres] p. 127	Theorem 10.1	metcn 15505
[Pierik], p. 8	Section 2.2.1	dfrex2fin 7174
[Pierik], p. 9	Definition 2.4	df-womni 7468
[Pierik], p. 9	Definition 2.5	df-markov 7456  omniwomnimkv 7471
[Pierik], p. 10	Section 2.3	dfdif3 3333
[Pierik], p. 14	Definition 3.1	df-omni 7439  exmidomniim 7445  finomni 7444
[Pierik], p. 15	Section 3.1	df-nninf 7424
[Pradic2025], p. 2	Section 1.1	nnnninfen 16925
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 16929
[PradicBrown2022], p. 2	Remark	exmidpw 7181
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7517
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7518  exmidfodomrlemrALT 7519
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7453
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 16911  peano4nninf 16910
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 16913
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 16921
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 16923
[PradicBrown2022], p. 5	Definition 3.3	nnsf 16909
[Quine] p. 16	Definition 2.1	df-clab 2221  rabid 2721
[Quine] p. 17	Definition 2.1''	dfsb7 2047
[Quine] p. 18	Definition 2.7	df-cleq 2227
[Quine] p. 19	Definition 2.9	df-v 2817
[Quine] p. 34	Theorem 5.1	abeq2 2343  eqabb 2370
[Quine] p. 35	Theorem 5.2	abid1 2368  abid2 2357  abid2f 2412
[Quine] p. 40	Theorem 6.1	sb5 1938
[Quine] p. 40	Theorem 6.2	sb56 1936  sb6 1937
[Quine] p. 41	Theorem 6.3	df-clel 2230
[Quine] p. 41	Theorem 6.4	eqid 2234
[Quine] p. 41	Theorem 6.5	eqcom 2236
[Quine] p. 42	Theorem 6.6	df-sbc 3046
[Quine] p. 42	Theorem 6.7	dfsbcq 3047  dfsbcq2 3048
[Quine] p. 43	Theorem 6.8	vex 2818
[Quine] p. 43	Theorem 6.9	isset 2822
[Quine] p. 44	Theorem 7.3	spcgf 2901  spcgv 2906  spcimgf 2899
[Quine] p. 44	Theorem 6.11	spsbc 3057  spsbcd 3058
[Quine] p. 44	Theorem 6.12	elex 2827
[Quine] p. 44	Theorem 6.13	elab 2964  elabg 2966  elabgf 2962
[Quine] p. 44	Theorem 6.14	noel 3516
[Quine] p. 48	Theorem 7.2	snprc 3759
[Quine] p. 48	Definition 7.1	df-pr 3701  df-sn 3700
[Quine] p. 49	Theorem 7.4	snss 3834  snssg 3833
[Quine] p. 49	Theorem 7.5	prss 3855  prssg 3856
[Quine] p. 49	Theorem 7.6	prid1 3802  prid1g 3800  prid2 3803  prid2g 3801  snid 3725  snidg 3723
[Quine] p. 51	Theorem 7.12	snexg 4302  snexprc 4304
[Quine] p. 51	Theorem 7.13	prexg 4330
[Quine] p. 53	Theorem 8.2	unisn 3935  unisng 3936
[Quine] p. 53	Theorem 8.3	uniun 3938
[Quine] p. 54	Theorem 8.6	elssuni 3947
[Quine] p. 54	Theorem 8.7	uni0 3946
[Quine] p. 56	Theorem 8.17	uniabio 5328
[Quine] p. 56	Definition 8.18	dfiota2 5318
[Quine] p. 57	Theorem 8.19	iotaval 5329
[Quine] p. 57	Theorem 8.22	iotanul 5333
[Quine] p. 58	Theorem 8.23	euiotaex 5334
[Quine] p. 58	Definition 9.1	df-op 3703
[Quine] p. 61	Theorem 9.5	opabid 4379  opabidw 4380  opelopab 4395  opelopaba 4389  opelopabaf 4397  opelopabf 4398  opelopabg 4391  opelopabga 4386  opelopabgf 4393  oprabid 6090
[Quine] p. 64	Definition 9.11	df-xp 4760
[Quine] p. 64	Definition 9.12	df-cnv 4762
[Quine] p. 64	Definition 9.15	df-id 4419
[Quine] p. 65	Theorem 10.3	fun0 5419
[Quine] p. 65	Theorem 10.4	funi 5389
[Quine] p. 65	Theorem 10.5	funsn 5409  funsng 5407
[Quine] p. 65	Definition 10.1	df-fun 5359
[Quine] p. 65	Definition 10.2	args 5136  dffv4g 5672
[Quine] p. 68	Definition 10.11	df-fv 5365  fv2 5670
[Quine] p. 124	Theorem 17.3	nn0opth2 11111  nn0opth2d 11110  nn0opthd 11109
[Quine] p. 284	Axiom 39(vi)	funimaex 5446  funimaexg 5445
[Roman] p. 18	Part Preliminaries	df-rng 14172
[Roman] p. 19	Part Preliminaries	df-ring 14241
[Rudin] p. 164	Equation 27	efcan 12387
[Rudin] p. 164	Equation 30	efzval 12394
[Rudin] p. 167	Equation 48	absefi 12480
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1471
[Sanford] p. 39	Rule 4	mptxor 1469
[Sanford] p. 40	Rule 1	mptnan 1468
[Schechter] p. 51	Definition of antisymmetry	intasym 5152
[Schechter] p. 51	Definition of irreflexivity	intirr 5154
[Schechter] p. 51	Definition of symmetry	cnvsym 5151
[Schechter] p. 51	Definition of transitivity	cotr 5149
[Schechter] p. 187	Definition of "ring with unit"	isring 14243
[Schechter] p. 428	Definition 15.35	bastop1 15074
[Stoll] p. 13	Definition of symmetric difference	symdif1 3490
[Stoll] p. 16	Exercise 4.4	0dif 3584  dif0 3583
[Stoll] p. 16	Exercise 4.8	difdifdirss 3598
[Stoll] p. 19	Theorem 5.2(13)	undm 3483
[Stoll] p. 19	Theorem 5.2(13')	indmss 3484
[Stoll] p. 20	Remark	invdif 3467
[Stoll] p. 25	Definition of ordered triple	df-ot 3704
[Stoll] p. 43	Definition	uniiun 4050
[Stoll] p. 44	Definition	intiin 4051
[Stoll] p. 45	Definition	df-iin 3999
[Stoll] p. 45	Definition indexed union	df-iun 3998
[Stoll] p. 176	Theorem 3.4(27)	imandc 897  imanst 896
[Stoll] p. 262	Example 4.1	symdif1 3490
[Suppes] p. 22	Theorem 2	eq0 3531
[Suppes] p. 22	Theorem 4	eqss 3257  eqssd 3259  eqssi 3258
[Suppes] p. 23	Theorem 5	ss0 3553  ss0b 3552
[Suppes] p. 23	Theorem 6	sstr 3250
[Suppes] p. 25	Theorem 12	elin 3406  elun 3364
[Suppes] p. 26	Theorem 15	inidm 3434
[Suppes] p. 26	Theorem 16	in0 3547
[Suppes] p. 27	Theorem 23	unidm 3366
[Suppes] p. 27	Theorem 24	un0 3546
[Suppes] p. 27	Theorem 25	ssun1 3386
[Suppes] p. 27	Theorem 26	ssequn1 3393
[Suppes] p. 27	Theorem 27	unss 3397
[Suppes] p. 27	Theorem 28	indir 3474
[Suppes] p. 27	Theorem 29	undir 3475
[Suppes] p. 28	Theorem 32	difid 3581  difidALT 3582
[Suppes] p. 29	Theorem 33	difin 3462
[Suppes] p. 29	Theorem 34	indif 3468
[Suppes] p. 29	Theorem 35	undif1ss 3588
[Suppes] p. 29	Theorem 36	difun2 3593
[Suppes] p. 29	Theorem 37	difin0 3587
[Suppes] p. 29	Theorem 38	disjdif 3585
[Suppes] p. 29	Theorem 39	difundi 3477
[Suppes] p. 29	Theorem 40	difindiss 3479
[Suppes] p. 30	Theorem 41	nalset 4245
[Suppes] p. 39	Theorem 61	uniss 3940
[Suppes] p. 39	Theorem 65	uniop 4377
[Suppes] p. 41	Theorem 70	intsn 3989
[Suppes] p. 42	Theorem 71	intpr 3986  intprg 3987
[Suppes] p. 42	Theorem 73	op1stb 4604  op1stbg 4605
[Suppes] p. 42	Theorem 78	intun 3985
[Suppes] p. 44	Definition 15(a)	dfiun2 4030  dfiun2g 4028
[Suppes] p. 44	Definition 15(b)	dfiin2 4031
[Suppes] p. 47	Theorem 86	elpw 3680  elpw2 4274  elpw2g 4273  elpwg 3682
[Suppes] p. 47	Theorem 87	pwid 3692
[Suppes] p. 47	Theorem 89	pw0 3846
[Suppes] p. 48	Theorem 90	pwpw0ss 3914
[Suppes] p. 52	Theorem 101	xpss12 4862
[Suppes] p. 52	Theorem 102	xpindi 4895  xpindir 4896
[Suppes] p. 52	Theorem 103	xpundi 4811  xpundir 4812
[Suppes] p. 54	Theorem 105	elirrv 4675
[Suppes] p. 58	Theorem 2	relss 4842
[Suppes] p. 59	Theorem 4	eldm 4958  eldm2 4959  eldm2g 4957  eldmg 4956
[Suppes] p. 59	Definition 3	df-dm 4764
[Suppes] p. 60	Theorem 6	dmin 4969
[Suppes] p. 60	Theorem 8	rnun 5176
[Suppes] p. 60	Theorem 9	rnin 5177
[Suppes] p. 60	Definition 4	dfrn2 4948
[Suppes] p. 61	Theorem 11	brcnv 4943  brcnvg 4941
[Suppes] p. 62	Equation 5	elcnv 4937  elcnv2 4938
[Suppes] p. 62	Theorem 12	relcnv 5145
[Suppes] p. 62	Theorem 15	cnvin 5175
[Suppes] p. 62	Theorem 16	cnvun 5173
[Suppes] p. 63	Theorem 20	co02 5281
[Suppes] p. 63	Theorem 21	dmcoss 5032
[Suppes] p. 63	Definition 7	df-co 4763
[Suppes] p. 64	Theorem 26	cnvco 4945
[Suppes] p. 64	Theorem 27	coass 5286
[Suppes] p. 65	Theorem 31	resundi 5056
[Suppes] p. 65	Theorem 34	elima 5111  elima2 5112  elima3 5113  elimag 5110
[Suppes] p. 65	Theorem 35	imaundi 5180
[Suppes] p. 66	Theorem 40	dminss 5182
[Suppes] p. 66	Theorem 41	imainss 5183
[Suppes] p. 67	Exercise 11	cnvxp 5186
[Suppes] p. 81	Definition 34	dfec2 6783
[Suppes] p. 82	Theorem 72	elec 6821  elecg 6820
[Suppes] p. 82	Theorem 73	erth 6826  erth2 6827
[Suppes] p. 89	Theorem 96	map0b 6934
[Suppes] p. 89	Theorem 97	map0 6937  map0g 6935
[Suppes] p. 89	Theorem 98	mapsn 6938  mapsnd 6936
[Suppes] p. 89	Theorem 99	mapss 6939
[Suppes] p. 92	Theorem 1	enref 7017  enrefg 7016
[Suppes] p. 92	Theorem 2	ensym 7034  ensymb 7033  ensymi 7035
[Suppes] p. 92	Theorem 3	entr 7037
[Suppes] p. 92	Theorem 4	unen 7071
[Suppes] p. 94	Theorem 15	endom 7015
[Suppes] p. 94	Theorem 16	ssdomg 7031
[Suppes] p. 94	Theorem 17	domtr 7038
[Suppes] p. 95	Theorem 18	isbth 7250
[Suppes] p. 98	Exercise 4	fundmen 7060  fundmeng 7061
[Suppes] p. 98	Exercise 6	xpdom3m 7098
[Suppes] p. 130	Definition 3	df-tr 4214
[Suppes] p. 132	Theorem 9	ssonuni 4615
[Suppes] p. 134	Definition 6	df-suc 4497
[Suppes] p. 136	Theorem Schema 22	findes 4730  finds 4727  finds1 4729  finds2 4728
[Suppes] p. 162	Definition 5	df-ltnqqs 7684  df-ltpq 7677
[Suppes] p. 228	Theorem Schema 61	onintss 4516
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2216
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2227
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2230
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2229
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2252
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 6062
[TakeutiZaring] p. 14	Proposition 4.14	ru 3044
[TakeutiZaring] p. 15	Exercise 1	elpr 3715  elpr2 3716  elprg 3714
[TakeutiZaring] p. 15	Exercise 2	elsn 3710  elsn2 3728  elsn2g 3727  elsng 3709  velsn 3711
[TakeutiZaring] p. 15	Exercise 3	elop 4352
[TakeutiZaring] p. 15	Exercise 4	sneq 3705  sneqr 3869
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3713  dfsn2 3708
[TakeutiZaring] p. 16	Axiom 3	uniex 4563
[TakeutiZaring] p. 16	Exercise 6	opth 4358
[TakeutiZaring] p. 16	Exercise 8	rext 4336
[TakeutiZaring] p. 16	Corollary 5.8	unex 4567  unexg 4569
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3743
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3920
[TakeutiZaring] p. 16	Definition 5.6	df-in 3220  df-un 3218
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3933  uniprg 3934
[TakeutiZaring] p. 17	Axiom 4	vpwex 4297
[TakeutiZaring] p. 17	Exercise 1	eltp 3742
[TakeutiZaring] p. 17	Exercise 5	elsuc 4532  elsucg 4530  sstr2 3249
[TakeutiZaring] p. 17	Exercise 6	uncom 3367
[TakeutiZaring] p. 17	Exercise 7	incom 3415
[TakeutiZaring] p. 17	Exercise 8	unass 3380
[TakeutiZaring] p. 17	Exercise 9	inass 3435
[TakeutiZaring] p. 17	Exercise 10	indi 3472
[TakeutiZaring] p. 17	Exercise 11	undi 3473
[TakeutiZaring] p. 17	Definition 5.9	ssalel 3229
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3676
[TakeutiZaring] p. 18	Exercise 7	unss2 3394
[TakeutiZaring] p. 18	Exercise 9	df-ss 3227  dfss2 3231  sseqin2 3444
[TakeutiZaring] p. 18	Exercise 10	ssid 3262
[TakeutiZaring] p. 18	Exercise 12	inss1 3445  inss2 3446
[TakeutiZaring] p. 18	Exercise 13	nssr 3302
[TakeutiZaring] p. 18	Exercise 15	unieq 3928
[TakeutiZaring] p. 18	Exercise 18	sspwb 4337
[TakeutiZaring] p. 18	Exercise 19	pweqb 4344
[TakeutiZaring] p. 20	Definition	df-rab 2531
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4242
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3216
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3514
[TakeutiZaring] p. 20	Proposition 5.15	difid 3581  difidALT 3582
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3525
[TakeutiZaring] p. 21	Theorem 5.22	setind 4666
[TakeutiZaring] p. 21	Definition 5.20	df-v 2817
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4247
[TakeutiZaring] p. 22	Exercise 1	0ss 3551
[TakeutiZaring] p. 22	Exercise 3	ssex 4252  ssexg 4254
[TakeutiZaring] p. 22	Exercise 4	inex1 4249
[TakeutiZaring] p. 22	Exercise 5	ruv 4677
[TakeutiZaring] p. 22	Exercise 6	elirr 4668
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3577
[TakeutiZaring] p. 22	Exercise 11	difdif 3348
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3486
[TakeutiZaring] p. 22	Exercise 14	difss 3349
[TakeutiZaring] p. 22	Exercise 15	sscon 3357
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2527
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2528
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4871  xpexg 4869  xpexgALT 6339
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4761
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5425
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5589  fun11 5428
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5368  svrelfun 5426
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4947
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4949
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4766
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4767
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4763
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5222  dfrel2 5218
[TakeutiZaring] p. 25	Exercise 3	xpss 4863
[TakeutiZaring] p. 25	Exercise 5	relun 4874
[TakeutiZaring] p. 25	Exercise 6	reluni 4880
[TakeutiZaring] p. 25	Exercise 9	inxp 4894
[TakeutiZaring] p. 25	Exercise 12	relres 5071
[TakeutiZaring] p. 25	Exercise 13	opelres 5048  opelresg 5050
[TakeutiZaring] p. 25	Exercise 14	dmres 5064
[TakeutiZaring] p. 25	Exercise 15	resss 5067
[TakeutiZaring] p. 25	Exercise 17	resabs1 5072
[TakeutiZaring] p. 25	Exercise 18	funres 5398
[TakeutiZaring] p. 25	Exercise 24	relco 5266
[TakeutiZaring] p. 25	Exercise 29	funco 5397
[TakeutiZaring] p. 25	Exercise 30	f1co 5590
[TakeutiZaring] p. 26	Definition 6.10	eu2 2127
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5365  fv3 5698
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5306  cnvexg 5305
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 5029  dmexg 5026
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 5030  rnexg 5027
[TakeutiZaring] p. 26	Corollary 6.9(2)	xpexcnvm 5122
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5692
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5702  tz6.12 5703  tz6.12c 5705
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5666
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5360
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5361
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5363  wfo 5355
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5362  wf1 5354
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5364  wf1o 5356
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5780  eqfnfv2 5781  eqfnfv2f 5784
[TakeutiZaring] p. 28	Exercise 5	fvco 5752
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5911  fnexALT 6313
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5910  resfunexgALT 6310
[TakeutiZaring] p. 29	Exercise 9	funimaex 5446  funimaexg 5445
[TakeutiZaring] p. 29	Definition 6.18	df-br 4115
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5137  iniseg 5139
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4415
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5366
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5989
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5990
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5995
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5997
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 6005
[TakeutiZaring] p. 35	Notation	wtr 4213
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4480
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4217
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4703
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4507
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4511
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4619
[TakeutiZaring] p. 38	Definition 7.11	df-on 4494
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4613
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4679
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4709
[TakeutiZaring] p. 40	Exercise 7	dftr2 4215
[TakeutiZaring] p. 40	Exercise 11	unon 4638
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4614
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3947
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4497
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4541  sucidg 4542
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4628
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4495
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4633  ordelsuc 4632
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4721
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4722
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4723
[TakeutiZaring] p. 43	Axiom 7	omex 4720
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4734
[TakeutiZaring] p. 43	Corollary 7.31	find 4726
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4724
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4725
[TakeutiZaring] p. 44	Exercise 2	int0 3968
[TakeutiZaring] p. 44	Exercise 3	trintssm 4229
[TakeutiZaring] p. 44	Exercise 4	intss1 3969
[TakeutiZaring] p. 44	Exercise 6	onintonm 4644
[TakeutiZaring] p. 44	Definition 7.35	df-int 3955
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6552
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6609  tfri1d 6579
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6610  tfri2d 6580
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6611
[TakeutiZaring] p. 50	Exercise 3	smoiso 6546
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6530
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6710
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6706
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6703
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6707
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6755  nnaordi 6754
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 4041  uniss2 3950
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6716
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6726
[TakeutiZaring] p. 62	Exercise 5	oaword1 6717
[TakeutiZaring] p. 62	Definition 8.15	om0 6704  omsuc 6718
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6727
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6763  nnmordi 6762
[TakeutiZaring] p. 67	Definition 8.30	oei0 6705
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7496
[TakeutiZaring] p. 88	Exercise 1	en0 7048
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 7124
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 7125
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6991  isfi 7013
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 7095
[TakeutiZaring] p. 95	Definition 10.42	df-map 6897
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 7101
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 7114
[Tarski] p. 67	Axiom B5	ax-4 1559
[Tarski] p. 68	Lemma 6	equid 1749
[Tarski] p. 69	Lemma 7	equcomi 1752
[Tarski] p. 70	Lemma 14	spim 1787  spime 1790  spimeh 1788  spimh 1786
[Tarski] p. 70	Lemma 16	ax-11 1555  ax-11o 1872  ax11i 1762
[Tarski] p. 70	Lemmas 16 and 17	sb6 1937
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1575
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2207  ax-14 2208
[WhiteheadRussell] p. 96	Axiom *1.3	olc 719
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 735
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 764
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 773
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 797
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 621
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 648
[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 845
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2181  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 745
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 844
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 634
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 893
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 851
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 864
[WhiteheadRussell] p. 103	Theorem *2.16	con3 647
[WhiteheadRussell] p. 103	Theorem *2.17	condc 861
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 863
[WhiteheadRussell] p. 104	Theorem *2.2	orc 720
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 783
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 622
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 626
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 901
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 915
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 776
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 777
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 812
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 813
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 811
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 1006
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 786
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 784
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 785
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 746
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 747
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 875  pm2.5gdc 874
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 870
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 748
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 749
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 750
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 661
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 662
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 730
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 899
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 733
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 734
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 873
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 756
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 808
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 809
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 665
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 721  pm2.67 751
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 877  pm2.521gdc 876
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 755
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 818
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 902
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 923
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 814
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 815
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 817
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 816
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 819
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 820
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 913
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 762
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 966
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 967
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 968
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 761
[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 701
[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 868
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 867
[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 696
[WhiteheadRussell] p. 113	Fact)	pm3.45 601
[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 763  pm3.44 723
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 344
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 606
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 793
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 879
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 880
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 898
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 702
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 961  bitr 472
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 395
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 765  pm4.25 766
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 826
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 736
[WhiteheadRussell] p. 118	Theorem *4.32	anass 401
[WhiteheadRussell] p. 118	Theorem *4.33	orass 775
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 466
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 800
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 609
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 830
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 1007
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 824
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 980
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 958
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 787
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 822  pm4.45 792  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1530
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 965
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 905  imorr 729
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 907
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 758
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 759
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 910
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 947
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 760  pm4.56 788
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 948  oranim 789
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 693
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 906
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 894
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 908
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 694
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 909
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 895
[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 835
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 752
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 607  pm4.76 608
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 718  pm4.77 807
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 790
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 911
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 715
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 916
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 959
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 960
[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 559
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 605
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 917
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 918
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 920
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 919
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1434
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 836
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 912
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1439  pm5.18dc 891
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 714
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 703
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1437
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1442
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1443
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 903
[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 934  pm5.6r 935
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 963
[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 613
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 925
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 614
[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 933
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 810
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 926
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 921
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 802
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 954
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 955
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 970
[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 971
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1684
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1534
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1681
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1947
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2085
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2495
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2496
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2958
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3102
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5337
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5338
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2162  eupickbi 2165
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5365
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7500
[vandenDries] p. 43	Theorem 62	pellexlem1 15971