Bibliographic Cross-Reference - New Foundations Explorer

Bibliographic Cross-References   This table collects in one place the bibliographic references made in the New Foundations 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 Higher-Order Logic Explorer

Bibliographic Reference	Description	Higher-Order Logic Explorer Page(s)
[BellMachover] p. 36	Lemma 10.3	idALT 20
[BellMachover] p. 97	Definition 10.1	df-eu 2208
[BellMachover] p. 460	Notation	df-mo 2209
[BellMachover] p. 460	Definition	mo3 2235
[BellMachover] p. 461	Axiom Ext	ax-ext 2334
[BellMachover] p. 462	Theorem 1.1	bm1.1 2338
[ChoquetDD] p. 2	Definition of mapping	df-mpt 5652
[Eisenberg] p. 125	Definition 8.21	df-map 6001
[Enderton] p. 19	Definition	df-tp 3743
[Enderton] p. 26	Exercise 5	unissb 3921
[Enderton] p. 30	Theorem "Distributive laws"	iinin1 4037  iinin2 4036  iinun2 4032  iunin1 4031  iunin2 4030
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 4035  iundif2 4033
[Enderton] p. 32	Exercise 20	unineq 3505
[Enderton] p. 33	Exercise 23	iinuni 4049
[Enderton] p. 33	Exercise 25	iununi 4050
[Enderton] p. 33	Exercise 24(a)	iinpw 4054
[Enderton] p. 33	Exercise 24(b)	iunpwss 4055
[Enderton] p. 38	Exercise 6(a)	unipw 4117
[Enderton] p. 41	Lemma 3D	rnex 5107  rnexg 5104
[Enderton] p. 41	Exercise 8	dmuni 4914  rnuni 5038
[Enderton] p. 42	Definition of a function	dffun7 5133  dffun8 5134
[Enderton] p. 43	Definition of function value	funfv2 5376
[Enderton] p. 43	Definition of single-rooted	funcnv 5156
[Enderton] p. 44	Definition (d)	dfima4 4952
[Enderton] p. 47	Theorem 3H	fvco2 5382
[Enderton] p. 50	Theorem 3K(a)	imauni 5465
[Enderton] p. 52	Definition	df-map 6001
[Enderton] p. 53	Exercise 21	coass 5097
[Enderton] p. 53	Exercise 27	dmco 5089
[Enderton] p. 53	Exercise 14(a)	funin 5163
[Enderton] p. 53	Exercise 22(a)	imass2 5024
[Enderton] p. 56	Theorem 3M	erref 5959
[Enderton] p. 57	Lemma 3N	erthi 5970
[Enderton] p. 57	Definition	df-ec 5947
[Enderton] p. 58	Definition	df-qs 5951
[Enderton] p. 61	Exercise 35	df-ec 5947
[Enderton] p. 65	Exercise 56(a)	dmun 4912
[Enderton] p. 79	Definition of operation value	df-ov 5526
[Enderton] p. 129	Definition	df-en 6029
[Enderton] p. 144	Corollary 6K	undif2 3626
[Enderton] p. 145	Figure 38	ffoss 5314
[Gleason] p. 119	Proposition 9-2.4	caovmo 5645
[Hailperin] p. 6	Axiom P1	ax-nin 4078  df-nin 3211
[Hailperin] p. 10	Axiom P2	ax-si 4083
[Hailperin] p. 10	Axiom P3	ax-ins2 4084
[Hailperin] p. 10	Axiom P4	ax-ins3 4085
[Hailperin] p. 10	Axiom P5	ax-xp 4079
[Hailperin] p. 10	Axiom P6	ax-typlower 4086
[Hailperin] p. 10	Axiom P7	ax-cnv 4080
[Hailperin] p. 10	Axiom P8	ax-1c 4081
[Hailperin] p. 10	Axiom P9	ax-sset 4082
[Hamilton] p. 28	Definition 2.1	ax-1 5
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 8
[Hamilton] p. 74	Rule 2	ax-gen 1546
[Hitchcock] p. 5	Rule A3	mpto1 1533
[Hitchcock] p. 5	Rule A4	mpto2 1534
[Hitchcock] p. 5	Rule A5	mtp-xor 1536
[Holmes] p. 40	Definition	df-txp 5736
[Holmes] p. 134	Definition	df-scan 6326
[Holmes], p. 134	Observation	scancan 6331
[Jech] p. 4	Definition of class	cv 1641  cvjust 2348
[KalishMontague] p. 81	Note 1	ax-9 1654
[KalishMontague] p. 85	Lemma 2	equid 1676
[KalishMontague] p. 85	Lemma 3	equcomi 1679
[KalishMontague] p. 86	Lemma 7	cbvalivw 1674  cbvaliw 1673
[KalishMontague] p. 87	Lemma 8	spimvw 1669  spimw 1668
[KalishMontague] p. 87	Lemma 9	spfw 1691  spw 1694
[Kunen] p. 10	Axiom 0	a9e 1951
[Kunen] p. 24	Definition 10.24	mapval 6011  mapvalg 6009
[Kunen] p. 31	Definition 10.24	mapex 6006  mapexi 6003
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3979
[Levy] p. 338	Axiom	df-clab 2340  df-clel 2349  df-cleq 2346
[Lopez-Astorga] p. 12	Rule 1	mpto1 1533
[Lopez-Astorga] p. 12	Rule 2	mpto2 1534
[Lopez-Astorga] p. 12	Rule 3	mtp-xor 1536
[Margaris] p. 40	Rule C	exlimiv 1634
[Margaris] p. 49	Axiom A1	ax-1 5
[Margaris] p. 49	Axiom A2	ax-2 6
[Margaris] p. 49	Axiom A3	ax-3 7
[Margaris] p. 49	Definition	df-an 360  df-ex 1542  df-or 359  dfbi2 609
[Margaris] p. 51	Theorem 1	idALT 20
[Margaris] p. 56	Theorem 3	syld 40
[Margaris] p. 60	Theorem 8	mth8 138
[Margaris] p. 89	Theorem 19.2	19.2 1659  19.2g 1757  r19.2z 3639
[Margaris] p. 89	Theorem 19.3	19.3 1785  19.3v 1665  rr19.3v 2980
[Margaris] p. 89	Theorem 19.5	alcom 1737
[Margaris] p. 89	Theorem 19.6	alex 1572
[Margaris] p. 89	Theorem 19.7	alnex 1543
[Margaris] p. 89	Theorem 19.8	19.8a 1756
[Margaris] p. 89	Theorem 19.9	19.9 1783  19.9h 1780  19.9v 1664
[Margaris] p. 89	Theorem 19.11	excom 1741  excomim 1742
[Margaris] p. 89	Theorem 19.12	19.12 1847  r19.12 2727
[Margaris] p. 90	Theorem 19.14	exnal 1574
[Margaris] p. 90	Theorem 19.15	albi 1564  ralbi 2750
[Margaris] p. 90	Theorem 19.16	19.16 1860
[Margaris] p. 90	Theorem 19.17	19.17 1861
[Margaris] p. 90	Theorem 19.18	exbi 1581
[Margaris] p. 90	Theorem 19.19	19.19 1862
[Margaris] p. 90	Theorem 19.20	alim 1558  alimd 1764  alimdh 1563  alimdv 1621  ralimdaa 2691  ralimdv 2693  ralimdva 2692  sbcimdv 3107
[Margaris] p. 90	Theorem 19.21	19.21-2 1864  19.21 1796  19.21bi 1758  19.21h 1797  19.21t 1795  19.21v 1890  alrimd 1769  alrimdd 1768  alrimdh 1587  alrimdv 1633  alrimi 1765  alrimih 1565  alrimiv 1631  alrimivv 1632  r19.21 2700  r19.21be 2715  r19.21bi 2712  r19.21t 2699  r19.21v 2701  ralrimd 2702  ralrimdv 2703  ralrimdva 2704  ralrimdvv 2708  ralrimdvva 2709  ralrimi 2695  ralrimiv 2696  ralrimiva 2697  ralrimivv 2705  ralrimivva 2706  ralrimivvva 2707  ralrimivw 2698  rexlimi 2731
[Margaris] p. 90	Theorem 19.22	2alimdv 1623  2eximdv 1624  exim 1575  eximd 1770  eximdh 1588  eximdv 1622  rexim 2718  reximdai 2722  reximdv 2725  reximdv2 2723  reximdva 2726  reximdvai 2724  reximi2 2720
[Margaris] p. 90	Theorem 19.23	19.23 1801  19.23bi 1759  19.23h 1802  19.23t 1800  19.23v 1891  19.23vv 1892  exlimd 1806  exlimdh 1807  exlimdv 1636  exlimdvv 1637  exlimi 1803  exlimih 1804  exlimiv 1634  exlimivv 1635  r19.23 2729  r19.23v 2730  rexlimd 2735  rexlimdv 2737  rexlimdv3a 2740  rexlimdva 2738  rexlimdvaa 2739  rexlimdvv 2744  rexlimdvva 2745  rexlimdvw 2741  rexlimiv 2732  rexlimiva 2733  rexlimivv 2743
[Margaris] p. 90	Theorem 19.24	19.24 1662
[Margaris] p. 90	Theorem 19.25	19.25 1603
[Margaris] p. 90	Theorem 19.26	19.26-2 1594  19.26-3an 1595  19.26 1593  r19.26-2 2747  r19.26-3 2748  r19.26 2746  r19.26m 2749
[Margaris] p. 90	Theorem 19.27	19.27 1869  19.27v 1894  r19.27av 2752  r19.27z 3648  r19.27zv 3649
[Margaris] p. 90	Theorem 19.28	19.28 1870  19.28v 1895  r19.28av 2753  r19.28z 3642  r19.28zv 3645  rr19.28v 2981
[Margaris] p. 90	Theorem 19.29	19.29 1596  19.29r 1597  19.29r2 1598  19.29x 1599  r19.29 2754  r19.29r 2755
[Margaris] p. 90	Theorem 19.30	19.30 1604  r19.30 2756
[Margaris] p. 90	Theorem 19.31	19.31 1876
[Margaris] p. 90	Theorem 19.32	19.32 1875  r19.32v 2757
[Margaris] p. 90	Theorem 19.33	19.33 1607  19.33b 1608
[Margaris] p. 90	Theorem 19.34	19.34 1663
[Margaris] p. 90	Theorem 19.35	19.35 1600  19.35i 1601  19.35ri 1602  r19.35 2758
[Margaris] p. 90	Theorem 19.36	19.36 1871  19.36aiv 1897  19.36i 1872  19.36v 1896  r19.36av 2759  r19.36zv 3650
[Margaris] p. 90	Theorem 19.37	19.37 1873  19.37aiv 1900  19.37v 1899  r19.37 2760  r19.37av 2761  r19.37zv 3646
[Margaris] p. 90	Theorem 19.38	19.38 1794
[Margaris] p. 90	Theorem 19.39	19.39 1661
[Margaris] p. 90	Theorem 19.40	19.40-2 1610  19.40 1609  r19.40 2762
[Margaris] p. 90	Theorem 19.41	19.41 1879  19.41v 1901  19.41vv 1902  19.41vvv 1903  19.41vvvv 1904  r19.41 2763  r19.41v 2764
[Margaris] p. 90	Theorem 19.42	19.42 1880  19.42v 1905  19.42vv 1907  19.42vvv 1908  r19.42v 2765
[Margaris] p. 90	Theorem 19.43	19.43 1605  r19.43 2766
[Margaris] p. 90	Theorem 19.44	19.44 1877  r19.44av 2767
[Margaris] p. 90	Theorem 19.45	19.45 1878  r19.45av 2768  r19.45zv 3647
[Margaris] p. 110	Exercise 2(b)	eu1 2225
[Megill] p. 444	Axiom C5	ax-17 1616  ax17o 2157
[Megill] p. 445	Lemma L12	aecom-o 2151  aecom 1946  ax-10 2140
[Megill] p. 446	Lemma L17	equtrr 1683
[Megill] p. 446	Lemma L18	ax9from9o 2148
[Megill] p. 446	Lemma L19	hbnae-o 2179  hbnae 1955
[Megill] p. 447	Remark 9.1	df-sb 1649  sbid 1922
[Megill] p. 448	Remark 9.6	ax15 2021
[Megill] p. 448	Scheme C4'	ax-5o 2136
[Megill] p. 448	Scheme C5'	ax-4 2135  sp 1747
[Megill] p. 448	Scheme C6'	ax-7 1734
[Megill] p. 448	Scheme C7'	ax-6o 2137
[Megill] p. 448	Scheme C8'	ax-8 1675
[Megill] p. 448	Scheme C9'	ax-12o 2142
[Megill] p. 448	Scheme C10'	ax-9 1654  ax-9o 2138
[Megill] p. 448	Scheme C11'	ax-10o 2139
[Megill] p. 448	Scheme C12'	ax-13 1712
[Megill] p. 448	Scheme C13'	ax-14 1714
[Megill] p. 448	Scheme C14'	ax-15 2143
[Megill] p. 448	Scheme C15'	ax-11o 2141
[Megill] p. 448	Scheme C16'	ax-16 2144
[Megill] p. 448	Theorem 9.4	dral1-o 2154  dral1 1965  dral2-o 2181  dral2 1966  drex1 1967  drex2 1968  drsb1 2022  drsb2 2061
[Megill] p. 449	Theorem 9.7	sbcom2 2114  sbequ 2060  sbid2v 2123
[Megill] p. 450	Example in Appendix	hba1-o 2149  hba1 1786
[Mendelson] p. 36	Lemma 1.8	idALT 20
[Mendelson] p. 69	Axiom 4	rspsbc 3124  rspsbca 3125  stdpc4 2024
[Mendelson] p. 69	Axiom 5	ax-5o 2136  ra5 3130  stdpc5 1798
[Mendelson] p. 81	Rule C	exlimiv 1634
[Mendelson] p. 95	Axiom 6	stdpc6 1687
[Mendelson] p. 95	Axiom 7	stdpc7 1917
[Mendelson] p. 225	Axiom system NBG	ru 3045
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3577
[Mendelson] p. 231	Exercise 4.10(l)	unv 3578
[Mendelson] p. 231	Exercise 4.10(n)	dfin3 3494
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3551
[Mendelson] p. 231	Exercise 4.10(q)	dfin4 3495
[Mendelson] p. 231	Exercise 4.10(s)	ddif 3398
[Mendelson] p. 231	Definition of union	dfun3 3493
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3886
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3911
[Mendelson] p. 235	Exercise 4.12(t)	ssdmrn 5099
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6055
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6049  xpsneng 6050
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6052  xpcomeng 6053
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6057
[Mendelson] p. 255	Exercise 4.39	endisj 6051
[Mendelson] p. 255	Exercise 4.41	mapprc 6004
[Mendelson] p. 287	Axiom system MK	ru 3045
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3477
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4844
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4845
[Monk1] p. 34	Definition 3.3	df-opab 4623
[Monk1] p. 36	Theorem 3.7(i)	coi1 5094  coi2 5095
[Monk1] p. 36	Theorem 3.8(v)	dm0 4918  rn0 4969
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5032
[Monk1] p. 37	Theorem 3.13(x)	dmxp 4923  rnxp 5051
[Monk1] p. 37	Theorem 3.13(ii)	xp0 5044  xp0r 4842
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5013
[Monk1] p. 38	Theorem 3.16(viii)	imai 5010
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5009
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5412  funfvop 5400
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5361
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5369
[Monk1] p. 43	Theorem 4.6	funun 5146
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5471  dff13f 5472
[Monk1] p. 50	Definition 5.4	fniunfv 5466
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3942
[Monk2] p. 105	Axiom C4	ax-5 1557
[Monk2] p. 105	Axiom C7	ax-8 1675
[Monk2] p. 105	Axiom C8	ax-11 1746  ax-11o 2141
[Monk2] p. 105	Axiom (C8)	ax11v 2096
[Monk2] p. 108	Lemma 5	ax-5o 2136
[Monk2] p. 109	Lemma 12	ax-7 1734
[Monk2] p. 109	Lemma 15	equvin 2001  equvini 1987  eqvinop 4606
[Monk2] p. 113	Axiom C5-1	ax-17 1616  ax17o 2157
[Monk2] p. 113	Axiom C5-2	ax-6 1729
[Monk2] p. 113	Axiom C5-3	ax-7 1734
[Monk2] p. 114	Lemma 21	sp 1747
[Monk2] p. 114	Lemma 22	ax5o 1749  hba1-o 2149  hba1 1786
[Monk2] p. 114	Lemma 23	nfia1 1856
[Monk2] p. 114	Lemma 24	nfa2 1855  nfra2 2668
[Pfenning] p. 17	Definition NNC	notnotrd 105
[Quine] p. 16	Definition 2.1	df-clab 2340  rabid 2787
[Quine] p. 17	Definition 2.1''	dfsb7 2119
[Quine] p. 18	Definition 2.7	df-cleq 2346
[Quine] p. 19	Definition 2.9	df-v 2861
[Quine] p. 34	Theorem 5.1	abeq2 2458
[Quine] p. 35	Theorem 5.2	abid2 2470  abid2f 2514
[Quine] p. 40	Theorem 6.1	sb5 2100
[Quine] p. 40	Theorem 6.2	sb56 2098  sb6 2099
[Quine] p. 41	Theorem 6.3	df-clel 2349
[Quine] p. 41	Theorem 6.4	eqid 2353
[Quine] p. 41	Theorem 6.5	eqcom 2355
[Quine] p. 42	Theorem 6.6	df-sbc 3047
[Quine] p. 42	Theorem 6.7	dfsbcq 3048  dfsbcq2 3049
[Quine] p. 43	Theorem 6.8	vex 2862
[Quine] p. 43	Theorem 6.9	isset 2863
[Quine] p. 44	Theorem 7.3	spcgf 2934  spcgv 2939  spcimgf 2932
[Quine] p. 44	Theorem 6.11	spsbc 3058  spsbcd 3059
[Quine] p. 44	Theorem 6.12	elex 2867
[Quine] p. 44	Theorem 6.13	elab 2985  elabg 2986  elabgf 2983
[Quine] p. 44	Theorem 6.14	noel 3554
[Quine] p. 48	Theorem 7.2	snprc 3788
[Quine] p. 48	Definition 7.1	df-pr 3742  df-sn 3741
[Quine] p. 49	Theorem 7.4	snss 3838  snssg 3844
[Quine] p. 49	Theorem 7.5	prss 3861  prssg 3862
[Quine] p. 49	Theorem 7.6	prid1 3827  prid1g 3825  prid2 3828  prid2g 3826  snid 3760  snidg 3758
[Quine] p. 53	Theorem 8.2	unisn 3907  unisng 3908
[Quine] p. 53	Theorem 8.3	uniun 3910
[Quine] p. 54	Theorem 8.6	elssuni 3919
[Quine] p. 54	Theorem 8.7	uni0 3918
[Quine] p. 56	Theorem 8.17	uniabio 4349
[Quine] p. 56	Definition 8.18	dfiota2 4340
[Quine] p. 57	Theorem 8.19	iotaval 4350
[Quine] p. 57	Theorem 8.22	iotanul 4354
[Quine] p. 58	Theorem 8.23	iotaex 4356
[Quine] p. 61	Theorem 9.5	opabid 4695  opelopab 4708  opelopaba 4703  opelopabaf 4710  opelopabf 4711  opelopabg 4705  opelopabga 4700  oprabid 5550
[Quine] p. 64	Definition 9.11	df-xp 4784
[Quine] p. 64	Definition 9.12	df-cnv 4785
[Quine] p. 64	Definition 9.15	df-id 4767
[Quine] p. 65	Theorem 10.3	fun0 5154
[Quine] p. 65	Theorem 10.4	funi 5137
[Quine] p. 65	Theorem 10.5	funsn 5147
[Quine] p. 65	Definition 10.1	df-fun 4789
[Quine] p. 68	Definition 10.11	fv2 5324
[Quine] p. 331	Axiom system NF	ru 3045
[Rosser] p. 236	Theorem IX.4.21	dfpss4 3888
[Rosser] p. 238	Definition IX.9.10,	df-symdif 3216
[Rosser] p. 245	Definition	df-clos1 5873
[Rosser] p. 246	Theorem IX.5.13	clos1base 5878
[Rosser] p. 246	Theorem IX.5.14	clos1conn 5879
[Rosser] p. 247	Theorem IX.5.15	clos1induct 5880
[Rosser] p. 248	Theorem IX.5.16	clos1basesuc 5882  clos1basesucg 5884
[Rosser] p. 252	Definition	df-pw1 4137
[Rosser] p. 255	Theorem IX.6.14	sspw1 4335
[Rosser] p. 275	Definition	df-addc 4378  df-nnc 4379
[Rosser] p. 275	Theorem X.1.1	eladdc 4398
[Rosser] p. 275	Theorem X.1.2	0cnsuc 4401
[Rosser] p. 276	Theorem X.1.3	dfnnc3 5885
[Rosser] p. 276	Theorem X.1.4	peano1 4402
[Rosser] p. 276	Theorem X.1.5	peano2 4403
[Rosser] p. 276	Theorem X.1.6	peano5 4409
[Rosser] p. 276	Theorem X.1.7	nnc0suc 4412
[Rosser] p. 276	Theorem X.1.8	addcid1 4405  addcid2 4407
[Rosser] p. 276	Theorem X.1.9	addccom 4406
[Rosser] p. 277	Corollary 1	addcass 4415
[Rosser] p. 277	Theorem X.1.12	1cnnc 4408
[Rosser] p. 277	Theorem X.1.13	finds 4411  findsd 4410
[Rosser] p. 278	Theorem X.1.14	nncaddccl 4419
[Rosser] p. 279	Theorem X.1.16	elsuc 4413
[Rosser] p. 279	Definition from Ex. X.1.4	df-lefin 4440
[Rosser] p. 281	Definition	df-op 4566  df-proj1 4567  df-proj2 4568
[Rosser] p. 282	Theorem X.2.2	phi11 4596
[Rosser] p. 282	Theorem X.2.3	0cnelphi 4597
[Rosser] p. 282	Theorem X.2.4	phi011 4599
[Rosser] p. 282	Theorem X.2.7	proj1op 4600
[Rosser] p. 283	Theorem X.2.8	proj2op 4601
[Rosser] p. 301	Theorem X.4.29.I	dmsi 5519
[Rosser] p. 302	Theorem X.4.29.II	rnsi 5521
[Rosser] p. 303	Theorem X.4.37	clos1baseima 5883
[Rosser] p. 347	Definition	df-can 6324  df-can 6324
[Rosser] p. 347	Theorem XI.1.6	nenpw1pw 6086
[Rosser] p. 348	Theorem XI.1.8	vncan 6337
[Rosser] p. 348	Theorem XI.1.10	ensn 6058
[Rosser] p. 348	Theorem XI.1.13	enadj 6060
[Rosser] p. 350	Theorem XI.1.14	sbthlem1 6203  sbthlem2 6204
[Rosser] p. 353	Theorem XI.1.15	sbthlem3 6205
[Rosser] p. 357	Theorem XI.1.22	enmap2 6068
[Rosser] p. 357	Theorem XI.1.23	enmap1 6074
[Rosser] p. 360	Theorem XI.1.28	enprmap 6082  enprmapc 6083
[Rosser] p. 368	Theorem XI.1.33	enpw1 6062
[Rosser] p. 368	Theorem XI.1.35	enpw1pw 6075
[Rosser] p. 369	Theorem XI.1.36	enpw 6087
[Rosser] p. 371	Definition	df-nc 6101
[Rosser] p. 372	Definition	df-ncs 6098
[Rosser] p. 372	Theorem XI.2.4	ncpw1pwneg 6201
[Rosser] p. 372	Theorem XI.2.7	df0c2 6137
[Rosser] p. 373	Theorem XI.2.7	0cnc 6138
[Rosser] p. 373	Theorem XI.2.8	1cnc 6139  df1c3 6140  df1c3g 6141
[Rosser] p. 374	Theorem XI.2.10	ncaddccl 6144
[Rosser] p. 374	Theorem XI.2.11	nnssnc 6147
[Rosser] p. 375	Definition	df-lec 6099  df-ltc 6100
[Rosser] p. 375	Theorem XI.2.12	peano4nc 6150
[Rosser] p. 375	Theorem XI.2.14	lecidg 6196
[Rosser] p. 376	Theorem XI.2.14	nclecid 6197
[Rosser] p. 376	Theorem XI.2.15	le0nc 6200  lec0cg 6198
[Rosser] p. 376	Theorem XI.2.16	lecncvg 6199
[Rosser] p. 376	Theorem XI.2.17	ltcpw1pwg 6202
[Rosser] p. 376	Theorem XI.2.19	addlec 6208  addlecncs 6209
[Rosser] p. 376	Theorem XI.2.20	sbth 6206
[Rosser] p. 377	Theorem XI.2.21	ltlenlec 6207
[Rosser] p. 377	Theorem XI.2.22	dflec2 6210
[Rosser] p. 377	Theorem XI.2.23	leaddc1 6214  leaddc2 6215
[Rosser] p. 377	Theorem XI.2.24	nc0le1 6216  nc0suc 6217
[Rosser] p. 378	Definition	df-muc 6102
[Rosser] p. 378	Theorem XI.2.27	mucnc 6131
[Rosser] p. 378	Theorem XI.2.28	muccom 6134
[Rosser] p. 378	Theorem XI.2.29	mucass 6135
[Rosser] p. 379	Theorem XI.2.30	addcdir 6251
[Rosser] p. 379	Theorem XI.2.31	addcdi 6250
[Rosser] p. 379	Theorem XI.2.32	muc0 6142
[Rosser] p. 380	Theorem XI.2.34	muc0or 6252
[Rosser] p. 380	Theorem XI.2.35	lemuc1 6253
[Rosser] p. 381	Definition	df-ce 6106
[Rosser] p. 381	Theorem XI.2.36	ncslemuc 6255
[Rosser] p. 381	Theorem XI.2.37	ncvsq 6256  vvsqenvv 6257
[Rosser] p. 382	Theorem XI.2.38	elce 6175
[Rosser] p. 382	Theorem XI.2.39	cenc 6181
[Rosser] p. 382	Theorem XI.2.42	ce0nnul 6177
[Rosser] p. 383	Theorem XI.2.43	ce0addcnnul 6179
[Rosser] p. 383	Theorem XI.2.44	ce0nn 6180
[Rosser] p. 384	Theorem XI.2.38	ce0nulnc 6184
[Rosser] p. 384	Theorem XI.2.47	ce0nnulb 6182
[Rosser] p. 384	Theorem XI.2.48	ce0ncpw1 6185  cecl 6186  ceclb 6183
[Rosser] p. 385	Theorem XI.2.49	ce0 6190
[Rosser] p. 389	Theorem XI.2.70	ce2 6192
[Rosser] p. 390	Theorem XI.2.71	ce2lt 6220
[Rosser] p. 391	Theorem XI.3.2	addccan2nc 6265  lecadd2 6266
[Rosser] p. 391	Theorem XI.3.3	nclenn 6249
[Rosser] p. 412	Theorem XI.3.24	df-frec 6310
[Rosser] p. 525	Theorem X.1.17	nnsucelr 4428
[Rosser] p. 526	Corollary 1	addcnul1 4452
[Rosser] p. 526	Theorem X.1.18	nndisjeq 4429
[Rosser] p. 526	Theorem X.1.19	prepeano4 4451
[Rosser] p. 526	Theorem X.1.20	addcnnul 4453
[Rosser] p. 527	Definition	df-ltfin 4441  df-ncfin 4442
[Rosser] p. 527	Theorem X.1.21	ssfin 4470
[Rosser] p. 527	Theorem X.1.22	vfinnc 4471
[Rosser] p. 527	Theorem X.1.23	ncfinprop 4474
[Rosser] p. 527	Theorem X.1.24	ncfineleq 4477
[Rosser] p. 527	Theorem X.1.25	ncfinraise 4481
[Rosser] p. 527	Theorem X.1.26	ncfinlower 4483
[Rosser] p. 528	Definition	df-tfin 4443
[Rosser] p. 528	Theorem X.1.27	nnpw1ex 4484
[Rosser] p. 528	Theorem X.1.28	tfinnnul 4490  tfinprop 4489
[Rosser] p. 528	Theorem X.1.29	tfinnul 4491
[Rosser] p. 528	Theorem X.1.30	tfin11 4493
[Rosser] p. 528	Theorem X.1.31	tfinpw1 4494
[Rosser] p. 528	Definition adapted	df-tc 6103
[Rosser] p. 529	Definition	df-evenfin 4444  df-oddfin 4445
[Rosser] p. 529	Theorem X.1.31	ncfintfin 4495
[Rosser] p. 529	Theorem X.1.32	tfindi 4496
[Rosser] p. 529	Theorem X.1.33	tfinlefin 4502  tfinltfin 4501
[Rosser] p. 529	Theorem X.1.35	evenoddnnnul 4514
[Rosser] p. 529	Theorem X.1.36	evenodddisj 4516
[Rosser] p. 529	Theorem X.1.34(a)	tfin1c 4499
[Rosser] p. 530	Definition	df-sfin 4446
[Rosser] p. 530	Theorem X.1.37	eventfin 4517
[Rosser] p. 530	Theorem X.1.38	oddtfin 4518
[Rosser] p. 530	Theorem X.1.39	nnadjoin 4520
[Rosser] p. 530	Theorem X.1.40	nnadjoinpw 4521
[Rosser] p. 530	Theorem X.1.41	nnpweq 4523
[Rosser] p. 530	Theorem X.1.42	sfin01 4528
[Rosser] p. 530	Theorem X.1.43	sfin112 4529
[Rosser] p. 531	Theorem X.1.44	sfindbl 4530
[Rosser] p. 532	Theorem X.1.45	sfintfin 4532
[Rosser] p. 532	Theorem X.1.46	tfinnn 4534
[Rosser] p. 532	Theorem X.1.47	sfinltfin 4535
[Rosser] p. 533	Definition	df-spfin 4447
[Rosser] p. 533	Theorem X.1.48	sfin111 4536
[Rosser] p. 534	Theorem X.1.49	ncvspfin 4538
[Rosser] p. 534	Theorem X.1.50	spfinsfincl 4539
[Rosser] p. 534	Theorem X.1.51	spfininduct 4540
[Rosser] p. 534	Theorem X.1.53	vfinspnn 4541
[Rosser] p. 534	Theorem X.1.54	1cspfin 4543  1cvsfin 4542
[Rosser] p. 534	Theorem X.1.55	tncveqnc1fin 4544
[Rosser] p. 534	Theorem X.1.56	t1csfin1c 4545  vfintle 4546
[Rosser] p. 534	Theorem X.1.57	vfin1cltv 4547
[Rosser] p. 534	Theorem X.1.58	vfinncvntnn 4548  vfinncvntsp 4549
[Rosser] p. 534	Theorem X.1.59	vfinspss 4551
[Rosser] p. 536	Theorem X.1.60	vfinspclt 4552
[Rosser] p. 536	Theorem X.1.61	vfinspeqtncv 4553
[Rosser] p. 536	Theorem X.1.62	vfinncsp 4554
[Rosser] p. 536	Theorem X.1.63	vinf 4555
[Rosser] p. 536	Theorem X.1.65	nulnnn 4556
[Rosser] p. 537	Theorem X.1.66	peano4 4557
[Rosser], p. 417	Definition	df-fin 4380
[Sanford] p. 39	Rule 3	mtp-xor 1536
[Sanford] p. 39	Rule 4	mpto2 1534
[Sanford] p. 39	Rule is sometimes called "detachment," since it detaches the minor premise	ax-mp 8
[Sanford] p. 39	Rule says, "if ` ` is not true, and ` ` implies ` ` , then ` ` must also be not true." Modus tollens is short for "modus tollendo tollens," a Latin phrase that means "the mood that by denying affirms"	mto 167
[Sanford] p. 40	Rule 1	mpto1 1533
[Schechter] p. 51	Definition of antisymmetry	intasym 5028
[Schechter] p. 51	Definition of irreflexivity	intirr 5029
[Schechter] p. 51	Definition of symmetry	cnvsym 5027
[Schechter] p. 51	Definition of transitivity	cotr 5026
[Specker] p. 972	Theorem 2.4	tc11 6228
[Specker] p. 973	Theorem 3.4	nnc3n3p1 6278  nnc3n3p2 6279  nnc3p1n3p2 6280  nncdiv3 6277
[Specker] p. 973	Theorem 4.3	ce2nc1 6193
[Specker] p. 973	Theorem 4.4	ce2ncpw11c 6194
[Specker] p. 973	Theorem 4.5	nchoicelem8 6296
[Specker] p. 973	Theorem 4.8	ce2le 6233
[Specker] p. 973	Theorem 5.2	tcnc1c 6227  tcncv 6226
[Specker] p. 973	Theorem 5.5	tlecg 6230
[Specker] p. 973	Theorem 5.6	letc 6231
[Specker] p. 973	Theorem 5.8	ce2t 6235
[Specker] p. 973	Theorem 6.2	nchoicelem3 6291
[Specker] p. 973	Theorem 6.4	nchoicelem4 6292
[Specker] p. 973	Theorem 6.5	nchoicelem5 6293
[Specker] p. 973	Theorem 6.6	nchoicelem6 6294
[Specker] p. 973	Definition 6.1	df-spac 6274
[Specker] p. 974	Theorem 6.7	nchoicelem7 6295
[Specker] p. 974	Theorem 6.8	nchoicelem9 6297
[Specker] p. 974	Theorem 7.1	nchoicelem12 6300
[Specker] p. 974	Theorem 7.2	nchoicelem17 6305
[Specker] p. 974	Theorem 7.3	nchoicelem19 6307
[Specker] p. 974	Theorem 7.5	nchoice 6308
[Stoll] p. 13	Definition of symmetric difference	symdif1 3519
[Stoll] p. 16	Exercise 4.4	0dif 3621  dif0 3620
[Stoll] p. 16	Exercise 4.8	difdifdir 3637
[Stoll] p. 17	Theorem 5.1(5)	undifv 3624
[Stoll] p. 19	Theorem 5.2(13)	undm 3512
[Stoll] p. 19	Theorem 5.2(13')	indm 3513
[Stoll] p. 20	Remark	invdif 3496
[Stoll] p. 43	Definition	uniiun 4019
[Stoll] p. 44	Definition	intiin 4020
[Stoll] p. 45	Definition	df-iin 3972
[Stoll] p. 45	Definition indexed union	df-iun 3971
[Stoll] p. 176	Theorem 3.4(27)	iman 413
[Stoll] p. 262	Example 4.1	symdif1 3519
[Suppes] p. 22	Theorem 2	eq0 3564
[Suppes] p. 22	Theorem 4	eqss 3287  eqssd 3289  eqssi 3288
[Suppes] p. 23	Theorem 5	ss0 3581  ss0b 3580
[Suppes] p. 23	Theorem 6	sstr 3280
[Suppes] p. 23	Theorem 7	pssirr 3369
[Suppes] p. 23	Theorem 8	pssn2lp 3370
[Suppes] p. 23	Theorem 9	psstr 3373
[Suppes] p. 23	Theorem 10	pssss 3364
[Suppes] p. 26	Theorem 15	inidm 3464
[Suppes] p. 26	Theorem 16	in0 3576
[Suppes] p. 27	Theorem 23	unidm 3407
[Suppes] p. 27	Theorem 24	un0 3575
[Suppes] p. 27	Theorem 25	ssun1 3426
[Suppes] p. 27	Theorem 26	ssequn1 3433
[Suppes] p. 27	Theorem 27	unss 3437
[Suppes] p. 27	Theorem 28	indir 3503
[Suppes] p. 27	Theorem 29	undir 3504
[Suppes] p. 28	Theorem 32	difid 3618  difidALT 3619
[Suppes] p. 29	Theorem 33	difin 3492
[Suppes] p. 29	Theorem 34	indif 3497
[Suppes] p. 29	Theorem 35	undif1 3625
[Suppes] p. 29	Theorem 36	difun2 3629
[Suppes] p. 29	Theorem 37	difin0 3623
[Suppes] p. 29	Theorem 38	disjdif 3622
[Suppes] p. 29	Theorem 39	difundi 3507
[Suppes] p. 29	Theorem 40	difindi 3509
[Suppes] p. 39	Theorem 61	uniss 3912
[Suppes] p. 41	Theorem 70	intsn 3962
[Suppes] p. 42	Theorem 71	intpr 3959  intprg 3960
[Suppes] p. 42	Theorem 78	intun 3958
[Suppes] p. 44	Definition 15(a)	dfiun2 4001  dfiun2g 3999
[Suppes] p. 44	Definition 15(b)	dfiin2 4002
[Suppes] p. 47	Theorem 86	elpw 3728  elpwg 3729
[Suppes] p. 47	Theorem 87	pwid 3735
[Suppes] p. 47	Theorem 89	pw0 4160
[Suppes] p. 48	Theorem 90	pwpw0 3855
[Suppes] p. 52	Theorem 101	xpss12 4855
[Suppes] p. 52	Theorem 102	xpindi 4864  xpindir 4865
[Suppes] p. 52	Theorem 103	xpundi 4832  xpundir 4833
[Suppes] p. 59	Theorem 4	eldm 4898  eldm2 4899
[Suppes] p. 60	Theorem 6	dmin 4913
[Suppes] p. 60	Theorem 8	rnun 5036
[Suppes] p. 60	Theorem 9	rnin 5037
[Suppes] p. 60	Definition 4	dfrn2 4902
[Suppes] p. 61	Theorem 11	brcnv 4892
[Suppes] p. 62	Equation 5	elcnv 4889  elcnv2 4890
[Suppes] p. 62	Theorem 15	cnvin 5035
[Suppes] p. 62	Theorem 16	cnvun 5033
[Suppes] p. 63	Theorem 20	co02 5092
[Suppes] p. 63	Theorem 21	dmcoss 4971
[Suppes] p. 64	Theorem 26	cnvco 4894
[Suppes] p. 64	Theorem 27	coass 5097
[Suppes] p. 65	Theorem 31	resundi 4981
[Suppes] p. 65	Theorem 34	elima 4754  elima2 4755  elima3 4756
[Suppes] p. 65	Theorem 35	imaundi 5039
[Suppes] p. 66	Theorem 40	dminss 5041
[Suppes] p. 66	Theorem 41	imainss 5042
[Suppes] p. 67	Exercise 11	cnvxp 5043
[Suppes] p. 81	Definition 34	dfec2 5948
[Suppes] p. 82	Theorem 72	elec 5964
[Suppes] p. 82	Theorem 73	erth 5968  erth2 5969
[Suppes] p. 83	Theorem 74	erdisj 5972
[Suppes] p. 89	Theorem 96	map0b 6024
[Suppes] p. 89	Theorem 97	map0 6025
[Suppes] p. 89	Theorem 98	mapsn 6026
[Suppes] p. 89	Theorem 99	mapss 6027
[Suppes] p. 92	Theorem 4	unen 6048
[Suppes] p. 98	Exercise 4	fundmen 6043  fundmeng 6044
[TakeutiZaring] p. 8	Axiom 1	ax-ext 2334
[TakeutiZaring] p. 13	Definition 4.5	df-cleq 2346
[TakeutiZaring] p. 13	Proposition 4.6	df-clel 2349
[TakeutiZaring] p. 13	Proposition 4.9	cvjust 2348
[TakeutiZaring] p. 13	Proposition 4.7(3)	eqtr 2370
[TakeutiZaring] p. 14	Definition 4.16	df-oprab 5528
[TakeutiZaring] p. 14	Proposition 4.14	ru 3045
[TakeutiZaring] p. 15	Exercise 1	elpr 3751  elpr2 3752  elprg 3750
[TakeutiZaring] p. 15	Exercise 2	elsn 3748  elsnc 3756  elsnc2 3762  elsnc2g 3761  elsncg 3755
[TakeutiZaring] p. 15	Exercise 4	sneq 3744  sneqr 3872
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3749  dfsn2 3747
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3772
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3892
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3905  uniprg 3906
[TakeutiZaring] p. 17	Exercise 1	eltp 3771
[TakeutiZaring] p. 17	Exercise 5	sstr2 3279
[TakeutiZaring] p. 17	Exercise 6	uncom 3408
[TakeutiZaring] p. 17	Exercise 7	incom 3448
[TakeutiZaring] p. 17	Exercise 8	unass 3420
[TakeutiZaring] p. 17	Exercise 9	inass 3465
[TakeutiZaring] p. 17	Exercise 10	indi 3501
[TakeutiZaring] p. 17	Exercise 11	undi 3502
[TakeutiZaring] p. 17	Definition 5.9	df-pss 3261  dfss2 3262
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3724
[TakeutiZaring] p. 18	Exercise 7	unss2 3434
[TakeutiZaring] p. 18	Exercise 9	df-ss 3259  sseqin2 3474
[TakeutiZaring] p. 18	Exercise 10	ssid 3290
[TakeutiZaring] p. 18	Exercise 12	inss1 3475  inss2 3476
[TakeutiZaring] p. 18	Exercise 13	nss 3329
[TakeutiZaring] p. 18	Exercise 15	unieq 3900
[TakeutiZaring] p. 18	Exercise 18	sspwb 4118
[TakeutiZaring] p. 20	Definition	df-rab 2623
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3552
[TakeutiZaring] p. 20	Proposition 5.15	difid 3618  difidALT 3619
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0 3559  n0f 3558  neq0 3560
[TakeutiZaring] p. 21	Definition 5.20	df-v 2861
[TakeutiZaring] p. 22	Exercise 1	0ss 3579
[TakeutiZaring] p. 22	Exercise 7	ssdif0 3609
[TakeutiZaring] p. 22	Exercise 11	difdif 3392
[TakeutiZaring] p. 22	Exercise 13	undif3 3515
[TakeutiZaring] p. 22	Exercise 14	difss 3393
[TakeutiZaring] p. 22	Exercise 15	sscon 3400
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2619
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2620
[TakeutiZaring] p. 23	Proposition 6.2	xpex 5115  xpexg 5114
[TakeutiZaring] p. 24	Definition 6.4(3)	f1funfun 5263  fun11 5159
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5121
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4901
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4903
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4788
[TakeutiZaring] p. 25	Exercise 9	inxp 4863
[TakeutiZaring] p. 25	Exercise 13	opelres 4950
[TakeutiZaring] p. 25	Exercise 14	dmres 4986
[TakeutiZaring] p. 25	Exercise 15	resss 4988
[TakeutiZaring] p. 25	Exercise 17	resabs1 4992
[TakeutiZaring] p. 25	Exercise 18	funres 5143
[TakeutiZaring] p. 25	Exercise 29	funco 5142
[TakeutiZaring] p. 25	Exercise 30	f1co 5264
[TakeutiZaring] p. 26	Definition 6.10	eu2 2229
[TakeutiZaring] p. 26	Definition 6.11	fv3 5341
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5102  cnvexg 5101
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 5106  dmexg 5105
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 5107  rnexg 5104
[TakeutiZaring] p. 27	Corollary 6.13	fvex 5339
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5344  tz6.12 5345  tz6.12c 5347
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5346  tz6.12i 5348
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 4790
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 4791
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 4793  wfo 4779
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 4792  wf1 4778
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 4794  wf1o 4780
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5392  eqfnfv2 5393  eqfnfv2f 5396
[TakeutiZaring] p. 28	Exercise 5	fvco 5383
[TakeutiZaring] p. 29	Definition 6.18	df-br 4640
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5020  iniseg 5022
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4764
[TakeutiZaring] p. 32	Definition 6.28	df-iso 4796
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5490
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5491
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5495
[TakeutiZaring] p. 33	Proposition 6.31(1)	isomin 5496
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5497
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5499
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3919
[TakeutiZaring] p. 44	Exercise 2	int0 3940
[TakeutiZaring] p. 44	Exercise 4	intss1 3941
[TakeutiZaring] p. 44	Definition 7.35	df-int 3927
[TakeutiZaring] p. 53	Proposition 7.53	2eu5 2288
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 4011  uniss2 3922
[TakeutiZaring] p. 88	Exercise 1	en0 6042
[TakeutiZaring] p. 95	Definition 10.42	df-map 6001
[Tarski] p. 67	Axiom B5	ax-4 2135
[Tarski] p. 67	Scheme B5	sp 1747
[Tarski] p. 68	Lemma 6	equid 1676  equid1 2158  equid1ALT 2176
[Tarski] p. 69	Lemma 7	equcomi 1679
[Tarski] p. 70	Lemma 14	spim 1975  spime 1976  spimeh 1667
[Tarski] p. 70	Lemma 16	ax-11 1746  ax-11o 2141  ax11i 1647
[Tarski] p. 70	Lemmas 16 and 17	sb6 2099
[Tarski] p. 75	Axiom B7	ax9v 1655
[Tarski] p. 77	Axiom B6 (p. 75) of system S2	ax-17 1616  ax17o 2157
[Tarski], p. 75	Scheme B8 of system S2	ax-13 1712  ax-14 1714  ax-8 1675
[WhiteheadRussell] p. 86	Theorem *110.64	1p1e2c 6155
[WhiteheadRussell] p. 96	Axiom *1.2	pm1.2 499
[WhiteheadRussell] p. 96	Axiom *1.3	olc 373
[WhiteheadRussell] p. 96	Axiom *1.4	pm1.4 375
[WhiteheadRussell] p. 96	Axiom *1.5 (Assoc)	pm1.5 508
[WhiteheadRussell] p. 97	Axiom *1.6 (Sum)	orim2 814
[WhiteheadRussell] p. 100	Theorem *2.01	pm2.01 160
[WhiteheadRussell] p. 100	Theorem *2.02	ax-1 5
[WhiteheadRussell] p. 100	Theorem *2.03	con2 108
[WhiteheadRussell] p. 100	Theorem *2.04	pm2.04 76
[WhiteheadRussell] p. 100	Theorem *2.05	imim2 49
[WhiteheadRussell] p. 100	Theorem *2.06	imim1 70
[WhiteheadRussell] p. 101	Theorem *2.1	pm2.1 406
[WhiteheadRussell] p. 101	Theorem *2.06	barbara 2301  syl 15
[WhiteheadRussell] p. 101	Theorem *2.07	pm2.07 385
[WhiteheadRussell] p. 101	Theorem *2.08	id 19  idALT 20
[WhiteheadRussell] p. 101	Theorem *2.11	exmid 404
[WhiteheadRussell] p. 101	Theorem *2.12	notnot1 114
[WhiteheadRussell] p. 101	Theorem *2.13	pm2.13 407
[WhiteheadRussell] p. 102	Theorem *2.14	notnot2 104
[WhiteheadRussell] p. 102	Theorem *2.15	con1 120
[WhiteheadRussell] p. 103	Theorem *2.16	con3 126  con3th 924
[WhiteheadRussell] p. 103	Theorem *2.17	ax-3 7
[WhiteheadRussell] p. 103	Theorem *2.18	pm2.18 102
[WhiteheadRussell] p. 104	Theorem *2.2	orc 374
[WhiteheadRussell] p. 104	Theorem *2.3	pm2.3 555
[WhiteheadRussell] p. 104	Theorem *2.21	pm2.21 100
[WhiteheadRussell] p. 104	Theorem *2.24	pm2.24 101
[WhiteheadRussell] p. 104	Theorem *2.25	pm2.25 393
[WhiteheadRussell] p. 104	Theorem *2.26	pm2.26 853
[WhiteheadRussell] p. 104	Theorem *2.27	pm2.27 35
[WhiteheadRussell] p. 104	Theorem *2.31	pm2.31 511
[WhiteheadRussell] p. 105	Theorem *2.32	pm2.32 512
[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 935
[WhiteheadRussell] p. 106	Theorem *2.4	pm2.4 558
[WhiteheadRussell] p. 106	Theorem *2.41	pm2.41 556
[WhiteheadRussell] p. 106	Theorem *2.42	pm2.42 557
[WhiteheadRussell] p. 106	Theorem *2.43	pm2.43 47
[WhiteheadRussell] p. 106	Theorem *2.45	pm2.45 386
[WhiteheadRussell] p. 106	Theorem *2.46	pm2.46 387
[WhiteheadRussell] p. 107	Theorem *2.5	pm2.5 144
[WhiteheadRussell] p. 107	Theorem *2.6	pm2.6 162
[WhiteheadRussell] p. 107	Theorem *2.47	pm2.47 388
[WhiteheadRussell] p. 107	Theorem *2.48	pm2.48 389
[WhiteheadRussell] p. 107	Theorem *2.49	pm2.49 390
[WhiteheadRussell] p. 107	Theorem *2.51	pm2.51 145
[WhiteheadRussell] p. 107	Theorem *2.52	pm2.52 147
[WhiteheadRussell] p. 107	Theorem *2.53	pm2.53 362
[WhiteheadRussell] p. 107	Theorem *2.54	pm2.54 363
[WhiteheadRussell] p. 107	Theorem *2.55	orel1 371
[WhiteheadRussell] p. 107	Theorem *2.56	orel2 372
[WhiteheadRussell] p. 107	Theorem *2.61	pm2.61 163
[WhiteheadRussell] p. 107	Theorem *2.62	pm2.62 398
[WhiteheadRussell] p. 107	Theorem *2.63	pm2.63 763
[WhiteheadRussell] p. 107	Theorem *2.64	pm2.64 764
[WhiteheadRussell] p. 107	Theorem *2.65	pm2.65 164
[WhiteheadRussell] p. 107	Theorem *2.67	pm2.67-2 391  pm2.67 392
[WhiteheadRussell] p. 107	Theorem *2.521	pm2.521 146
[WhiteheadRussell] p. 107	Theorem *2.621	pm2.621 397
[WhiteheadRussell] p. 108	Theorem *2.8	pm2.8 823
[WhiteheadRussell] p. 108	Theorem *2.68	pm2.68 399
[WhiteheadRussell] p. 108	Theorem *2.69	looinv 174
[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 822
[WhiteheadRussell] p. 108	Theorem *2.76	pm2.76 821
[WhiteheadRussell] p. 108	Theorem *2.77	ax-2 6
[WhiteheadRussell] p. 108	Theorem *2.81	pm2.81 824
[WhiteheadRussell] p. 108	Theorem *2.82	pm2.82 825
[WhiteheadRussell] p. 108	Theorem *2.83	pm2.83 71
[WhiteheadRussell] p. 108	Theorem *2.85	pm2.85 826
[WhiteheadRussell] p. 108	Theorem *2.86	pm2.86 94
[WhiteheadRussell] p. 111	Theorem *3.1	pm3.1 484
[WhiteheadRussell] p. 111	Theorem *3.2	pm3.2 434  pm3.2im 137
[WhiteheadRussell] p. 111	Theorem *3.11	pm3.11 485
[WhiteheadRussell] p. 111	Theorem *3.12	pm3.12 486
[WhiteheadRussell] p. 111	Theorem *3.13	pm3.13 487
[WhiteheadRussell] p. 111	Theorem *3.14	pm3.14 488
[WhiteheadRussell] p. 111	Theorem *3.21	pm3.21 435
[WhiteheadRussell] p. 111	Theorem *3.22	pm3.22 436
[WhiteheadRussell] p. 111	Theorem *3.24	pm3.24 852
[WhiteheadRussell] p. 112	Theorem *3.35	pm3.35 570
[WhiteheadRussell] p. 112	Theorem *3.3 (Exp)	pm3.3 431
[WhiteheadRussell] p. 112	Theorem *3.31 (Imp)	pm3.31 432
[WhiteheadRussell] p. 112	Theorem *3.26 (Simp)	simpl 443  simplim 143
[WhiteheadRussell] p. 112	Theorem *3.27 (Simp)	simpr 447  simprim 142
[WhiteheadRussell] p. 112	Theorem *3.33 (Syll)	pm3.33 568
[WhiteheadRussell] p. 112	Theorem *3.34 (Syll)	pm3.34 569
[WhiteheadRussell] p. 112	Theorem *3.37 (Transp)	pm3.37 562
[WhiteheadRussell] p. 113	Fact)	pm3.45 807
[WhiteheadRussell] p. 113	Theorem *3.4	pm3.4 544
[WhiteheadRussell] p. 113	Theorem *3.41	pm3.41 542
[WhiteheadRussell] p. 113	Theorem *3.42	pm3.42 543
[WhiteheadRussell] p. 113	Theorem *3.44	jao 498  pm3.44 497
[WhiteheadRussell] p. 113	Theorem *3.47	prth 554
[WhiteheadRussell] p. 113	Theorem *3.43 (Comp)	pm3.43 832
[WhiteheadRussell] p. 114	Theorem *3.48	pm3.48 806
[WhiteheadRussell] p. 116	Theorem *4.1	con34b 283
[WhiteheadRussell] p. 117	Theorem *4.2	biid 227
[WhiteheadRussell] p. 117	Theorem *4.11	notbi 286
[WhiteheadRussell] p. 117	Theorem *4.12	con2bi 318
[WhiteheadRussell] p. 117	Theorem *4.13	notnot 282
[WhiteheadRussell] p. 117	Theorem *4.14	pm4.14 561
[WhiteheadRussell] p. 117	Theorem *4.15	pm4.15 564
[WhiteheadRussell] p. 117	Theorem *4.21	bicom 191
[WhiteheadRussell] p. 117	Theorem *4.22	biantr 897  bitr 689
[WhiteheadRussell] p. 117	Theorem *4.24	pm4.24 624
[WhiteheadRussell] p. 117	Theorem *4.25	oridm 500  pm4.25 501
[WhiteheadRussell] p. 118	Theorem *4.3	ancom 437
[WhiteheadRussell] p. 118	Theorem *4.4	andi 837
[WhiteheadRussell] p. 118	Theorem *4.31	orcom 376
[WhiteheadRussell] p. 118	Theorem *4.32	anass 630
[WhiteheadRussell] p. 118	Theorem *4.33	orass 510
[WhiteheadRussell] p. 118	Theorem *4.36	anbi1 687
[WhiteheadRussell] p. 118	Theorem *4.37	orbi1 686
[WhiteheadRussell] p. 118	Theorem *4.38	pm4.38 842
[WhiteheadRussell] p. 118	Theorem *4.39	pm4.39 841
[WhiteheadRussell] p. 118	Definition *4.34	df-3an 936
[WhiteheadRussell] p. 119	Theorem *4.41	ordi 834
[WhiteheadRussell] p. 119	Theorem *4.42	pm4.42 926
[WhiteheadRussell] p. 119	Theorem *4.43	pm4.43 893
[WhiteheadRussell] p. 119	Theorem *4.44	pm4.44 560
[WhiteheadRussell] p. 119	Theorem *4.45	orabs 828  pm4.45 669  pm4.45im 545
[WhiteheadRussell] p. 120	Theorem *4.5	anor 475
[WhiteheadRussell] p. 120	Theorem *4.6	imor 401
[WhiteheadRussell] p. 120	Theorem *4.7	anclb 530
[WhiteheadRussell] p. 120	Theorem *4.51	ianor 474
[WhiteheadRussell] p. 120	Theorem *4.52	pm4.52 477
[WhiteheadRussell] p. 120	Theorem *4.53	pm4.53 478
[WhiteheadRussell] p. 120	Theorem *4.54	pm4.54 479
[WhiteheadRussell] p. 120	Theorem *4.55	pm4.55 480
[WhiteheadRussell] p. 120	Theorem *4.56	ioran 476  pm4.56 481
[WhiteheadRussell] p. 120	Theorem *4.57	oran 482  pm4.57 483
[WhiteheadRussell] p. 120	Theorem *4.61	pm4.61 415
[WhiteheadRussell] p. 120	Theorem *4.62	pm4.62 408
[WhiteheadRussell] p. 120	Theorem *4.63	pm4.63 410
[WhiteheadRussell] p. 120	Theorem *4.64	pm4.64 361
[WhiteheadRussell] p. 120	Theorem *4.65	pm4.65 416
[WhiteheadRussell] p. 120	Theorem *4.66	pm4.66 409
[WhiteheadRussell] p. 120	Theorem *4.67	pm4.67 417
[WhiteheadRussell] p. 120	Theorem *4.71	pm4.71 611  pm4.71d 615  pm4.71i 613  pm4.71r 612  pm4.71rd 616  pm4.71ri 614
[WhiteheadRussell] p. 121	Theorem *4.72	pm4.72 846
[WhiteheadRussell] p. 121	Theorem *4.73	iba 489
[WhiteheadRussell] p. 121	Theorem *4.74	biorf 394
[WhiteheadRussell] p. 121	Theorem *4.76	jcab 833  pm4.76 836
[WhiteheadRussell] p. 121	Theorem *4.77	jaob 758  pm4.77 762
[WhiteheadRussell] p. 121	Theorem *4.78	pm4.78 565
[WhiteheadRussell] p. 121	Theorem *4.79	pm4.79 566
[WhiteheadRussell] p. 122	Theorem *4.8	pm4.8 354
[WhiteheadRussell] p. 122	Theorem *4.81	pm4.81 355
[WhiteheadRussell] p. 122	Theorem *4.82	pm4.82 894
[WhiteheadRussell] p. 122	Theorem *4.83	pm4.83 895
[WhiteheadRussell] p. 122	Theorem *4.84	imbi1 313
[WhiteheadRussell] p. 122	Theorem *4.85	imbi2 314
[WhiteheadRussell] p. 122	Theorem *4.86	bibi1 317
[WhiteheadRussell] p. 122	Theorem *4.87	bi2.04 350  impexp 433  pm4.87 567
[WhiteheadRussell] p. 123	Theorem *5.1	pm5.1 830
[WhiteheadRussell] p. 123	Theorem *5.11	pm5.11 854
[WhiteheadRussell] p. 123	Theorem *5.12	pm5.12 855
[WhiteheadRussell] p. 123	Theorem *5.13	pm5.13 857
[WhiteheadRussell] p. 123	Theorem *5.14	pm5.14 856
[WhiteheadRussell] p. 124	Theorem *5.15	pm5.15 859
[WhiteheadRussell] p. 124	Theorem *5.16	pm5.16 860
[WhiteheadRussell] p. 124	Theorem *5.17	pm5.17 858
[WhiteheadRussell] p. 124	Theorem *5.18	nbbn 347  pm5.18 345
[WhiteheadRussell] p. 124	Theorem *5.19	pm5.19 349
[WhiteheadRussell] p. 124	Theorem *5.21	pm5.21 831
[WhiteheadRussell] p. 124	Theorem *5.22	xor 861
[WhiteheadRussell] p. 124	Theorem *5.23	dfbi3 863
[WhiteheadRussell] p. 124	Theorem *5.24	pm5.24 864
[WhiteheadRussell] p. 124	Theorem *5.25	dfor2 400
[WhiteheadRussell] p. 125	Theorem *5.3	pm5.3 692
[WhiteheadRussell] p. 125	Theorem *5.4	pm5.4 351
[WhiteheadRussell] p. 125	Theorem *5.5	pm5.5 326
[WhiteheadRussell] p. 125	Theorem *5.6	pm5.6 878
[WhiteheadRussell] p. 125	Theorem *5.7	pm5.7 900
[WhiteheadRussell] p. 125	Theorem *5.31	pm5.31 571
[WhiteheadRussell] p. 125	Theorem *5.32	pm5.32 617
[WhiteheadRussell] p. 125	Theorem *5.33	pm5.33 848
[WhiteheadRussell] p. 125	Theorem *5.35	pm5.35 869
[WhiteheadRussell] p. 125	Theorem *5.36	pm5.36 849
[WhiteheadRussell] p. 125	Theorem *5.41	imdi 352  pm5.41 353
[WhiteheadRussell] p. 125	Theorem *5.42	pm5.42 531
[WhiteheadRussell] p. 125	Theorem *5.44	pm5.44 877
[WhiteheadRussell] p. 125	Theorem *5.53	pm5.53 771
[WhiteheadRussell] p. 125	Theorem *5.54	pm5.54 870
[WhiteheadRussell] p. 125	Theorem *5.55	pm5.55 867
[WhiteheadRussell] p. 125	Theorem *5.61	pm5.61 693
[WhiteheadRussell] p. 125	Theorem *5.62	pm5.62 889
[WhiteheadRussell] p. 125	Theorem *5.63	pm5.63 890
[WhiteheadRussell] p. 125	Theorem *5.71	pm5.71 902
[WhiteheadRussell] p. 125	Theorem *5.501	pm5.501 330
[WhiteheadRussell] p. 126	Theorem *5.74	pm5.74 235
[WhiteheadRussell] p. 126	Theorem *5.75	pm5.75 903
[WhiteheadRussell] p. 147	Theorem *10.22	19.26 1593
[WhiteheadRussell] p. 150	Theorem *10.3	alsyl 1615
[WhiteheadRussell] p. 159	Theorem *11.07	pm11.07 2115
[WhiteheadRussell] p. 160	Theorem *11.21	alrot3 1738
[WhiteheadRussell] p. 163	Theorem *11.42	19.40-2 1610
[WhiteheadRussell] p. 164	Theorem *11.5	2nalexn 1573
[WhiteheadRussell] p. 164	Theorem *11.51	2exnexn 1580
[WhiteheadRussell] p. 164	Theorem *11.53	pm11.53 1893
[WhiteheadRussell] p. 175	Definition *14.02	df-eu 2208
[WhiteheadRussell] p. 178	Theorem *13.18	pm13.18 2588
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2589
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2979
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3098
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 4357
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 4358
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2267  eupickbi 2270