P. 24 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2301-2400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2sb6rf 2301*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.)
|- F/ z ph   &    |- F/ w ph   =>    |- ( ph <-> A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) )
Theorem	sb7f 2302*	This version of dfsb7 2304 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-5 1766 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1806 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ z ph   =>    |- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb7h 2303*	This version of dfsb7 2304 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-5 1766 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1806 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	dfsb7 2304*	An alternate definition of proper substitution df-sb 1806. 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 2279, first z for x then y for z. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2458. Theorem sb7h 2303 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	sb10f 2305*	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.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ x ph   =>    |- ( [ y / z ] ph <-> E. x ( x = y /\ [ x / z ] ph ) )
Theorem	sbid2v 2306*	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 2307*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> E. x ( x = y /\ [ x / y ] ph ) )
Theorem	sbel2x 2308*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
|- ( ph <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
Theorem	sbal1 2309*	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, 15-May-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2018.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbal2 2310*	Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 3-Oct-2018.)
|- ( -. A. x x = y -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbal 2311*	Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
Theorem	sbex 2312*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.)
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
Theorem	sbalv 2313*	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 2314*	Lemma for sbco4 2315. 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 2315*	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	2sb8e 2316*	An equivalent expression for double existence. (Contributed by Wolf Lammen, 2-Nov-2019.)
|- ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )
Theorem	exsb 2317*	An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
|- ( E. x ph <-> E. y A. x ( x = y -> ph ) )
Theorem	2exsb 2318*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
|- ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
1.6  Existential uniqueness
Syntax	weu 2319	Extend wff definition to include existential uniqueness ("there exists a unique x such that ph").
wff E! x ph
Syntax	wmo 2320	Extend wff definition to include uniqueness ("there exists at most one x such that ph").
wff E* x ph
Theorem	eujust 2321*	A soundness justification theorem for df-eu 2323, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. See eujustALT 2322 for a proof that provides an example of how it can be achieved through the use of dvelim 2186. (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 ) )
Theorem	eujustALT 2322*	Alternate proof of eujust 2321 illustrating the use of dvelim 2186. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) )
Definition	df-eu 2323*	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 2359, eu2 2358, eu3v 2347, and eu5 2345 (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 2405). (Contributed by NM, 12-Aug-1993.)
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Definition	df-mo 2324	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 2356. For other possible definitions see mo2 2328 and mo4 2366. (Contributed by NM, 8-Mar-1995.)
|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
Theorem	euequ1 2325*	Equality has existential uniqueness. Special case of eueq1 3199 proved using only predicate calculus. The proof needs y = z be free of x. This is ensured by having x and y be distinct. Alternatively, a distinctor -. A. x x = y could have been used instead. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof shortened by Wolf Lammen, 8-Sep-2019.)
|- E! x x = y
Theorem	mo2v 2326*	Alternate definition of "at most one." Unlike mo2 2328, which is slightly more general, it does not depend on ax-11 1937 and ax-13 2104, whence it is preferable within predicate logic. Elsewhere, most theorems depend on these axioms anyway, so this advantage is no longer important. (Contributed by Wolf Lammen, 27-May-2019.) (Proof shortened by Wolf Lammen, 10-Nov-2019.)
|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
Theorem	euf 2327*	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2018.)
|- F/ y ph   =>    |- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Theorem	mo2 2328*	Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.) Restrict dummy variable z. (Revised by Wolf Lammen, 28-May-2019.)
|- F/ y ph   =>    |- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
Theorem	nfeu1 2329	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 2330	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	nfeud2 2331	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by Wolf Lammen, 4-Oct-2018.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/ x E! y ps )
Theorem	nfmod2 2332	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/ x E* y ps )
Theorem	nfeud 2333	Deduction version of nfeu 2335. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E! y ps )
Theorem	nfmod 2334	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	nfeu 2335	Bound-variable hypothesis builder for uniqueness. Note that x and y needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x ph   =>    |- F/ x E! y ph
Theorem	nfmo 2336	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
|- F/ x ph   =>    |- F/ x E* y ph
Theorem	eubid 2337	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	mobid 2338	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	eubidv 2339*	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	mobidv 2340*	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	eubii 2341	Introduce uniqueness 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	mobii 2342	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	euex 2343	Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2360. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)
|- ( E! x ph -> E. x ph )
Theorem	exmo 2344	Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)
|- ( E. x ph \/ E* x ph )
Theorem	eu5 2345	Uniqueness in terms of "at most one." Revised to reduce dependencies on axioms. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.)
|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
Theorem	exmoeu2 2346	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	eu3v 2347*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) Add a distinct variable condition on ph. (Revised by Wolf Lammen, 29-May-2019.)
|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
Theorem	eumo 2348	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
|- ( E! x ph -> E* x ph )
Theorem	eumoi 2349	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
|- E! x ph   =>    |- E* x ph
Theorem	moabs 2350	Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
|- ( E* x ph <-> ( E. x ph -> E* x ph ) )
Theorem	exmoeu 2351	Existence in terms of "at most one" and uniqueness. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Wolf Lammen, 5-Dec-2018.)
|- ( E. x ph <-> ( E* x ph -> E! x ph ) )
Theorem	sb8eu 2352	Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Aug-2019.)
|- F/ y ph   =>    |- ( E! x ph <-> E! y [ y / x ] ph )
Theorem	sb8mo 2353	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	cbveu 2354	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	cbvmo 2355	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	mo3 2356*	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.) (Proof shortened by Wolf Lammen, 18-Aug-2019.)
|- F/ y ph   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	mo 2357*	Equivalent definitions of "there exists at most one." (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Dec-2018.)
|- F/ y ph   =>    |- ( E. y A. x ( ph -> x = y ) <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	eu2 2358*	An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.) (Proof shortened by Wolf Lammen, 2-Dec-2018.)
|- F/ y ph   =>    |- ( E! x ph <-> ( E. x ph /\ A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
Theorem	eu1 2359*	An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 29-Oct-2018.)
|- F/ y ph   =>    |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
Theorem	euexALT 2360	Alternate proof of euex 2343. Shorter but uses more axioms. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E! x ph -> E. x ph )
Theorem	euor 2361	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.)
|- F/ x ph   =>    |- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) )
Theorem	euorv 2362*	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) )
Theorem	euor2 2363	Introduce or eliminate a disjunct in a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)
|- ( -. E. x ph -> ( E! x ( ph \/ ps ) <-> E! x ps ) )
Theorem	sbmo 2364*	Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( [ y / x ] E* z ph <-> E* z [ y / x ] ph )
Theorem	mo4f 2365*	"At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )
Theorem	mo4 2366*	"At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ ps ) -> x = y ) )
Theorem	eu4 2367*	Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E! x ph <-> ( E. x ph /\ A. x A. y ( ( ph /\ ps ) -> x = y ) ) )
Theorem	moim 2368	"At most one" reverses implication. (Contributed by NM, 22-Apr-1995.)
|- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )
Theorem	moimi 2369	"At most one" reverses implication. (Contributed by NM, 15-Feb-2006.)
|- ( ph -> ps )   =>    |- ( E* x ps -> E* x ph )
Theorem	moa1 2370	If an implication holds for at most one value, then its consequent holds for at most one value. See also ala1 1718 and exa1 1719. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.) (Revised by BJ, 29-Mar-2021.)
|- ( E* x ( ph -> ps ) -> E* x ps )
Theorem	euimmo 2371	Uniqueness implies "at most one" through reverse implication. (Contributed by NM, 22-Apr-1995.)
|- ( A. x ( ph -> ps ) -> ( E! x ps -> E* x ph ) )
Theorem	euim 2372	Add existential uniqueness quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( ( E. x ph /\ A. x ( ph -> ps ) ) -> ( E! x ps -> E! x ph ) )
Theorem	moan 2373	"At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
|- ( E* x ph -> E* x ( ps /\ ph ) )
Theorem	moani 2374	"At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
|- E* x ph   =>    |- E* x ( ps /\ ph )
Theorem	moor 2375	"At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
|- ( E* x ( ph \/ ps ) -> E* x ph )
Theorem	mooran1 2376	"At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ( E* x ph \/ E* x ps ) -> E* x ( ph /\ ps ) )
Theorem	mooran2 2377	"At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( E* x ( ph \/ ps ) -> ( E* x ph /\ E* x ps ) )
Theorem	moanim 2378	Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 24-Dec-2018.)
|- F/ x ph   =>    |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )
Theorem	euan 2379	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 24-Dec-2018.)
|- F/ x ph   =>    |- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )
Theorem	moanimv 2380*	Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )
Theorem	moanmo 2381	Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.)
|- E* x ( ph /\ E* x ph )
Theorem	moaneu 2382	Nested "at most one" and uniqueness quantifiers. (Contributed by NM, 25-Jan-2006.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)
|- E* x ( ph /\ E! x ph )
Theorem	euanv 2383*	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )
Theorem	mopick 2384	"At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.) (Proof shortened by Wolf Lammen, 17-Sep-2019.)
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
Theorem	eupick 2385	Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing x such that ph is true, and there is also an x (actually the same one) such that ph and ps are both true, then ph implies ps regardless of x. This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.)
|- ( ( E! x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
Theorem	eupicka 2386	Version of eupick 2385 with closed formulas. (Contributed by NM, 6-Sep-2008.)
|- ( ( E! x ph /\ E. x ( ph /\ ps ) ) -> A. x ( ph -> ps ) )
Theorem	eupickb 2387	Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)
|- ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ph <-> ps ) )
Theorem	eupickbi 2388	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof shortened by Wolf Lammen, 27-Dec-2018.)
|- ( E! x ph -> ( E. x ( ph /\ ps ) <-> A. x ( ph -> ps ) ) )
Theorem	mopick2 2389	"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 1739. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ( E* x ph /\ E. x ( ph /\ ps ) /\ E. x ( ph /\ ch ) ) -> E. x ( ph /\ ps /\ ch ) )
Theorem	moexex 2390	"At most one" double quantification. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 28-Dec-2018.)
|- F/ y ph   =>    |- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )
Theorem	moexexv 2391*	"At most one" double quantification. (Contributed by NM, 26-Jan-1997.)
|- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )
Theorem	2moex 2392	Double quantification with "at most one." (Contributed by NM, 3-Dec-2001.)
|- ( E* x E. y ph -> A. y E* x ph )
Theorem	2euex 2393	Double quantification with existential uniqueness. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( E! x E. y ph -> E. y E! x ph )
Theorem	2eumo 2394	Double quantification with existential uniqueness and "at most one." (Contributed by NM, 3-Dec-2001.)
|- ( E! x E* y ph -> E* x E! y ph )
Theorem	2eu2ex 2395	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- ( E! x E! y ph -> E. x E. y ph )
Theorem	2moswap 2396	A condition allowing swap of "at most one" and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
|- ( A. x E* y ph -> ( E* x E. y ph -> E* y E. x ph ) )
Theorem	2euswap 2397	A condition allowing swap of uniqueness and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
|- ( A. x E* y ph -> ( E! x E. y ph -> E! y E. x ph ) )
Theorem	2exeu 2398	Double existential uniqueness implies double uniqueness quantification. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Mario Carneiro, 22-Dec-2016.)
|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
Theorem	2mo2 2399*	This theorem extends the idea of "at most one" to expressions in two set variables ("at most one pair x and y". Note: this is not expressed by E* x E* y ph). 2eu4 2405 relates this extension to double existential uniqueness, if at least one pair exists. (Contributed by Wolf Lammen, 26-Oct-2019.)
|- ( ( E* x E. y ph /\ E* y E. x ph ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
Theorem	2mo 2400*	Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-Nov-2019.)
|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )