P. 21 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 2001-2100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nf5-1 2001	One direction of nf5 . (Contributed by Wolf Lammen, 16-Sep-2021.)
|- ( A. x ( ph -> A. x ph ) -> F/ x ph )
Theorem	nf5d 2002	Deduce that x is not free in ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
|- F/ x ph   &    |- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
1.4.6  Existential uniqueness
Syntax	weu 2003	Extend wff definition to include existential uniqueness ("there exists a unique x such that ph").
wff E! x ph
Syntax	wmo 2004	Extend wff definition to include uniqueness ("there exists at most one x such that ph").
wff E* x ph
Theorem	eujust 2005*	A soundness justification theorem for df-eu 2006, 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 2006*	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 2028, eu2 2047, eu3 2049, and eu5 2050 (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 2096). (Contributed by NM, 5-Aug-1993.)
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Definition	df-mo 2007	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 2057. For another possible definition see mo4 2064. (Contributed by NM, 5-Aug-1993.)
|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
Theorem	euf 2008*	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 2009	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	eubid 2010	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	eubidv 2011*	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	eubii 2012	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 2013	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
|- ( E! x ph -> A. x E! x ph )
Theorem	nfeu1 2014	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 2015	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 2016	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 2017	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 2018*	Deduction version of nfeu 2022. Similar to nfeud 2019 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 2019	Deduction version of nfeu 2022. (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 2020	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 2021*	Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 2022 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 2022	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 2023	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
|- F/ x ph   =>    |- F/ x E* y ph
Theorem	hbeu 2024	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 2025	Deduction version of hbeu 2024. (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 2026	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 2027	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 2028*	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 2029	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 2030*	Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( ( -. ph /\ E! x ps ) -> E! x ( ph \/ ps ) )
Theorem	mo2n 2031*	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 2032	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 2033	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 2034*	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 2035	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 2036	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
|- E! x ph   =>    |- E* x ph
Theorem	mobidh 2037	Formula-building rule for "at most one" quantifier (deduction form). (Contributed by NM, 8-Mar-1995.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	mobid 2038	Formula-building rule for "at most one" quantifier (deduction form). (Contributed by NM, 8-Mar-1995.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	mobidv 2039*	Formula-building rule for "at most one" quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	mobii 2040	Formula-building rule for "at most one" quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ps <-> ch )   =>    |- ( E* x ps <-> E* x ch )
Theorem	hbmo1 2041	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.)
|- ( E* x ph -> A. x E* x ph )
Theorem	hbmo 2042	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 2043	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 2044*	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 2045*	Converse of mo23 2044 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 2046*	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 2047*	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 2048*	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 2049*	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 2050	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 2051	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 2052	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 2053	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 2054	There is at most one of something which does not exist. Unlike exmodc 2053 there is no decidability condition. (Contributed by Jim Kingdon, 22-Sep-2018.)
|- ( -. E. x ph -> E* x ph )
Theorem	mo2r 2055*	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 2056*	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 2057*	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 2058*	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 ) ) )
Theorem	euan 2059	Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( ph -> A. x ph )   =>    |- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )
Theorem	euanv 2060*	Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )
Theorem	euor2 2061	Introduce or eliminate a disjunct in a unique existential quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( -. E. x ph -> ( E! x ( ph \/ ps ) <-> E! x ps ) )
Theorem	sbmo 2062*	Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ( [ y / x ] E* z ph <-> E* z [ y / x ] ph )
Theorem	mo4f 2063*	"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 2064*	"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 2065*	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	exmoeudc 2066	Existence in terms of "at most one" and uniqueness. (Contributed by Jim Kingdon, 3-Jul-2018.)
|- (DECID E. x ph -> ( E. x ph <-> ( E* x ph -> E! x ph ) ) )
Theorem	moim 2067	"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 2068	"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	moimv 2069*	Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.)
|- ( E* x ( ph -> ps ) -> ( ph -> E* x ps ) )
Theorem	euimmo 2070	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 2071	Add existential unique existential 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 2072	"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 2073	"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 2074	"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 2075	"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 2076	"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 2077	Introduction of a conjunct into at-most-one quantifier. (Contributed by NM, 3-Dec-2001.)
|- F/ x ph   =>    |- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )
Theorem	moanimv 2078*	Introduction of a conjunct into at-most-one quantifier. (Contributed by NM, 23-Mar-1995.)
|- ( E* x ( ph /\ ps ) <-> ( ph -> E* x ps ) )
Theorem	moaneu 2079	Nested at-most-one and unique existential quantifiers. (Contributed by NM, 25-Jan-2006.)
|- E* x ( ph /\ E! x ph )
Theorem	moanmo 2080	Nested at-most-one quantifiers. (Contributed by NM, 25-Jan-2006.)
|- E* x ( ph /\ E* x ph )
Theorem	mopick 2081	"At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.)
|- ( ( E* x ph /\ E. x ( ph /\ ps ) ) -> ( ph -> ps ) )
Theorem	eupick 2082	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 2083	Version of eupick 2082 with closed formulas. (Contributed by NM, 6-Sep-2008.)
|- ( ( E! x ph /\ E. x ( ph /\ ps ) ) -> A. x ( ph -> ps ) )
Theorem	eupickb 2084	Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.)
|- ( ( E! x ph /\ E! x ps /\ E. x ( ph /\ ps ) ) -> ( ph <-> ps ) )
Theorem	eupickbi 2085	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- ( E! x ph -> ( E. x ( ph /\ ps ) <-> A. x ( ph -> ps ) ) )
Theorem	mopick2 2086	"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 1608. (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	moexexdc 2087	"At most one" double quantification. (Contributed by Jim Kingdon, 5-Jul-2018.)
|- F/ y ph   =>    |- (DECID E. x ph -> ( ( E* x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) ) )
Theorem	euexex 2088	Existential uniqueness and "at most one" double quantification. (Contributed by Jim Kingdon, 28-Dec-2018.)
|- F/ y ph   =>    |- ( ( E! x ph /\ A. x E* y ps ) -> E* y E. x ( ph /\ ps ) )
Theorem	2moex 2089	Double quantification with "at most one." (Contributed by NM, 3-Dec-2001.)
|- ( E* x E. y ph -> A. y E* x ph )
Theorem	2euex 2090	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 2091	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 2092	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- ( E! x E! y ph -> E. x E. y ph )
Theorem	2moswapdc 2093	A condition allowing swap of "at most one" and existential quantifiers. (Contributed by Jim Kingdon, 6-Jul-2018.)
|- (DECID E. x E. y ph -> ( A. x E* y ph -> ( E* x E. y ph -> E* y E. x ph ) ) )
Theorem	2euswapdc 2094	A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Jim Kingdon, 7-Jul-2018.)
|- (DECID E. x E. y ph -> ( A. x E* y ph -> ( E! x E. y ph -> E! y E. x ph ) ) )
Theorem	2exeu 2095	Double existential uniqueness implies double unique existential quantification. (Contributed by NM, 3-Dec-2001.)
|- ( ( E! x E. y ph /\ E! y E. x ph ) -> E! x E! y ph )
Theorem	2eu4 2096*	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 2exeu 2095 for a one-way implication. (Contributed by NM, 3-Dec-2001.)
|- ( ( 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	2eu7 2097	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	euequ1 2098*	Equality has existential uniqueness. (Contributed by Stefan Allan, 4-Dec-2008.)
|- E! x x = y
Theorem	exists1 2099*	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. (Contributed by NM, 5-Apr-2004.)
|- ( E! x x = x <-> A. x x = y )
Theorem	exists2 2100	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 )