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 7462  fidcenum 7279
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 7279
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 7462
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 13375
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 7244
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 7230
[AczelRathjen], p. 74	Theorem 8.1.19	ctiunct 13390
[AczelRathjen], p. 75	Corollary 8.1.20	unct 13392
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 13381  znnen 13348
[AczelRathjen], p. 77	Lemma 8.1.27	omctfn 13393
[AczelRathjen], p. 78	Theorem 8.1.28	omiunct 13394
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 11238
[AczelRathjen], p. 183	Chapter 20	ax-setind 4686
[AhoHopUll] p. 318	Section 9.1	df-concat 11382  df-pfx 11468  df-substr 11441  df-word 11328  lencl 11331  wrd0 11352
[Apostol] p. 18	Theorem I.1	addcan 8514  addcan2d 8519  addcan2i 8517  addcand 8518  addcani 8516
[Apostol] p. 18	Theorem I.2	negeu 8525
[Apostol] p. 18	Theorem I.3	negsub 8582  negsubd 8651  negsubi 8612
[Apostol] p. 18	Theorem I.4	negneg 8584  negnegd 8636  negnegi 8604
[Apostol] p. 18	Theorem I.5	subdi 8720  subdid 8749  subdii 8742  subdir 8721  subdird 8750  subdiri 8743
[Apostol] p. 18	Theorem I.6	mul01 8724  mul01d 8728  mul01i 8726  mul02 8722  mul02d 8727  mul02i 8725
[Apostol] p. 18	Theorem I.9	divrecapd 9132
[Apostol] p. 18	Theorem I.10	recrecapi 9083
[Apostol] p. 18	Theorem I.12	mul2neg 8733  mul2negd 8748  mul2negi 8741  mulneg1 8730  mulneg1d 8746  mulneg1i 8739
[Apostol] p. 18	Theorem I.14	rdivmuldivd 14561
[Apostol] p. 18	Theorem I.15	divdivdivap 9052
[Apostol] p. 20	Axiom 7	rpaddcl 10096  rpaddcld 10131  rpmulcl 10097  rpmulcld 10132
[Apostol] p. 20	Axiom 9	0nrp 10108
[Apostol] p. 20	Theorem I.17	lttri 8438
[Apostol] p. 20	Theorem I.18	ltadd1d 8874  ltadd1dd 8892  ltadd1i 8838
[Apostol] p. 20	Theorem I.19	ltmul1 8929  ltmul1a 8928  ltmul1i 9259  ltmul1ii 9267  ltmul2 9195  ltmul2d 10158  ltmul2dd 10172  ltmul2i 9262
[Apostol] p. 20	Theorem I.21	0lt1 8461
[Apostol] p. 20	Theorem I.23	lt0neg1 8804  lt0neg1d 8851  ltneg 8798  ltnegd 8859  ltnegi 8829
[Apostol] p. 20	Theorem I.25	lt2add 8781  lt2addd 8904  lt2addi 8846
[Apostol] p. 20	Definition of positive numbers	df-rp 10073
[Apostol] p. 21	Exercise 4	recgt0 9189  recgt0d 9273  recgt0i 9245  recgt0ii 9246
[Apostol] p. 22	Definition of integers	df-z 9657
[Apostol] p. 22	Definition of rationals	df-q 10037
[Apostol] p. 24	Theorem I.26	supeuti 7341
[Apostol] p. 26	Theorem I.29	arch 9572
[Apostol] p. 28	Exercise 2	btwnz 9777
[Apostol] p. 28	Exercise 3	nnrecl 9573
[Apostol] p. 28	Exercise 6	qbtwnre 10709
[Apostol] p. 28	Exercise 10(a)	zeneo 12664  zneo 9759
[Apostol] p. 29	Theorem I.35	resqrtth 11820  sqrtthi 11909
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 9317
[Apostol] p. 34	Theorem I.37 (well-ordering principle)	nnwodc 12839
[Apostol] p. 363	Remark	absgt0api 11936
[Apostol] p. 363	Example	abssubd 11983  abssubi 11940
[ApostolNT] p. 8	Definition	df-ppi 16249
[ApostolNT] p. 14	Definition	df-dvds 12581
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 12597
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 12621
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 12617
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 12611
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 12613
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 12598
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 12599
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 12604
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 12638
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 12640
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 12642
[ApostolNT] p. 15	Definition	dfgcd2 12817
[ApostolNT] p. 16	Definition	isprm2 12921
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 12896
[ApostolNT] p. 16	Theorem 1.7	prminf 13405
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 12776
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 12818
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 12820
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 12790
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 12783
[ApostolNT] p. 17	Theorem 1.8	coprm 12949
[ApostolNT] p. 17	Theorem 1.9	euclemma 12951
[ApostolNT] p. 17	Theorem 1.10	1arith2 13177
[ApostolNT] p. 19	Theorem 1.14	divalg 12717
[ApostolNT] p. 20	Theorem 1.15	eucalg 12863
[ApostolNT] p. 25	Definition	df-phi 13019
[ApostolNT] p. 26	Theorem 2.2	phisum 13049
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 13030
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 13034
[ApostolNT] p. 38	Remark	df-sgm 16250
[ApostolNT] p. 38	Definition	df-sgm 16250
[ApostolNT] p. 75	Definition	df-cht 16248
[ApostolNT] p. 104	Definition	congr 12904
[ApostolNT] p. 106	Remark	dvdsval3 12584
[ApostolNT] p. 106	Definition	moddvds 12592
[ApostolNT] p. 107	Example 2	mod2eq0even 12671
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 12672
[ApostolNT] p. 107	Example 4	zmod1congr 10800
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10837
[ApostolNT] p. 107	Theorem 5.2(c)	modqexp 11126
[ApostolNT] p. 108	Theorem 5.3	modmulconst 12616
[ApostolNT] p. 109	Theorem 5.4	cncongr1 12907
[ApostolNT] p. 109	Theorem 5.6	gcdmodi 13231
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 12909
[ApostolNT] p. 113	Theorem 5.17	eulerth 13041
[ApostolNT] p. 113	Theorem 5.18	vfermltl 13060
[ApostolNT] p. 114	Theorem 5.19	fermltl 13042
[ApostolNT] p. 179	Definition	df-lgs 16334  lgsprme0 16378
[ApostolNT] p. 180	Example 1	1lgs 16379
[ApostolNT] p. 180	Theorem 9.2	lgsvalmod 16355
[ApostolNT] p. 180	Theorem 9.3	lgsdirprm 16370
[ApostolNT] p. 181	Theorem 9.4	m1lgs 16421
[ApostolNT] p. 181	Theorem 9.5	2lgs 16440  2lgsoddprm 16449
[ApostolNT] p. 182	Theorem 9.6	gausslemma2d 16405
[ApostolNT] p. 185	Theorem 9.8	lgsquad 16416
[ApostolNT] p. 188	Definition	df-lgs 16334  lgs1 16380
[ApostolNT] p. 188	Theorem 9.9(a)	lgsdir 16371
[ApostolNT] p. 188	Theorem 9.9(b)	lgsdi 16373
[ApostolNT] p. 188	Theorem 9.9(c)	lgsmodeq 16381
[ApostolNT] p. 188	Theorem 9.9(d)	lgsmulsqcoprm 16382
[Bauer] p. 482	Section 1.2	pm2.01 625  pm2.65 669
[Bauer] p. 483	Theorem 1.3	acexmid 6087  onsucelsucexmidlem 4678
[Bauer], p. 481	Section 1.1	pwtrufal 17244
[Bauer], p. 483	Definition	n0rf 3534
[Bauer], p. 483	Theorem 1.2	2irrexpq 16224  2irrexpqap 16226
[Bauer], p. 485	Theorem 2.1	exmidssfi 7251  ssfiexmid 7183  ssfiexmidt 7185
[Bauer], p. 493	Section 5.1	ivthdich 15891
[Bauer], p. 494	Theorem 5.5	ivthinc 15881
[BauerHanson], p. 27	Proposition 5.2	cnstab 8982
[BauerSwan], p. 3	Definition on page 14:3	enumct 7462
[BauerSwan], p. 14	Remark	0ct 7454  ctm 7456
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 17247
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7875
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7788
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7877
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7911  addlocpr 7910
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7937
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7940
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7945
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2089
[BellMachover] p. 460	Notation	df-mo 2090
[BellMachover] p. 460	Definition	mo3 2141  mo3h 2140
[BellMachover] p. 462	Theorem 1.1	bm1.1 2223
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4256
[BellMachover] p. 466	Axiom Pow	axpow3 4316
[BellMachover] p. 466	Axiom Union	axun2 4582
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4691
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4531
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4694
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4645
[BellMachover] p. 471	Definition of Lim	df-ilim 4516
[BellMachover] p. 472	Axiom Inf	zfinf2 4738
[BellMachover] p. 473	Theorem 2.8	limom 4763
[Bobzien] p. 116	Statement T3	stoic3 1480
[Bobzien] p. 117	Statement T2	stoic2a 1478
[Bobzien] p. 117	Statement T4	stoic4a 1481
[Bobzien] p. 117	Conclusion the contradictory	stoic1a 1476
[Bollobas] p. 1	Section I.1	df-edg 16516  isuhgropm 16539  isusgropen 16623  isuspgropen 16622
[Bollobas] p. 2	Section I.1	df-subgr 16712  uhgrspansubgr 16735
[Bollobas] p. 4	Definition	df-wlks 16776
[Bollobas] p. 5	Definition	df-trls 16839
[Bollobas] p. 7	Section I.1	df-ushgrm 16528
[BourbakiAlg1] p. 1	Definition 1	df-mgm 13736
[BourbakiAlg1] p. 4	Definition 5	df-sgrp 13777
[BourbakiAlg1] p. 12	Definition 2	df-mnd 13790
[BourbakiAlg1] p. 92	Definition 1	df-ring 14410
[BourbakiAlg1] p. 93	Section I.8.1	df-rng 14340
[BourbakiEns] p.	Proposition 8	fcof1 5992  fcofo 5993
[BourbakiTop1] p.	Remark	xnegmnf 10249  xnegpnf 10248
[BourbakiTop1] p.	Remark	rexneg 10250
[BourbakiTop1] p.	Proposition	ishmeo 15542
[BourbakiTop1] p.	Property V_i	ssnei2 15395
[BourbakiTop1] p.	Property V_ii	innei 15401
[BourbakiTop1] p.	Property V_iv	neissex 15403
[BourbakiTop1] p.	Proposition 1	neipsm 15392  neiss 15388
[BourbakiTop1] p.	Proposition 2	cnptopco 15460
[BourbakiTop1] p.	Proposition 4	imasnopn 15537
[BourbakiTop1] p.	Property V_iii	elnei 15390
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 15236
[Bruck] p. 1	Section I.1	df-mgm 13736
[Bruck] p. 23	Section II.1	df-sgrp 13777
[Bruck] p. 28	Theorem 3.2	dfgrp3m 13964
[ChoquetDD] p. 2	Definition of mapping	df-mpt 4195
[Church] p. 129	Section II.24	df-ifp 991  dfifp2dc 994
[Cohen] p. 301	Remark	relogoprlem 16110
[Cohen] p. 301	Property 2	relogmul 16111  relogmuld 16126
[Cohen] p. 301	Property 3	relogdiv 16112  relogdivd 16127
[Cohen] p. 301	Property 4	relogexp 16114
[Cohen] p. 301	Property 1a	log1 16107
[Cohen] p. 301	Property 1b	loge 16108
[Cohen4] p. 348	Observation	relogbcxpbap 16213
[Cohen4] p. 352	Definition	rpelogb 16197
[Cohen4] p. 361	Property 2	rprelogbmul 16203
[Cohen4] p. 361	Property 3	logbrec 16208  rprelogbdiv 16205
[Cohen4] p. 361	Property 4	rplogbreexp 16201
[Cohen4] p. 361	Property 6	relogbexpap 16206
[Cohen4] p. 361	Property 1(a)	rplogbid1 16195
[Cohen4] p. 361	Property 1(b)	rplogb1 16196
[Cohen4] p. 367	Property	rplogbchbase 16198
[Cohen4] p. 377	Property 2	logblt 16210
[Crosilla] p.	Axiom 1	ax-ext 2220
[Crosilla] p.	Axiom 2	ax-pr 4348
[Crosilla] p.	Axiom 3	ax-un 4580
[Crosilla] p.	Axiom 4	ax-nul 4261
[Crosilla] p.	Axiom 5	ax-iinf 4737
[Crosilla] p.	Axiom 6	ru 3050
[Crosilla] p.	Axiom 8	ax-pow 4313
[Crosilla] p.	Axiom 9	ax-setind 4686
[Crosilla], p.	Axiom 6	ax-sep 4251
[Crosilla], p.	Axiom 7	ax-coll 4248
[Crosilla], p.	Axiom 7'	repizf 4249
[Crosilla], p.	Theorem is stated	ordtriexmid 4670
[Crosilla], p.	Axiom of choice implies instances	acexmid 6087
[Crosilla], p.	Definition of ordinal	df-iord 4513
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4684
[Diestel] p. 4	Section 1.1	df-subgr 16712  uhgrspansubgr 16735
[Diestel] p. 27	Section 1.10	df-ushgrm 16528
[Eisenberg] p. 67	Definition 5.3	df-dif 3222
[Eisenberg] p. 82	Definition 6.3	df-iom 4740
[Eisenberg] p. 125	Definition 8.21	df-map 6928
[Enderton] p. 18	Axiom of Empty Set	axnul 4260
[Enderton] p. 19	Definition	df-tp 3717
[Enderton] p. 26	Exercise 5	unissb 3965
[Enderton] p. 26	Exercise 10	pwel 4360
[Enderton] p. 28	Exercise 7(b)	pwunim 4433
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 4082  iinin2m 4081  iunin1 4077  iunin2 4076
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 4080  iundif2ss 4078
[Enderton] p. 33	Exercise 23	iinuniss 4095
[Enderton] p. 33	Exercise 25	iununir 4096
[Enderton] p. 33	Exercise 24(a)	iinpw 4103
[Enderton] p. 33	Exercise 24(b)	iunpw 4628  iunpwss 4104
[Enderton] p. 38	Exercise 6(a)	unipw 4359
[Enderton] p. 38	Exercise 6(b)	pwuni 4331
[Enderton] p. 41	Lemma 3D	opeluu 4598  rnex 5052  rnexg 5049
[Enderton] p. 41	Exercise 8	dmuni 4993  rnuni 5202
[Enderton] p. 42	Definition of a function	dffun7 5407  dffun8 5408
[Enderton] p. 43	Definition of function value	funfvdm2 5770
[Enderton] p. 43	Definition of single-rooted	funcnv 5445
[Enderton] p. 44	Definition (d)	dfima2 5131  dfima3 5132
[Enderton] p. 47	Theorem 3H	fvco2 5777
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7569
[Enderton] p. 50	Theorem 3K(a)	imauni 5970
[Enderton] p. 52	Definition	df-map 6928
[Enderton] p. 53	Exercise 21	coass 5309
[Enderton] p. 53	Exercise 27	dmco 5299
[Enderton] p. 53	Exercise 14(a)	funin 5455
[Enderton] p. 53	Exercise 22(a)	imass2 5166
[Enderton] p. 54	Remark	ixpf 7007  ixpssmap 7019
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6986
[Enderton] p. 56	Theorem 3M	erref 6831
[Enderton] p. 57	Lemma 3N	erthi 6859
[Enderton] p. 57	Definition	df-ec 6813
[Enderton] p. 58	Definition	df-qs 6817
[Enderton] p. 60	Theorem 3Q	th3q 6918  th3qcor 6917  th3qlem1 6915  th3qlem2 6916
[Enderton] p. 61	Exercise 35	df-ec 6813
[Enderton] p. 65	Exercise 56(a)	dmun 4990
[Enderton] p. 68	Definition of successor	df-suc 4518
[Enderton] p. 71	Definition	df-tr 4232  dftr4 4236
[Enderton] p. 72	Theorem 4E	unisuc 4560  unisucg 4561
[Enderton] p. 73	Exercise 6	unisuc 4560  unisucg 4561
[Enderton] p. 73	Exercise 5(a)	truni 4245
[Enderton] p. 73	Exercise 5(b)	trint 4246
[Enderton] p. 79	Theorem 4I(A1)	nna0 6751
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6753  onasuc 6743
[Enderton] p. 79	Definition of operation value	df-ov 6091
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6752
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6754  onmsuc 6750
[Enderton] p. 81	Theorem 4K(1)	nnaass 6762
[Enderton] p. 81	Theorem 4K(2)	nna0r 6755  nnacom 6761
[Enderton] p. 81	Theorem 4K(3)	nndi 6763
[Enderton] p. 81	Theorem 4K(4)	nnmass 6764
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6766
[Enderton] p. 82	Exercise 16	nnm0r 6756  nnmsucr 6765
[Enderton] p. 88	Exercise 23	nnaordex 6805
[Enderton] p. 129	Definition	df-en 7028
[Enderton] p. 132	Theorem 6B(b)	canth 6039
[Enderton] p. 133	Exercise 1	xpomen 13345
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 7172
[Enderton] p. 136	Corollary 6E	nneneq 7163
[Enderton] p. 139	Theorem 6H(c)	mapen 7151
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7581
[Enderton] p. 143	Theorem 6J	dju0en 7577  dju1en 7576
[Enderton] p. 144	Corollary 6K	undif2ss 3603
[Enderton] p. 145	Figure 38	ffoss 5675
[Enderton] p. 145	Definition	df-dom 7029
[Enderton] p. 146	Example 1	domen 7040  domeng 7041
[Enderton] p. 146	Example 3	nndomo 7170
[Enderton] p. 149	Theorem 6L(c)	xpdom1 7138  xpdom1g 7136  xpdom2g 7135
[Enderton] p. 168	Definition	df-po 4443
[Enderton] p. 192	Theorem 7M(a)	oneli 4575
[Enderton] p. 192	Theorem 7M(b)	ontr1 4536
[Enderton] p. 192	Theorem 7M(c)	onirri 4692
[Enderton] p. 193	Corollary 7N(b)	0elon 4539
[Enderton] p. 193	Corollary 7N(c)	onsuci 4665
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4638
[Enderton] p. 194	Remark	onprc 4701
[Enderton] p. 194	Exercise 16	suc11 4707
[Enderton] p. 197	Definition	df-card 7531
[Enderton] p. 200	Exercise 25	tfis 4732
[Enderton] p. 206	Theorem 7X(b)	en2lp 4703
[Enderton] p. 207	Exercise 34	opthreg 4705
[Enderton] p. 208	Exercise 35	suc11g 4706
[Geuvers], p. 1	Remark	expap0 11028
[Geuvers], p. 6	Lemma 2.13	mulap0r 8952
[Geuvers], p. 6	Lemma 2.15	mulap0 8991
[Geuvers], p. 9	Lemma 2.35	msqge0 8953
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 8305
[Geuvers], p. 10	Lemma 3.9	maxcom 11993
[Geuvers], p. 10	Lemma 3.10	maxle1 12001  maxle2 12002
[Geuvers], p. 10	Lemma 3.11	maxleast 12003
[Geuvers], p. 10	Lemma 3.12	maxleb 12006
[Geuvers], p. 11	Definition 3.13	dfabsmax 12007
[Geuvers], p. 17	Definition 6.1	df-ap 8919
[Gleason] p. 117	Proposition 9-2.1	df-enq 7721  enqer 7732
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7725  df-nqqs 7722
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7718  df-plqqs 7723
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7719  df-mqqs 7724
[Gleason] p. 119	Proposition 9-2.5	df-rq 7726
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7782
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7785  ltbtwnnq 7790  ltbtwnnqq 7789
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7774
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7775
[Gleason] p. 123	Proposition 9-3.5	addclpr 7911
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7953
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7952
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7971
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7987
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7993  ltaprlem 7992
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7990
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7946
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7966
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7955
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7954
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7962
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 8012
[Gleason] p. 126	Proposition 9-4.1	df-enr 8100  enrer 8109
[Gleason] p. 126	Proposition 9-4.2	df-0r 8105  df-1r 8106  df-nr 8101
[Gleason] p. 126	Proposition 9-4.3	df-mr 8103  df-plr 8102  negexsr 8146  recexsrlem 8148
[Gleason] p. 127	Proposition 9-4.4	df-ltr 8104
[Gleason] p. 130	Proposition 10-1.3	creui 9299  creur 9298  cru 8939
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 8297  axcnre 8255
[Gleason] p. 132	Definition 10-3.1	crim 11646  crimd 11766  crimi 11726  crre 11645  crred 11765  crrei 11725
[Gleason] p. 132	Definition 10-3.2	remim 11648  remimd 11731
[Gleason] p. 133	Definition 10.36	absval2 11846  absval2d 11975  absval2i 11934
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 11672  cjaddd 11754  cjaddi 11721
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 11673  cjmuld 11755  cjmuli 11722
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 11671  cjcjd 11732  cjcji 11704
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 11670  cjreb 11654  cjrebd 11735  cjrebi 11707  cjred 11760  rere 11653  rereb 11651  rerebd 11734  rerebi 11706  rered 11758
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 11679  addcjd 11746  addcji 11716
[Gleason] p. 133	Proposition 10-3.7(a)	absval 11790
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 11841  abscjd 11980  abscji 11938
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 11853  abs00d 11976  abs00i 11935  absne0d 11977
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 11886  releabsd 11981  releabsi 11939
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 11858  absmuld 11984  absmuli 11941
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 11844  sqabsaddi 11942
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 11894  abstrid 11986  abstrii 11945
[Gleason] p. 134	Definition 10-4.1	df-exp 10998  exp0 11002  expp1 11005  expp1d 11134
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 11040  expaddd 11135
[Gleason] p. 135	Proposition 10-4.2(b)	cxpmul 16157  cxpmuld 16184  expmul 11043  expmuld 11136
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 11037  mulexpd 11148  rpmulcxp 16154
[Gleason] p. 141	Definition 11-2.1	fzval 10431
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 12118
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 12120
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 12119
[Gleason] p. 171	Corollary 12-2.2	climmulc2 12123
[Gleason] p. 172	Corollary 12-2.5	climrecl 12116
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 12112  climcj 12113  climim 12115  climre 12114
[Gleason] p. 173	Definition 12-3.1	df-ltxr 8372  df-xr 8371  ltxr 10195
[Gleason] p. 180	Theorem 12-5.3	climcau 12139
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10757
[Gleason] p. 223	Definition 14-1.1	df-met 14992
[Gleason] p. 223	Definition 14-1.1(a)	met0 15602  xmet0 15601
[Gleason] p. 223	Definition 14-1.1(c)	metsym 15609
[Gleason] p. 223	Definition 14-1.1(d)	mettri 15611  mstri 15711  xmettri 15610  xmstri 15710
[Gleason] p. 230	Proposition 14-2.6	txlm 15517
[Gleason] p. 240	Proposition 14-4.2	metcnp3 15749
[Gleason] p. 243	Proposition 14-4.16	addcn2 12102  addcncntop 15800  mulcn2 12104  mulcncntop 15802  subcn2 12103  subcncntop 15801
[Gleason] p. 295	Remark	bcval3 11212  bcval4 11213
[Gleason] p. 295	Equation 2	bcpasc 11227
[Gleason] p. 295	Definition of binomial coefficient	bcval 11210  df-bc 11209
[Gleason] p. 296	Remark	bcn0 11216  bcnn 11218
[Gleason] p. 296	Theorem 15-2.8	binom 12277
[Gleason] p. 308	Equation 2	ef0 12465
[Gleason] p. 308	Equation 3	efcj 12466
[Gleason] p. 309	Corollary 15-4.3	efne0 12471
[Gleason] p. 309	Corollary 15-4.4	efexp 12475
[Gleason] p. 310	Equation 14	sinadd 12529
[Gleason] p. 310	Equation 15	cosadd 12530
[Gleason] p. 311	Equation 17	sincossq 12541
[Gleason] p. 311	Equation 18	cosbnd 12546  sinbnd 12545
[Gleason] p. 311	Definition of ` `	df-pi 12446
[Golan] p. 1	Remark	srgisid 14398
[Golan] p. 1	Definition	df-srg 14376
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1502
[Herstein] p. 55	Lemma 2.2.1(a)	grpideu 13876  mndideu 13799
[Herstein] p. 55	Lemma 2.2.1(b)	grpinveu 13903
[Herstein] p. 55	Lemma 2.2.1(c)	grpinvinv 13932
[Herstein] p. 55	Lemma 2.2.1(d)	grpinvadd 13943
[Herstein] p. 57	Exercise 1	dfgrp3me 13965
[Heyting] p. 127	Axiom #1	ax1hfs 17343
[Hitchcock] p. 5	Rule A3	mptnan 1472
[Hitchcock] p. 5	Rule A4	mptxor 1473
[Hitchcock] p. 5	Rule A5	mtpxor 1475
[HoTT], p.	Lemma 10.4.1	exmidontriim 7588
[HoTT], p.	Theorem 7.2.6	nndceq 6776
[HoTT], p.	Exercise 11.10	neapmkv 17337
[HoTT], p.	Exercise 11.11	mulap0bd 8994
[HoTT], p.	Section 11.2.1	df-iltp 7844  df-imp 7843  df-iplp 7842  df-reap 8912
[HoTT], p.	Theorem 11.2.4	recapb 9010  rerecapb 9182
[HoTT], p.	Corollary 3.9.2	uchoice 6375
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 8036
[HoTT], p.	Corollary 11.4.3	conventions 16952
[HoTT], p.	Exercise 11.6(i)	dcapnconst 17330  dceqnconst 17329
[HoTT], p.	Corollary 11.2.13	axcaucvg 8274  caucvgpr 8056  caucvgprpr 8086  caucvgsr 8176
[HoTT], p.	Definition 11.2.1	df-inp 7840
[HoTT], p.	Exercise 11.6(ii)	nconstwlpo 17335
[HoTT], p.	Proposition 11.2.3	df-iso 4444  ltpopr 7969  ltsopr 7970
[HoTT], p.	Definition 11.2.7(v)	apsym 8943  reapcotr 8935  reapirr 8914
[HoTT], p.	Definition 11.2.7(vi)	0lt1 8461  gt0add 8910  leadd1 8766  lelttr 8421  lemul1a 9197  lenlt 8408  ltadd1 8765  ltletr 8422  ltmul1 8929  reaplt 8925
[Huneke] p. 2	Statement	df-clwwlknon 16885
[Jech] p. 4	Definition of class	cv 1401  cvjust 2233
[Jech] p. 78	Note	opthprc 4828
[KalishMontague] p. 81	Note 1	ax-i9 1583
[Kreyszig] p. 3	Property M1	metcl 15591  xmetcl 15590
[Kreyszig] p. 4	Property M2	meteq0 15598
[Kreyszig] p. 12	Equation 5	muleqadd 9007
[Kreyszig] p. 18	Definition 1.3-2	mopnval 15680
[Kreyszig] p. 19	Remark	mopntopon 15681
[Kreyszig] p. 19	Theorem T1	mopn0 15726  mopnm 15686
[Kreyszig] p. 19	Theorem T2	unimopn 15724
[Kreyszig] p. 19	Definition of neighborhood	neibl 15729
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 15751
[Kreyszig] p. 25	Definition 1.4-1	lmbr 15451
[Kreyszig] p. 51	Equation 2	lmodvneg1 14777
[Kreyszig] p. 51	Equation 1a	lmod0vs 14768
[Kreyszig] p. 51	Equation 1b	lmodvs0 14769
[Kunen] p. 10	Axiom 0	a9e 1748
[Kunen] p. 12	Axiom 6	zfrep6 4250
[Kunen] p. 24	Definition 10.24	mapval 6938  mapvalg 6936
[Kunen] p. 31	Definition 10.24	mapex 6932
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 4022
[Lang] p. 3	Statement	lidrideqd 13761  mndbn0 13804
[Lang] p. 3	Definition	df-mnd 13790
[Lang] p. 4	Definition of a (finite) product	gzsumsplit1r 13775
[Lang] p. 5	Equation	gzsumreidx 14232
[Lang] p. 6	Definition	mulgnn0gzsum 13991
[Lang] p. 7	Definition	dfgrp2e 13893
[Lang2] p. 3	Notations	df-ind 9304
[Levy] p. 338	Axiom	df-clab 2225  df-clel 2234  df-cleq 2231
[Lopez-Astorga] p. 12	Rule 1	mptnan 1472
[Lopez-Astorga] p. 12	Rule 2	mptxor 1473
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1475
[Margaris] p. 40	Rule C	exlimiv 1651
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 865
[Margaris] p. 49	Definition	dfbi2 392  dfordc 904  exalim 1555
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	jcn 661
[Margaris] p. 89	Theorem 19.2	19.2 1691  r19.2m 3614
[Margaris] p. 89	Theorem 19.3	19.3 1607  19.3h 1606  rr19.3v 2965
[Margaris] p. 89	Theorem 19.5	alcom 1531
[Margaris] p. 89	Theorem 19.6	alexdc 1672  alexim 1698
[Margaris] p. 89	Theorem 19.7	alnex 1552
[Margaris] p. 89	Theorem 19.8	19.8a 1643  spsbe 1895
[Margaris] p. 89	Theorem 19.9	19.9 1697  19.9h 1696  19.9v 1924  exlimd 1650
[Margaris] p. 89	Theorem 19.11	excom 1716  excomim 1715
[Margaris] p. 89	Theorem 19.12	19.12 1717  r19.12 2657
[Margaris] p. 90	Theorem 19.14	exnalim 1699
[Margaris] p. 90	Theorem 19.15	albi 1521  ralbi 2683
[Margaris] p. 90	Theorem 19.16	19.16 1608
[Margaris] p. 90	Theorem 19.17	19.17 1609
[Margaris] p. 90	Theorem 19.18	exbi 1657  rexbi 2684
[Margaris] p. 90	Theorem 19.19	19.19 1718
[Margaris] p. 90	Theorem 19.20	alim 1510  alimd 1574  alimdh 1520  alimdv 1932  ralimdaa 2616  ralimdv 2618  ralimdva 2617  ralimdvva 2619  sbcimdv 3117
[Margaris] p. 90	Theorem 19.21	19.21-2 1719  19.21 1636  19.21bi 1611  19.21h 1610  19.21ht 1634  19.21t 1635  19.21v 1926  alrimd 1663  alrimdd 1662  alrimdh 1532  alrimdv 1929  alrimi 1575  alrimih 1522  alrimiv 1927  alrimivv 1928  r19.21 2626  r19.21be 2641  r19.21bi 2638  r19.21t 2625  r19.21v 2627  ralrimd 2628  ralrimdv 2629  ralrimdva 2630  ralrimdvv 2634  ralrimdvva 2635  ralrimi 2621  ralrimiv 2622  ralrimiva 2623  ralrimivv 2631  ralrimivva 2632  ralrimivvva 2633  ralrimivw 2624  rexlimi 2661
[Margaris] p. 90	Theorem 19.22	2alimdv 1934  2eximdv 1935  exim 1652  eximd 1665  eximdh 1664  eximdv 1933  rexim 2644  reximdai 2648  reximddv 2653  reximddv2 2655  reximdv 2651  reximdv2 2649  reximdva 2652  reximdvai 2650  reximi2 2646
[Margaris] p. 90	Theorem 19.23	19.23 1730  19.23bi 1645  19.23h 1551  19.23ht 1550  19.23t 1729  19.23v 1936  19.23vv 1937  exlimd2 1648  exlimdh 1649  exlimdv 1872  exlimdvv 1953  exlimi 1647  exlimih 1646  exlimiv 1651  exlimivv 1952  r19.23 2659  r19.23v 2660  rexlimd 2665  rexlimdv 2667  rexlimdv3a 2670  rexlimdva 2668  rexlimdva2 2671  rexlimdvaa 2669  rexlimdvv 2675  rexlimdvva 2676  rexlimdvw 2672  rexlimiv 2662  rexlimiva 2663  rexlimivv 2674
[Margaris] p. 90	Theorem 19.24	i19.24 1692
[Margaris] p. 90	Theorem 19.25	19.25 1679
[Margaris] p. 90	Theorem 19.26	19.26-2 1535  19.26-3an 1536  19.26 1534  r19.26-2 2680  r19.26-3 2681  r19.26 2677  r19.26m 2682
[Margaris] p. 90	Theorem 19.27	19.27 1614  19.27h 1613  19.27v 1955  r19.27av 2686  r19.27m 3623  r19.27mv 3624
[Margaris] p. 90	Theorem 19.28	19.28 1616  19.28h 1615  19.28v 1956  r19.28av 2687  r19.28m 3617  r19.28mv 3620  rr19.28v 2966
[Margaris] p. 90	Theorem 19.29	19.29 1673  19.29r 1674  19.29r2 1675  19.29x 1676  r19.29 2688  r19.29d2r 2695  r19.29r 2689
[Margaris] p. 90	Theorem 19.30	19.30dc 1680
[Margaris] p. 90	Theorem 19.31	19.31r 1733
[Margaris] p. 90	Theorem 19.32	19.32dc 1731  19.32r 1732  r19.32r 2697  r19.32vdc 2700  r19.32vr 2699
[Margaris] p. 90	Theorem 19.33	19.33 1537  19.33b2 1682  19.33bdc 1683
[Margaris] p. 90	Theorem 19.34	19.34 1736
[Margaris] p. 90	Theorem 19.35	19.35-1 1677  19.35i 1678
[Margaris] p. 90	Theorem 19.36	19.36-1 1725  19.36aiv 1957  19.36i 1724  r19.36av 2702
[Margaris] p. 90	Theorem 19.37	19.37-1 1726  19.37aiv 1727  r19.37 2703  r19.37av 2704
[Margaris] p. 90	Theorem 19.38	19.38 1728
[Margaris] p. 90	Theorem 19.39	i19.39 1693
[Margaris] p. 90	Theorem 19.40	19.40-2 1685  19.40 1684  r19.40 2705
[Margaris] p. 90	Theorem 19.41	19.41 1738  19.41h 1737  19.41v 1958  19.41vv 1959  19.41vvv 1960  19.41vvvv 1961  r19.41 2706  r19.41v 2707
[Margaris] p. 90	Theorem 19.42	19.42 1740  19.42h 1739  19.42v 1962  19.42vv 1967  19.42vvv 1968  19.42vvvv 1969  r19.42v 2708
[Margaris] p. 90	Theorem 19.43	19.43 1681  r19.43 2709
[Margaris] p. 90	Theorem 19.44	19.44 1734  r19.44av 2710  r19.44mv 3622
[Margaris] p. 90	Theorem 19.45	19.45 1735  r19.45av 2711  r19.45mv 3621
[Margaris] p. 110	Exercise 2(b)	eu1 2111
[Megill] p. 444	Axiom C5	ax-17 1579
[Megill] p. 445	Lemma L12	alequcom 1568  ax-10 1558
[Megill] p. 446	Lemma L17	equtrr 1762
[Megill] p. 446	Lemma L19	hbnae 1773
[Megill] p. 447	Remark 9.1	df-sb 1816  sbid 1827
[Megill] p. 448	Scheme C5'	ax-4 1563
[Megill] p. 448	Scheme C6'	ax-7 1501
[Megill] p. 448	Scheme C8'	ax-8 1557
[Megill] p. 448	Scheme C9'	ax-i12 1560
[Megill] p. 448	Scheme C11'	ax-10o 1768
[Megill] p. 448	Scheme C12'	ax-13 2211
[Megill] p. 448	Scheme C13'	ax-14 2212
[Megill] p. 448	Scheme C15'	ax-11o 1876
[Megill] p. 448	Scheme C16'	ax-16 1867
[Megill] p. 448	Theorem 9.4	dral1 1783  dral2 1784  drex1 1851  drex2 1785  drsb1 1852  drsb2 1894
[Megill] p. 449	Theorem 9.7	sbcom2 2047  sbequ 1893  sbid2v 2056
[Megill] p. 450	Example in Appendix	hba1 1593
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3135  rspsbca 3136  stdpc4 1828
[Mendelson] p. 69	Axiom 5	ra5 3141  stdpc5 1637
[Mendelson] p. 81	Rule C	exlimiv 1651
[Mendelson] p. 95	Axiom 6	stdpc6 1755
[Mendelson] p. 95	Axiom 7	stdpc7 1823
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3559
[Mendelson] p. 231	Exercise 4.10(l)	unv 3560
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3471
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3521
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3472
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3360
[Mendelson] p. 231	Definition of union	unssin 3470
[Mendelson] p. 235	Exercise 4.12(c)	univ 4624
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3934
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4429
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4430
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4431
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3955
[Mendelson] p. 235	Exercise 4.12(p)	reli 4911
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5311
[Mendelson] p. 246	Definition of successor	df-suc 4518
[Mendelson] p. 254	Proposition 4.22(b)	xpen 7150
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 7124  xpsneng 7125
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 7130  xpcomeng 7131
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 7133
[Mendelson] p. 255	Exercise 4.39	endisj 7127
[Mendelson] p. 255	Exercise 4.41	mapprc 6930
[Mendelson] p. 255	Exercise 4.43	mapsnen 7105  mapsnend 7104
[Mendelson] p. 255	Exercise 4.45	mapunen 7156
[Mendelson] p. 255	Exercise 4.47	xpmapen 7155
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6971
[Mendelson] p. 255	Exercise 4.42(b)	map1 7106
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7580  djucomen 7579
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7578
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6744
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3453
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4865
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4866
[Monk1] p. 34	Definition 3.3	df-opab 4194
[Monk1] p. 36	Theorem 3.7(i)	coi1 5306  coi2 5307
[Monk1] p. 36	Theorem 3.8(v)	dm0 4997  rn0 5040
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5195
[Monk1] p. 37	Theorem 3.13(i)	relxp 4886
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 5004  rnxpm 5220
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4857  xp0 5210
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5149
[Monk1] p. 38	Theorem 3.16(viii)	imai 5146
[Monk1] p. 39	Theorem 3.17	imaex 5144  imaexg 5143
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5140
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5841  funfvop 5824
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5747
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5757
[Monk1] p. 43	Theorem 4.6	funun 5425
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5977  dff13f 5979
[Monk1] p. 46	Theorem 4.15(v)	funex 5943  funrnex 6347
[Monk1] p. 50	Definition 5.4	fniunfv 5971
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5274
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3986
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6393  df-1st 6378
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6394  df-2nd 6379
[Monk2] p. 105	Axiom C4	ax-5 1500
[Monk2] p. 105	Axiom C7	ax-8 1557
[Monk2] p. 105	Axiom C8	ax-11 1559  ax-11o 1876
[Monk2] p. 105	Axiom (C8)	ax11v 1880
[Monk2] p. 109	Lemma 12	ax-7 1501
[Monk2] p. 109	Lemma 15	equvin 1916  equvini 1811  eqvinop 4385
[Monk2] p. 113	Axiom C5-1	ax-17 1579
[Monk2] p. 113	Axiom C5-2	hbn1 1704
[Monk2] p. 113	Axiom C5-3	ax-7 1501
[Monk2] p. 114	Lemma 22	hba1 1593
[Monk2] p. 114	Lemma 23	hbia1 1605  nfia1 1633
[Monk2] p. 114	Lemma 24	hba2 1604  nfa2 1632
[Moschovakis] p. 2	Chapter 2	df-stab 843  dftest 17344
[Munkres] p. 77	Example 2	distop 15323
[Munkres] p. 78	Definition of basis	df-bases 15281  isbasis3g 15284
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 13674  tgval2 15289
[Munkres] p. 79	Remark	tgcl 15302
[Munkres] p. 80	Lemma 2.1	tgval3 15296
[Munkres] p. 80	Lemma 2.2	tgss2 15317  tgss3 15316
[Munkres] p. 81	Lemma 2.3	basgen 15318  basgen2 15319
[Munkres] p. 89	Definition of subspace topology	resttop 15408
[Munkres] p. 93	Theorem 6.1(1)	0cld 15350  topcld 15347
[Munkres] p. 93	Theorem 6.1(3)	uncld 15351
[Munkres] p. 94	Definition of closure	clsval 15349
[Munkres] p. 94	Definition of interior	ntrval 15348
[Munkres] p. 102	Definition of continuous function	df-cn 15426  iscn 15435  iscn2 15438
[Munkres] p. 107	Theorem 7.2(g)	cncnp 15468  cncnp2m 15469  cncnpi 15466  df-cnp 15427  iscnp 15437
[Munkres] p. 127	Theorem 10.1	metcn 15752
[Pierik], p. 8	Section 2.2.1	dfrex2fin 7213
[Pierik], p. 9	Definition 2.4	df-womni 7511
[Pierik], p. 9	Definition 2.5	df-markov 7499  omniwomnimkv 7514
[Pierik], p. 10	Section 2.3	dfdif3 3339
[Pierik], p. 14	Definition 3.1	df-omni 7482  exmidomniim 7488  finomni 7487
[Pierik], p. 15	Section 3.1	df-nninf 7467
[Pradic2025], p. 2	Section 1.1	nnnninfen 17282
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 17286
[PradicBrown2022], p. 2	Remark	exmidpw 7220
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7560
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7561  exmidfodomrlemrALT 7562
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7496
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 17268  peano4nninf 17267
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 17270
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 17278
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 17280
[PradicBrown2022], p. 5	Definition 3.3	nnsf 17266
[Quine] p. 16	Definition 2.1	df-clab 2225  rabid 2727
[Quine] p. 17	Definition 2.1''	dfsb7 2051
[Quine] p. 18	Definition 2.7	df-cleq 2231
[Quine] p. 19	Definition 2.9	df-v 2823
[Quine] p. 34	Theorem 5.1	abeq2 2347  eqabb 2374
[Quine] p. 35	Theorem 5.2	abid1 2372  abid2 2361  abid2f 2418
[Quine] p. 40	Theorem 6.1	sb5 1942
[Quine] p. 40	Theorem 6.2	sb56 1940  sb6 1941
[Quine] p. 41	Theorem 6.3	df-clel 2234
[Quine] p. 41	Theorem 6.4	eqid 2238
[Quine] p. 41	Theorem 6.5	eqcom 2240
[Quine] p. 42	Theorem 6.6	df-sbc 3052
[Quine] p. 42	Theorem 6.7	dfsbcq 3053  dfsbcq2 3054
[Quine] p. 43	Theorem 6.8	vex 2824
[Quine] p. 43	Theorem 6.9	isset 2828
[Quine] p. 44	Theorem 7.3	spcgf 2907  spcgv 2912  spcimgf 2905
[Quine] p. 44	Theorem 6.11	spsbc 3063  spsbcd 3064
[Quine] p. 44	Theorem 6.12	elex 2833
[Quine] p. 44	Theorem 6.13	elab 2970  elabg 2972  elabgf 2968
[Quine] p. 44	Theorem 6.14	noel 3525
[Quine] p. 48	Theorem 7.2	snprc 3774
[Quine] p. 48	Definition 7.1	df-pr 3716  df-sn 3715
[Quine] p. 49	Theorem 7.4	snss 3850  snssg 3849
[Quine] p. 49	Theorem 7.5	prss 3871  prssg 3872
[Quine] p. 49	Theorem 7.6	prid1 3817  prid1g 3815  prid2 3818  prid2g 3816  snid 3740  snidg 3738
[Quine] p. 51	Theorem 7.12	snexg 4323  snexprc 4325
[Quine] p. 51	Theorem 7.13	prexg 4351
[Quine] p. 53	Theorem 8.2	unisn 3951  unisng 3952
[Quine] p. 53	Theorem 8.3	uniun 3954
[Quine] p. 54	Theorem 8.6	elssuni 3963
[Quine] p. 54	Theorem 8.7	uni0 3962
[Quine] p. 56	Theorem 8.17	uniabio 5351
[Quine] p. 56	Definition 8.18	dfiota2 5341
[Quine] p. 57	Theorem 8.19	iotaval 5352
[Quine] p. 57	Theorem 8.22	iotanul 5356
[Quine] p. 58	Theorem 8.23	euiotaex 5357
[Quine] p. 58	Definition 9.1	df-op 3718
[Quine] p. 61	Theorem 9.5	opabid 4400  opabidw 4401  opelopab 4416  opelopaba 4410  opelopabaf 4418  opelopabf 4419  opelopabg 4412  opelopabga 4407  opelopabgf 4414  oprabid 6120
[Quine] p. 64	Definition 9.11	df-xp 4782
[Quine] p. 64	Definition 9.12	df-cnv 4784
[Quine] p. 64	Definition 9.15	df-id 4440
[Quine] p. 65	Theorem 10.3	fun0 5442
[Quine] p. 65	Theorem 10.4	funi 5412
[Quine] p. 65	Theorem 10.5	funsn 5432  funsng 5430
[Quine] p. 65	Definition 10.1	df-fun 5382
[Quine] p. 65	Definition 10.2	args 5159  dffv4g 5695
[Quine] p. 68	Definition 10.11	df-fv 5388  fv2 5693
[Quine] p. 124	Theorem 17.3	nn0opth2 11185  nn0opth2d 11184  nn0opthd 11183
[Quine] p. 284	Axiom 39(vi)	funimaex 5469  funimaexg 5468
[Roman] p. 18	Part Preliminaries	df-rng 14340
[Roman] p. 19	Part Preliminaries	df-ring 14410
[Rudin] p. 164	Equation 27	efcan 12469
[Rudin] p. 164	Equation 30	efzval 12476
[Rudin] p. 167	Equation 48	absefi 12562
[Russell1905] p. 482	Example of "the father	dfalseu2 17396
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1475
[Sanford] p. 39	Rule 4	mptxor 1473
[Sanford] p. 40	Rule 1	mptnan 1472
[Schechter] p. 51	Definition of antisymmetry	intasym 5175
[Schechter] p. 51	Definition of irreflexivity	intirr 5177
[Schechter] p. 51	Definition of symmetry	cnvsym 5174
[Schechter] p. 51	Definition of transitivity	cotr 5172
[Schechter] p. 187	Definition of "ring with unit"	isring 14412
[Schechter] p. 428	Definition 15.35	bastop1 15321
[Stoll] p. 13	Definition of symmetric difference	symdif1 3496
[Stoll] p. 16	Exercise 4.4	0dif 3597  dif0 3596
[Stoll] p. 16	Exercise 4.8	difdifdirss 3612
[Stoll] p. 19	Theorem 5.2(13)	undm 3489
[Stoll] p. 19	Theorem 5.2(13')	indmss 3490
[Stoll] p. 20	Remark	invdif 3473
[Stoll] p. 25	Definition of ordered triple	df-ot 3719
[Stoll] p. 43	Definition	uniiun 4066
[Stoll] p. 44	Definition	intiin 4067
[Stoll] p. 45	Definition	df-iin 4015
[Stoll] p. 45	Definition indexed union	df-iun 4014
[Stoll] p. 176	Theorem 3.4(27)	imandc 901  imanst 900
[Stoll] p. 262	Example 4.1	symdif1 3496
[Suppes] p. 22	Theorem 2	eq0 3540
[Suppes] p. 22	Theorem 4	eqss 3263  eqssd 3265  eqssi 3264
[Suppes] p. 23	Theorem 5	ss0 3563  ss0b 3562
[Suppes] p. 23	Theorem 6	sstr 3256
[Suppes] p. 25	Theorem 12	elin 3412  elun 3370
[Suppes] p. 26	Theorem 15	inidm 3440
[Suppes] p. 26	Theorem 16	in0 3557
[Suppes] p. 27	Theorem 23	unidm 3372
[Suppes] p. 27	Theorem 24	un0 3556
[Suppes] p. 27	Theorem 25	ssun1 3392
[Suppes] p. 27	Theorem 26	ssequn1 3399
[Suppes] p. 27	Theorem 27	unss 3403
[Suppes] p. 27	Theorem 28	indir 3480
[Suppes] p. 27	Theorem 29	undir 3481
[Suppes] p. 28	Theorem 32	difid 3594  difidALT 3595
[Suppes] p. 29	Theorem 33	difin 3468
[Suppes] p. 29	Theorem 34	indif 3474
[Suppes] p. 29	Theorem 35	undif1ss 3602
[Suppes] p. 29	Theorem 36	difun2 3607
[Suppes] p. 29	Theorem 37	difin0 3601
[Suppes] p. 29	Theorem 38	disjdif 3599
[Suppes] p. 29	Theorem 39	difundi 3483
[Suppes] p. 29	Theorem 40	difindiss 3485
[Suppes] p. 30	Theorem 41	nalset 4265
[Suppes] p. 39	Theorem 61	uniss 3956
[Suppes] p. 39	Theorem 65	uniop 4398
[Suppes] p. 41	Theorem 70	intsn 4005
[Suppes] p. 42	Theorem 71	intpr 4002  intprg 4003
[Suppes] p. 42	Theorem 73	op1stb 4626  op1stbg 4627
[Suppes] p. 42	Theorem 78	intun 4001
[Suppes] p. 44	Definition 15(a)	dfiun2 4046  dfiun2g 4044
[Suppes] p. 44	Definition 15(b)	dfiin2 4047
[Suppes] p. 47	Theorem 86	elpw 3694  elpw2 4295  elpw2g 4294  elpwg 3696
[Suppes] p. 47	Theorem 87	pwid 3707
[Suppes] p. 47	Theorem 89	pw0 3862
[Suppes] p. 48	Theorem 90	pwpw0ss 3930
[Suppes] p. 52	Theorem 101	xpss12 4884
[Suppes] p. 52	Theorem 102	xpindi 4917  xpindir 4918
[Suppes] p. 52	Theorem 103	xpundi 4833  xpundir 4834
[Suppes] p. 54	Theorem 105	elirrv 4697
[Suppes] p. 58	Theorem 2	relss 4864
[Suppes] p. 59	Theorem 4	eldm 4980  eldm2 4981  eldm2g 4979  eldmg 4978
[Suppes] p. 59	Definition 3	df-dm 4786
[Suppes] p. 60	Theorem 6	dmin 4991
[Suppes] p. 60	Theorem 8	rnun 5199
[Suppes] p. 60	Theorem 9	rnin 5200
[Suppes] p. 60	Definition 4	dfrn2 4970
[Suppes] p. 61	Theorem 11	brcnv 4965  brcnvg 4963
[Suppes] p. 62	Equation 5	elcnv 4959  elcnv2 4960
[Suppes] p. 62	Theorem 12	relcnv 5168
[Suppes] p. 62	Theorem 15	cnvin 5198
[Suppes] p. 62	Theorem 16	cnvun 5196
[Suppes] p. 63	Theorem 20	co02 5304
[Suppes] p. 63	Theorem 21	dmcoss 5054
[Suppes] p. 63	Definition 7	df-co 4785
[Suppes] p. 64	Theorem 26	cnvco 4967
[Suppes] p. 64	Theorem 27	coass 5309
[Suppes] p. 65	Theorem 31	resundi 5078
[Suppes] p. 65	Theorem 34	elima 5134  elima2 5135  elima3 5136  elimag 5133
[Suppes] p. 65	Theorem 35	imaundi 5203
[Suppes] p. 66	Theorem 40	dminss 5205
[Suppes] p. 66	Theorem 41	imainss 5206
[Suppes] p. 67	Exercise 11	cnvxp 5209
[Suppes] p. 81	Definition 34	dfec2 6814
[Suppes] p. 82	Theorem 72	elec 6852  elecg 6851
[Suppes] p. 82	Theorem 73	erth 6857  erth2 6858
[Suppes] p. 89	Theorem 96	map0b 6972
[Suppes] p. 89	Theorem 97	map0 6976  map0g 6973
[Suppes] p. 89	Theorem 98	mapsn 6977  mapsnd 6975
[Suppes] p. 89	Theorem 99	mapss 6978
[Suppes] p. 92	Theorem 1	enref 7056  enrefg 7055
[Suppes] p. 92	Theorem 2	ensym 7073  ensymb 7072  ensymi 7074
[Suppes] p. 92	Theorem 3	entr 7076
[Suppes] p. 92	Theorem 4	unen 7110
[Suppes] p. 94	Theorem 15	endom 7054
[Suppes] p. 94	Theorem 16	ssdomg 7070
[Suppes] p. 94	Theorem 17	domtr 7077
[Suppes] p. 95	Theorem 18	isbth 7290
[Suppes] p. 98	Exercise 4	fundmen 7099  fundmeng 7100
[Suppes] p. 98	Exercise 6	xpdom3m 7137
[Suppes] p. 130	Definition 3	df-tr 4232
[Suppes] p. 132	Theorem 9	ssonuni 4637
[Suppes] p. 134	Definition 6	df-suc 4518
[Suppes] p. 136	Theorem Schema 22	findes 4752  finds 4749  finds1 4751  finds2 4750
[Suppes] p. 162	Definition 5	df-ltnqqs 7727  df-ltpq 7720
[Suppes] p. 228	Theorem Schema 61	onintss 4537
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2220
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2231
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2234
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2233
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2256
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 6092
[TakeutiZaring] p. 14	Proposition 4.14	ru 3050
[TakeutiZaring] p. 15	Exercise 1	elpr 3730  elpr2 3731  elprg 3729
[TakeutiZaring] p. 15	Exercise 2	elsn 3725  elsn2 3743  elsn2g 3742  elsng 3724  velsn 3726
[TakeutiZaring] p. 15	Exercise 3	elop 4373
[TakeutiZaring] p. 15	Exercise 4	sneq 3720  sneqr 3885
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3728  dfsn2 3723
[TakeutiZaring] p. 16	Axiom 3	uniex 4585
[TakeutiZaring] p. 16	Exercise 6	opth 4379
[TakeutiZaring] p. 16	Exercise 8	rext 4357
[TakeutiZaring] p. 16	Corollary 5.8	unex 4589  unexg 4591
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3758
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3936
[TakeutiZaring] p. 16	Definition 5.6	df-in 3226  df-un 3224
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3949  uniprg 3950
[TakeutiZaring] p. 17	Axiom 4	vpwex 4318
[TakeutiZaring] p. 17	Exercise 1	eltp 3757
[TakeutiZaring] p. 17	Exercise 5	elsuc 4553  elsucg 4551  sstr2 3255
[TakeutiZaring] p. 17	Exercise 6	uncom 3373
[TakeutiZaring] p. 17	Exercise 7	incom 3421
[TakeutiZaring] p. 17	Exercise 8	unass 3386
[TakeutiZaring] p. 17	Exercise 9	inass 3441
[TakeutiZaring] p. 17	Exercise 10	indi 3478
[TakeutiZaring] p. 17	Exercise 11	undi 3479
[TakeutiZaring] p. 17	Definition 5.9	ssalel 3235
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3690
[TakeutiZaring] p. 18	Exercise 7	unss2 3400
[TakeutiZaring] p. 18	Exercise 9	df-ss 3233  dfss2 3237  sseqin2 3450
[TakeutiZaring] p. 18	Exercise 10	ssid 3268
[TakeutiZaring] p. 18	Exercise 12	inss1 3451  inss2 3452
[TakeutiZaring] p. 18	Exercise 13	nssr 3308
[TakeutiZaring] p. 18	Exercise 15	unieq 3944
[TakeutiZaring] p. 18	Exercise 18	sspwb 4358
[TakeutiZaring] p. 18	Exercise 19	pweqb 4365
[TakeutiZaring] p. 20	Definition	df-rab 2537
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4262
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3222
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3523
[TakeutiZaring] p. 20	Proposition 5.15	difid 3594  difidALT 3595
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3534
[TakeutiZaring] p. 21	Theorem 5.22	setind 4688
[TakeutiZaring] p. 21	Definition 5.20	df-v 2823
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4267
[TakeutiZaring] p. 22	Exercise 1	0ss 3561
[TakeutiZaring] p. 22	Exercise 3	ssex 4272  ssexg 4274
[TakeutiZaring] p. 22	Exercise 4	inex1 4269
[TakeutiZaring] p. 22	Exercise 5	ruv 4699
[TakeutiZaring] p. 22	Exercise 6	elirr 4690
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3589
[TakeutiZaring] p. 22	Exercise 11	difdif 3354
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3492
[TakeutiZaring] p. 22	Exercise 14	difss 3355
[TakeutiZaring] p. 22	Exercise 15	sscon 3363
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2533
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2534
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4893  xpexg 4891  xpexgALT 6370
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4783
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5448
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5612  fun11 5451
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5391  svrelfun 5449
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4969
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4971
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4788
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4789
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4785
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 5245  dfrel2 5241
[TakeutiZaring] p. 25	Exercise 3	xpss 4885
[TakeutiZaring] p. 25	Exercise 5	relun 4896
[TakeutiZaring] p. 25	Exercise 6	reluni 4902
[TakeutiZaring] p. 25	Exercise 9	inxp 4916
[TakeutiZaring] p. 25	Exercise 12	relres 5093
[TakeutiZaring] p. 25	Exercise 13	opelres 5070  opelresg 5072
[TakeutiZaring] p. 25	Exercise 14	dmres 5086
[TakeutiZaring] p. 25	Exercise 15	resss 5089
[TakeutiZaring] p. 25	Exercise 17	resabs1 5094
[TakeutiZaring] p. 25	Exercise 18	funres 5421
[TakeutiZaring] p. 25	Exercise 24	relco 5289
[TakeutiZaring] p. 25	Exercise 29	funco 5420
[TakeutiZaring] p. 25	Exercise 30	f1co 5613
[TakeutiZaring] p. 26	Definition 6.10	eu2 2131
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5388  fv3 5721
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5329  cnvexg 5328
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 5051  dmexg 5048
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 5052  rnexg 5049
[TakeutiZaring] p. 26	Corollary 6.9(2)	xpexcnvm 5145
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5715
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5725  tz6.12 5726  tz6.12c 5728
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5689
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5383
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5384
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5386  wfo 5378
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5385  wf1 5377
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5387  wf1o 5379
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5809  eqfnfv2 5810  eqfnfv2f 5813
[TakeutiZaring] p. 28	Exercise 5	fvco 5778
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5940  fnexALT 6344
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5939  resfunexgALT 6341
[TakeutiZaring] p. 29	Exercise 9	funimaex 5469  funimaexg 5468
[TakeutiZaring] p. 29	Definition 6.18	df-br 4132
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5160  iniseg 5162
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4436
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5389
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 6019
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 6020
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 6025
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 6027
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 6035
[TakeutiZaring] p. 35	Notation	wtr 4231
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4501
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4235
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4725
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4528
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4532
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4641
[TakeutiZaring] p. 38	Definition 7.11	df-on 4515
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4635
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4701
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4731
[TakeutiZaring] p. 40	Exercise 7	dftr2 4233
[TakeutiZaring] p. 40	Exercise 11	unon 4660
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4636
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3963
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4518
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4562  sucidg 4563
[TakeutiZaring] p. 41	Proposition 7.24	onsuc 4650
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4516
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4655  ordelsuc 4654
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4743
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4744
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4745
[TakeutiZaring] p. 43	Axiom 7	omex 4742
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4756
[TakeutiZaring] p. 43	Corollary 7.31	find 4748
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4746
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4747
[TakeutiZaring] p. 44	Exercise 2	int0 3984
[TakeutiZaring] p. 44	Exercise 3	trintssm 4247
[TakeutiZaring] p. 44	Exercise 4	intss1 3985
[TakeutiZaring] p. 44	Exercise 6	onintonm 4666
[TakeutiZaring] p. 44	Definition 7.35	df-int 3971
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6583
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6640  tfri1d 6610
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6641  tfri2d 6611
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6642
[TakeutiZaring] p. 50	Exercise 3	smoiso 6577
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6561
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6741
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6737
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6734
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6738
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6786  nnaordi 6785
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 4057  uniss2 3966
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6747
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6757
[TakeutiZaring] p. 62	Exercise 5	oaword1 6748
[TakeutiZaring] p. 62	Definition 8.15	om0 6735  omsuc 6749
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6758
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6794  nnmordi 6793
[TakeutiZaring] p. 67	Definition 8.30	oei0 6736
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7539
[TakeutiZaring] p. 88	Exercise 1	en0 7087
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 7163
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 7164
[TakeutiZaring] p. 91	Definition 10.29	df-fin 7030  isfi 7052
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 7134
[TakeutiZaring] p. 95	Definition 10.42	df-map 6928
[TakeutiZaring] p. 96	Proposition 10.44	pw2f1odc 7140
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 7153
[Tarski] p. 67	Axiom B5	ax-4 1563
[Tarski] p. 68	Lemma 6	equid 1753
[Tarski] p. 69	Lemma 7	equcomi 1756
[Tarski] p. 70	Lemma 14	spim 1791  spime 1794  spimeh 1792  spimh 1790
[Tarski] p. 70	Lemma 16	ax-11 1559  ax-11o 1876  ax11i 1766
[Tarski] p. 70	Lemmas 16 and 17	sb6 1941
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1579
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 2211  ax-14 2212
[WhiteheadRussell] p. 96	Axiom *1.3	olc 723
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 739
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 768
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 777
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 801
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 625
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 652
[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 849
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2185  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 749
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 848
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 638
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 897
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 855
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 868
[WhiteheadRussell] p. 103	Theorem *2.16	con3 651
[WhiteheadRussell] p. 103	Theorem *2.17	condc 865
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 867
[WhiteheadRussell] p. 104	Theorem *2.2	orc 724
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 787
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 626
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 630
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 905
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 919
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 780
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 781
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 816
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 817
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 815
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 1010
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 790
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 788
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 789
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 750
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 751
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 879  pm2.5gdc 878
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 874
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 752
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 753
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 754
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 665
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 666
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 734
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 903
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 737
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 738
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 877
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 760
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 812
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 813
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 669
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 725  pm2.67 755
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 881  pm2.521gdc 880
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 759
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 822
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 906
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 927
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 818
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 819
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 821
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 820
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 823
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 824
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 917
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 101
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 766
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 139
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 970
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 971
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 972
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 765
[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 705
[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 872
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 110  simprimdc 871
[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 700
[WhiteheadRussell] p. 113	Fact)	pm3.45 605
[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 767  pm3.44 727
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 344
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 610
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 797
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 883
[WhiteheadRussell] p. 117	Theorem *4.2	biid 171
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 884
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 902
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 706
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 140
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 965  bitr 476
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 399
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 769  pm4.25 770
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 266
[WhiteheadRussell] p. 118	Theorem *4.4	andi 830
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 740
[WhiteheadRussell] p. 118	Theorem *4.32	anass 405
[WhiteheadRussell] p. 118	Theorem *4.33	orass 779
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 470
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 804
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 613
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 834
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 1011
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 828
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 984
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 962
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 791
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 826  pm4.45 796  pm4.45im 334
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1534
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 969
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 909  imorr 733
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 319
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 911
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 762
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 763
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 914
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 951
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 764  pm4.56 792
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 952  oranim 793
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 697
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 910
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 898
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 912
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 698
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 913
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 899
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 393  pm4.71d 397  pm4.71i 395  pm4.71r 394  pm4.71rd 398  pm4.71ri 396
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 839
[WhiteheadRussell] p. 121	Theorem *4.73	iba 300
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 756
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 611  pm4.76 612
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 722  pm4.77 811
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 794
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 915
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 719
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 920
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 963
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 964
[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 563
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 609
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 921
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 922
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 924
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 923
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1438
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 840
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 916
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1443  pm5.18dc 895
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 718
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 707
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1441
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1446
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1447
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 907
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 479
[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 938  pm5.6r 939
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 967
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 348
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 457
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 617
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 929
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 618
[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 937
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 814
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 930
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 925
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 806
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 958
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 959
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 974
[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 975
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1688
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1538
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1685
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1951
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2089
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2501
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2502
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2964
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3108
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5360
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5361
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2166  eupickbi 2169
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5388
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7543
[vandenDries] p. 43	Theorem 62	pellexlem1 16241