mmtheorems21 - Metamath Proof Explorer

Home	Metamath Proof Explorer	< Previous Next >
		Browser slow? Try the Unicode version.

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Color key:

Metamath Proof Explorer
(1-11257)

Hilbert Space Explorer
(11258-12844)

Users' Mathboxes
(12845-19026)

**Statement List for Metamath Proof Explorer -** 2001-2100 - Page 21 of 191
Type	Label	Description
Statement

Theorem	sbal1 2001	A theorem used in elimination of disjoint variable restriction on and by replacing it with a distinctor .


Theorem	sbal 2002	Move universal quantifier in and out of substitution.


Theorem	sbex 2003	Move existential quantifier in and out of substitution.


Theorem	sbalv 2004	Quantify with new variable inside substitution.


Theorem	exsb 2005	An equivalent expression for existence.


Theorem	2exsb 2006	An equivalent expression for double existence.
$/\$

Theorem	dvelim 2007	This theorem can be used to eliminate a distinct variable restriction on and and replace it with the "distinctor" as an antecedent. normally has free and can be read , and substitutes for and can be read . We don't require that and be distinct: if they aren't, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent. To obtain a closed-theorem form of this inference, prefix the hypotheses with , conjoin them, and apply dvelimdf 1898. Other variants of this theorem are dvelimf 1897 (with no distinct variable restrictions), dvelimfALT 1794 (that avoids ax-11 1597), and dvelimALT 2008 (that avoids ax-10 1596).


Theorem	dvelimALT 2008	Version of dvelim 2007 that doesn't use ax-10 1596. (See dvelimfALT 1794 for a version that doesn't use ax-11 1597.)


Theorem	dveeq1 2009	Quantifier introduction when one pair of variables is distinct.


Theorem	dveeq1ALT 2010	Version of dveeq1 2009 using ax-16 1854 instead of ax-17 1605.


Theorem	dveel1 2011	Quantifier introduction when one pair of variables is distinct.


Theorem	dveel2 2012	Quantifier introduction when one pair of variables is distinct.


Theorem	sbal2 2013	Move quantifier in and out of substitution.


Theorem	ax15 2014	Axiom ax-15 2015 is redundant if we assume ax-17 1605. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'. Note that is a dummy variable introduced in the proof. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 2012 and ax-17 1605. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. This theorem should not be referenced in any proof. Instead, use ax-15 2015 below so that theorems needing ax-15 2015 can be more easily identified.


Axiom	ax-15 2015	Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 1605; see theorem ax15 2014. Alternately, ax-17 1605 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1605. We retain ax-15 2015 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1605, which might be easier to study for some theoretical purposes.


Theorem	ax17el 2016	Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-17 1605 considered as a metatheorem.)


Theorem	dveel2ALT 2017	Version of dveel2 2012 using ax-16 1854 instead of ax-17 1605.


Theorem	ax11eq 2018	Basis step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Atomic formula for equality predicate.


Theorem	ax11el 2019	Basis step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Atomic formula for membership predicate.


Theorem	ax11f 2020	Basis step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. We can start with any formula in which is not free.


Theorem	ax11indn 2021	Induction step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Negation case.


Theorem	ax11indi 2022	Induction step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Implication case.


Theorem	ax11indalem 2023	Lemma for ax11inda2 2025 and ax11inda 2026. [Auxiliary lemma - not displayed.]

Theorem	ax11inda2ALT 2024	A proof of ax11inda2 2025 that is slightly more direct.


Theorem	ax11inda2 2025	Induction step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Quantification case. When and are distinct, this theorem avoids the dummy variables needed by the more general ax11inda 2026.


Theorem	ax11inda 2026	Induction step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Quantification case. (When and are distinct, ax11inda2 2025 may be used instead to avoid the dummy variable in the proof.)


Theorem	a12stdy1 2027	Part of a study related to ax-12 1598. The consequent introduces a new variable . There are no distinct variable restrictions.


Theorem	a12stdy2 2028	Part of a study related to ax-12 1598. The consequent is quantified with a different variable. There are no distinct variable restrictions.
$/\$

Theorem	a12stdy3 2029	Part of a study related to ax-12 1598. The consequent introduces two new variables. There are no distinct variable restrictions.
$/\$

Theorem	a12stdy4 2030	Part of a study related to ax-12 1598. The second antecedent of ax-12 1598 is replaced. There are no distinct variable restrictions.


Theorem	a12lem1 2031	Proof of first hypothesis of a12study 2033.


Theorem	a12lem2 2032	Proof of second hypothesis of a12study 2033.


Theorem	a12study 2033	Rederivation of axiom ax-12 1598 from two shorter formulas, without using ax-12 1598. See a12lem1 2031 and a12lem2 2032 for the proofs of the hypotheses (using ax-12 1598). This is the only known breakdown of ax-12 1598 into shorter formulas. See a12studyALT 2034 for an alternate proof. Note that the proof depends on ax-11o 1864, whose proof ax11o 1863 depends on ax-12 1598, meaning that we would have to replace ax-11 1597 with ax-11o 1864 in an axiomatization that uses the hypotheses in place of ax-12 1598. Whether this can be avoided is an open problem.


Theorem	a12studyALT 2034	Alternate proof of a12study 2033, also without using ax-12 1598.


Theorem	a12study2 2035	Reprove ax-12 1598 using dvelimfALT2 1858, showing that ax-12 1598 can be replaced by dveeq2 1856 if we allow distinct variables in axioms other than ax-17 1605. (Contributed by Andrew Salmon, 21-Jul-2011.)


Theorem	a12study3 2036	Rederivation of axiom ax-12 1598 from two other formulas, without using ax-12 1598. See equvini 1811 and equveli 1812 for the proofs of the hypotheses (using ax-12 1598). Although the second hypothesis (when expanded to primitives) is longer than ax-12 1598, an open problem is whether it can be derived without ax-12 1598 or from a simpler axiom. Note also that the proof depends on ax-11o 1864, whose proof ax11o 1863 depends on ax-12 1598, meaning that we would have to replace ax-11 1597 with ax-11o 1864 in an axiomatization that uses the hypotheses in place of ax-12 1598. Whether this can be avoided is an open problem.
$/\$

Existential uniqueness

Syntax	weu 2037	Extend wff definition to include existential uniqueness ("there exists a unique such that ").


Syntax	wmo 2038	Extend wff definition to include uniqueness ("there exists at most one such that ").


Theorem	eujust 2039	A soundness justification theorem for df-eu 2041, showing that the definition is equivalent to itself with its dummy variable renamed. Note that and needn't be distinct variables. See eujustALT 2040 for a proof that provides an example of how it can be achieved through the use of dvelim 2007. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)


Theorem	eujustALT 2040	A soundness justification theorem for df-eu 2041, showing that the definition is equivalent to itself with its dummy variable renamed. Note that and needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 2007.


Definition	df-eu 2041	Define existential uniqueness, i.e. "there exists exactly one such that ." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2052, eu2 2056, eu3 2057, and eu5 2070 (which in some cases we show with a hypothesis in place of a distinct variable condition on and ). Double uniqueness is tricky: does not mean "exactly one and one " (see 2eu4 2115).


Definition	df-mo 2042	Define "there exists at most one such that ." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2062. For other possible definitions see mo2 2060 and mo4 2064.


Theorem	euf 2043	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition.


Theorem	eubid 2044	Formula-building rule for uniqueness quantifier (deduction rule).


Theorem	eubidv 2045	Formula-building rule for uniqueness quantifier (deduction rule).


Theorem	eubii 2046	Introduce uniqueness quantifier to both sides of an equivalence.


Theorem	hbeu1 2047	Bound-variable hypothesis builder for uniqueness.


Theorem	hbeu 2048	Bound-variable hypothesis builder for "at most one." Note that and needn't be distinct (this makes the proof more difficult).


Theorem	hbeud 2049	Deduction version of hbeu 2048.


Theorem	sb8eu 2050	Variable substitution in uniqueness quantifier. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.)


Theorem	cbveu 2051	Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.)


Theorem	eu1 2052	An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110.
$/\$

Theorem	mo 2053	Equivalent definitions of "there exists at most one."
$/\$

Theorem	euex 2054	Existential uniqueness implies existence. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)


Theorem	eumo0 2055	Existential uniqueness implies "at most one."


Theorem	eu2 2056	An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26.
$/\$ $/\$

Theorem	eu3 2057	An alternate way to express existential uniqueness.
$/\$

Theorem	euor 2058	Introduce a disjunct into a uniqueness quantifier.
$/\$ $\/$

Theorem	euorv 2059	Introduce a disjunct into a uniqueness quantifier.
$/\$ $\/$

Theorem	mo2 2060	Alternate definition of "at most one."


Theorem	sbmo 2061	Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)


Theorem	mo3 2062	Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that not occur in in place of our hypothesis.
$/\$

Theorem	mo4f 2063	"At most one" expressed using implicit substitution.
$/\$

Theorem	mo4 2064	"At most one" expressed using implicit substitution.
$/\$

Theorem	mobid 2065	Formula-building rule for "at most one" quantifier (deduction rule).


Theorem	mobii 2066	Formula-building rule for "at most one" quantifier (inference rule).


Theorem	hbmo1 2067	Bound-variable hypothesis builder for "at most one."


Theorem	hbmo 2068	Bound-variable hypothesis builder for "at most one."


Theorem	cbvmo 2069	Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.)


Theorem	eu5 2070	Uniqueness in terms of "at most one."
$/\$

Theorem	eu4 2071	Uniqueness using implicit substitution.
$/\$ $/\$

Theorem	eumo 2072	Existential uniqueness implies "at most one."


Theorem	eumoi 2073	"At most one" inferred from existential uniqueness.


Theorem	exmoeu 2074	Existence in terms of "at most one" and uniqueness.


Theorem	exmoeu2 2075	Existence implies "at most one" is equivalent to uniqueness.


Theorem	moabs 2076	Absorption of existence condition by "at most one."


Theorem	exmo 2077	Something exists or at most one exists.
$\/$

Theorem	immo 2078	"At most one" is preserved through implication (notice wff reversal).


Theorem	immoi 2079	"At most one" is preserved through implication (notice wff reversal).


Theorem	moimv 2080	Move antecedent outside of "at most one."


Theorem	euimmo 2081	Uniqueness implies "at most one" through implication.


Theorem	euim 2082	Add existential uniqueness quantifiers to an implication. Note the reversed implication in the antecedent. (The proof was shortened by Andrew Salmon, 14-Jun-2011.)
$/\$

Theorem	moan 2083	"At most one" is still the case when a conjunct is added.
$/\$

Theorem	moani 2084	"At most one" is still true when a conjunct is added.
$/\$

Theorem	moor 2085	"At most one" is still the case when a disjunct is removed.
$\/$

Theorem	mooran1 2086	"At most one" imports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
$\/$ $/\$

Theorem	mooran2 2087	"At most one" exports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
$\/$ $/\$

Theorem	moanim 2088	Introduction of a conjunct into "at most one" quantifier.
$/\$

Theorem	euan 2089	Introduction of a conjunct into uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
$/\$ $/\$

Theorem	moanimv 2090	Introduction of a conjunct into "at most one" quantifier.
$/\$

Theorem	moaneu 2091	Nested "at most one" and uniqueness quantifiers.
$/\$

Theorem	moanmo 2092	Nested "at most one" quantifiers.
$/\$

Theorem	euanv 2093	Introduction of a conjunct into uniqueness quantifier.
$/\$ $/\$

Theorem	mopick 2094	"At most one" picks a variable value, eliminating an existential quantifier.
$/\$ $/\$

Theorem	eupick 2095	Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing such that is true, and there is also an (actually the same one) such that and are both true, then implies regardless of . This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192.
$/\$ $/\$

Theorem	eupicka 2096	Version of eupick 2095 with closed formulas.
$/\$ $/\$

Theorem	eupickb 2097	Existential uniqueness "pick" showing wff equivalence.
$/\$ $/\$ $/\$

Theorem	eupickbi 2098	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
$/\$

Theorem	mopick2 2099	"At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 1731. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	euor2 2100	Introduce or eliminate a disjunct in a uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)
$\/$

MPE Home Contents

< Previous Next >