P. 23 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2201-2300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ax11v2-o 2201*	Recovery of ax-11o 2141 from ax11v 2096 without using ax-11o 2141. The hypothesis is even weaker than ax11v 2096, with z both distinct from x and not occurring in ph. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-11o 2141. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (x = z -> (ph -> A.x(x = z -> ph)))   =>   |- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
Theorem	ax11a2-o 2202*	Derive ax-11o 2141 from a hypothesis in the form of ax-11 1746, without using ax-11 1746 or ax-11o 2141. The hypothesis is even weaker than ax-11 1746, with z both distinct from x and not occurring in ph. Thus, the hypothesis provides an alternate axiom that can be used in place of ax-11 1746, if we also hvae ax-10o 2139 which this proof uses . As Theorem ax11 2155 shows, the distinct variable conditions are optional. An open problem is whether we can derive this with ax-10 2140 instead of ax-10o 2139. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (x = z -> (A.zph -> A.x(x = z -> ph)))   =>   |- (-. A.x x = y -> (x = y -> (ph -> A.x(x = y -> ph))))
Theorem	ax10o-o 2203	Show that ax-10o 2139 can be derived from ax-10 2140. An open problem is whether this theorem can be derived from ax-10 2140 and the others when ax-11 1746 is replaced with ax-11o 2141. See Theorem ax10from10o 2177 for the rederivation of ax-10 2140 from ax10o 1952. Normally, ax10o 1952 should be used rather than ax-10o 2139 or ax10o-o 2203, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (A.x x = y -> (A.xph -> A.yph))
1.7  Existential uniqueness
Syntax	weu 2204	Extend wff definition to include existential uniqueness ("there exists a unique x such that ph").
wff E!xph
Syntax	wmo 2205	Extend wff definition to include uniqueness ("there exists at most one x such that ph").
wff E*xph
Theorem	eujust 2206*	A soundness justification theorem for df-eu 2208, 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 2207 for a proof that provides an example of how it can be achieved through the use of dvelim 2016. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z))
Theorem	eujustALT 2207*	A soundness justification theorem for df-eu 2208, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. While this isn't strictly necessary for soundness, the proof provides an example of how it can be achieved through the use of dvelim 2016. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
|- (E.yA.x(ph <-> x = y) <-> E.zA.x(ph <-> x = z))
Definition	df-eu 2208*	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 2225, eu2 2229, eu3 2230, and eu5 2242 (which in some cases we show with a hypothesis ph -> A.yph in place of a distinct variable condition on y and ph). Double uniqueness is tricky: E!xE!yph does not mean "exactly one x and one y " (see 2eu4 2287). (Contributed by NM, 12-Aug-1993.)
|- (E!xph <-> E.yA.x(ph <-> x = y))
Definition	df-mo 2209	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 2235. For other possible definitions see mo2 2233 and mo4 2237. (Contributed by NM, 8-Mar-1995.)
|- (E*xph <-> (E.xph -> E!xph))
Theorem	euf 2210*	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.)
|- F/yph   =>   |- (E!xph <-> E.yA.x(ph <-> x = y))
Theorem	eubid 2211	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- F/xph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E!xps <-> E!xch))
Theorem	eubidv 2212*	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E!xps <-> E!xch))
Theorem	eubii 2213	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!xph <-> E!xps)
Theorem	nfeu1 2214	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/xE!xph
Theorem	nfmo1 2215	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/xE*xph
Theorem	nfeud2 2216	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/yph   &   |- ((ph /\ -. A.x x = y) -> F/xps)   =>   |- (ph -> F/xE!yps)
Theorem	nfmod2 2217	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/yph   &   |- ((ph /\ -. A.x x = y) -> F/xps)   =>   |- (ph -> F/xE*yps)
Theorem	nfeud 2218	Deduction version of nfeu 2220. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/xE!yps)
Theorem	nfmod 2219	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/yph   &   |- (ph -> F/xps)   =>   |- (ph -> F/xE*yps)
Theorem	nfeu 2220	Bound-variable hypothesis builder for "at most one." Note that x and y needn't be distinct (this makes the proof more difficult). (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/xph   =>   |- F/xE!yph
Theorem	nfmo 2221	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
|- F/xph   =>   |- F/xE*yph
Theorem	sb8eu 2222	Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/yph   =>   |- (E!xph <-> E!y[y / x]ph)
Theorem	sb8mo 2223	Variable substitution in uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- F/yph   =>   |- (E*xph <-> E*y[y / x]ph)
Theorem	cbveu 2224	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/yph   &   |- F/xps   &   |- (x = y -> (ph <-> ps))   =>   |- (E!xph <-> E!yps)
Theorem	eu1 2225*	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.)
|- F/yph   =>   |- (E!xph <-> E.x(ph /\ A.y([y / x]ph -> x = y)))
Theorem	mo 2226*	Equivalent definitions of "there exists at most one." (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/yph   =>   |- (E.yA.x(ph -> x = y) <-> A.xA.y((ph /\ [y / x]ph) -> x = y))
Theorem	euex 2227	Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (E!xph -> E.xph)
Theorem	eumo0 2228*	Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.)
|- F/yph   =>   |- (E!xph -> E.yA.x(ph -> x = y))
Theorem	eu2 2229*	An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.)
|- F/yph   =>   |- (E!xph <-> (E.xph /\ A.xA.y((ph /\ [y / x]ph) -> x = y)))
Theorem	eu3 2230*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.)
|- F/yph   =>   |- (E!xph <-> (E.xph /\ E.yA.x(ph -> x = y)))
Theorem	euor 2231	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.)
|- F/xph   =>   |- ((-. ph /\ E!xps) -> E!x(ph \/ ps))
Theorem	euorv 2232*	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
|- ((-. ph /\ E!xps) -> E!x(ph \/ ps))
Theorem	mo2 2233*	Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.)
|- F/yph   =>   |- (E*xph <-> E.yA.x(ph -> x = y))
Theorem	sbmo 2234*	Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
|- ([y / x]E*zph <-> E*z[y / x]ph)
Theorem	mo3 2235*	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/yph   =>   |- (E*xph <-> A.xA.y((ph /\ [y / x]ph) -> x = y))
Theorem	mo4f 2236*	"At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.)
|- F/xps   &   |- (x = y -> (ph <-> ps))   =>   |- (E*xph <-> A.xA.y((ph /\ ps) -> x = y))
Theorem	mo4 2237*	"At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
|- (x = y -> (ph <-> ps))   =>   |- (E*xph <-> A.xA.y((ph /\ ps) -> x = y))
Theorem	mobid 2238	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
|- F/xph   &   |- (ph -> (ps <-> ch))   =>   |- (ph -> (E*xps <-> E*xch))
Theorem	mobidv 2239*	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- (ph -> (ps <-> ch))   =>   |- (ph -> (E*xps <-> E*xch))
Theorem	mobii 2240	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*xps <-> E*xch)
Theorem	cbvmo 2241	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
|- F/yph   &   |- F/xps   &   |- (x = y -> (ph <-> ps))   =>   |- (E*xph <-> E*yps)
Theorem	eu5 2242	Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.)
|- (E!xph <-> (E.xph /\ E*xph))
Theorem	eu4 2243*	Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
|- (x = y -> (ph <-> ps))   =>   |- (E!xph <-> (E.xph /\ A.xA.y((ph /\ ps) -> x = y)))
Theorem	eumo 2244	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
|- (E!xph -> E*xph)
Theorem	eumoi 2245	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
|- E!xph   =>   |- E*xph
Theorem	exmoeu 2246	Existence in terms of "at most one" and uniqueness. (Contributed by NM, 5-Apr-2004.)
|- (E.xph <-> (E*xph -> E!xph))
Theorem	exmoeu2 2247	Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
|- (E.xph -> (E*xph <-> E!xph))
Theorem	moabs 2248	Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
|- (E*xph <-> (E.xph -> E*xph))
Theorem	exmo 2249	Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)
|- (E.xph \/ E*xph)
Theorem	moim 2250	"At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
|- (A.x(ph -> ps) -> (E*xps -> E*xph))
Theorem	moimi 2251	"At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
|- (ph -> ps)   =>   |- (E*xps -> E*xph)
Theorem	morimv 2252*	Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.)
|- (E*x(ph -> ps) -> (ph -> E*xps))
Theorem	euimmo 2253	Uniqueness implies "at most one" through implication. (Contributed by NM, 22-Apr-1995.)
|- (A.x(ph -> ps) -> (E!xps -> E*xph))
Theorem	euim 2254	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.xph /\ A.x(ph -> ps)) -> (E!xps -> E!xph))
Theorem	moan 2255	"At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
|- (E*xph -> E*x(ps /\ ph))
Theorem	moani 2256	"At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
|- E*xph   =>   |- E*x(ps /\ ph)
Theorem	moor 2257	"At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
|- (E*x(ph \/ ps) -> E*xph)
Theorem	mooran1 2258	"At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ((E*xph \/ E*xps) -> E*x(ph /\ ps))
Theorem	mooran2 2259	"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*xph /\ E*xps))
Theorem	moanim 2260	Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 3-Dec-2001.)
|- F/xph   =>   |- (E*x(ph /\ ps) <-> (ph -> E*xps))
Theorem	euan 2261	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- F/xph   =>   |- (E!x(ph /\ ps) <-> (ph /\ E!xps))
Theorem	moanimv 2262*	Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
|- (E*x(ph /\ ps) <-> (ph -> E*xps))
Theorem	moaneu 2263	Nested "at most one" and uniqueness quantifiers. (Contributed by NM, 25-Jan-2006.)
|- E*x(ph /\ E!xph)
Theorem	moanmo 2264	Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.)
|- E*x(ph /\ E*xph)
Theorem	euanv 2265*	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
|- (E!x(ph /\ ps) <-> (ph /\ E!xps))
Theorem	mopick 2266	"At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.)
|- ((E*xph /\ E.x(ph /\ ps)) -> (ph -> ps))
Theorem	eupick 2267	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!xph /\ E.x(ph /\ ps)) -> (ph -> ps))
Theorem	eupicka 2268	Version of eupick 2267 with closed formulas. (Contributed by NM, 6-Sep-2008.)
|- ((E!xph /\ E.x(ph /\ ps)) -> A.x(ph -> ps))
Theorem	eupickb 2269	Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.)
|- ((E!xph /\ E!xps /\ E.x(ph /\ ps)) -> (ph <-> ps))
Theorem	eupickbi 2270	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
|- (E!xph -> (E.x(ph /\ ps) <-> A.x(ph -> ps)))
Theorem	mopick2 2271	"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 1609. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ((E*xph /\ E.x(ph /\ ps) /\ E.x(ph /\ ch)) -> E.x(ph /\ ps /\ ch))
Theorem	euor2 2272	Introduce or eliminate a disjunct in a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (-. E.xph -> (E!x(ph \/ ps) <-> E!xps))
Theorem	moexex 2273	"At most one" double quantification. (Contributed by NM, 3-Dec-2001.)
|- F/yph   =>   |- ((E*xph /\ A.xE*yps) -> E*yE.x(ph /\ ps))
Theorem	moexexv 2274*	"At most one" double quantification. (Contributed by NM, 26-Jan-1997.)
|- ((E*xph /\ A.xE*yps) -> E*yE.x(ph /\ ps))
Theorem	2moex 2275	Double quantification with "at most one." (Contributed by NM, 3-Dec-2001.)
|- (E*xE.yph -> A.yE*xph)
Theorem	2euex 2276	Double quantification with existential uniqueness. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- (E!xE.yph -> E.yE!xph)
Theorem	2eumo 2277	Double quantification with existential uniqueness and "at most one." (Contributed by NM, 3-Dec-2001.)
|- (E!xE*yph -> E*xE!yph)
Theorem	2eu2ex 2278	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- (E!xE!yph -> E.xE.yph)
Theorem	2moswap 2279	A condition allowing swap of "at most one" and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
|- (A.xE*yph -> (E*xE.yph -> E*yE.xph))
Theorem	2euswap 2280	A condition allowing swap of uniqueness and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
|- (A.xE*yph -> (E!xE.yph -> E!yE.xph))
Theorem	2exeu 2281	Double existential uniqueness implies double uniqueness quantification. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Mario Carneiro, 22-Dec-2016.)
|- ((E!xE.yph /\ E!yE.xph) -> E!xE!yph)
Theorem	2mo 2282*	Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> A.xA.yA.zA.w((ph /\ [z / x][w / y]ph) -> (x = z /\ y = w)))
Theorem	2mos 2283*	Double "exists at most one", using implicit substitution. (Contributed by NM, 10-Feb-2005.)
|- ((x = z /\ y = w) -> (ph <-> ps))   =>   |- (E.zE.wA.xA.y(ph -> (x = z /\ y = w)) <-> A.xA.yA.zA.w((ph /\ ps) -> (x = z /\ y = w)))
Theorem	2eu1 2284	Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. (Contributed by NM, 3-Dec-2001.)
|- (A.xE*yph -> (E!xE!yph <-> (E!xE.yph /\ E!yE.xph)))
Theorem	2eu2 2285	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- (E!yE.xph -> (E!xE!yph <-> E!xE.yph))
Theorem	2eu3 2286	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
|- (A.xA.y(E*xph \/ E*yph) -> ((E!xE!yph /\ E!yE!xph) <-> (E!xE.yph /\ E!yE.xph)))
Theorem	2eu4 2287*	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!xE!yph. See 2eu1 2284 for a condition under which the naive definition holds and 2exeu 2281 for a one-way implication. See 2eu5 2288 and 2eu8 2291 for alternate definitions. (Contributed by NM, 3-Dec-2001.)
|- ((E!xE.yph /\ E!yE.xph) <-> (E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
Theorem	2eu5 2288*	An alternate definition of double existential uniqueness (see 2eu4 2287). A mistake sometimes made in the literature is to use E!xE!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.xE*yph as an additional condition. The correct definition apparently has never been published. (E* means "there exists at most one".) (Contributed by NM, 26-Oct-2003.)
|- ((E!xE!yph /\ A.xE*yph) <-> (E.xE.yph /\ E.zE.wA.xA.y(ph -> (x = z /\ y = w))))
Theorem	2eu6 2289*	Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ((E!xE.yph /\ E!yE.xph) <-> E.zE.wA.xA.y(ph <-> (x = z /\ y = w)))
Theorem	2eu7 2290	Two equivalent expressions for double existential uniqueness. (Contributed by NM, 19-Feb-2005.)
|- ((E!xE.yph /\ E!yE.xph) <-> E!xE!y(E.xph /\ E.yph))
Theorem	2eu8 2291	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!xE!y using 2eu7 2290. (Contributed by NM, 20-Feb-2005.)
|- (E!xE!y(E.xph /\ E.yph) <-> E!xE!y(E!xph /\ E.yph))
Theorem	euequ1 2292*	Equality has existential uniqueness. Special case of eueq1 3010 proved using only predicate calculus. (Contributed by Stefan Allan, 4-Dec-2008.)
|- E!x x = y
Theorem	exists1 2293*	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 in set.mm. (Contributed by NM, 5-Apr-2004.)
|- (E!x x = x <-> A.x x = y)
Theorem	exists2 2294	A condition implying that at least two things exist. (Contributed by NM, 10-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ((E.xph /\ 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 2295*	Distinct variable version of ax-7 1734. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (A.xA.yph -> A.yA.xph)
Axiom	ax-8d 2296*	Distinct variable version of ax-8 1675. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (x = y -> (x = z -> y = z))
Axiom	ax-9d1 2297	Distinct variable version of ax9 1949, equal variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- -. A.x -. x = x
Axiom	ax-9d2 2298*	Distinct variable version of ax9 1949, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- -. A.x -. x = y
Axiom	ax-10d 2299*	Distinct variable version of ax10 1944. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (A.x x = y -> A.y y = x)
Axiom	ax-11d 2300*	Distinct variable version of ax-11 1746. (Contributed by Mario Carneiro, 14-Aug-2015.)
|- (x = y -> (A.yph -> A.x(x = y -> ph)))