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 6993  fidcenum 6837
[AczelRathjen], p. 72	Proposition 8.1.11	fidcenum 6837
[AczelRathjen], p. 73	Lemma 8.1.14	enumct 6993
[AczelRathjen], p. 73	Corollary 8.1.13	ennnfone 11927
[AczelRathjen], p. 74	Lemma 8.1.16	xpfi 6811
[AczelRathjen], p. 74	Remark 8.1.17	unfiexmid 6799
[AczelRathjen], p. 75	Corollary 8.1.23	qnnen 11933  znnen 11900
[AczelRathjen], p. 80	Corollary 8.2.4	df-ihash 10515
[AczelRathjen], p. 183	Chapter 20	ax-setind 4447
[Apostol] p. 18	Theorem I.1	addcan 7935  addcan2d 7940  addcan2i 7938  addcand 7939  addcani 7937
[Apostol] p. 18	Theorem I.2	negeu 7946
[Apostol] p. 18	Theorem I.3	negsub 8003  negsubd 8072  negsubi 8033
[Apostol] p. 18	Theorem I.4	negneg 8005  negnegd 8057  negnegi 8025
[Apostol] p. 18	Theorem I.5	subdi 8140  subdid 8169  subdii 8162  subdir 8141  subdird 8170  subdiri 8163
[Apostol] p. 18	Theorem I.6	mul01 8144  mul01d 8148  mul01i 8146  mul02 8142  mul02d 8147  mul02i 8145
[Apostol] p. 18	Theorem I.9	divrecapd 8546
[Apostol] p. 18	Theorem I.10	recrecapi 8497
[Apostol] p. 18	Theorem I.12	mul2neg 8153  mul2negd 8168  mul2negi 8161  mulneg1 8150  mulneg1d 8166  mulneg1i 8159
[Apostol] p. 18	Theorem I.15	divdivdivap 8466
[Apostol] p. 20	Axiom 7	rpaddcl 9458  rpaddcld 9492  rpmulcl 9459  rpmulcld 9493
[Apostol] p. 20	Axiom 9	0nrp 9470
[Apostol] p. 20	Theorem I.17	lttri 7861
[Apostol] p. 20	Theorem I.18	ltadd1d 8293  ltadd1dd 8311  ltadd1i 8257
[Apostol] p. 20	Theorem I.19	ltmul1 8347  ltmul1a 8346  ltmul1i 8671  ltmul1ii 8679  ltmul2 8607  ltmul2d 9519  ltmul2dd 9533  ltmul2i 8674
[Apostol] p. 20	Theorem I.21	0lt1 7882
[Apostol] p. 20	Theorem I.23	lt0neg1 8223  lt0neg1d 8270  ltneg 8217  ltnegd 8278  ltnegi 8248
[Apostol] p. 20	Theorem I.25	lt2add 8200  lt2addd 8322  lt2addi 8265
[Apostol] p. 20	Definition of positive numbers	df-rp 9435
[Apostol] p. 21	Exercise 4	recgt0 8601  recgt0d 8685  recgt0i 8657  recgt0ii 8658
[Apostol] p. 22	Definition of integers	df-z 9048
[Apostol] p. 22	Definition of rationals	df-q 9405
[Apostol] p. 24	Theorem I.26	supeuti 6874
[Apostol] p. 26	Theorem I.29	arch 8967
[Apostol] p. 28	Exercise 2	btwnz 9163
[Apostol] p. 28	Exercise 3	nnrecl 8968
[Apostol] p. 28	Exercise 6	qbtwnre 10027
[Apostol] p. 28	Exercise 10(a)	zeneo 11557  zneo 9145
[Apostol] p. 29	Theorem I.35	resqrtth 10796  sqrtthi 10884
[Apostol] p. 34	Theorem I.36 (principle of mathematical induction)	peano5nni 8716
[Apostol] p. 363	Remark	absgt0api 10911
[Apostol] p. 363	Example	abssubd 10958  abssubi 10915
[ApostolNT] p. 14	Definition	df-dvds 11483
[ApostolNT] p. 14	Theorem 1.1(a)	iddvds 11495
[ApostolNT] p. 14	Theorem 1.1(b)	dvdstr 11519
[ApostolNT] p. 14	Theorem 1.1(c)	dvds2ln 11515
[ApostolNT] p. 14	Theorem 1.1(d)	dvdscmul 11509
[ApostolNT] p. 14	Theorem 1.1(e)	dvdscmulr 11511
[ApostolNT] p. 14	Theorem 1.1(f)	1dvds 11496
[ApostolNT] p. 14	Theorem 1.1(g)	dvds0 11497
[ApostolNT] p. 14	Theorem 1.1(h)	0dvds 11502
[ApostolNT] p. 14	Theorem 1.1(i)	dvdsleabs 11532
[ApostolNT] p. 14	Theorem 1.1(j)	dvdsabseq 11534
[ApostolNT] p. 14	Theorem 1.1(k)	divconjdvds 11536
[ApostolNT] p. 15	Definition	dfgcd2 11691
[ApostolNT] p. 16	Definition	isprm2 11787
[ApostolNT] p. 16	Theorem 1.5	coprmdvds 11762
[ApostolNT] p. 16	Theorem 1.4(a)	gcdcom 11651
[ApostolNT] p. 16	Theorem 1.4(b)	gcdass 11692
[ApostolNT] p. 16	Theorem 1.4(c)	absmulgcd 11694
[ApostolNT] p. 16	Theorem 1.4(d)1	gcd1 11664
[ApostolNT] p. 16	Theorem 1.4(d)2	gcdid0 11657
[ApostolNT] p. 17	Theorem 1.8	coprm 11811
[ApostolNT] p. 17	Theorem 1.9	euclemma 11813
[ApostolNT] p. 19	Theorem 1.14	divalg 11610
[ApostolNT] p. 20	Theorem 1.15	eucalg 11729
[ApostolNT] p. 25	Definition	df-phi 11876
[ApostolNT] p. 28	Theorem 2.5(a)	phiprmpw 11887
[ApostolNT] p. 28	Theorem 2.5(c)	phimul 11891
[ApostolNT] p. 104	Definition	congr 11770
[ApostolNT] p. 106	Remark	dvdsval3 11486
[ApostolNT] p. 106	Definition	moddvds 11491
[ApostolNT] p. 107	Example 2	mod2eq0even 11564
[ApostolNT] p. 107	Example 3	mod2eq1n2dvds 11565
[ApostolNT] p. 107	Example 4	zmod1congr 10107
[ApostolNT] p. 107	Theorem 5.2(b)	modqmul12d 10144
[ApostolNT] p. 108	Theorem 5.3	modmulconst 11514
[ApostolNT] p. 109	Theorem 5.4	cncongr1 11773
[ApostolNT] p. 109	Theorem 5.4 "Cancellation law"	cncongr 11775
[Bauer] p. 482	Section 1.2	pm2.01 605  pm2.65 648
[Bauer] p. 483	Theorem 1.3	acexmid 5766  onsucelsucexmidlem 4439
[Bauer], p. 481	Section 1.1	pwtrufal 13181
[Bauer], p. 483	Definition	n0rf 3370
[Bauer], p. 485	Theorem 2.1	ssfiexmid 6763
[Bauer], p. 494	Theorem 5.5	ivthinc 12779
[BauerHanson], p. 27	Proposition 5.2	cnstab 8400
[BauerSwan], p. 14	Remark	0ct 6985  ctm 6987
[BauerSwan], p. 14	Proposition 2.6	subctctexmid 13185
[BauerSwan], p. 14	Table" is defined as ` ` per	enumct 6993
[BauerTaylor], p. 32	Lemma 6.16	prarloclem 7302
[BauerTaylor], p. 50	Lemma 11.4	subhalfnqq 7215
[BauerTaylor], p. 52	Proposition 11.15	prarloc 7304
[BauerTaylor], p. 53	Lemma 11.16	addclpr 7338  addlocpr 7337
[BauerTaylor], p. 55	Proposition 12.7	appdivnq 7364
[BauerTaylor], p. 56	Lemma 12.8	prmuloc 7367
[BauerTaylor], p. 56	Lemma 12.9	mullocpr 7372
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2000
[BellMachover] p. 460	Notation	df-mo 2001
[BellMachover] p. 460	Definition	mo3 2051  mo3h 2050
[BellMachover] p. 462	Theorem 1.1	bm1.1 2122
[BellMachover] p. 463	Theorem 1.3ii	bm1.3ii 4044
[BellMachover] p. 466	Axiom Pow	axpow3 4096
[BellMachover] p. 466	Axiom Union	axun2 4352
[BellMachover] p. 469	Theorem 2.2(i)	ordirr 4452
[BellMachover] p. 469	Theorem 2.2(iii)	onelon 4301
[BellMachover] p. 469	Theorem 2.2(vii)	ordn2lp 4455
[BellMachover] p. 471	Problem 2.5(ii)	bm2.5ii 4407
[BellMachover] p. 471	Definition of Lim	df-ilim 4286
[BellMachover] p. 472	Axiom Inf	zfinf2 4498
[BellMachover] p. 473	Theorem 2.8	limom 4522
[Bobzien] p. 116	Statement T3	stoic3 1407
[Bobzien] p. 117	Statement T2	stoic2a 1405
[Bobzien] p. 117	Statement T4	stoic4a 1408
[BourbakiEns] p.	Proposition 8	fcof1 5677  fcofo 5678
[BourbakiTop1] p.	Remark	xnegmnf 9605  xnegpnf 9604
[BourbakiTop1] p.	Remark	rexneg 9606
[BourbakiTop1] p.	Proposition	ishmeo 12462
[BourbakiTop1] p.	Property V_i	ssnei2 12315
[BourbakiTop1] p.	Property V_ii	innei 12321
[BourbakiTop1] p.	Property V_iv	neissex 12323
[BourbakiTop1] p.	Proposition 1	neipsm 12312  neiss 12308
[BourbakiTop1] p.	Proposition 2	cnptopco 12380
[BourbakiTop1] p.	Proposition 4	imasnopn 12457
[BourbakiTop1] p.	Property V_iii	elnei 12310
[BourbakiTop1] p.	Definition is due to Bourbaki (Def. 1	df-top 12154
[ChoquetDD] p. 2	Definition of mapping	df-mpt 3986
[Crosilla] p.	Axiom 1	ax-ext 2119
[Crosilla] p.	Axiom 2	ax-pr 4126
[Crosilla] p.	Axiom 3	ax-un 4350
[Crosilla] p.	Axiom 4	ax-nul 4049
[Crosilla] p.	Axiom 5	ax-iinf 4497
[Crosilla] p.	Axiom 6	ru 2903
[Crosilla] p.	Axiom 8	ax-pow 4093
[Crosilla] p.	Axiom 9	ax-setind 4447
[Crosilla], p.	Axiom 6	ax-sep 4041
[Crosilla], p.	Axiom 7	ax-coll 4038
[Crosilla], p.	Axiom 7'	repizf 4039
[Crosilla], p.	Theorem is stated	ordtriexmid 4432
[Crosilla], p.	Axiom of choice implies instances	acexmid 5766
[Crosilla], p.	Definition of ordinal	df-iord 4283
[Crosilla], p.	Theorem "Foundation implies instances of EM"	regexmid 4445
[Eisenberg] p. 67	Definition 5.3	df-dif 3068
[Eisenberg] p. 82	Definition 6.3	df-iom 4500
[Eisenberg] p. 125	Definition 8.21	df-map 6537
[Enderton] p. 18	Axiom of Empty Set	axnul 4048
[Enderton] p. 19	Definition	df-tp 3530
[Enderton] p. 26	Exercise 5	unissb 3761
[Enderton] p. 26	Exercise 10	pwel 4135
[Enderton] p. 28	Exercise 7(b)	pwunim 4203
[Enderton] p. 30	Theorem "Distributive laws"	iinin1m 3877  iinin2m 3876  iunin1 3872  iunin2 3871
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2m 3875  iundif2ss 3873
[Enderton] p. 33	Exercise 23	iinuniss 3890
[Enderton] p. 33	Exercise 25	iununir 3891
[Enderton] p. 33	Exercise 24(a)	iinpw 3898
[Enderton] p. 33	Exercise 24(b)	iunpw 4396  iunpwss 3899
[Enderton] p. 38	Exercise 6(a)	unipw 4134
[Enderton] p. 38	Exercise 6(b)	pwuni 4111
[Enderton] p. 41	Lemma 3D	opeluu 4366  rnex 4801  rnexg 4799
[Enderton] p. 41	Exercise 8	dmuni 4744  rnuni 4945
[Enderton] p. 42	Definition of a function	dffun7 5145  dffun8 5146
[Enderton] p. 43	Definition of function value	funfvdm2 5478
[Enderton] p. 43	Definition of single-rooted	funcnv 5179
[Enderton] p. 44	Definition (d)	dfima2 4878  dfima3 4879
[Enderton] p. 47	Theorem 3H	fvco2 5483
[Enderton] p. 49	Axiom of Choice (first form)	df-ac 7055
[Enderton] p. 50	Theorem 3K(a)	imauni 5655
[Enderton] p. 52	Definition	df-map 6537
[Enderton] p. 53	Exercise 21	coass 5052
[Enderton] p. 53	Exercise 27	dmco 5042
[Enderton] p. 53	Exercise 14(a)	funin 5189
[Enderton] p. 53	Exercise 22(a)	imass2 4910
[Enderton] p. 54	Remark	ixpf 6607  ixpssmap 6619
[Enderton] p. 54	Definition of infinite Cartesian product	df-ixp 6586
[Enderton] p. 56	Theorem 3M	erref 6442
[Enderton] p. 57	Lemma 3N	erthi 6468
[Enderton] p. 57	Definition	df-ec 6424
[Enderton] p. 58	Definition	df-qs 6428
[Enderton] p. 60	Theorem 3Q	th3q 6527  th3qcor 6526  th3qlem1 6524  th3qlem2 6525
[Enderton] p. 61	Exercise 35	df-ec 6424
[Enderton] p. 65	Exercise 56(a)	dmun 4741
[Enderton] p. 68	Definition of successor	df-suc 4288
[Enderton] p. 71	Definition	df-tr 4022  dftr4 4026
[Enderton] p. 72	Theorem 4E	unisuc 4330  unisucg 4331
[Enderton] p. 73	Exercise 6	unisuc 4330  unisucg 4331
[Enderton] p. 73	Exercise 5(a)	truni 4035
[Enderton] p. 73	Exercise 5(b)	trint 4036
[Enderton] p. 79	Theorem 4I(A1)	nna0 6363
[Enderton] p. 79	Theorem 4I(A2)	nnasuc 6365  onasuc 6355
[Enderton] p. 79	Definition of operation value	df-ov 5770
[Enderton] p. 80	Theorem 4J(A1)	nnm0 6364
[Enderton] p. 80	Theorem 4J(A2)	nnmsuc 6366  onmsuc 6362
[Enderton] p. 81	Theorem 4K(1)	nnaass 6374
[Enderton] p. 81	Theorem 4K(2)	nna0r 6367  nnacom 6373
[Enderton] p. 81	Theorem 4K(3)	nndi 6375
[Enderton] p. 81	Theorem 4K(4)	nnmass 6376
[Enderton] p. 81	Theorem 4K(5)	nnmcom 6378
[Enderton] p. 82	Exercise 16	nnm0r 6368  nnmsucr 6377
[Enderton] p. 88	Exercise 23	nnaordex 6416
[Enderton] p. 129	Definition	df-en 6628
[Enderton] p. 133	Exercise 1	xpomen 11897
[Enderton] p. 134	Theorem (Pigeonhole Principle)	phpm 6752
[Enderton] p. 136	Corollary 6E	nneneq 6744
[Enderton] p. 139	Theorem 6H(c)	mapen 6733
[Enderton] p. 142	Theorem 6I(3)	xpdjuen 7067
[Enderton] p. 143	Theorem 6J	dju0en 7063  dju1en 7062
[Enderton] p. 144	Corollary 6K	undif2ss 3433
[Enderton] p. 145	Figure 38	ffoss 5392
[Enderton] p. 145	Definition	df-dom 6629
[Enderton] p. 146	Example 1	domen 6638  domeng 6639
[Enderton] p. 146	Example 3	nndomo 6751
[Enderton] p. 149	Theorem 6L(c)	xpdom1 6722  xpdom1g 6720  xpdom2g 6719
[Enderton] p. 168	Definition	df-po 4213
[Enderton] p. 192	Theorem 7M(a)	oneli 4345
[Enderton] p. 192	Theorem 7M(b)	ontr1 4306
[Enderton] p. 192	Theorem 7M(c)	onirri 4453
[Enderton] p. 193	Corollary 7N(b)	0elon 4309
[Enderton] p. 193	Corollary 7N(c)	onsuci 4427
[Enderton] p. 193	Corollary 7N(d)	ssonunii 4400
[Enderton] p. 194	Remark	onprc 4462
[Enderton] p. 194	Exercise 16	suc11 4468
[Enderton] p. 197	Definition	df-card 7029
[Enderton] p. 200	Exercise 25	tfis 4492
[Enderton] p. 206	Theorem 7X(b)	en2lp 4464
[Enderton] p. 207	Exercise 34	opthreg 4466
[Enderton] p. 208	Exercise 35	suc11g 4467
[Geuvers], p. 1	Remark	expap0 10316
[Geuvers], p. 6	Lemma 2.13	mulap0r 8370
[Geuvers], p. 6	Lemma 2.15	mulap0 8408
[Geuvers], p. 9	Lemma 2.35	msqge0 8371
[Geuvers], p. 9	Definition 3.1(2)	ax-arch 7732
[Geuvers], p. 10	Lemma 3.9	maxcom 10968
[Geuvers], p. 10	Lemma 3.10	maxle1 10976  maxle2 10977
[Geuvers], p. 10	Lemma 3.11	maxleast 10978
[Geuvers], p. 10	Lemma 3.12	maxleb 10981
[Geuvers], p. 11	Definition 3.13	dfabsmax 10982
[Geuvers], p. 17	Definition 6.1	df-ap 8337
[Gleason] p. 117	Proposition 9-2.1	df-enq 7148  enqer 7159
[Gleason] p. 117	Proposition 9-2.2	df-1nqqs 7152  df-nqqs 7149
[Gleason] p. 117	Proposition 9-2.3	df-plpq 7145  df-plqqs 7150
[Gleason] p. 119	Proposition 9-2.4	df-mpq 7146  df-mqqs 7151
[Gleason] p. 119	Proposition 9-2.5	df-rq 7153
[Gleason] p. 119	Proposition 9-2.6	ltexnqq 7209
[Gleason] p. 120	Proposition 9-2.6(i)	halfnq 7212  ltbtwnnq 7217  ltbtwnnqq 7216
[Gleason] p. 120	Proposition 9-2.6(ii)	ltanqg 7201
[Gleason] p. 120	Proposition 9-2.6(iii)	ltmnqg 7202
[Gleason] p. 123	Proposition 9-3.5	addclpr 7338
[Gleason] p. 123	Proposition 9-3.5(i)	addassprg 7380
[Gleason] p. 123	Proposition 9-3.5(ii)	addcomprg 7379
[Gleason] p. 123	Proposition 9-3.5(iii)	ltaddpr 7398
[Gleason] p. 123	Proposition 9-3.5(iv)	ltexpri 7414
[Gleason] p. 123	Proposition 9-3.5(v)	ltaprg 7420  ltaprlem 7419
[Gleason] p. 123	Proposition 9-3.5(vi)	addcanprg 7417
[Gleason] p. 124	Proposition 9-3.7	mulclpr 7373
[Gleason] p. 124	Theorem 9-3.7(iv)	1idpr 7393
[Gleason] p. 124	Proposition 9-3.7(i)	mulassprg 7382
[Gleason] p. 124	Proposition 9-3.7(ii)	mulcomprg 7381
[Gleason] p. 124	Proposition 9-3.7(iii)	distrprg 7389
[Gleason] p. 124	Proposition 9-3.7(v)	recexpr 7439
[Gleason] p. 126	Proposition 9-4.1	df-enr 7527  enrer 7536
[Gleason] p. 126	Proposition 9-4.2	df-0r 7532  df-1r 7533  df-nr 7528
[Gleason] p. 126	Proposition 9-4.3	df-mr 7530  df-plr 7529  negexsr 7573  recexsrlem 7575
[Gleason] p. 127	Proposition 9-4.4	df-ltr 7531
[Gleason] p. 130	Proposition 10-1.3	creui 8711  creur 8710  cru 8357
[Gleason] p. 130	Definition 10-1.1(v)	ax-cnre 7724  axcnre 7682
[Gleason] p. 132	Definition 10-3.1	crim 10623  crimd 10742  crimi 10702  crre 10622  crred 10741  crrei 10701
[Gleason] p. 132	Definition 10-3.2	remim 10625  remimd 10707
[Gleason] p. 133	Definition 10.36	absval2 10822  absval2d 10950  absval2i 10909
[Gleason] p. 133	Proposition 10-3.4(a)	cjadd 10649  cjaddd 10730  cjaddi 10697
[Gleason] p. 133	Proposition 10-3.4(c)	cjmul 10650  cjmuld 10731  cjmuli 10698
[Gleason] p. 133	Proposition 10-3.4(e)	cjcj 10648  cjcjd 10708  cjcji 10680
[Gleason] p. 133	Proposition 10-3.4(f)	cjre 10647  cjreb 10631  cjrebd 10711  cjrebi 10683  cjred 10736  rere 10630  rereb 10628  rerebd 10710  rerebi 10682  rered 10734
[Gleason] p. 133	Proposition 10-3.4(h)	addcj 10656  addcjd 10722  addcji 10692
[Gleason] p. 133	Proposition 10-3.7(a)	absval 10766
[Gleason] p. 133	Proposition 10-3.7(b)	abscj 10817  abscjd 10955  abscji 10913
[Gleason] p. 133	Proposition 10-3.7(c)	abs00 10829  abs00d 10951  abs00i 10910  absne0d 10952
[Gleason] p. 133	Proposition 10-3.7(d)	releabs 10861  releabsd 10956  releabsi 10914
[Gleason] p. 133	Proposition 10-3.7(f)	absmul 10834  absmuld 10959  absmuli 10916
[Gleason] p. 133	Proposition 10-3.7(g)	sqabsadd 10820  sqabsaddi 10917
[Gleason] p. 133	Proposition 10-3.7(h)	abstri 10869  abstrid 10961  abstrii 10920
[Gleason] p. 134	Definition 10-4.1	0exp0e1 10291  df-exp 10286  exp0 10290  expp1 10293  expp1d 10418
[Gleason] p. 135	Proposition 10-4.2(a)	expadd 10328  expaddd 10419
[Gleason] p. 135	Proposition 10-4.2(b)	expmul 10331  expmuld 10420
[Gleason] p. 135	Proposition 10-4.2(c)	mulexp 10325  mulexpd 10432
[Gleason] p. 141	Definition 11-2.1	fzval 9785
[Gleason] p. 168	Proposition 12-2.1(a)	climadd 11088
[Gleason] p. 168	Proposition 12-2.1(b)	climsub 11090
[Gleason] p. 168	Proposition 12-2.1(c)	climmul 11089
[Gleason] p. 171	Corollary 12-2.2	climmulc2 11093
[Gleason] p. 172	Corollary 12-2.5	climrecl 11086
[Gleason] p. 172	Proposition 12-2.4(c)	climabs 11082  climcj 11083  climim 11085  climre 11084
[Gleason] p. 173	Definition 12-3.1	df-ltxr 7798  df-xr 7797  ltxr 9555
[Gleason] p. 180	Theorem 12-5.3	climcau 11109
[Gleason] p. 217	Lemma 13-4.1	btwnzge0 10066
[Gleason] p. 223	Definition 14-1.1	df-met 12147
[Gleason] p. 223	Definition 14-1.1(a)	met0 12522  xmet0 12521
[Gleason] p. 223	Definition 14-1.1(c)	metsym 12529
[Gleason] p. 223	Definition 14-1.1(d)	mettri 12531  mstri 12631  xmettri 12530  xmstri 12630
[Gleason] p. 230	Proposition 14-2.6	txlm 12437
[Gleason] p. 240	Proposition 14-4.2	metcnp3 12669
[Gleason] p. 243	Proposition 14-4.16	addcn2 11072  addcncntop 12710  mulcn2 11074  mulcncntop 12712  subcn2 11073  subcncntop 12711
[Gleason] p. 295	Remark	bcval3 10490  bcval4 10491
[Gleason] p. 295	Equation 2	bcpasc 10505
[Gleason] p. 295	Definition of binomial coefficient	bcval 10488  df-bc 10487
[Gleason] p. 296	Remark	bcn0 10494  bcnn 10496
[Gleason] p. 296	Theorem 15-2.8	binom 11246
[Gleason] p. 308	Equation 2	ef0 11367
[Gleason] p. 308	Equation 3	efcj 11368
[Gleason] p. 309	Corollary 15-4.3	efne0 11373
[Gleason] p. 309	Corollary 15-4.4	efexp 11377
[Gleason] p. 310	Equation 14	sinadd 11432
[Gleason] p. 310	Equation 15	cosadd 11433
[Gleason] p. 311	Equation 17	sincossq 11444
[Gleason] p. 311	Equation 18	cosbnd 11449  sinbnd 11448
[Gleason] p. 311	Definition of ` `	df-pi 11348
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[Hamilton] p. 74	Rule 2	ax-gen 1425
[Heyting] p. 127	Axiom #1	ax1hfs 13229
[Hitchcock] p. 5	Rule A3	mptnan 1401
[Hitchcock] p. 5	Rule A4	mptxor 1402
[Hitchcock] p. 5	Rule A5	mtpxor 1404
[HoTT], p.	Theorem 7.2.6	nndceq 6388
[HoTT], p.	Exercise 11.11	mulap0bd 8411
[HoTT], p.	Section 11.2.1	df-iltp 7271  df-imp 7270  df-iplp 7269  df-reap 8330
[HoTT], p.	Theorem 11.2.12	cauappcvgpr 7463
[HoTT], p.	Corollary 11.4.3	conventions 12922
[HoTT], p.	Corollary 11.2.13	axcaucvg 7701  caucvgpr 7483  caucvgprpr 7513  caucvgsr 7603
[HoTT], p.	Definition 11.2.1	df-inp 7267
[HoTT], p.	Proposition 11.2.3	df-iso 4214  ltpopr 7396  ltsopr 7397
[HoTT], p.	Definition 11.2.7(v)	apsym 8361  reapcotr 8353  reapirr 8332
[HoTT], p.	Definition 11.2.7(vi)	0lt1 7882  gt0add 8328  leadd1 8185  lelttr 7845  lemul1a 8609  lenlt 7833  ltadd1 8184  ltletr 7846  ltmul1 8347  reaplt 8343
[Jech] p. 4	Definition of class	cv 1330  cvjust 2132
[Jech] p. 78	Note	opthprc 4585
[KalishMontague] p. 81	Note 1	ax-i9 1510
[Kreyszig] p. 3	Property M1	metcl 12511  xmetcl 12510
[Kreyszig] p. 4	Property M2	meteq0 12518
[Kreyszig] p. 12	Equation 5	muleqadd 8422
[Kreyszig] p. 18	Definition 1.3-2	mopnval 12600
[Kreyszig] p. 19	Remark	mopntopon 12601
[Kreyszig] p. 19	Theorem T1	mopn0 12646  mopnm 12606
[Kreyszig] p. 19	Theorem T2	unimopn 12644
[Kreyszig] p. 19	Definition of neighborhood	neibl 12649
[Kreyszig] p. 20	Definition 1.3-3	metcnp2 12671
[Kreyszig] p. 25	Definition 1.4-1	lmbr 12371
[Kunen] p. 10	Axiom 0	a9e 1674
[Kunen] p. 12	Axiom 6	zfrep6 4040
[Kunen] p. 24	Definition 10.24	mapval 6547  mapvalg 6545
[Kunen] p. 31	Definition 10.24	mapex 6541
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3818
[Levy] p. 338	Axiom	df-clab 2124  df-clel 2133  df-cleq 2130
[Lopez-Astorga] p. 12	Rule 1	mptnan 1401
[Lopez-Astorga] p. 12	Rule 2	mptxor 1402
[Lopez-Astorga] p. 12	Rule 3	mtpxor 1404
[Margaris] p. 40	Rule C	exlimiv 1577
[Margaris] p. 49	Axiom A1	ax-1 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	condc 838
[Margaris] p. 49	Definition	dfbi2 385  dfordc 877  exalim 1478
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 45
[Margaris] p. 60	Theorem 8	mth8 639
[Margaris] p. 89	Theorem 19.2	19.2 1617  r19.2m 3444
[Margaris] p. 89	Theorem 19.3	19.3 1533  19.3h 1532  rr19.3v 2818
[Margaris] p. 89	Theorem 19.5	alcom 1454
[Margaris] p. 89	Theorem 19.6	alexdc 1598  alexim 1624
[Margaris] p. 89	Theorem 19.7	alnex 1475
[Margaris] p. 89	Theorem 19.8	19.8a 1569  spsbe 1814
[Margaris] p. 89	Theorem 19.9	19.9 1623  19.9h 1622  19.9v 1843  exlimd 1576
[Margaris] p. 89	Theorem 19.11	excom 1642  excomim 1641
[Margaris] p. 89	Theorem 19.12	19.12 1643  r19.12 2536
[Margaris] p. 90	Theorem 19.14	exnalim 1625
[Margaris] p. 90	Theorem 19.15	albi 1444  ralbi 2562
[Margaris] p. 90	Theorem 19.16	19.16 1534
[Margaris] p. 90	Theorem 19.17	19.17 1535
[Margaris] p. 90	Theorem 19.18	exbi 1583  rexbi 2563
[Margaris] p. 90	Theorem 19.19	19.19 1644
[Margaris] p. 90	Theorem 19.20	alim 1433  alimd 1501  alimdh 1443  alimdv 1851  ralimdaa 2496  ralimdv 2498  ralimdva 2497  ralimdvva 2499  sbcimdv 2969
[Margaris] p. 90	Theorem 19.21	19.21-2 1645  19.21 1562  19.21bi 1537  19.21h 1536  19.21ht 1560  19.21t 1561  19.21v 1845  alrimd 1589  alrimdd 1588  alrimdh 1455  alrimdv 1848  alrimi 1502  alrimih 1445  alrimiv 1846  alrimivv 1847  r19.21 2506  r19.21be 2521  r19.21bi 2518  r19.21t 2505  r19.21v 2507  ralrimd 2508  ralrimdv 2509  ralrimdva 2510  ralrimdvv 2514  ralrimdvva 2515  ralrimi 2501  ralrimiv 2502  ralrimiva 2503  ralrimivv 2511  ralrimivva 2512  ralrimivvva 2513  ralrimivw 2504  rexlimi 2540
[Margaris] p. 90	Theorem 19.22	2alimdv 1853  2eximdv 1854  exim 1578  eximd 1591  eximdh 1590  eximdv 1852  rexim 2524  reximdai 2528  reximddv 2533  reximddv2 2535  reximdv 2531  reximdv2 2529  reximdva 2532  reximdvai 2530  reximi2 2526
[Margaris] p. 90	Theorem 19.23	19.23 1656  19.23bi 1571  19.23h 1474  19.23ht 1473  19.23t 1655  19.23v 1855  19.23vv 1856  exlimd2 1574  exlimdh 1575  exlimdv 1791  exlimdvv 1869  exlimi 1573  exlimih 1572  exlimiv 1577  exlimivv 1868  r19.23 2538  r19.23v 2539  rexlimd 2544  rexlimdv 2546  rexlimdv3a 2549  rexlimdva 2547  rexlimdva2 2550  rexlimdvaa 2548  rexlimdvv 2554  rexlimdvva 2555  rexlimdvw 2551  rexlimiv 2541  rexlimiva 2542  rexlimivv 2553
[Margaris] p. 90	Theorem 19.24	i19.24 1618
[Margaris] p. 90	Theorem 19.25	19.25 1605
[Margaris] p. 90	Theorem 19.26	19.26-2 1458  19.26-3an 1459  19.26 1457  r19.26-2 2559  r19.26-3 2560  r19.26 2556  r19.26m 2561
[Margaris] p. 90	Theorem 19.27	19.27 1540  19.27h 1539  19.27v 1871  r19.27av 2565  r19.27m 3453  r19.27mv 3454
[Margaris] p. 90	Theorem 19.28	19.28 1542  19.28h 1541  19.28v 1872  r19.28av 2566  r19.28m 3447  r19.28mv 3450  rr19.28v 2819
[Margaris] p. 90	Theorem 19.29	19.29 1599  19.29r 1600  19.29r2 1601  19.29x 1602  r19.29 2567  r19.29d2r 2574  r19.29r 2568
[Margaris] p. 90	Theorem 19.30	19.30dc 1606
[Margaris] p. 90	Theorem 19.31	19.31r 1659
[Margaris] p. 90	Theorem 19.32	19.32dc 1657  19.32r 1658  r19.32r 2576  r19.32vdc 2578  r19.32vr 2577
[Margaris] p. 90	Theorem 19.33	19.33 1460  19.33b2 1608  19.33bdc 1609
[Margaris] p. 90	Theorem 19.34	19.34 1662
[Margaris] p. 90	Theorem 19.35	19.35-1 1603  19.35i 1604
[Margaris] p. 90	Theorem 19.36	19.36-1 1651  19.36aiv 1873  19.36i 1650  r19.36av 2580
[Margaris] p. 90	Theorem 19.37	19.37-1 1652  19.37aiv 1653  r19.37 2581  r19.37av 2582
[Margaris] p. 90	Theorem 19.38	19.38 1654
[Margaris] p. 90	Theorem 19.39	i19.39 1619
[Margaris] p. 90	Theorem 19.40	19.40-2 1611  19.40 1610  r19.40 2583
[Margaris] p. 90	Theorem 19.41	19.41 1664  19.41h 1663  19.41v 1874  19.41vv 1875  19.41vvv 1876  19.41vvvv 1877  r19.41 2584  r19.41v 2585
[Margaris] p. 90	Theorem 19.42	19.42 1666  19.42h 1665  19.42v 1878  19.42vv 1883  19.42vvv 1884  19.42vvvv 1885  r19.42v 2586
[Margaris] p. 90	Theorem 19.43	19.43 1607  r19.43 2587
[Margaris] p. 90	Theorem 19.44	19.44 1660  r19.44av 2588  r19.44mv 3452
[Margaris] p. 90	Theorem 19.45	19.45 1661  r19.45av 2589  r19.45mv 3451
[Margaris] p. 110	Exercise 2(b)	eu1 2022
[Megill] p. 444	Axiom C5	ax-17 1506
[Megill] p. 445	Lemma L12	alequcom 1495  ax-10 1483
[Megill] p. 446	Lemma L17	equtrr 1686
[Megill] p. 446	Lemma L19	hbnae 1699
[Megill] p. 447	Remark 9.1	df-sb 1736  sbid 1747
[Megill] p. 448	Scheme C5'	ax-4 1487
[Megill] p. 448	Scheme C6'	ax-7 1424
[Megill] p. 448	Scheme C8'	ax-8 1482
[Megill] p. 448	Scheme C9'	ax-i12 1485
[Megill] p. 448	Scheme C11'	ax-10o 1694
[Megill] p. 448	Scheme C12'	ax-13 1491
[Megill] p. 448	Scheme C13'	ax-14 1492
[Megill] p. 448	Scheme C15'	ax-11o 1795
[Megill] p. 448	Scheme C16'	ax-16 1786
[Megill] p. 448	Theorem 9.4	dral1 1708  dral2 1709  drex1 1770  drex2 1710  drsb1 1771  drsb2 1813
[Megill] p. 449	Theorem 9.7	sbcom2 1960  sbequ 1812  sbid2v 1969
[Megill] p. 450	Example in Appendix	hba1 1520
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 2986  rspsbca 2987  stdpc4 1748
[Mendelson] p. 69	Axiom 5	ra5 2992  stdpc5 1563
[Mendelson] p. 81	Rule C	exlimiv 1577
[Mendelson] p. 95	Axiom 6	stdpc6 1679
[Mendelson] p. 95	Axiom 7	stdpc7 1743
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3394
[Mendelson] p. 231	Exercise 4.10(l)	unv 3395
[Mendelson] p. 231	Exercise 4.10(n)	inssun 3311
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3359
[Mendelson] p. 231	Exercise 4.10(q)	inssddif 3312
[Mendelson] p. 231	Exercise 4.10(s)	ddifnel 3202
[Mendelson] p. 231	Definition of union	unssin 3310
[Mendelson] p. 235	Exercise 4.12(c)	univ 4392
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3730
[Mendelson] p. 235	Exercise 4.12(j)	pwin 4199
[Mendelson] p. 235	Exercise 4.12(k)	pwunss 4200
[Mendelson] p. 235	Exercise 4.12(l)	pwssunim 4201
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3751
[Mendelson] p. 235	Exercise 4.12(p)	reli 4663
[Mendelson] p. 235	Exercise 4.12(t)	relssdmrn 5054
[Mendelson] p. 246	Definition of successor	df-suc 4288
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6732
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6708  xpsneng 6709
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6714  xpcomeng 6715
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6717
[Mendelson] p. 255	Exercise 4.39	endisj 6711
[Mendelson] p. 255	Exercise 4.41	mapprc 6539
[Mendelson] p. 255	Exercise 4.43	mapsnen 6698
[Mendelson] p. 255	Exercise 4.47	xpmapen 6737
[Mendelson] p. 255	Exercise 4.42(a)	map0e 6573
[Mendelson] p. 255	Exercise 4.42(b)	map1 6699
[Mendelson] p. 258	Exercise 4.56(c)	djuassen 7066  djucomen 7065
[Mendelson] p. 258	Exercise 4.56(g)	xp2dju 7064
[Mendelson] p. 266	Proposition 4.34(a)	oa1suc 6356
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3293
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4622
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4623
[Monk1] p. 34	Definition 3.3	df-opab 3985
[Monk1] p. 36	Theorem 3.7(i)	coi1 5049  coi2 5050
[Monk1] p. 36	Theorem 3.8(v)	dm0 4748  rn0 4790
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 4938
[Monk1] p. 37	Theorem 3.13(i)	relxp 4643
[Monk1] p. 37	Theorem 3.13(x)	dmxpm 4754  rnxpm 4963
[Monk1] p. 37	Theorem 3.13(ii)	0xp 4614  xp0 4953
[Monk1] p. 38	Theorem 3.16(ii)	ima0 4893
[Monk1] p. 38	Theorem 3.16(viii)	imai 4890
[Monk1] p. 39	Theorem 3.17	imaex 4889  imaexg 4888
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 4887
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5543  funfvop 5525
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5458
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5466
[Monk1] p. 43	Theorem 4.6	funun 5162
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5662  dff13f 5664
[Monk1] p. 46	Theorem 4.15(v)	funex 5636  funrnex 6005
[Monk1] p. 50	Definition 5.4	fniunfv 5656
[Monk1] p. 52	Theorem 5.12(ii)	op2ndb 5017
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3782
[Monk1] p. 52	Definition 5.13 (i)	1stval2 6046  df-1st 6031
[Monk1] p. 52	Definition 5.13 (ii)	2ndval2 6047  df-2nd 6032
[Monk2] p. 105	Axiom C4	ax-5 1423
[Monk2] p. 105	Axiom C7	ax-8 1482
[Monk2] p. 105	Axiom C8	ax-11 1484  ax-11o 1795
[Monk2] p. 105	Axiom (C8)	ax11v 1799
[Monk2] p. 109	Lemma 12	ax-7 1424
[Monk2] p. 109	Lemma 15	equvin 1835  equvini 1731  eqvinop 4160
[Monk2] p. 113	Axiom C5-1	ax-17 1506
[Monk2] p. 113	Axiom C5-2	ax6b 1629
[Monk2] p. 113	Axiom C5-3	ax-7 1424
[Monk2] p. 114	Lemma 22	hba1 1520
[Monk2] p. 114	Lemma 23	hbia1 1531  nfia1 1559
[Monk2] p. 114	Lemma 24	hba2 1530  nfa2 1558
[Moschovakis] p. 2	Chapter 2	df-stab 816  dftest 13230
[Munkres] p. 77	Example 2	distop 12243
[Munkres] p. 78	Definition of basis	df-bases 12199  isbasis3g 12202
[Munkres] p. 78	Definition of a topology generated by a basis	df-topgen 12130  tgval2 12209
[Munkres] p. 79	Remark	tgcl 12222
[Munkres] p. 80	Lemma 2.1	tgval3 12216
[Munkres] p. 80	Lemma 2.2	tgss2 12237  tgss3 12236
[Munkres] p. 81	Lemma 2.3	basgen 12238  basgen2 12239
[Munkres] p. 89	Definition of subspace topology	resttop 12328
[Munkres] p. 93	Theorem 6.1(1)	0cld 12270  topcld 12267
[Munkres] p. 93	Theorem 6.1(3)	uncld 12271
[Munkres] p. 94	Definition of closure	clsval 12269
[Munkres] p. 94	Definition of interior	ntrval 12268
[Munkres] p. 102	Definition of continuous function	df-cn 12346  iscn 12355  iscn2 12358
[Munkres] p. 107	Theorem 7.2(g)	cncnp 12388  cncnp2m 12389  cncnpi 12386  df-cnp 12347  iscnp 12357
[Munkres] p. 127	Theorem 10.1	metcn 12672
[Pierik], p. 8	Section 2.2.1	dfrex2fin 6790
[Pierik], p. 9	Definition 2.5	df-markov 7019
[Pierik], p. 10	Section 2.3	dfdif3 3181
[Pierik], p. 14	Definition 3.1	df-omni 6999  exmidomniim 7006  finomni 7005
[Pierik], p. 15	Section 3.1	df-nninf 7000
[PradicBrown2022], p. 1	Theorem 1	exmidsbthr 13207
[PradicBrown2022], p. 2	Remark	exmidpw 6795
[PradicBrown2022], p. 2	Proposition 1.1	exmidfodomrlemim 7050
[PradicBrown2022], p. 2	Proposition 1.2	exmidfodomrlemr 7051  exmidfodomrlemrALT 7052
[PradicBrown2022], p. 4	Lemma 3.2	fodjuomni 7014
[PradicBrown2022], p. 5	Lemma 3.4	peano3nninf 13190  peano4nninf 13189
[PradicBrown2022], p. 5	Lemma 3.5	nninfall 13193
[PradicBrown2022], p. 5	Theorem 3.6	nninfsel 13202
[PradicBrown2022], p. 5	Corollary 3.7	nninfomni 13204
[PradicBrown2022], p. 5	Definition 3.3	nnsf 13188
[Quine] p. 16	Definition 2.1	df-clab 2124  rabid 2604
[Quine] p. 17	Definition 2.1''	dfsb7 1964
[Quine] p. 18	Definition 2.7	df-cleq 2130
[Quine] p. 19	Definition 2.9	df-v 2683
[Quine] p. 34	Theorem 5.1	abeq2 2246
[Quine] p. 35	Theorem 5.2	abid2 2258  abid2f 2304
[Quine] p. 40	Theorem 6.1	sb5 1859
[Quine] p. 40	Theorem 6.2	sb56 1857  sb6 1858
[Quine] p. 41	Theorem 6.3	df-clel 2133
[Quine] p. 41	Theorem 6.4	eqid 2137
[Quine] p. 41	Theorem 6.5	eqcom 2139
[Quine] p. 42	Theorem 6.6	df-sbc 2905
[Quine] p. 42	Theorem 6.7	dfsbcq 2906  dfsbcq2 2907
[Quine] p. 43	Theorem 6.8	vex 2684
[Quine] p. 43	Theorem 6.9	isset 2687
[Quine] p. 44	Theorem 7.3	spcgf 2763  spcgv 2768  spcimgf 2761
[Quine] p. 44	Theorem 6.11	spsbc 2915  spsbcd 2916
[Quine] p. 44	Theorem 6.12	elex 2692
[Quine] p. 44	Theorem 6.13	elab 2823  elabg 2825  elabgf 2821
[Quine] p. 44	Theorem 6.14	noel 3362
[Quine] p. 48	Theorem 7.2	snprc 3583
[Quine] p. 48	Definition 7.1	df-pr 3529  df-sn 3528
[Quine] p. 49	Theorem 7.4	snss 3644  snssg 3651
[Quine] p. 49	Theorem 7.5	prss 3671  prssg 3672
[Quine] p. 49	Theorem 7.6	prid1 3624  prid1g 3622  prid2 3625  prid2g 3623  snid 3551  snidg 3549
[Quine] p. 51	Theorem 7.12	snexg 4103  snexprc 4105
[Quine] p. 51	Theorem 7.13	prexg 4128
[Quine] p. 53	Theorem 8.2	unisn 3747  unisng 3748
[Quine] p. 53	Theorem 8.3	uniun 3750
[Quine] p. 54	Theorem 8.6	elssuni 3759
[Quine] p. 54	Theorem 8.7	uni0 3758
[Quine] p. 56	Theorem 8.17	uniabio 5093
[Quine] p. 56	Definition 8.18	dfiota2 5084
[Quine] p. 57	Theorem 8.19	iotaval 5094
[Quine] p. 57	Theorem 8.22	iotanul 5098
[Quine] p. 58	Theorem 8.23	euiotaex 5099
[Quine] p. 58	Definition 9.1	df-op 3531
[Quine] p. 61	Theorem 9.5	opabid 4174  opelopab 4188  opelopaba 4183  opelopabaf 4190  opelopabf 4191  opelopabg 4185  opelopabga 4180  oprabid 5796
[Quine] p. 64	Definition 9.11	df-xp 4540
[Quine] p. 64	Definition 9.12	df-cnv 4542
[Quine] p. 64	Definition 9.15	df-id 4210
[Quine] p. 65	Theorem 10.3	fun0 5176
[Quine] p. 65	Theorem 10.4	funi 5150
[Quine] p. 65	Theorem 10.5	funsn 5166  funsng 5164
[Quine] p. 65	Definition 10.1	df-fun 5120
[Quine] p. 65	Definition 10.2	args 4903  dffv4g 5411
[Quine] p. 68	Definition 10.11	df-fv 5126  fv2 5409
[Quine] p. 124	Theorem 17.3	nn0opth2 10463  nn0opth2d 10462  nn0opthd 10461
[Quine] p. 284	Axiom 39(vi)	funimaex 5203  funimaexg 5202
[Rudin] p. 164	Equation 27	efcan 11371
[Rudin] p. 164	Equation 30	efzval 11378
[Rudin] p. 167	Equation 48	absefi 11464
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtpxor 1404
[Sanford] p. 39	Rule 4	mptxor 1402
[Sanford] p. 40	Rule 1	mptnan 1401
[Schechter] p. 51	Definition of antisymmetry	intasym 4918
[Schechter] p. 51	Definition of irreflexivity	intirr 4920
[Schechter] p. 51	Definition of symmetry	cnvsym 4917
[Schechter] p. 51	Definition of transitivity	cotr 4915
[Schechter] p. 428	Definition 15.35	bastop1 12241
[Stoll] p. 13	Definition of symmetric difference	symdif1 3336
[Stoll] p. 16	Exercise 4.4	0dif 3429  dif0 3428
[Stoll] p. 16	Exercise 4.8	difdifdirss 3442
[Stoll] p. 19	Theorem 5.2(13)	undm 3329
[Stoll] p. 19	Theorem 5.2(13')	indmss 3330
[Stoll] p. 20	Remark	invdif 3313
[Stoll] p. 25	Definition of ordered triple	df-ot 3532
[Stoll] p. 43	Definition	uniiun 3861
[Stoll] p. 44	Definition	intiin 3862
[Stoll] p. 45	Definition	df-iin 3811
[Stoll] p. 45	Definition indexed union	df-iun 3810
[Stoll] p. 176	Theorem 3.4(27)	imandc 874  imanst 873
[Stoll] p. 262	Example 4.1	symdif1 3336
[Suppes] p. 22	Theorem 2	eq0 3376
[Suppes] p. 22	Theorem 4	eqss 3107  eqssd 3109  eqssi 3108
[Suppes] p. 23	Theorem 5	ss0 3398  ss0b 3397
[Suppes] p. 23	Theorem 6	sstr 3100
[Suppes] p. 25	Theorem 12	elin 3254  elun 3212
[Suppes] p. 26	Theorem 15	inidm 3280
[Suppes] p. 26	Theorem 16	in0 3392
[Suppes] p. 27	Theorem 23	unidm 3214
[Suppes] p. 27	Theorem 24	un0 3391
[Suppes] p. 27	Theorem 25	ssun1 3234
[Suppes] p. 27	Theorem 26	ssequn1 3241
[Suppes] p. 27	Theorem 27	unss 3245
[Suppes] p. 27	Theorem 28	indir 3320
[Suppes] p. 27	Theorem 29	undir 3321
[Suppes] p. 28	Theorem 32	difid 3426  difidALT 3427
[Suppes] p. 29	Theorem 33	difin 3308
[Suppes] p. 29	Theorem 34	indif 3314
[Suppes] p. 29	Theorem 35	undif1ss 3432
[Suppes] p. 29	Theorem 36	difun2 3437
[Suppes] p. 29	Theorem 37	difin0 3431
[Suppes] p. 29	Theorem 38	disjdif 3430
[Suppes] p. 29	Theorem 39	difundi 3323
[Suppes] p. 29	Theorem 40	difindiss 3325
[Suppes] p. 30	Theorem 41	nalset 4053
[Suppes] p. 39	Theorem 61	uniss 3752
[Suppes] p. 39	Theorem 65	uniop 4172
[Suppes] p. 41	Theorem 70	intsn 3801
[Suppes] p. 42	Theorem 71	intpr 3798  intprg 3799
[Suppes] p. 42	Theorem 73	op1stb 4394  op1stbg 4395
[Suppes] p. 42	Theorem 78	intun 3797
[Suppes] p. 44	Definition 15(a)	dfiun2 3842  dfiun2g 3840
[Suppes] p. 44	Definition 15(b)	dfiin2 3843
[Suppes] p. 47	Theorem 86	elpw 3511  elpw2 4077  elpw2g 4076  elpwg 3513
[Suppes] p. 47	Theorem 87	pwid 3520
[Suppes] p. 47	Theorem 89	pw0 3662
[Suppes] p. 48	Theorem 90	pwpw0ss 3726
[Suppes] p. 52	Theorem 101	xpss12 4641
[Suppes] p. 52	Theorem 102	xpindi 4669  xpindir 4670
[Suppes] p. 52	Theorem 103	xpundi 4590  xpundir 4591
[Suppes] p. 54	Theorem 105	elirrv 4458
[Suppes] p. 58	Theorem 2	relss 4621
[Suppes] p. 59	Theorem 4	eldm 4731  eldm2 4732  eldm2g 4730  eldmg 4729
[Suppes] p. 59	Definition 3	df-dm 4544
[Suppes] p. 60	Theorem 6	dmin 4742
[Suppes] p. 60	Theorem 8	rnun 4942
[Suppes] p. 60	Theorem 9	rnin 4943
[Suppes] p. 60	Definition 4	dfrn2 4722
[Suppes] p. 61	Theorem 11	brcnv 4717  brcnvg 4715
[Suppes] p. 62	Equation 5	elcnv 4711  elcnv2 4712
[Suppes] p. 62	Theorem 12	relcnv 4912
[Suppes] p. 62	Theorem 15	cnvin 4941
[Suppes] p. 62	Theorem 16	cnvun 4939
[Suppes] p. 63	Theorem 20	co02 5047
[Suppes] p. 63	Theorem 21	dmcoss 4803
[Suppes] p. 63	Definition 7	df-co 4543
[Suppes] p. 64	Theorem 26	cnvco 4719
[Suppes] p. 64	Theorem 27	coass 5052
[Suppes] p. 65	Theorem 31	resundi 4827
[Suppes] p. 65	Theorem 34	elima 4881  elima2 4882  elima3 4883  elimag 4880
[Suppes] p. 65	Theorem 35	imaundi 4946
[Suppes] p. 66	Theorem 40	dminss 4948
[Suppes] p. 66	Theorem 41	imainss 4949
[Suppes] p. 67	Exercise 11	cnvxp 4952
[Suppes] p. 81	Definition 34	dfec2 6425
[Suppes] p. 82	Theorem 72	elec 6461  elecg 6460
[Suppes] p. 82	Theorem 73	erth 6466  erth2 6467
[Suppes] p. 89	Theorem 96	map0b 6574
[Suppes] p. 89	Theorem 97	map0 6576  map0g 6575
[Suppes] p. 89	Theorem 98	mapsn 6577
[Suppes] p. 89	Theorem 99	mapss 6578
[Suppes] p. 92	Theorem 1	enref 6652  enrefg 6651
[Suppes] p. 92	Theorem 2	ensym 6668  ensymb 6667  ensymi 6669
[Suppes] p. 92	Theorem 3	entr 6671
[Suppes] p. 92	Theorem 4	unen 6703
[Suppes] p. 94	Theorem 15	endom 6650
[Suppes] p. 94	Theorem 16	ssdomg 6665
[Suppes] p. 94	Theorem 17	domtr 6672
[Suppes] p. 95	Theorem 18	isbth 6848
[Suppes] p. 98	Exercise 4	fundmen 6693  fundmeng 6694
[Suppes] p. 98	Exercise 6	xpdom3m 6721
[Suppes] p. 130	Definition 3	df-tr 4022
[Suppes] p. 132	Theorem 9	ssonuni 4399
[Suppes] p. 134	Definition 6	df-suc 4288
[Suppes] p. 136	Theorem Schema 22	findes 4512  finds 4509  finds1 4511  finds2 4510
[Suppes] p. 162	Definition 5	df-ltnqqs 7154  df-ltpq 7147
[Suppes] p. 228	Theorem Schema 61	onintss 4307
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2119
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2130
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2133
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2132
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2155
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5771
[TakeutiZaring] p. 14	Proposition 4.14	ru 2903
[TakeutiZaring] p. 15	Exercise 1	elpr 3543  elpr2 3544  elprg 3542
[TakeutiZaring] p. 15	Exercise 2	elsn 3538  elsn2 3554  elsn2g 3553  elsng 3537  velsn 3539
[TakeutiZaring] p. 15	Exercise 3	elop 4148
[TakeutiZaring] p. 15	Exercise 4	sneq 3533  sneqr 3682
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3541  dfsn2 3536
[TakeutiZaring] p. 16	Axiom 3	uniex 4354
[TakeutiZaring] p. 16	Exercise 6	opth 4154
[TakeutiZaring] p. 16	Exercise 8	rext 4132
[TakeutiZaring] p. 16	Corollary 5.8	unex 4357  unexg 4359
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3567
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3732
[TakeutiZaring] p. 16	Definition 5.6	df-in 3072  df-un 3070
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3745  uniprg 3746
[TakeutiZaring] p. 17	Axiom 4	vpwex 4098
[TakeutiZaring] p. 17	Exercise 1	eltp 3566
[TakeutiZaring] p. 17	Exercise 5	elsuc 4323  elsucg 4321  sstr2 3099
[TakeutiZaring] p. 17	Exercise 6	uncom 3215
[TakeutiZaring] p. 17	Exercise 7	incom 3263
[TakeutiZaring] p. 17	Exercise 8	unass 3228
[TakeutiZaring] p. 17	Exercise 9	inass 3281
[TakeutiZaring] p. 17	Exercise 10	indi 3318
[TakeutiZaring] p. 17	Exercise 11	undi 3319
[TakeutiZaring] p. 17	Definition 5.9	dfss2 3081
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3507
[TakeutiZaring] p. 18	Exercise 7	unss2 3242
[TakeutiZaring] p. 18	Exercise 9	df-ss 3079  sseqin2 3290
[TakeutiZaring] p. 18	Exercise 10	ssid 3112
[TakeutiZaring] p. 18	Exercise 12	inss1 3291  inss2 3292
[TakeutiZaring] p. 18	Exercise 13	nssr 3152
[TakeutiZaring] p. 18	Exercise 15	unieq 3740
[TakeutiZaring] p. 18	Exercise 18	sspwb 4133
[TakeutiZaring] p. 18	Exercise 19	pweqb 4140
[TakeutiZaring] p. 20	Definition	df-rab 2423
[TakeutiZaring] p. 20	Corollary 5.16	0ex 4050
[TakeutiZaring] p. 20	Definition 5.12	df-dif 3068
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3360
[TakeutiZaring] p. 20	Proposition 5.15	difid 3426  difidALT 3427
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0rf 3370
[TakeutiZaring] p. 21	Theorem 5.22	setind 4449
[TakeutiZaring] p. 21	Definition 5.20	df-v 2683
[TakeutiZaring] p. 21	Proposition 5.21	vprc 4055
[TakeutiZaring] p. 22	Exercise 1	0ss 3396
[TakeutiZaring] p. 22	Exercise 3	ssex 4060  ssexg 4062
[TakeutiZaring] p. 22	Exercise 4	inex1 4057
[TakeutiZaring] p. 22	Exercise 5	ruv 4460
[TakeutiZaring] p. 22	Exercise 6	elirr 4451
[TakeutiZaring] p. 22	Exercise 7	ssdif0im 3422
[TakeutiZaring] p. 22	Exercise 11	difdif 3196
[TakeutiZaring] p. 22	Exercise 13	undif3ss 3332
[TakeutiZaring] p. 22	Exercise 14	difss 3197
[TakeutiZaring] p. 22	Exercise 15	sscon 3205
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2419
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2420
[TakeutiZaring] p. 23	Proposition 6.2	xpex 4649  xpexg 4648  xpexgALT 6024
[TakeutiZaring] p. 23	Definition 6.4(1)	df-rel 4541
[TakeutiZaring] p. 23	Definition 6.4(2)	fun2cnv 5182
[TakeutiZaring] p. 24	Definition 6.4(3)	f1cnvcnv 5334  fun11 5185
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5129  svrelfun 5183
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4721
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4723
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4546
[TakeutiZaring] p. 24	Definition 6.6(2)	df-ima 4547
[TakeutiZaring] p. 24	Definition 6.6(3)	df-co 4543
[TakeutiZaring] p. 25	Exercise 2	cnvcnvss 4988  dfrel2 4984
[TakeutiZaring] p. 25	Exercise 3	xpss 4642
[TakeutiZaring] p. 25	Exercise 5	relun 4651
[TakeutiZaring] p. 25	Exercise 6	reluni 4657
[TakeutiZaring] p. 25	Exercise 9	inxp 4668
[TakeutiZaring] p. 25	Exercise 12	relres 4842
[TakeutiZaring] p. 25	Exercise 13	opelres 4819  opelresg 4821
[TakeutiZaring] p. 25	Exercise 14	dmres 4835
[TakeutiZaring] p. 25	Exercise 15	resss 4838
[TakeutiZaring] p. 25	Exercise 17	resabs1 4843
[TakeutiZaring] p. 25	Exercise 18	funres 5159
[TakeutiZaring] p. 25	Exercise 24	relco 5032
[TakeutiZaring] p. 25	Exercise 29	funco 5158
[TakeutiZaring] p. 25	Exercise 30	f1co 5335
[TakeutiZaring] p. 26	Definition 6.10	eu2 2041
[TakeutiZaring] p. 26	Definition 6.11	df-fv 5126  fv3 5437
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5072  cnvexg 5071
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 4800  dmexg 4798
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 4801  rnexg 4799
[TakeutiZaring] p. 27	Corollary 6.13	funfvex 5431
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5441  tz6.12 5442  tz6.12c 5444
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5405
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 5121
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 5122
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 5124  wfo 5116
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 5123  wf1 5115
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 5125  wf1o 5117
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5511  eqfnfv2 5512  eqfnfv2f 5515
[TakeutiZaring] p. 28	Exercise 5	fvco 5484
[TakeutiZaring] p. 28	Theorem 6.16(1)	fnex 5635  fnexALT 6004
[TakeutiZaring] p. 28	Proposition 6.17	resfunexg 5634  resfunexgALT 6001
[TakeutiZaring] p. 29	Exercise 9	funimaex 5203  funimaexg 5202
[TakeutiZaring] p. 29	Definition 6.18	df-br 3925
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 4904  iniseg 4906
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4206
[TakeutiZaring] p. 32	Definition 6.28	df-isom 5127
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5704
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5705
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5710
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5712
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5720
[TakeutiZaring] p. 35	Notation	wtr 4021
[TakeutiZaring] p. 35	Theorem 7.2	tz7.2 4271
[TakeutiZaring] p. 35	Definition 7.1	dftr3 4025
[TakeutiZaring] p. 36	Proposition 7.4	ordwe 4485
[TakeutiZaring] p. 36	Proposition 7.6	ordelord 4298
[TakeutiZaring] p. 37	Proposition 7.9	ordin 4302
[TakeutiZaring] p. 38	Corollary 7.15	ordsson 4403
[TakeutiZaring] p. 38	Definition 7.11	df-on 4285
[TakeutiZaring] p. 38	Proposition 7.12	ordon 4397
[TakeutiZaring] p. 38	Proposition 7.13	onprc 4462
[TakeutiZaring] p. 39	Theorem 7.17	tfi 4491
[TakeutiZaring] p. 40	Exercise 7	dftr2 4023
[TakeutiZaring] p. 40	Exercise 11	unon 4422
[TakeutiZaring] p. 40	Proposition 7.19	ssorduni 4398
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3759
[TakeutiZaring] p. 41	Definition 7.22	df-suc 4288
[TakeutiZaring] p. 41	Proposition 7.23	sssucid 4332  sucidg 4333
[TakeutiZaring] p. 41	Proposition 7.24	suceloni 4412
[TakeutiZaring] p. 42	Exercise 1	df-ilim 4286
[TakeutiZaring] p. 42	Exercise 8	onsucssi 4417  ordelsuc 4416
[TakeutiZaring] p. 42	Proposition 7.30(1)	peano1 4503
[TakeutiZaring] p. 42	Proposition 7.30(2)	peano2 4504
[TakeutiZaring] p. 42	Proposition 7.30(3)	peano3 4505
[TakeutiZaring] p. 43	Axiom 7	omex 4502
[TakeutiZaring] p. 43	Theorem 7.32	ordom 4515
[TakeutiZaring] p. 43	Corollary 7.31	find 4508
[TakeutiZaring] p. 43	Proposition 7.30(4)	peano4 4506
[TakeutiZaring] p. 43	Proposition 7.30(5)	peano5 4507
[TakeutiZaring] p. 44	Exercise 2	int0 3780
[TakeutiZaring] p. 44	Exercise 3	trintssm 4037
[TakeutiZaring] p. 44	Exercise 4	intss1 3781
[TakeutiZaring] p. 44	Exercise 6	onintonm 4428
[TakeutiZaring] p. 44	Definition 7.35	df-int 3767
[TakeutiZaring] p. 47	Lemma 1	tfrlem1 6198
[TakeutiZaring] p. 47	Theorem 7.41(1)	tfri1 6255  tfri1d 6225
[TakeutiZaring] p. 47	Theorem 7.41(2)	tfri2 6256  tfri2d 6226
[TakeutiZaring] p. 47	Theorem 7.41(3)	tfri3 6257
[TakeutiZaring] p. 50	Exercise 3	smoiso 6192
[TakeutiZaring] p. 50	Definition 7.46	df-smo 6176
[TakeutiZaring] p. 56	Definition 8.1	oasuc 6353
[TakeutiZaring] p. 57	Proposition 8.2	oacl 6349
[TakeutiZaring] p. 57	Proposition 8.3	oa0 6346
[TakeutiZaring] p. 57	Proposition 8.16	omcl 6350
[TakeutiZaring] p. 58	Proposition 8.4	nnaord 6398  nnaordi 6397
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 3853  uniss2 3762
[TakeutiZaring] p. 59	Proposition 8.7	oawordriexmid 6359
[TakeutiZaring] p. 59	Proposition 8.9	nnacl 6369
[TakeutiZaring] p. 62	Exercise 5	oaword1 6360
[TakeutiZaring] p. 62	Definition 8.15	om0 6347  omsuc 6361
[TakeutiZaring] p. 63	Proposition 8.17	nnmcl 6370
[TakeutiZaring] p. 63	Proposition 8.19	nnmord 6406  nnmordi 6405
[TakeutiZaring] p. 67	Definition 8.30	oei0 6348
[TakeutiZaring] p. 85	Proposition 10.6(3)	cardonle 7036
[TakeutiZaring] p. 88	Exercise 1	en0 6682
[TakeutiZaring] p. 90	Proposition 10.20	nneneq 6744
[TakeutiZaring] p. 90	Corollary 10.21(1)	php5 6745
[TakeutiZaring] p. 91	Definition 10.29	df-fin 6630  isfi 6648
[TakeutiZaring] p. 92	Proposition 10.33(2)	xpdom2 6718
[TakeutiZaring] p. 95	Definition 10.42	df-map 6537
[TakeutiZaring] p. 96	Proposition 10.45	mapxpen 6735
[Tarski] p. 67	Axiom B5	ax-4 1487
[Tarski] p. 68	Lemma 6	equid 1677
[Tarski] p. 69	Lemma 7	equcomi 1680
[Tarski] p. 70	Lemma 14	spim 1716  spime 1719  spimeh 1717  spimh 1715
[Tarski] p. 70	Lemma 16	ax-11 1484  ax-11o 1795  ax11i 1692
[Tarski] p. 70	Lemmas 16 and 17	sb6 1858
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1506
[Tarski] p. 77	Axiom B8 (p. 75) of system S2	ax-13 1491  ax-14 1492
[WhiteheadRussell] p. 96	Axiom *1.3	olc 700
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 716
[WhiteheadRussell] p. 96	Axiom *1.2 (Taut)	pm1.2 745
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 754
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 778
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 605
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 6
[WhiteheadRussell] p. 100	Theorem *2.03	con2 632
[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 822
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2095  syl 14
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 726
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmiddc 821
[WhiteheadRussell] p. 101	Theorem *2.12	notnot 618
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13dc 870
[WhiteheadRussell] p. 102	Theorem *2.14	notnotrdc 828
[WhiteheadRussell] p. 102	Theorem *2.15	con1dc 841
[WhiteheadRussell] p. 103	Theorem *2.16	con3 631
[WhiteheadRussell] p. 103	Theorem *2.17	condc 838
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18dc 840
[WhiteheadRussell] p. 104	Theorem *2.2	orc 701
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 764
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 606
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 610
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25dc 878
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26dc 892
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 40
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 757
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 758
[WhiteheadRussell] p. 105	Theorem *2.36	pm2.36 793
[WhiteheadRussell] p. 105	Theorem *2.37	pm2.37 794
[WhiteheadRussell] p. 105	Theorem *2.38	pm2.38 792
[WhiteheadRussell] p. 105	Definition *2.33	df-3or 963
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 767
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 765
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 766
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 53
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 727
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 728
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5dc 852  pm2.5gdc 851
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6dc 847
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 729
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 730
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 731
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 644
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 645
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 711
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54dc 876
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 714
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 715
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61dc 850
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 737
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 789
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 790
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 648
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 702  pm2.67 732
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521dc 854  pm2.521gdc 853
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 736
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 799
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68dc 879
[WhiteheadRussell] p. 108	Theorem *2.69	looinvdc 900
[WhiteheadRussell] p. 108	Theorem *2.73	pm2.73 795
[WhiteheadRussell] p. 108	Theorem *2.74	pm2.74 796
[WhiteheadRussell] p. 108	Theorem *2.75	pm2.75 798
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 797
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 7
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 800
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 801
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 77
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85dc 890
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 100
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 743
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 138
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11dc 941
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12dc 942
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13dc 943
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 742
[WhiteheadRussell] p. 111	Theorem *3.21	pm3.21 262
[WhiteheadRussell] p. 111	Theorem *3.22	pm3.22 263
[WhiteheadRussell] p. 111	Theorem *3.24	pm3.24 682
[WhiteheadRussell] p. 112	Theorem *3.35	pm3.35 344
[WhiteheadRussell] p. 112	Theorem *3.3 (Exp)	pm3.3 259
[WhiteheadRussell] p. 112	Theorem *3.31 (Imp)	pm3.31 260
[WhiteheadRussell] p. 112	Theorem *3.26 (Simp)	simpl 108  simplimdc 845
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 109  simprimdc 844
[WhiteheadRussell] p. 112	Theorem *3.33 (Syll)	pm3.33 342
[WhiteheadRussell] p. 112	Theorem *3.34 (Syll)	pm3.34 343
[WhiteheadRussell] p. 112	Theorem *3.37 (Transp)	pm3.37 678
[WhiteheadRussell] p. 113	Fact)	pm3.45 586
[WhiteheadRussell] p. 113	Theorem *3.4	pm3.4 331
[WhiteheadRussell] p. 113	Theorem *3.41	pm3.41 329
[WhiteheadRussell] p. 113	Theorem *3.42	pm3.42 330
[WhiteheadRussell] p. 113	Theorem *3.44	jao 744  pm3.44 704
[WhiteheadRussell] p. 113	Theorem *3.47	anim12 341
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 591
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 774
[WhiteheadRussell] p. 116	Theorem *4.1	con34bdc 856
[WhiteheadRussell] p. 117	Theorem *4.2	biid 170
[WhiteheadRussell] p. 117	Theorem *4.13	notnotbdc 857
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14dc 875
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 683
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 139
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 936  bitr 463
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 392
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 746  pm4.25 747
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 264
[WhiteheadRussell] p. 118	Theorem *4.4	andi 807
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 717
[WhiteheadRussell] p. 118	Theorem *4.32	anass 398
[WhiteheadRussell] p. 118	Theorem *4.33	orass 756
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 461
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 781
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 594
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 811
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 964
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 805
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42r 955
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 933
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 768
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 803  pm4.45 773  pm4.45im 332
[WhiteheadRussell] p. 119	Theorem *10.22	19.26 1457
[WhiteheadRussell] p. 120	Theorem *4.5	anordc 940
[WhiteheadRussell] p. 120	Theorem *4.6	imordc 882  imorr 710
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 317
[WhiteheadRussell] p. 120	Theorem *4.51	ianordc 884
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52im 739
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53r 740
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54dc 887
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55dc 922
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 741  pm4.56 769
[WhiteheadRussell] p. 120	Theorem *4.57	orandc 923  oranim 770
[WhiteheadRussell] p. 120	Theorem *4.61	annimim 675
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62dc 883
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63dc 871
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64dc 885
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65r 676
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66dc 886
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67dc 872
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 386  pm4.71d 390  pm4.71i 388  pm4.71r 387  pm4.71rd 391  pm4.71ri 389
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 812
[WhiteheadRussell] p. 121	Theorem *4.73	iba 298
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 733
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 592  pm4.76 593
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 699  pm4.77 788
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78i 771
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79dc 888
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 696
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81dc 893
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 934
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83dc 935
[WhiteheadRussell] p. 122	Theorem *4.84	imbi1 235
[WhiteheadRussell] p. 122	Theorem *4.85	imbi2 236
[WhiteheadRussell] p. 122	Theorem *4.86	bibi1 239
[WhiteheadRussell] p. 122	Theorem *4.87	bi2.04 247  impexp 261  pm4.87 546
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 590
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11dc 894
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12dc 895
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13dc 897
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14dc 896
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15dc 1367
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 813
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17dc 889
[WhiteheadRussell] p. 124	Theorem *5.18	nbbndc 1372  pm5.18dc 868
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 695
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 684
[WhiteheadRussell] p. 124	Theorem *5.22	xordc 1370
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3dc 1375
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24dc 1376
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2dc 880
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 466
[WhiteheadRussell] p. 125	Theorem *5.4	pm5.4 248
[WhiteheadRussell] p. 125	Theorem *5.5	pm5.5 241
[WhiteheadRussell] p. 125	Theorem *5.6	pm5.6dc 911  pm5.6r 912
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7dc 938
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 345
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 448
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 598
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 902
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 599
[WhiteheadRussell] p. 125	Theorem *5.41	imdi 249  pm5.41 250
[WhiteheadRussell] p. 125	Theorem *5.42	pm5.42 318
[WhiteheadRussell] p. 125	Theorem *5.44	pm5.44 910
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 791
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54dc 903
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55dc 898
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 783
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62dc 929
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63dc 930
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71dc 945
[WhiteheadRussell] p. 125	Theorem *5.501	pm5.501 243
[WhiteheadRussell] p. 126	Theorem *5.74	pm5.74 178
[WhiteheadRussell] p. 126	Theorem *5.75	pm5.75 946
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1614
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1461
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1611
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1867
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2000
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2387
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2388
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2817
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 2960
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 5101
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 5102
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2076  eupickbi 2079
[WhiteheadRussell] p. 235	Definition *30.01	df-fv 5126
[WhiteheadRussell] p. 360	Theorem *54.43	pm54.43 7039