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 φ. 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 → (φ → ∀x(x = z → φ)))    ⇒   ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
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 φ. 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 → (∀zφ → ∀x(x = z → φ)))    ⇒   ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
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.)
⊢ (∀x x = y → (∀xφ → ∀yφ))
1.7  Existential uniqueness
Syntax	weu 2204	Extend wff definition to include existential uniqueness ("there exists a unique x such that φ").
wff ∃!xφ
Syntax	wmo 2205	Extend wff definition to include uniqueness ("there exists at most one x such that φ").
wff ∃*xφ
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.)
⊢ (∃y∀x(φ ↔ x = y) ↔ ∃z∀x(φ ↔ 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.)
⊢ (∃y∀x(φ ↔ x = y) ↔ ∃z∀x(φ ↔ x = z))
Definition	df-eu 2208*	Define existential uniqueness, i.e. "there exists exactly one x such that φ." 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 φ → ∀yφ in place of a distinct variable condition on y and φ). Double uniqueness is tricky: ∃!x∃!yφ does not mean "exactly one x and one y " (see 2eu4 2287). (Contributed by NM, 12-Aug-1993.)
⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
Definition	df-mo 2209	Define "there exists at most one x such that φ." 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.)
⊢ (∃*xφ ↔ (∃xφ → ∃!xφ))
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.)
⊢ Ⅎyφ    ⇒   ⊢ (∃!xφ ↔ ∃y∀x(φ ↔ x = y))
Theorem	eubid 2211	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃!xψ ↔ ∃!xχ))
Theorem	eubidv 2212*	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃!xψ ↔ ∃!xχ))
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.)
⊢ (φ ↔ ψ)    ⇒   ⊢ (∃!xφ ↔ ∃!xψ)
Theorem	nfeu1 2214	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎx∃!xφ
Theorem	nfmo1 2215	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎx∃*xφ
Theorem	nfeud2 2216	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎyφ    &   ⊢ ((φ ∧ ¬ ∀x x = y) → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃!yψ)
Theorem	nfmod2 2217	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎyφ    &   ⊢ ((φ ∧ ¬ ∀x x = y) → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃*yψ)
Theorem	nfeud 2218	Deduction version of nfeu 2220. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃!yψ)
Theorem	nfmod 2219	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎxψ)    ⇒   ⊢ (φ → Ⅎx∃*yψ)
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.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∃!yφ
Theorem	nfmo 2221	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx∃*yφ
Theorem	sb8eu 2222	Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ (∃!xφ ↔ ∃!y[y / x]φ)
Theorem	sb8mo 2223	Variable substitution in uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ Ⅎyφ    ⇒   ⊢ (∃*xφ ↔ ∃*y[y / x]φ)
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.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃!xφ ↔ ∃!yψ)
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.)
⊢ Ⅎyφ    ⇒   ⊢ (∃!xφ ↔ ∃x(φ ∧ ∀y([y / x]φ → 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.)
⊢ Ⅎyφ    ⇒   ⊢ (∃y∀x(φ → x = y) ↔ ∀x∀y((φ ∧ [y / x]φ) → x = y))
Theorem	euex 2227	Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃!xφ → ∃xφ)
Theorem	eumo0 2228*	Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.)
⊢ Ⅎyφ    ⇒   ⊢ (∃!xφ → ∃y∀x(φ → 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.)
⊢ Ⅎyφ    ⇒   ⊢ (∃!xφ ↔ (∃xφ ∧ ∀x∀y((φ ∧ [y / x]φ) → x = y)))
Theorem	eu3 2230*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.)
⊢ Ⅎyφ    ⇒   ⊢ (∃!xφ ↔ (∃xφ ∧ ∃y∀x(φ → x = y)))
Theorem	euor 2231	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.)
⊢ Ⅎxφ    ⇒   ⊢ ((¬ φ ∧ ∃!xψ) → ∃!x(φ ∨ ψ))
Theorem	euorv 2232*	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
⊢ ((¬ φ ∧ ∃!xψ) → ∃!x(φ ∨ ψ))
Theorem	mo2 2233*	Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.)
⊢ Ⅎyφ    ⇒   ⊢ (∃*xφ ↔ ∃y∀x(φ → x = y))
Theorem	sbmo 2234*	Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
⊢ ([y / x]∃*zφ ↔ ∃*z[y / x]φ)
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 φ in place of our hypothesis. (Contributed by NM, 8-Mar-1995.)
⊢ Ⅎyφ    ⇒   ⊢ (∃*xφ ↔ ∀x∀y((φ ∧ [y / x]φ) → x = y))
Theorem	mo4f 2236*	"At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.)
⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃*xφ ↔ ∀x∀y((φ ∧ ψ) → x = y))
Theorem	mo4 2237*	"At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃*xφ ↔ ∀x∀y((φ ∧ ψ) → x = y))
Theorem	mobid 2238	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃*xψ ↔ ∃*xχ))
Theorem	mobidv 2239*	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃*xψ ↔ ∃*xχ))
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.)
⊢ (ψ ↔ χ)    ⇒   ⊢ (∃*xψ ↔ ∃*xχ)
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.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃*xφ ↔ ∃*yψ)
Theorem	eu5 2242	Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.)
⊢ (∃!xφ ↔ (∃xφ ∧ ∃*xφ))
Theorem	eu4 2243*	Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃!xφ ↔ (∃xφ ∧ ∀x∀y((φ ∧ ψ) → x = y)))
Theorem	eumo 2244	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
⊢ (∃!xφ → ∃*xφ)
Theorem	eumoi 2245	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
⊢ ∃!xφ    ⇒   ⊢ ∃*xφ
Theorem	exmoeu 2246	Existence in terms of "at most one" and uniqueness. (Contributed by NM, 5-Apr-2004.)
⊢ (∃xφ ↔ (∃*xφ → ∃!xφ))
Theorem	exmoeu2 2247	Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
⊢ (∃xφ → (∃*xφ ↔ ∃!xφ))
Theorem	moabs 2248	Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
⊢ (∃*xφ ↔ (∃xφ → ∃*xφ))
Theorem	exmo 2249	Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)
⊢ (∃xφ ∨ ∃*xφ)
Theorem	moim 2250	"At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
⊢ (∀x(φ → ψ) → (∃*xψ → ∃*xφ))
Theorem	moimi 2251	"At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
⊢ (φ → ψ)    ⇒   ⊢ (∃*xψ → ∃*xφ)
Theorem	morimv 2252*	Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.)
⊢ (∃*x(φ → ψ) → (φ → ∃*xψ))
Theorem	euimmo 2253	Uniqueness implies "at most one" through implication. (Contributed by NM, 22-Apr-1995.)
⊢ (∀x(φ → ψ) → (∃!xψ → ∃*xφ))
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.)
⊢ ((∃xφ ∧ ∀x(φ → ψ)) → (∃!xψ → ∃!xφ))
Theorem	moan 2255	"At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
⊢ (∃*xφ → ∃*x(ψ ∧ φ))
Theorem	moani 2256	"At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
⊢ ∃*xφ    ⇒   ⊢ ∃*x(ψ ∧ φ)
Theorem	moor 2257	"At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
⊢ (∃*x(φ ∨ ψ) → ∃*xφ)
Theorem	mooran1 2258	"At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ((∃*xφ ∨ ∃*xψ) → ∃*x(φ ∧ ψ))
Theorem	mooran2 2259	"At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃*x(φ ∨ ψ) → (∃*xφ ∧ ∃*xψ))
Theorem	moanim 2260	Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 3-Dec-2001.)
⊢ Ⅎxφ    ⇒   ⊢ (∃*x(φ ∧ ψ) ↔ (φ → ∃*xψ))
Theorem	euan 2261	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ Ⅎxφ    ⇒   ⊢ (∃!x(φ ∧ ψ) ↔ (φ ∧ ∃!xψ))
Theorem	moanimv 2262*	Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
⊢ (∃*x(φ ∧ ψ) ↔ (φ → ∃*xψ))
Theorem	moaneu 2263	Nested "at most one" and uniqueness quantifiers. (Contributed by NM, 25-Jan-2006.)
⊢ ∃*x(φ ∧ ∃!xφ)
Theorem	moanmo 2264	Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.)
⊢ ∃*x(φ ∧ ∃*xφ)
Theorem	euanv 2265*	Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
⊢ (∃!x(φ ∧ ψ) ↔ (φ ∧ ∃!xψ))
Theorem	mopick 2266	"At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.)
⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
Theorem	eupick 2267	Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing x such that φ is true, and there is also an x (actually the same one) such that φ and ψ are both true, then φ implies ψ 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.)
⊢ ((∃!xφ ∧ ∃x(φ ∧ ψ)) → (φ → ψ))
Theorem	eupicka 2268	Version of eupick 2267 with closed formulas. (Contributed by NM, 6-Sep-2008.)
⊢ ((∃!xφ ∧ ∃x(φ ∧ ψ)) → ∀x(φ → ψ))
Theorem	eupickb 2269	Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.)
⊢ ((∃!xφ ∧ ∃!xψ ∧ ∃x(φ ∧ ψ)) → (φ ↔ ψ))
Theorem	eupickbi 2270	Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
⊢ (∃!xφ → (∃x(φ ∧ ψ) ↔ ∀x(φ → ψ)))
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.)
⊢ ((∃*xφ ∧ ∃x(φ ∧ ψ) ∧ ∃x(φ ∧ χ)) → ∃x(φ ∧ ψ ∧ χ))
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.)
⊢ (¬ ∃xφ → (∃!x(φ ∨ ψ) ↔ ∃!xψ))
Theorem	moexex 2273	"At most one" double quantification. (Contributed by NM, 3-Dec-2001.)
⊢ Ⅎyφ    ⇒   ⊢ ((∃*xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ))
Theorem	moexexv 2274*	"At most one" double quantification. (Contributed by NM, 26-Jan-1997.)
⊢ ((∃*xφ ∧ ∀x∃*yψ) → ∃*y∃x(φ ∧ ψ))
Theorem	2moex 2275	Double quantification with "at most one." (Contributed by NM, 3-Dec-2001.)
⊢ (∃*x∃yφ → ∀y∃*xφ)
Theorem	2euex 2276	Double quantification with existential uniqueness. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃!x∃yφ → ∃y∃!xφ)
Theorem	2eumo 2277	Double quantification with existential uniqueness and "at most one." (Contributed by NM, 3-Dec-2001.)
⊢ (∃!x∃*yφ → ∃*x∃!yφ)
Theorem	2eu2ex 2278	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
⊢ (∃!x∃!yφ → ∃x∃yφ)
Theorem	2moswap 2279	A condition allowing swap of "at most one" and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
⊢ (∀x∃*yφ → (∃*x∃yφ → ∃*y∃xφ))
Theorem	2euswap 2280	A condition allowing swap of uniqueness and existential quantifiers. (Contributed by NM, 10-Apr-2004.)
⊢ (∀x∃*yφ → (∃!x∃yφ → ∃!y∃xφ))
Theorem	2exeu 2281	Double existential uniqueness implies double uniqueness quantification. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Mario Carneiro, 22-Dec-2016.)
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) → ∃!x∃!yφ)
Theorem	2mo 2282*	Two equivalent expressions for double "at most one." (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (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) → (φ ↔ ψ))    ⇒   ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ ψ) → (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.)
⊢ (∀x∃*yφ → (∃!x∃!yφ ↔ (∃!x∃yφ ∧ ∃!y∃xφ)))
Theorem	2eu2 2285	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
⊢ (∃!y∃xφ → (∃!x∃!yφ ↔ ∃!x∃yφ))
Theorem	2eu3 2286	Double existential uniqueness. (Contributed by NM, 3-Dec-2001.)
⊢ (∀x∀y(∃*xφ ∨ ∃*yφ) → ((∃!x∃!yφ ∧ ∃!y∃!xφ) ↔ (∃!x∃yφ ∧ ∃!y∃xφ)))
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 ∃!x∃!yφ. 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.)
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ (∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (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 ∃!x∃!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 ∀x∃*yφ as an additional condition. The correct definition apparently has never been published. (∃* means "exists at most one.") (Contributed by NM, 26-Oct-2003.)
⊢ ((∃!x∃!yφ ∧ ∀x∃*yφ) ↔ (∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (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.)
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)))
Theorem	2eu7 2290	Two equivalent expressions for double existential uniqueness. (Contributed by NM, 19-Feb-2005.)
⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ∃!x∃!y(∃xφ ∧ ∃yφ))
Theorem	2eu8 2291	Two equivalent expressions for double existential uniqueness. Curiously, we can put ∃! on either of the internal conjuncts but not both. We can also commute ∃!x∃!y using 2eu7 2290. (Contributed by NM, 20-Feb-2005.)
⊢ (∃!x∃!y(∃xφ ∧ ∃yφ) ↔ ∃!x∃!y(∃!xφ ∧ ∃yφ))
Theorem	euequ1 2292*	Equality has existential uniqueness. Special case of eueq1 3009 proved using only predicate calculus. (Contributed by Stefan Allan, 4-Dec-2008.)
⊢ ∃!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.)
⊢ (∃!x x = x ↔ ∀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.)
⊢ ((∃xφ ∧ ∃x ¬ φ) → ¬ ∃!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.)
⊢ (∀x∀yφ → ∀y∀xφ)
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.)
⊢ ¬ ∀x ¬ x = x
Axiom	ax-9d2 2298*	Distinct variable version of ax9 1949, distinct variables case. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ ¬ ∀x ¬ x = y
Axiom	ax-10d 2299*	Distinct variable version of ax10 1944. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (∀x x = y → ∀y y = x)
Axiom	ax-11d 2300*	Distinct variable version of ax-11 1746. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ (x = y → (∀yφ → ∀x(x = y → φ)))