P. 20 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1901-2000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sb9i 1901	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|- ( A. x [ x / y ] ph -> A. y [ y / x ] ph )
Theorem	sbnf2 1902*	Two ways of expressing " x is (effectively) not free in ph." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- ( F/ x ph <-> A. y A. z ( [ y / x ] ph <-> [ z / x ] ph ) )
Theorem	hbsbd 1903*	Deduction version of hbsb 1868. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|- ( ph -> A. x ph )   &    |- ( ph -> A. z ph )   &    |- ( ph -> ( ps -> A. z ps ) )   =>    |- ( ph -> ( [ y / x ] ps -> A. z [ y / x ] ps ) )
Theorem	2sb5 1904*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( [ z / x ] [ w / y ] ph <-> E. x E. y ( ( x = z /\ y = w ) /\ ph ) )
Theorem	2sb6 1905*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( [ z / x ] [ w / y ] ph <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
Theorem	sbcom2v 1906*	Lemma for proving sbcom2 1908. It is the same as sbcom2 1908 but with additional distinct variable constraints on x and y, and on w and z. (Contributed by Jim Kingdon, 19-Feb-2018.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sbcom2v2 1907*	Lemma for proving sbcom2 1908. It is the same as sbcom2v 1906 but removes the distinct variable constraint on x and y. (Contributed by Jim Kingdon, 19-Feb-2018.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sbcom2 1908*	Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sb6a 1909*	Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
|- ( [ y / x ] ph <-> A. x ( x = y -> [ x / y ] ph ) )
Theorem	2sb5rf 1910*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( ph -> A. z ph )   &    |- ( ph -> A. w ph )   =>    |- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )
Theorem	2sb6rf 1911*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( ph -> A. z ph )   &    |- ( ph -> A. w ph )   =>    |- ( ph <-> A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) )
Theorem	dfsb7 1912*	An alternate definition of proper substitution df-sb 1690. By introducing a dummy variable z in the definiens, we are able to eliminate any distinct variable restrictions among the variables x, y, and ph of the definiendum. No distinct variable conflicts arise because z effectively insulates x from y. To achieve this, we use a chain of two substitutions in the form of sb5 1812, first z for x then y for z. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1913 provides a version where ph and z don't have to be distinct. (Contributed by NM, 28-Jan-2004.)
|- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb7f 1913*	This version of dfsb7 1912 does not require that ph and z be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1462 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1690 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A. z ph )   =>    |- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb7af 1914*	An alternate definition of proper substitution df-sb 1690. Similar to dfsb7a 1915 but does not require that ph and z be distinct. Similar to sb7f 1913 in that it involves a dummy variable z, but expressed in terms of A. rather than E.. (Contributed by Jim Kingdon, 5-Feb-2018.)
|- F/ z ph   =>    |- ( [ y / x ] ph <-> A. z ( z = y -> A. x ( x = z -> ph ) ) )
Theorem	dfsb7a 1915*	An alternate definition of proper substitution df-sb 1690. Similar to dfsb7 1912 in that it involves a dummy variable z, but expressed in terms of A. rather than E.. For a version which only requires F/ z ph rather than z and ph being distinct, see sb7af 1914. (Contributed by Jim Kingdon, 5-Feb-2018.)
|- ( [ y / x ] ph <-> A. z ( z = y -> A. x ( x = z -> ph ) ) )
Theorem	sb10f 1916*	Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. (Contributed by NM, 9-May-2005.)
|- ( ph -> A. x ph )   =>    |- ( [ y / z ] ph <-> E. x ( x = y /\ [ x / z ] ph ) )
Theorem	sbid2v 1917*	An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
|- ( [ y / x ] [ x / y ] ph <-> ph )
Theorem	sbelx 1918*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> E. x ( x = y /\ [ x / y ] ph ) )
Theorem	sbel2x 1919*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
Theorem	sbalyz 1920*	Move universal quantifier in and out of substitution. Identical to sbal 1921 except that it has an additional distinct variable constraint on y and z. (Contributed by Jim Kingdon, 29-Dec-2017.)
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
Theorem	sbal 1921*	Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
Theorem	sbal1yz 1922*	Lemma for proving sbal1 1923. Same as sbal1 1923 but with an additional distinct variable constraint on y and z. (Contributed by Jim Kingdon, 23-Feb-2018.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbal1 1923*	A theorem used in elimination of disjoint variable restriction on x and y by replacing it with a distinctor -. A. x x = z. (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbexyz 1924*	Move existential quantifier in and out of substitution. Identical to sbex 1925 except that it has an additional distinct variable constraint on y and z. (Contributed by Jim Kingdon, 29-Dec-2017.)
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
Theorem	sbex 1925*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
Theorem	sbalv 1926*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] A. z ph <-> A. z ps )
Theorem	sbco4lem 1927*	Lemma for sbco4 1928. It replaces the temporary variable v with another temporary variable w. (Contributed by Jim Kingdon, 26-Sep-2018.)
|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
Theorem	sbco4 1928*	Two ways of exchanging two variables. Both sides of the biconditional exchange x and y, either via two temporary variables u and v, or a single temporary w. (Contributed by Jim Kingdon, 25-Sep-2018.)
|- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
Theorem	exsb 1929*	An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
|- ( E. x ph <-> E. y A. x ( x = y -> ph ) )
Theorem	2exsb 1930*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.)
|- ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
Theorem	dvelimALT 1931*	Version of dvelim 1938 that doesn't use ax-10 1439. Because it has different distinct variable constraints than dvelim 1938 and is used in important proofs, it would be better if it had a name which does not end in ALT (ideally more close to set.mm naming). (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelimfv 1932*	Like dvelimf 1936 but with a distinct variable constraint on x and z. (Contributed by Jim Kingdon, 6-Mar-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	hbsb4 1933	A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|- ( ph -> A. z ph )   =>    |- ( -. A. z z = y -> ( [ y / x ] ph -> A. z [ y / x ] ph ) )
Theorem	hbsb4t 1934	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1933). (Contributed by NM, 7-Apr-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A. x A. z ( ph -> A. z ph ) -> ( -. A. z z = y -> ( [ y / x ] ph -> A. z [ y / x ] ph ) ) )
Theorem	nfsb4t 1935	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1933). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof rewritten by Jim Kingdon, 9-May-2018.)
|- ( A. x F/ z ph -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )
Theorem	dvelimf 1936	Version of dvelim 1938 without any variable restrictions. (Contributed by NM, 1-Oct-2002.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelimdf 1937	Deduction form of dvelimf 1936. This version may be useful if we want to avoid ax-17 1462 and use ax-16 1739 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
|- F/ x ph   &    |- F/ z ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> F/ z ch )   &    |- ( ph -> ( z = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( -. A. x x = y -> F/ x ch ) )
Theorem	dvelim 1938*	This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -. A. x x = y as an antecedent. ph normally has z free and can be read ph ( z ), and ps substitutes y for z and can be read ph ( y ). We don't require that x and y 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 A. x A. z, conjoin them, and apply dvelimdf 1937. Other variants of this theorem are dvelimf 1936 (with no distinct variable restrictions) and dvelimALT 1931 (that avoids ax-10 1439). (Contributed by NM, 23-Nov-1994.)
|- ( ph -> A. x ph )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelimor 1939*	Disjunctive distinct variable constraint elimination. A user of this theorem starts with a formula ph (containing z) and a distinct variable constraint between x and z. The theorem makes it possible to replace the distinct variable constraint with the disjunct A. x x = y ( ps is just a version of ph with y substituted for z). (Contributed by Jim Kingdon, 11-May-2018.)
|- F/ x ph   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y \/ F/ x ps )
Theorem	dveeq1 1940*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.)
|- ( -. A. x x = y -> ( y = z -> A. x y = z ) )
Theorem	dveel1 1941*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. x x = y -> ( y e. z -> A. x y e. z ) )
Theorem	dveel2 1942*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. x x = y -> ( z e. y -> A. x z e. y ) )
Theorem	sbal2 1943*	Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. x x = y -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	nfsb4or 1944	A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.)
|- F/ z ph   =>    |- ( A. z z = y \/ F/ z [ y / x ] ph )
1.4.6  Existential uniqueness
Syntax	weu 1945	Extend wff definition to include existential uniqueness ("there exists a unique x such that ph").
wff E! x ph
Syntax	wmo 1946	Extend wff definition to include uniqueness ("there exists at most one x such that ph").
wff E* x ph
Theorem	eujust 1947*	A soundness justification theorem for df-eu 1948, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) )
Definition	df-eu 1948*	Define existential uniqueness, i.e. "there exists exactly one x such that ph." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1970, eu2 1989, eu3 1991, and eu5 1992 (which in some cases we show with a hypothesis ph -> A. y ph in place of a distinct variable condition on y and ph). Double uniqueness is tricky: E! x E! y ph does not mean "exactly one x and one y " (see 2eu4 2038). (Contributed by NM, 5-Aug-1993.)
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Definition	df-mo 1949	Define "there exists at most one x such that ph." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 1999. For another possible definition see mo4 2006. (Contributed by NM, 5-Aug-1993.)
|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
Theorem	euf 1950*	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.)
|- ( ph -> A. y ph )   =>    |- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Theorem	eubidh 1951	Formula-building rule for unique existential quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	eubid 1952	Formula-building rule for unique existential quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	eubidv 1953*	Formula-building rule for unique existential quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	eubii 1954	Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( E! x ph <-> E! x ps )
Theorem	hbeu1 1955	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
|- ( E! x ph -> A. x E! x ph )
Theorem	nfeu1 1956	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x E! x ph
Theorem	nfmo1 1957	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x E* x ph
Theorem	sb8eu 1958	Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ y ph   =>    |- ( E! x ph <-> E! y [ y / x ] ph )
Theorem	sb8mo 1959	Variable substitution for "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- F/ y ph   =>    |- ( E* x ph <-> E* y [ y / x ] ph )
Theorem	nfeudv 1960*	Deduction version of nfeu 1964. Similar to nfeud 1961 but has the additional constraint that x and y must be distinct. (Contributed by Jim Kingdon, 25-May-2018.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E! y ps )
Theorem	nfeud 1961	Deduction version of nfeu 1964. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 25-May-2018.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E! y ps )
Theorem	nfmod 1962	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E* y ps )
Theorem	nfeuv 1963*	Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1964 but has the additional constraint that x and y must be distinct. (Contributed by Jim Kingdon, 23-May-2018.)
|- F/ x ph   =>    |- F/ x E! y ph
Theorem	nfeu 1964	Bound-variable hypothesis builder for existential uniqueness. Note that x and y needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 23-May-2018.)
|- F/ x ph   =>    |- F/ x E! y ph
Theorem	nfmo 1965	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
|- F/ x ph   =>    |- F/ x E* y ph
Theorem	hbeu 1966	Bound-variable hypothesis builder for uniqueness. Note that x and y needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Proof rewritten by Jim Kingdon, 24-May-2018.)
|- ( ph -> A. x ph )   =>    |- ( E! y ph -> A. x E! y ph )
Theorem	hbeud 1967	Deduction version of hbeu 1966. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 25-May-2018.)
|- ( ph -> A. x ph )   &    |- ( ph -> A. y ph )   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> ( E! y ps -> A. x E! y ps ) )
Theorem	sb8euh 1968	Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.)
|- ( ph -> A. y ph )   =>    |- ( E! x ph <-> E! y [ y / x ] ph )
Theorem	cbveu 1969	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x ph <-> E! y ps )
Theorem	eu1 1970*	An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.)
|- ( ph -> A. y ph )   =>    |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
Theorem	euor 1971	Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 21-Oct-2005.)
|- ( ph -> A. x ph )   =>    |- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) )
Theorem	euorv 1972*	Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) )
Theorem	mo2n 1973*	There is at most one of something which does not exist. (Contributed by Jim Kingdon, 2-Jul-2018.)
|- F/ y ph   =>    |- ( -. E. x ph -> E. y A. x ( ph -> x = y ) )
Theorem	mon 1974	There is at most one of something which does not exist. (Contributed by Jim Kingdon, 5-Jul-2018.)
|- ( -. E. x ph -> E* x ph )
Theorem	euex 1975	Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( E! x ph -> E. x ph )
Theorem	eumo0 1976*	Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.)
|- ( ph -> A. y ph )   =>    |- ( E! x ph -> E. y A. x ( ph -> x = y ) )
Theorem	eumo 1977	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
|- ( E! x ph -> E* x ph )
Theorem	eumoi 1978	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
|- E! x ph   =>    |- E* x ph
Theorem	mobidh 1979	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	mobid 1980	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	mobidv 1981*	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	mobii 1982	Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ps <-> ch )   =>    |- ( E* x ps <-> E* x ch )
Theorem	hbmo1 1983	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.)
|- ( E* x ph -> A. x E* x ph )
Theorem	hbmo 1984	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
|- ( ph -> A. x ph )   =>    |- ( E* y ph -> A. x E* y ph )
Theorem	cbvmo 1985	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
|- F/ y ph   &    |- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x ph <-> E* y ps )
Theorem	mo23 1986*	An implication between two definitions of "there exists at most one." (Contributed by Jim Kingdon, 25-Jun-2018.)
|- F/ y ph   =>    |- ( E. y A. x ( ph -> x = y ) -> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	mor 1987*	Converse of mo23 1986 with an additional E. x ph condition. (Contributed by Jim Kingdon, 25-Jun-2018.)
|- F/ y ph   =>    |- ( E. x ph -> ( A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) -> E. y A. x ( ph -> x = y ) ) )
Theorem	modc 1988*	Equivalent definitions of "there exists at most one," given decidable existence. (Contributed by Jim Kingdon, 1-Jul-2018.)
|- F/ y ph   =>    |- (DECID E. x ph -> ( E. y A. x ( ph -> x = y ) <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
Theorem	eu2 1989*	An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.)
|- F/ y ph   =>    |- ( E! x ph <-> ( E. x ph /\ A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
Theorem	eu3h 1990*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) (New usage is discouraged.)
|- ( ph -> A. y ph )   =>    |- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
Theorem	eu3 1991*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.)
|- F/ y ph   =>    |- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
Theorem	eu5 1992	Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
Theorem	exmoeu2 1993	Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
|- ( E. x ph -> ( E* x ph <-> E! x ph ) )
Theorem	moabs 1994	Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
|- ( E* x ph <-> ( E. x ph -> E* x ph ) )
Theorem	exmodc 1995	If existence is decidable, something exists or at most one exists. (Contributed by Jim Kingdon, 30-Jun-2018.)
|- (DECID E. x ph -> ( E. x ph \/ E* x ph ) )
Theorem	exmonim 1996	There is at most one of something which does not exist. Unlike exmodc 1995 there is no decidability condition. (Contributed by Jim Kingdon, 22-Sep-2018.)
|- ( -. E. x ph -> E* x ph )
Theorem	mo2r 1997*	A condition which implies "at most one." (Contributed by Jim Kingdon, 2-Jul-2018.)
|- F/ y ph   =>    |- ( E. y A. x ( ph -> x = y ) -> E* x ph )
Theorem	mo3h 1998*	Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that y not occur in ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (New usage is discouraged.)
|- ( ph -> A. y ph )   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	mo3 1999*	Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that y not occur in ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995.)
|- F/ y ph   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	mo2dc 2000*	Alternate definition of "at most one" where existence is decidable. (Contributed by Jim Kingdon, 2-Jul-2018.)
|- F/ y ph   =>    |- (DECID E. x ph -> ( E* x ph <-> E. y A. x ( ph -> x = y ) ) )