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 5653
[Eisenberg] p. 125	Definition 8.21	df-map 6002
[Enderton] p. 19	Definition	df-tp 3744
[Enderton] p. 26	Exercise 5	unissb 3922
[Enderton] p. 30	Theorem "Distributive laws"	iinin1 4038  iinin2 4037  iinun2 4033  iunin1 4032  iunin2 4031
[Enderton] p. 31	Theorem "De Morgan's laws"	iindif2 4036  iundif2 4034
[Enderton] p. 32	Exercise 20	unineq 3506
[Enderton] p. 33	Exercise 23	iinuni 4050
[Enderton] p. 33	Exercise 25	iununi 4051
[Enderton] p. 33	Exercise 24(a)	iinpw 4055
[Enderton] p. 33	Exercise 24(b)	iunpwss 4056
[Enderton] p. 38	Exercise 6(a)	unipw 4118
[Enderton] p. 41	Lemma 3D	rnex 5108  rnexg 5105
[Enderton] p. 41	Exercise 8	dmuni 4915  rnuni 5039
[Enderton] p. 42	Definition of a function	dffun7 5134  dffun8 5135
[Enderton] p. 43	Definition of function value	funfv2 5377
[Enderton] p. 43	Definition of single-rooted	funcnv 5157
[Enderton] p. 44	Definition (d)	dfima4 4953
[Enderton] p. 47	Theorem 3H	fvco2 5383
[Enderton] p. 50	Theorem 3K(a)	imauni 5466
[Enderton] p. 52	Definition	df-map 6002
[Enderton] p. 53	Exercise 21	coass 5098
[Enderton] p. 53	Exercise 27	dmco 5090
[Enderton] p. 53	Exercise 14(a)	funin 5164
[Enderton] p. 53	Exercise 22(a)	imass2 5025
[Enderton] p. 56	Theorem 3M	erref 5960
[Enderton] p. 57	Lemma 3N	erthi 5971
[Enderton] p. 57	Definition	df-ec 5948
[Enderton] p. 58	Definition	df-qs 5952
[Enderton] p. 61	Exercise 35	df-ec 5948
[Enderton] p. 65	Exercise 56(a)	dmun 4913
[Enderton] p. 79	Definition of operation value	df-ov 5527
[Enderton] p. 129	Definition	df-en 6030
[Enderton] p. 144	Corollary 6K	undif2 3627
[Enderton] p. 145	Figure 38	ffoss 5315
[Gleason] p. 119	Proposition 9-2.4	caovmo 5646
[Hailperin] p. 6	Axiom P1	ax-nin 4079  df-nin 3212
[Hailperin] p. 10	Axiom P2	ax-si 4084
[Hailperin] p. 10	Axiom P3	ax-ins2 4085
[Hailperin] p. 10	Axiom P4	ax-ins3 4086
[Hailperin] p. 10	Axiom P5	ax-xp 4080
[Hailperin] p. 10	Axiom P6	ax-typlower 4087
[Hailperin] p. 10	Axiom P7	ax-cnv 4081
[Hailperin] p. 10	Axiom P8	ax-1c 4082
[Hailperin] p. 10	Axiom P9	ax-sset 4083
[Hamilton] p. 28	Definition 2.1	ax-1 6
[Hamilton] p. 31	Example 2.7(a)	idALT 20
[Hamilton] p. 73	Rule 1	ax-mp 5
[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 5737
[Holmes] p. 134	Definition	df-scan 6327
[Holmes], p. 134	Observation	scancan 6332
[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 6012  mapvalg 6010
[Kunen] p. 31	Definition 10.24	mapex 6007  mapexi 6004
[KuratowskiMostowski] p. 109	Section. Eq. 14	iuniin 3980
[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 6
[Margaris] p. 49	Axiom A2	ax-2 7
[Margaris] p. 49	Axiom A3	ax-3 8
[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 3640
[Margaris] p. 89	Theorem 19.3	19.3 1785  19.3v 1665  rr19.3v 2981
[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 2728
[Margaris] p. 90	Theorem 19.14	exnal 1574
[Margaris] p. 90	Theorem 19.15	albi 1564  ralbi 2751
[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 2692  ralimdv 2694  ralimdva 2693  sbcimdv 3108
[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 2701  r19.21be 2716  r19.21bi 2713  r19.21t 2700  r19.21v 2702  ralrimd 2703  ralrimdv 2704  ralrimdva 2705  ralrimdvv 2709  ralrimdvva 2710  ralrimi 2696  ralrimiv 2697  ralrimiva 2698  ralrimivv 2706  ralrimivva 2707  ralrimivvva 2708  ralrimivw 2699  rexlimi 2732
[Margaris] p. 90	Theorem 19.22	2alimdv 1623  2eximdv 1624  exim 1575  eximd 1770  eximdh 1588  eximdv 1622  rexim 2719  reximdai 2723  reximdv 2726  reximdv2 2724  reximdva 2727  reximdvai 2725  reximi2 2721
[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 2730  r19.23v 2731  rexlimd 2736  rexlimdv 2738  rexlimdv3a 2741  rexlimdva 2739  rexlimdvaa 2740  rexlimdvv 2745  rexlimdvva 2746  rexlimdvw 2742  rexlimiv 2733  rexlimiva 2734  rexlimivv 2744
[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 2748  r19.26-3 2749  r19.26 2747  r19.26m 2750
[Margaris] p. 90	Theorem 19.27	19.27 1869  19.27v 1894  r19.27av 2753  r19.27z 3649  r19.27zv 3650
[Margaris] p. 90	Theorem 19.28	19.28 1870  19.28v 1895  r19.28av 2754  r19.28z 3643  r19.28zv 3646  rr19.28v 2982
[Margaris] p. 90	Theorem 19.29	19.29 1596  19.29r 1597  19.29r2 1598  19.29x 1599  r19.29 2755  r19.29r 2756
[Margaris] p. 90	Theorem 19.30	19.30 1604  r19.30 2757
[Margaris] p. 90	Theorem 19.31	19.31 1876
[Margaris] p. 90	Theorem 19.32	19.32 1875  r19.32v 2758
[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 2759
[Margaris] p. 90	Theorem 19.36	19.36 1871  19.36aiv 1897  19.36i 1872  19.36v 1896  r19.36av 2760  r19.36zv 3651
[Margaris] p. 90	Theorem 19.37	19.37 1873  19.37aiv 1900  19.37v 1899  r19.37 2761  r19.37av 2762  r19.37zv 3647
[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 2763
[Margaris] p. 90	Theorem 19.41	19.41 1879  19.41v 1901  19.41vv 1902  19.41vvv 1903  19.41vvvv 1904  r19.41 2764  r19.41v 2765
[Margaris] p. 90	Theorem 19.42	19.42 1880  19.42v 1905  19.42vv 1907  19.42vvv 1908  r19.42v 2766
[Margaris] p. 90	Theorem 19.43	19.43 1605  r19.43 2767
[Margaris] p. 90	Theorem 19.44	19.44 1877  r19.44av 2768
[Margaris] p. 90	Theorem 19.45	19.45 1878  r19.45av 2769  r19.45zv 3648
[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 3125  rspsbca 3126  stdpc4 2024
[Mendelson] p. 69	Axiom 5	ax-5o 2136  ra5 3131  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 3046
[Mendelson] p. 231	Exercise 4.10(k)	inv1 3578
[Mendelson] p. 231	Exercise 4.10(l)	unv 3579
[Mendelson] p. 231	Exercise 4.10(n)	dfin3 3495
[Mendelson] p. 231	Exercise 4.10(o)	df-nul 3552
[Mendelson] p. 231	Exercise 4.10(q)	dfin4 3496
[Mendelson] p. 231	Exercise 4.10(s)	ddif 3399
[Mendelson] p. 231	Definition of union	dfun3 3494
[Mendelson] p. 235	Exercise 4.12(d)	pwv 3887
[Mendelson] p. 235	Exercise 4.12(n)	uniin 3912
[Mendelson] p. 235	Exercise 4.12(t)	ssdmrn 5100
[Mendelson] p. 254	Proposition 4.22(b)	xpen 6056
[Mendelson] p. 254	Proposition 4.22(c)	xpsnen 6050  xpsneng 6051
[Mendelson] p. 254	Proposition 4.22(d)	xpcomen 6053  xpcomeng 6054
[Mendelson] p. 254	Proposition 4.22(e)	xpassen 6058
[Mendelson] p. 255	Exercise 4.39	endisj 6052
[Mendelson] p. 255	Exercise 4.41	mapprc 6005
[Mendelson] p. 287	Axiom system MK	ru 3046
[Monk1] p. 26	Theorem 2.8(vii)	ssin 3478
[Monk1] p. 33	Theorem 3.2(i)	ssrel 4845
[Monk1] p. 33	Theorem 3.2(ii)	eqrel 4846
[Monk1] p. 34	Definition 3.3	df-opab 4624
[Monk1] p. 36	Theorem 3.7(i)	coi1 5095  coi2 5096
[Monk1] p. 36	Theorem 3.8(v)	dm0 4919  rn0 4970
[Monk1] p. 36	Theorem 3.7(ii)	cnvi 5033
[Monk1] p. 37	Theorem 3.13(x)	dmxp 4924  rnxp 5052
[Monk1] p. 37	Theorem 3.13(ii)	xp0 5045  xp0r 4843
[Monk1] p. 38	Theorem 3.16(ii)	ima0 5014
[Monk1] p. 38	Theorem 3.16(viii)	imai 5011
[Monk1] p. 39	Theorem 3.16(xi)	imassrn 5010
[Monk1] p. 41	Theorem 4.3(i)	fnopfv 5413  funfvop 5401
[Monk1] p. 42	Theorem 4.3(ii)	funopfvb 5362
[Monk1] p. 42	Theorem 4.4(iii)	fvelima 5370
[Monk1] p. 43	Theorem 4.6	funun 5147
[Monk1] p. 43	Theorem 4.8(iv)	dff13 5472  dff13f 5473
[Monk1] p. 50	Definition 5.4	fniunfv 5467
[Monk1] p. 52	Theorem 5.11(viii)	ssint 3943
[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 4607
[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 2669
[Pfenning] p. 17	Definition NNC	notnotrd 105
[Quine] p. 16	Definition 2.1	df-clab 2340  rabid 2788
[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 2862
[Quine] p. 34	Theorem 5.1	eqabb 2459
[Quine] p. 35	Theorem 5.2	abid2 2471  abid2f 2515
[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 3048
[Quine] p. 42	Theorem 6.7	dfsbcq 3049  dfsbcq2 3050
[Quine] p. 43	Theorem 6.8	vex 2863
[Quine] p. 43	Theorem 6.9	isset 2864
[Quine] p. 44	Theorem 7.3	spcgf 2935  spcgv 2940  spcimgf 2933
[Quine] p. 44	Theorem 6.11	spsbc 3059  spsbcd 3060
[Quine] p. 44	Theorem 6.12	elex 2868
[Quine] p. 44	Theorem 6.13	elab 2986  elabg 2987  elabgf 2984
[Quine] p. 44	Theorem 6.14	noel 3555
[Quine] p. 48	Theorem 7.2	snprc 3789
[Quine] p. 48	Definition 7.1	df-pr 3743  df-sn 3742
[Quine] p. 49	Theorem 7.4	snss 3839  snssg 3845
[Quine] p. 49	Theorem 7.5	prss 3862  prssg 3863
[Quine] p. 49	Theorem 7.6	prid1 3828  prid1g 3826  prid2 3829  prid2g 3827  snid 3761  snidg 3759
[Quine] p. 53	Theorem 8.2	unisn 3908  unisng 3909
[Quine] p. 53	Theorem 8.3	uniun 3911
[Quine] p. 54	Theorem 8.6	elssuni 3920
[Quine] p. 54	Theorem 8.7	uni0 3919
[Quine] p. 56	Theorem 8.17	uniabio 4350
[Quine] p. 56	Definition 8.18	dfiota2 4341
[Quine] p. 57	Theorem 8.19	iotaval 4351
[Quine] p. 57	Theorem 8.22	iotanul 4355
[Quine] p. 58	Theorem 8.23	iotaex 4357
[Quine] p. 61	Theorem 9.5	opabid 4696  opelopab 4709  opelopaba 4704  opelopabaf 4711  opelopabf 4712  opelopabg 4706  opelopabga 4701  oprabid 5551
[Quine] p. 64	Definition 9.11	df-xp 4785
[Quine] p. 64	Definition 9.12	df-cnv 4786
[Quine] p. 64	Definition 9.15	df-id 4768
[Quine] p. 65	Theorem 10.3	fun0 5155
[Quine] p. 65	Theorem 10.4	funi 5138
[Quine] p. 65	Theorem 10.5	funsn 5148
[Quine] p. 65	Definition 10.1	df-fun 4790
[Quine] p. 68	Definition 10.11	fv2 5325
[Quine] p. 331	Axiom system NF	ru 3046
[Rosser] p. 236	Theorem IX.4.21	dfpss4 3889
[Rosser] p. 238	Definition IX.9.10,	df-symdif 3217
[Rosser] p. 245	Definition	df-clos1 5874
[Rosser] p. 246	Theorem IX.5.13	clos1base 5879
[Rosser] p. 246	Theorem IX.5.14	clos1conn 5880
[Rosser] p. 247	Theorem IX.5.15	clos1induct 5881
[Rosser] p. 248	Theorem IX.5.16	clos1basesuc 5883  clos1basesucg 5885
[Rosser] p. 252	Definition	df-pw1 4138
[Rosser] p. 255	Theorem IX.6.14	sspw1 4336
[Rosser] p. 275	Definition	df-addc 4379  df-nnc 4380
[Rosser] p. 275	Theorem X.1.1	eladdc 4399
[Rosser] p. 275	Theorem X.1.2	0cnsuc 4402
[Rosser] p. 276	Theorem X.1.3	dfnnc3 5886
[Rosser] p. 276	Theorem X.1.4	peano1 4403
[Rosser] p. 276	Theorem X.1.5	peano2 4404
[Rosser] p. 276	Theorem X.1.6	peano5 4410
[Rosser] p. 276	Theorem X.1.7	nnc0suc 4413
[Rosser] p. 276	Theorem X.1.8	addcid1 4406  addcid2 4408
[Rosser] p. 276	Theorem X.1.9	addccom 4407
[Rosser] p. 277	Corollary 1	addcass 4416
[Rosser] p. 277	Theorem X.1.12	1cnnc 4409
[Rosser] p. 277	Theorem X.1.13	finds 4412  findsd 4411
[Rosser] p. 278	Theorem X.1.14	nncaddccl 4420
[Rosser] p. 279	Theorem X.1.16	elsuc 4414
[Rosser] p. 279	Definition from Ex. X.1.4	df-lefin 4441
[Rosser] p. 281	Definition	df-op 4567  df-proj1 4568  df-proj2 4569
[Rosser] p. 282	Theorem X.2.2	phi11 4597
[Rosser] p. 282	Theorem X.2.3	0cnelphi 4598
[Rosser] p. 282	Theorem X.2.4	phi011 4600
[Rosser] p. 282	Theorem X.2.7	proj1op 4601
[Rosser] p. 283	Theorem X.2.8	proj2op 4602
[Rosser] p. 301	Theorem X.4.29.I	dmsi 5520
[Rosser] p. 302	Theorem X.4.29.II	rnsi 5522
[Rosser] p. 303	Theorem X.4.37	clos1baseima 5884
[Rosser] p. 347	Definition	df-can 6325  df-can 6325
[Rosser] p. 347	Theorem XI.1.6	nenpw1pw 6087
[Rosser] p. 348	Theorem XI.1.8	vncan 6338
[Rosser] p. 348	Theorem XI.1.10	ensn 6059
[Rosser] p. 348	Theorem XI.1.13	enadj 6061
[Rosser] p. 350	Theorem XI.1.14	sbthlem1 6204  sbthlem2 6205
[Rosser] p. 353	Theorem XI.1.15	sbthlem3 6206
[Rosser] p. 357	Theorem XI.1.22	enmap2 6069
[Rosser] p. 357	Theorem XI.1.23	enmap1 6075
[Rosser] p. 360	Theorem XI.1.28	enprmap 6083  enprmapc 6084
[Rosser] p. 368	Theorem XI.1.33	enpw1 6063
[Rosser] p. 368	Theorem XI.1.35	enpw1pw 6076
[Rosser] p. 369	Theorem XI.1.36	enpw 6088
[Rosser] p. 371	Definition	df-nc 6102
[Rosser] p. 372	Definition	df-ncs 6099
[Rosser] p. 372	Theorem XI.2.4	ncpw1pwneg 6202
[Rosser] p. 372	Theorem XI.2.7	df0c2 6138
[Rosser] p. 373	Theorem XI.2.7	0cnc 6139
[Rosser] p. 373	Theorem XI.2.8	1cnc 6140  df1c3 6141  df1c3g 6142
[Rosser] p. 374	Theorem XI.2.10	ncaddccl 6145
[Rosser] p. 374	Theorem XI.2.11	nnssnc 6148
[Rosser] p. 375	Definition	df-lec 6100  df-ltc 6101
[Rosser] p. 375	Theorem XI.2.12	peano4nc 6151
[Rosser] p. 375	Theorem XI.2.14	lecidg 6197
[Rosser] p. 376	Theorem XI.2.14	nclecid 6198
[Rosser] p. 376	Theorem XI.2.15	le0nc 6201  lec0cg 6199
[Rosser] p. 376	Theorem XI.2.16	lecncvg 6200
[Rosser] p. 376	Theorem XI.2.17	ltcpw1pwg 6203
[Rosser] p. 376	Theorem XI.2.19	addlec 6209  addlecncs 6210
[Rosser] p. 376	Theorem XI.2.20	sbth 6207
[Rosser] p. 377	Theorem XI.2.21	ltlenlec 6208
[Rosser] p. 377	Theorem XI.2.22	dflec2 6211
[Rosser] p. 377	Theorem XI.2.23	leaddc1 6215  leaddc2 6216
[Rosser] p. 377	Theorem XI.2.24	nc0le1 6217  nc0suc 6218
[Rosser] p. 378	Definition	df-muc 6103
[Rosser] p. 378	Theorem XI.2.27	mucnc 6132
[Rosser] p. 378	Theorem XI.2.28	muccom 6135
[Rosser] p. 378	Theorem XI.2.29	mucass 6136
[Rosser] p. 379	Theorem XI.2.30	addcdir 6252
[Rosser] p. 379	Theorem XI.2.31	addcdi 6251
[Rosser] p. 379	Theorem XI.2.32	muc0 6143
[Rosser] p. 380	Theorem XI.2.34	muc0or 6253
[Rosser] p. 380	Theorem XI.2.35	lemuc1 6254
[Rosser] p. 381	Definition	df-ce 6107
[Rosser] p. 381	Theorem XI.2.36	ncslemuc 6256
[Rosser] p. 381	Theorem XI.2.37	ncvsq 6257  vvsqenvv 6258
[Rosser] p. 382	Theorem XI.2.38	elce 6176
[Rosser] p. 382	Theorem XI.2.39	cenc 6182
[Rosser] p. 382	Theorem XI.2.42	ce0nnul 6178
[Rosser] p. 383	Theorem XI.2.43	ce0addcnnul 6180
[Rosser] p. 383	Theorem XI.2.44	ce0nn 6181
[Rosser] p. 384	Theorem XI.2.38	ce0nulnc 6185
[Rosser] p. 384	Theorem XI.2.47	ce0nnulb 6183
[Rosser] p. 384	Theorem XI.2.48	ce0ncpw1 6186  cecl 6187  ceclb 6184
[Rosser] p. 385	Theorem XI.2.49	ce0 6191
[Rosser] p. 389	Theorem XI.2.70	ce2 6193
[Rosser] p. 390	Theorem XI.2.71	ce2lt 6221
[Rosser] p. 391	Theorem XI.3.2	addccan2nc 6266  lecadd2 6267
[Rosser] p. 391	Theorem XI.3.3	nclenn 6250
[Rosser] p. 412	Theorem XI.3.24	df-frec 6311
[Rosser] p. 525	Theorem X.1.17	nnsucelr 4429
[Rosser] p. 526	Corollary 1	addcnul1 4453
[Rosser] p. 526	Theorem X.1.18	nndisjeq 4430
[Rosser] p. 526	Theorem X.1.19	prepeano4 4452
[Rosser] p. 526	Theorem X.1.20	addcnnul 4454
[Rosser] p. 527	Definition	df-ltfin 4442  df-ncfin 4443
[Rosser] p. 527	Theorem X.1.21	ssfin 4471
[Rosser] p. 527	Theorem X.1.22	vfinnc 4472
[Rosser] p. 527	Theorem X.1.23	ncfinprop 4475
[Rosser] p. 527	Theorem X.1.24	ncfineleq 4478
[Rosser] p. 527	Theorem X.1.25	ncfinraise 4482
[Rosser] p. 527	Theorem X.1.26	ncfinlower 4484
[Rosser] p. 528	Definition	df-tfin 4444
[Rosser] p. 528	Theorem X.1.27	nnpw1ex 4485
[Rosser] p. 528	Theorem X.1.28	tfinnnul 4491  tfinprop 4490
[Rosser] p. 528	Theorem X.1.29	tfinnul 4492
[Rosser] p. 528	Theorem X.1.30	tfin11 4494
[Rosser] p. 528	Theorem X.1.31	tfinpw1 4495
[Rosser] p. 528	Definition adapted	df-tc 6104
[Rosser] p. 529	Definition	df-evenfin 4445  df-oddfin 4446
[Rosser] p. 529	Theorem X.1.31	ncfintfin 4496
[Rosser] p. 529	Theorem X.1.32	tfindi 4497
[Rosser] p. 529	Theorem X.1.33	tfinlefin 4503  tfinltfin 4502
[Rosser] p. 529	Theorem X.1.35	evenoddnnnul 4515
[Rosser] p. 529	Theorem X.1.36	evenodddisj 4517
[Rosser] p. 529	Theorem X.1.34(a)	tfin1c 4500
[Rosser] p. 530	Definition	df-sfin 4447
[Rosser] p. 530	Theorem X.1.37	eventfin 4518
[Rosser] p. 530	Theorem X.1.38	oddtfin 4519
[Rosser] p. 530	Theorem X.1.39	nnadjoin 4521
[Rosser] p. 530	Theorem X.1.40	nnadjoinpw 4522
[Rosser] p. 530	Theorem X.1.41	nnpweq 4524
[Rosser] p. 530	Theorem X.1.42	sfin01 4529
[Rosser] p. 530	Theorem X.1.43	sfin112 4530
[Rosser] p. 531	Theorem X.1.44	sfindbl 4531
[Rosser] p. 532	Theorem X.1.45	sfintfin 4533
[Rosser] p. 532	Theorem X.1.46	tfinnn 4535
[Rosser] p. 532	Theorem X.1.47	sfinltfin 4536
[Rosser] p. 533	Definition	df-spfin 4448
[Rosser] p. 533	Theorem X.1.48	sfin111 4537
[Rosser] p. 534	Theorem X.1.49	ncvspfin 4539
[Rosser] p. 534	Theorem X.1.50	spfinsfincl 4540
[Rosser] p. 534	Theorem X.1.51	spfininduct 4541
[Rosser] p. 534	Theorem X.1.53	vfinspnn 4542
[Rosser] p. 534	Theorem X.1.54	1cspfin 4544  1cvsfin 4543
[Rosser] p. 534	Theorem X.1.55	tncveqnc1fin 4545
[Rosser] p. 534	Theorem X.1.56	t1csfin1c 4546  vfintle 4547
[Rosser] p. 534	Theorem X.1.57	vfin1cltv 4548
[Rosser] p. 534	Theorem X.1.58	vfinncvntnn 4549  vfinncvntsp 4550
[Rosser] p. 534	Theorem X.1.59	vfinspss 4552
[Rosser] p. 536	Theorem X.1.60	vfinspclt 4553
[Rosser] p. 536	Theorem X.1.61	vfinspeqtncv 4554
[Rosser] p. 536	Theorem X.1.62	vfinncsp 4555
[Rosser] p. 536	Theorem X.1.63	vinf 4556
[Rosser] p. 536	Theorem X.1.65	nulnnn 4557
[Rosser] p. 537	Theorem X.1.66	peano4 4558
[Rosser], p. 417	Definition	df-fin 4381
[Sanford] p. 39	Remark	ax-mp 5
[Sanford] p. 39	Rule 3	mtp-xor 1536
[Sanford] p. 39	Rule 4	mpto2 1534
[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 5029
[Schechter] p. 51	Definition of irreflexivity	intirr 5030
[Schechter] p. 51	Definition of symmetry	cnvsym 5028
[Schechter] p. 51	Definition of transitivity	cotr 5027
[Specker] p. 972	Theorem 2.4	tc11 6229
[Specker] p. 973	Theorem 3.4	nnc3n3p1 6279  nnc3n3p2 6280  nnc3p1n3p2 6281  nncdiv3 6278
[Specker] p. 973	Theorem 4.3	ce2nc1 6194
[Specker] p. 973	Theorem 4.4	ce2ncpw11c 6195
[Specker] p. 973	Theorem 4.5	nchoicelem8 6297
[Specker] p. 973	Theorem 4.8	ce2le 6234
[Specker] p. 973	Theorem 5.2	tcnc1c 6228  tcncv 6227
[Specker] p. 973	Theorem 5.5	tlecg 6231
[Specker] p. 973	Theorem 5.6	letc 6232
[Specker] p. 973	Theorem 5.8	ce2t 6236
[Specker] p. 973	Theorem 6.2	nchoicelem3 6292
[Specker] p. 973	Theorem 6.4	nchoicelem4 6293
[Specker] p. 973	Theorem 6.5	nchoicelem5 6294
[Specker] p. 973	Theorem 6.6	nchoicelem6 6295
[Specker] p. 973	Definition 6.1	df-spac 6275
[Specker] p. 974	Theorem 6.7	nchoicelem7 6296
[Specker] p. 974	Theorem 6.8	nchoicelem9 6298
[Specker] p. 974	Theorem 7.1	nchoicelem12 6301
[Specker] p. 974	Theorem 7.2	nchoicelem17 6306
[Specker] p. 974	Theorem 7.3	nchoicelem19 6308
[Specker] p. 974	Theorem 7.5	nchoice 6309
[Stoll] p. 13	Definition of symmetric difference	symdif1 3520
[Stoll] p. 16	Exercise 4.4	0dif 3622  dif0 3621
[Stoll] p. 16	Exercise 4.8	difdifdir 3638
[Stoll] p. 17	Theorem 5.1(5)	undifv 3625
[Stoll] p. 19	Theorem 5.2(13)	undm 3513
[Stoll] p. 19	Theorem 5.2(13')	indm 3514
[Stoll] p. 20	Remark	invdif 3497
[Stoll] p. 43	Definition	uniiun 4020
[Stoll] p. 44	Definition	intiin 4021
[Stoll] p. 45	Definition	df-iin 3973
[Stoll] p. 45	Definition indexed union	df-iun 3972
[Stoll] p. 176	Theorem 3.4(27)	iman 413
[Stoll] p. 262	Example 4.1	symdif1 3520
[Suppes] p. 22	Theorem 2	eq0 3565
[Suppes] p. 22	Theorem 4	eqss 3288  eqssd 3290  eqssi 3289
[Suppes] p. 23	Theorem 5	ss0 3582  ss0b 3581
[Suppes] p. 23	Theorem 6	sstr 3281
[Suppes] p. 23	Theorem 7	pssirr 3370
[Suppes] p. 23	Theorem 8	pssn2lp 3371
[Suppes] p. 23	Theorem 9	psstr 3374
[Suppes] p. 23	Theorem 10	pssss 3365
[Suppes] p. 26	Theorem 15	inidm 3465
[Suppes] p. 26	Theorem 16	in0 3577
[Suppes] p. 27	Theorem 23	unidm 3408
[Suppes] p. 27	Theorem 24	un0 3576
[Suppes] p. 27	Theorem 25	ssun1 3427
[Suppes] p. 27	Theorem 26	ssequn1 3434
[Suppes] p. 27	Theorem 27	unss 3438
[Suppes] p. 27	Theorem 28	indir 3504
[Suppes] p. 27	Theorem 29	undir 3505
[Suppes] p. 28	Theorem 32	difid 3619  difidALT 3620
[Suppes] p. 29	Theorem 33	difin 3493
[Suppes] p. 29	Theorem 34	indif 3498
[Suppes] p. 29	Theorem 35	undif1 3626
[Suppes] p. 29	Theorem 36	difun2 3630
[Suppes] p. 29	Theorem 37	difin0 3624
[Suppes] p. 29	Theorem 38	disjdif 3623
[Suppes] p. 29	Theorem 39	difundi 3508
[Suppes] p. 29	Theorem 40	difindi 3510
[Suppes] p. 39	Theorem 61	uniss 3913
[Suppes] p. 41	Theorem 70	intsn 3963
[Suppes] p. 42	Theorem 71	intpr 3960  intprg 3961
[Suppes] p. 42	Theorem 78	intun 3959
[Suppes] p. 44	Definition 15(a)	dfiun2 4002  dfiun2g 4000
[Suppes] p. 44	Definition 15(b)	dfiin2 4003
[Suppes] p. 47	Theorem 86	elpw 3729  elpwg 3730
[Suppes] p. 47	Theorem 87	pwid 3736
[Suppes] p. 47	Theorem 89	pw0 4161
[Suppes] p. 48	Theorem 90	pwpw0 3856
[Suppes] p. 52	Theorem 101	xpss12 4856
[Suppes] p. 52	Theorem 102	xpindi 4865  xpindir 4866
[Suppes] p. 52	Theorem 103	xpundi 4833  xpundir 4834
[Suppes] p. 59	Theorem 4	eldm 4899  eldm2 4900
[Suppes] p. 60	Theorem 6	dmin 4914
[Suppes] p. 60	Theorem 8	rnun 5037
[Suppes] p. 60	Theorem 9	rnin 5038
[Suppes] p. 60	Definition 4	dfrn2 4903
[Suppes] p. 61	Theorem 11	brcnv 4893
[Suppes] p. 62	Equation 5	elcnv 4890  elcnv2 4891
[Suppes] p. 62	Theorem 15	cnvin 5036
[Suppes] p. 62	Theorem 16	cnvun 5034
[Suppes] p. 63	Theorem 20	co02 5093
[Suppes] p. 63	Theorem 21	dmcoss 4972
[Suppes] p. 64	Theorem 26	cnvco 4895
[Suppes] p. 64	Theorem 27	coass 5098
[Suppes] p. 65	Theorem 31	resundi 4982
[Suppes] p. 65	Theorem 34	elima 4755  elima2 4756  elima3 4757
[Suppes] p. 65	Theorem 35	imaundi 5040
[Suppes] p. 66	Theorem 40	dminss 5042
[Suppes] p. 66	Theorem 41	imainss 5043
[Suppes] p. 67	Exercise 11	cnvxp 5044
[Suppes] p. 81	Definition 34	dfec2 5949
[Suppes] p. 82	Theorem 72	elec 5965
[Suppes] p. 82	Theorem 73	erth 5969  erth2 5970
[Suppes] p. 83	Theorem 74	erdisj 5973
[Suppes] p. 89	Theorem 96	map0b 6025
[Suppes] p. 89	Theorem 97	map0 6026
[Suppes] p. 89	Theorem 98	mapsn 6027
[Suppes] p. 89	Theorem 99	mapss 6028
[Suppes] p. 92	Theorem 4	unen 6049
[Suppes] p. 98	Exercise 4	fundmen 6044  fundmeng 6045
[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 5529
[TakeutiZaring] p. 14	Proposition 4.14	ru 3046
[TakeutiZaring] p. 15	Exercise 1	elpr 3752  elpr2 3753  elprg 3751
[TakeutiZaring] p. 15	Exercise 2	elsn 3749  elsnc 3757  elsnc2 3763  elsnc2g 3762  elsncg 3756
[TakeutiZaring] p. 15	Exercise 4	sneq 3745  sneqr 3873
[TakeutiZaring] p. 15	Definition 5.1	dfpr2 3750  dfsn2 3748
[TakeutiZaring] p. 16	Definition 5.3	dftp2 3773
[TakeutiZaring] p. 16	Definition 5.5	df-uni 3893
[TakeutiZaring] p. 16	Proposition 5.7	unipr 3906  uniprg 3907
[TakeutiZaring] p. 17	Exercise 1	eltp 3772
[TakeutiZaring] p. 17	Exercise 5	sstr2 3280
[TakeutiZaring] p. 17	Exercise 6	uncom 3409
[TakeutiZaring] p. 17	Exercise 7	incom 3449
[TakeutiZaring] p. 17	Exercise 8	unass 3421
[TakeutiZaring] p. 17	Exercise 9	inass 3466
[TakeutiZaring] p. 17	Exercise 10	indi 3502
[TakeutiZaring] p. 17	Exercise 11	undi 3503
[TakeutiZaring] p. 17	Definition 5.9	df-pss 3262  dfss2 3263
[TakeutiZaring] p. 17	Definition 5.10	df-pw 3725
[TakeutiZaring] p. 18	Exercise 7	unss2 3435
[TakeutiZaring] p. 18	Exercise 9	df-ss 3260  sseqin2 3475
[TakeutiZaring] p. 18	Exercise 10	ssid 3291
[TakeutiZaring] p. 18	Exercise 12	inss1 3476  inss2 3477
[TakeutiZaring] p. 18	Exercise 13	nss 3330
[TakeutiZaring] p. 18	Exercise 15	unieq 3901
[TakeutiZaring] p. 18	Exercise 18	sspwb 4119
[TakeutiZaring] p. 20	Definition	df-rab 2624
[TakeutiZaring] p. 20	Definition 5.14	dfnul2 3553
[TakeutiZaring] p. 20	Proposition 5.15	difid 3619  difidALT 3620
[TakeutiZaring] p. 20	Proposition 5.17(1)	n0 3560  n0f 3559  neq0 3561
[TakeutiZaring] p. 21	Definition 5.20	df-v 2862
[TakeutiZaring] p. 22	Exercise 1	0ss 3580
[TakeutiZaring] p. 22	Exercise 7	ssdif0 3610
[TakeutiZaring] p. 22	Exercise 11	difdif 3393
[TakeutiZaring] p. 22	Exercise 13	undif3 3516
[TakeutiZaring] p. 22	Exercise 14	difss 3394
[TakeutiZaring] p. 22	Exercise 15	sscon 3401
[TakeutiZaring] p. 22	Definition 4.15(3)	df-ral 2620
[TakeutiZaring] p. 22	Definition 4.15(4)	df-rex 2621
[TakeutiZaring] p. 23	Proposition 6.2	xpex 5116  xpexg 5115
[TakeutiZaring] p. 24	Definition 6.4(3)	f1funfun 5264  fun11 5160
[TakeutiZaring] p. 24	Definition 6.4(4)	dffun4 5122
[TakeutiZaring] p. 24	Definition 6.5(1)	dfdm3 4902
[TakeutiZaring] p. 24	Definition 6.5(2)	dfrn3 4904
[TakeutiZaring] p. 24	Definition 6.6(1)	df-res 4789
[TakeutiZaring] p. 25	Exercise 9	inxp 4864
[TakeutiZaring] p. 25	Exercise 13	opelres 4951
[TakeutiZaring] p. 25	Exercise 14	dmres 4987
[TakeutiZaring] p. 25	Exercise 15	resss 4989
[TakeutiZaring] p. 25	Exercise 17	resabs1 4993
[TakeutiZaring] p. 25	Exercise 18	funres 5144
[TakeutiZaring] p. 25	Exercise 29	funco 5143
[TakeutiZaring] p. 25	Exercise 30	f1co 5265
[TakeutiZaring] p. 26	Definition 6.10	eu2 2229
[TakeutiZaring] p. 26	Definition 6.11	fv3 5342
[TakeutiZaring] p. 26	Corollary 6.8(1)	cnvex 5103  cnvexg 5102
[TakeutiZaring] p. 26	Corollary 6.8(2)	dmex 5107  dmexg 5106
[TakeutiZaring] p. 26	Corollary 6.8(3)	rnex 5108  rnexg 5105
[TakeutiZaring] p. 27	Corollary 6.13	fvex 5340
[TakeutiZaring] p. 27	Theorem 6.12(1)	tz6.12-1 5345  tz6.12 5346  tz6.12c 5348
[TakeutiZaring] p. 27	Theorem 6.12(2)	tz6.12-2 5347  tz6.12i 5349
[TakeutiZaring] p. 27	Definition 6.15(1)	df-fn 4791
[TakeutiZaring] p. 27	Definition 6.15(3)	df-f 4792
[TakeutiZaring] p. 27	Definition 6.15(4)	df-fo 4794  wfo 4780
[TakeutiZaring] p. 27	Definition 6.15(5)	df-f1 4793  wf1 4779
[TakeutiZaring] p. 27	Definition 6.15(6)	df-f1o 4795  wf1o 4781
[TakeutiZaring] p. 28	Exercise 4	eqfnfv 5393  eqfnfv2 5394  eqfnfv2f 5397
[TakeutiZaring] p. 28	Exercise 5	fvco 5384
[TakeutiZaring] p. 29	Definition 6.18	df-br 4641
[TakeutiZaring] p. 30	Definition 6.21	eliniseg 5021  iniseg 5023
[TakeutiZaring] p. 30	Definition 6.22	df-eprel 4765
[TakeutiZaring] p. 32	Definition 6.28	df-iso 4797
[TakeutiZaring] p. 33	Proposition 6.30(1)	isoid 5491
[TakeutiZaring] p. 33	Proposition 6.30(2)	isocnv 5492
[TakeutiZaring] p. 33	Proposition 6.30(3)	isotr 5496
[TakeutiZaring] p. 33	Proposition 6.31(1)	isomin 5497
[TakeutiZaring] p. 33	Proposition 6.31(2)	isoini 5498
[TakeutiZaring] p. 34	Proposition 6.33	f1oiso 5500
[TakeutiZaring] p. 40	Proposition 7.20	elssuni 3920
[TakeutiZaring] p. 44	Exercise 2	int0 3941
[TakeutiZaring] p. 44	Exercise 4	intss1 3942
[TakeutiZaring] p. 44	Definition 7.35	df-int 3928
[TakeutiZaring] p. 53	Proposition 7.53	2eu5 2288
[TakeutiZaring] p. 59	Proposition 8.6	iunss2 4012  uniss2 3923
[TakeutiZaring] p. 88	Exercise 1	en0 6043
[TakeutiZaring] p. 95	Definition 10.42	df-map 6002
[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 6156
[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 6
[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 8
[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 7
[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 2589
[WhiteheadRussell] p. 178	Theorem *13.181	pm13.181 2590
[WhiteheadRussell] p. 178	Theorem *13.183	pm13.183 2980
[WhiteheadRussell] p. 185	Theorem *14.121	sbeqalb 3099
[WhiteheadRussell] p. 190	Theorem *14.22	iota4 4358
[WhiteheadRussell] p. 191	Theorem *14.23	iota4an 4359
[WhiteheadRussell] p. 192	Theorem *14.26	eupick 2267  eupickbi 2270