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	exmoeu2 2301	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 2302*	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 2303	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
|- ( E! x ph -> E* x ph )
Theorem	eumoi 2304	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
|- E! x ph   =>    |- E* x ph
Theorem	moabs 2305	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 2306	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	exmoeuOLD 2307	Obsolete proof of exmoeu 2306 as of 5-Dec-2018. (Contributed by NM, 5-Apr-2004.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. x ph <-> ( E* x ph -> E! x ph ) )
Theorem	eumo0OLD 2308*	Obsolete as of 6-Jun-2018. Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ y ph   =>    |- ( E! x ph -> E. y A. x ( ph -> x = y ) )
Theorem	sb8eu 2309	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	sb8euOLD 2310	Obsolete proof of sb8eu 2309 as of 24-Aug-2019. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 8-Oct-2018.)
|- F/ y ph   =>    |- ( E! x ph <-> E! y [ y / x ] ph )
Theorem	sb8euOLDOLD 2311	Obsolete proof of sb8eu 2309 as of 8-Oct-2018. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E! x ph <-> E! y [ y / x ] ph )
Theorem	sb8mo 2312	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 2313	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 2314	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 2315*	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	mo3OLD 2316*	Obsolete proof of mo3 2315 as of 20-Jul-2019. (Contributed by NM, 8-Mar-1995.) (Revised by Wolf Lammen, 3-Dec-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	mo 2317*	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	mo3OLDOLD 2318*	Obsolete proof of mo3 2315 as of 2-Dec-2018. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E* x ph <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	eu2 2319*	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 2320*	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	eu1OLD 2321*	Obsolete proof of eu1 2320 as of 29-Oct-2018. (Contributed by NM, 20-Aug-1993.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E! x ph <-> E. x ( ph /\ A. y ( [ y / x ] ph -> x = y ) ) )
Theorem	moOLD 2322*	Obsolete proof of mo 2317 as of 7-Oct-2018. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E. y A. x ( ph -> x = y ) <-> A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) )
Theorem	euexALT 2323	Alternate proof of euex 2298. 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	eu2OLD 2324*	Obsolete proof of eu2 2319 as of 2-Dec-2018. (Contributed by NM, 8-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E! x ph <-> ( E. x ph /\ A. x A. y ( ( ph /\ [ y / x ] ph ) -> x = y ) ) )
Theorem	eu3OLD 2325*	Obsolete theorem as of 29-May-2018. Superseded by eu3v 2302 that better fits common usage pattern. (Contributed by NM, 8-Jul-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
Theorem	eu5OLD 2326	Obsolete proof of eu5 2300 as of 25-May-2019 (Contributed by NM, 23-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
Theorem	euor 2327	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 2328*	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) )
Theorem	euor2 2329	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	euor2OLD 2330	Obsolete proof of euor2 2329 as of 27-Dec-2018. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. E. x ph -> ( E! x ( ph \/ ps ) <-> E! x ps ) )
Theorem	mo2OLD 2331*	Obsolete proof of mo2 2282 as of 28-May-2019. (Contributed by NM, 8-Mar-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
Theorem	sbmo 2332*	Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( [ y / x ] E* z ph <-> E* z [ y / x ] ph )
Theorem	mo4f 2333*	"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 2334*	"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 2335*	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 2336	"At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
|- ( A. x ( ph -> ps ) -> ( E* x ps -> E* x ph ) )
Theorem	moimi 2337	"At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
|- ( ph -> ps )   =>    |- ( E* x ps -> E* x ph )
Theorem	morimOLD 2338	Obsolete theorem as of 22-Dec-2018. Use moimi 2337 applied to ax-1 6, as demonstrated in the proof. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( E* x ( ph -> ps ) -> ( ph -> E* x ps ) )
Theorem	morimvOLD 2339*	Obsolete proof of morimOLD 2338 as of 22-Dec-2018. (Contributed by NM, 28-Jul-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E* x ( ph -> ps ) -> ( ph -> E* x ps ) )
Theorem	euimmo 2340	Uniqueness implies "at most one" through implication. (Contributed by NM, 22-Apr-1995.)
|- ( A. x ( ph -> ps ) -> ( E! x ps -> E* x ph ) )
Theorem	euim 2341	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 2342	"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 2343	"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 2344	"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 2345	"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 2346	"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 2347	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 2348	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	euanOLD 2349	Obsolete poof of euan 2348 as of 24-Dec-2018. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )
Theorem	moanimOLD 2350	Obsolete proof of moanim 2347 as of 23-Dec-2018. (Contributed by NM, 3-Dec-2001.) (New usage is discouraged.) (Proof modification is discouraged.)
|- F/ x ph   =>    |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )
Theorem	moanimv 2351*	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 2352	Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.)
|- E* x ( ph /\ E* x ph )
Theorem	moaneu 2353	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	moaneuOLD 2354	Obsolete proof of moaneu 2353 as of 27-Dec-2018. (Contributed by NM, 25-Jan-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E* x ( ph /\ E! x ph )
Theorem	euanv 2355*	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )
Theorem	mopick 2356	"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	mopickOLD 2357	Obsolete proof of mopick 2356 as of 15-Sep-2019. (Contributed by NM, 27-Jan-1997.) (Proof shortened by Wolf Lammen, 29-Dec-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
Theorem	mopickOLDOLD 2358	Obsolete proof of mopick 2356 as of 27-Dec-2018. (Contributed by NM, 27-Jan-1997.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
Theorem	eupick 2359	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 2360	Version of eupick 2359 with closed formulas. (Contributed by NM, 6-Sep-2008.)
|- ( ( E! x ph /\ E. x ( ph /\ ps ) ) -> A. x ( ph -> ps ) )
Theorem	eupickb 2361	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	eupickbOLD 2362	Obsolete proof of eupickb 2361 as of 27-Dec-2018. (Contributed by NM, 25-Nov-1994.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ph <-> ps ) )
Theorem	eupickbi 2363	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	eupickbiOLD 2364	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E! x ph -> ( E. x ( ph /\ ps ) <-> A. x ( ph -> ps ) ) )
Theorem	mopick2 2365	"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 1651. (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 2366	"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	moexexOLD 2367	Obsolete proof of moexex 2366 as of 28-Dec.2018. (Contributed by NM, 3-Dec-2001.) (Proof modification is discouraged.) (New usage is discouraged.)
|- F/ y ph   =>    |- ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )
Theorem	moexexv 2368*	"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 2369	Double quantification with "at most one." (Contributed by NM, 3-Dec-2001.)
|- ( E* x E. y ph -> A. y E* x ph )
Theorem	2euex 2370	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 2371	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 2372	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- ( E! x E! y ph -> E. x E. y ph )
Theorem	2moswap 2373	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 2374	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 2375	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 2376*	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 2385 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 2377*	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 ) ) )
Theorem	2moOLD 2378*	Obsolete proof of 2mo 2377 as of 2-Nov-2019. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 25-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( 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 ) ) )
Theorem	2moOLDOLD 2379*	Obsolete proof of 2mo 2377 as of 19-Jan-2019. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( 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 ) ) )
Theorem	2mos 2380*	Double "exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ ps ) -> ( x = z /\ y = w ) ) )
Theorem	2eu1 2381	Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 11-Nov-2019.)
|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
Theorem	2eu1OLD 2382	Obsolete proof of 2eu1 2381 as of 11-Nov-2019. (Contributed by NM, 3-Dec-2001.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
Theorem	2eu2 2383	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- ( E! y E. x ph -> ( E! x E! y ph <-> E! x E. y ph ) )
Theorem	2eu3 2384	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- ( A. x A. y ( E* x ph \/ E* y ph ) -> ( ( E! x E! y ph /\ E! y E! x ph ) <-> ( E! x E. y ph /\ E! y E. x ph ) ) )
Theorem	2eu4 2385*	This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y"). Naively one might think (incorrectly) that it could be defined by E! x E! y ph. See 2eu1 2381 for a condition under which the naive definition holds and 2exeu 2375 for a one-way implication. See 2eu5 2387 and 2eu8 2391 for alternate definitions. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf Lammen, 14-Sep-2019.)
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
Theorem	2eu4OLD 2386*	Obsolete proof of 2eu4 2385 as of 14-Sep-2019. (Contributed by NM, 3-Dec-2001.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
Theorem	2eu5 2387*	An alternate definition of double existential uniqueness (see 2eu4 2385). A mistake sometimes made in the literature is to use E! x E! y to mean "exactly one x and exactly one y." (For example, see Proposition 7.53 of [TakeutiZaring] p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining A. x E* y ph as an additional condition. The correct definition apparently has never been published. ( E* means "exists at most one.") (Contributed by NM, 26-Oct-2003.)
|- ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
Theorem	2eu6 2388*	Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 2-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	2eu6OLD 2389*	Obsolete proof of 2eu6 2388 as of 21-Sep-2019. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> E. z E. w A. x A. y ( ph <-> ( x = z /\ y = w ) ) )
Theorem	2eu7 2390	Two equivalent expressions for double existential uniqueness. (Contributed by NM, 19-Feb-2005.)
|- ( ( E! x E. y ph /\ E! y E. x ph ) <-> E! x E! y ( E. x ph /\ E. y ph ) )
Theorem	2eu8 2391	Two equivalent expressions for double existential uniqueness. Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E! x E! y using 2eu7 2390. (Contributed by NM, 20-Feb-2005.)
|- ( E! x E! y ( E. x ph /\ E. y ph ) <-> E! x E! y ( E! x ph /\ E. y ph ) )
Theorem	euequ1OLD 2392*	Obsolete proof of euequ1 2276 as of 8-Sep-2019. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- E! x x = y
Theorem	exists1 2393*	Two ways to express "only one thing exists." The left-hand side requires only one variable to express this. Both sides are false in set theory; see theorem dtru 4633. (Contributed by NM, 5-Apr-2004.)
|- ( E! x x = x <-> A. x x = y )
Theorem	exists2 2394	A condition implying that at least two things exist. (Contributed by NM, 10-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ( E. x ph /\ E. x -. ph ) -> -. E! x x = x )
1.8  Other axiomatizations related to classical predicate calculus
1.8.1  Predicate calculus with all distinct variables
Axiom	ax-7d 2395*	Distinct variable version of ax-11 1786. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( A. x A. y ph -> A. y A. x ph )
Axiom	ax-8d 2396*	Distinct variable version of ax-7 1734. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( x = y -> ( x = z -> y = z ) )
Axiom	ax-9d1 2397	Distinct variable version of ax-6 1714, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- -. A. x -. x = x
Axiom	ax-9d2 2398*	Distinct variable version of ax-6 1714, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- -. A. x -. x = y
Axiom	ax-10d 2399*	Distinct variable version of axc11n 2017. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( A. x x = y -> A. y y = x )
Axiom	ax-11d 2400*	Distinct variable version of ax-12 1798. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )