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	sbcocom 2001	Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑)
Theorem	sbcomv 2002*	Version of sbcom 2006 with a distinct variable constraint between 𝑥 and 𝑧. (Contributed by Jim Kingdon, 28-Feb-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	sbcomxyyz 2003*	Version of sbcom 2006 with distinct variable constraints between 𝑥 and 𝑦, and 𝑦 and 𝑧. (Contributed by Jim Kingdon, 21-Mar-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	sbco3xzyz 2004*	Version of sbco3 2005 with distinct variable constraints between 𝑥 and 𝑧, and 𝑦 and 𝑧. Lemma for proving sbco3 2005. (Contributed by Jim Kingdon, 22-Mar-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbco3 2005	A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbcom 2006	A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	nfsbt 2007*	Closed form of nfsb 1977. (Contributed by Jim Kingdon, 9-May-2018.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	nfsbd 2008*	Deduction version of nfsb 1977. (Contributed by NM, 15-Feb-2013.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓)
Theorem	sb9v 2009*	Like sb9 2010 but with a distinct variable constraint between 𝑥 and 𝑦. (Contributed by Jim Kingdon, 28-Feb-2018.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9 2010	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9i 2011	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sbnf2 2012*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
Theorem	hbsbd 2013*	Deduction version of hbsb 1980. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑧𝜓))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → ∀𝑧[𝑦 / 𝑥]𝜓))
Theorem	2sb5 2014*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑))
Theorem	2sb6 2015*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	sbcom2v 2016*	Lemma for proving sbcom2 2018. It is the same as sbcom2 2018 but with additional distinct variable constraints on 𝑥 and 𝑦, and on 𝑤 and 𝑧. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sbcom2v2 2017*	Lemma for proving sbcom2 2018. It is the same as sbcom2v 2016 but removes the distinct variable constraint on 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sbcom2 2018*	Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sb6a 2019*	Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	2sb5rf 2020*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → ∀𝑤𝜑)    ⇒   ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	2sb6rf 2021*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ (𝜑 → ∀𝑧𝜑)    &   ⊢ (𝜑 → ∀𝑤𝜑)    ⇒   ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	dfsb7 2022*	An alternate definition of proper substitution df-sb 1789. By introducing a dummy variable 𝑧 in the definiens, we are able to eliminate any distinct variable restrictions among the variables 𝑥, 𝑦, and 𝜑 of the definiendum. No distinct variable conflicts arise because 𝑧 effectively insulates 𝑥 from 𝑦. To achieve this, we use a chain of two substitutions in the form of sb5 1914, first 𝑧 for 𝑥 then 𝑦 for 𝑧. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 2023 provides a version where 𝜑 and 𝑧 don't have to be distinct. (Contributed by NM, 28-Jan-2004.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7f 2023*	This version of dfsb7 2022 does not require that 𝜑 and 𝑧 be disjoint. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1552, i.e., that does not have the concept of a variable not occurring in a formula. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7af 2024*	An alternate definition of proper substitution df-sb 1789. Similar to dfsb7a 2025 but does not require that 𝜑 and 𝑧 be distinct. Similar to sb7f 2023 in that it involves a dummy variable 𝑧, but expressed in terms of ∀ rather than ∃. (Contributed by Jim Kingdon, 5-Feb-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Theorem	dfsb7a 2025*	An alternate definition of proper substitution df-sb 1789. Similar to dfsb7 2022 in that it involves a dummy variable 𝑧, but expressed in terms of ∀ rather than ∃. For a version which only requires Ⅎ𝑧𝜑 rather than 𝑧 and 𝜑 being distinct, see sb7af 2024. (Contributed by Jim Kingdon, 5-Feb-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))
Theorem	sb10f 2026*	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.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑))
Theorem	sbid2v 2027*	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.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbelx 2028*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbel2x 2029*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑))
Theorem	sbalyz 2030*	Move universal quantifier in and out of substitution. Identical to sbal 2031 except that it has an additional distinct variable constraint on 𝑦 and 𝑧. (Contributed by Jim Kingdon, 29-Dec-2017.)
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbal 2031*	Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbal1yz 2032*	Lemma for proving sbal1 2033. Same as sbal1 2033 but with an additional disjoint variable condition on 𝑦, 𝑧. (Contributed by Jim Kingdon, 23-Feb-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	sbal1 2033*	A theorem used in elimination of disjoint variable conditions on 𝑥, 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	sbexyz 2034*	Move existential quantifier in and out of substitution. Identical to sbex 2035 except that it has an additional disjoint variable condition on 𝑦, 𝑧. (Contributed by Jim Kingdon, 29-Dec-2017.)
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbex 2035*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbalv 2036*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥]∀𝑧𝜑 ↔ ∀𝑧𝜓)
Theorem	sbco4lem 2037*	Lemma for sbco4 2038. It replaces the temporary variable 𝑣 with another temporary variable 𝑤. (Contributed by Jim Kingdon, 26-Sep-2018.)
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbco4 2038*	Two ways of exchanging two variables. Both sides of the biconditional exchange 𝑥 and 𝑦, either via two temporary variables 𝑢 and 𝑣, or a single temporary 𝑤. (Contributed by Jim Kingdon, 25-Sep-2018.)
⊢ ([𝑦 / 𝑢][𝑥 / 𝑣][𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	exsb 2039*	An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2exsb 2040*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	dvelimALT 2041*	Version of dvelim 2048 that doesn't use ax-10 1531. Because it has different distinct variable constraints than dvelim 2048 and is used in important proofs, it would be better if it had a name which does not end in ALT (ideally more close to set.mm naming). (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimfv 2042*	Like dvelimf 2046 but with a distinct variable constraint on 𝑥 and 𝑧. (Contributed by Jim Kingdon, 6-Mar-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	hbsb4 2043	A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑))
Theorem	hbsb4t 2044	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 2043). (Contributed by NM, 7-Apr-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥∀𝑧(𝜑 → ∀𝑧𝜑) → (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)))
Theorem	nfsb4t 2045	A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 2043). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof rewritten by Jim Kingdon, 9-May-2018.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑))
Theorem	dvelimf 2046	Version of dvelim 2048 without any variable restrictions. (Contributed by NM, 1-Oct-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimdf 2047	Deduction form of dvelimf 2046. This version may be useful if we want to avoid ax-17 1552 and use ax-16 1840 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑧𝜒)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))
Theorem	dvelim 2048*	This theorem can be used to eliminate a distinct variable restriction on 𝑥 and 𝑧 and replace it with the "distinctor" ¬ ∀𝑥𝑥 = 𝑦 as an antecedent. 𝜑 normally has 𝑧 free and can be read 𝜑(𝑧), and 𝜓 substitutes 𝑦 for 𝑧 and can be read 𝜑(𝑦). We don't require that 𝑥 and 𝑦 be distinct: if they aren't, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent. To obtain a closed-theorem form of this inference, prefix the hypotheses with ∀𝑥∀𝑧, conjoin them, and apply dvelimdf 2047. Other variants of this theorem are dvelimf 2046 (with no distinct variable restrictions) and dvelimALT 2041 (that avoids ax-10 1531). (Contributed by NM, 23-Nov-1994.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimor 2049*	Disjunctive distinct variable constraint elimination. A user of this theorem starts with a formula 𝜑 (containing 𝑧) and a distinct variable constraint between 𝑥 and 𝑧. The theorem makes it possible to replace the distinct variable constraint with the disjunct ∀𝑥𝑥 = 𝑦 (𝜓 is just a version of 𝜑 with 𝑦 substituted for 𝑧). (Contributed by Jim Kingdon, 11-May-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥𝜓)
Theorem	dveeq1 2050*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	sbal2 2051*	Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	nfsb4or 2052	A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∀𝑧 𝑧 = 𝑦 ∨ Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	nfd2 2053	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Wolf Lammen, 16-Sep-2021.)
⊢ (𝜑 → (∃𝑥𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	hbe1a 2054	Dual statement of hbe1 1521. (Contributed by Wolf Lammen, 15-Sep-2021.)
⊢ (∃𝑥∀𝑥𝜑 → ∀𝑥𝜑)
Theorem	nf5-1 2055	One direction of nf5 . (Contributed by Wolf Lammen, 16-Sep-2021.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → Ⅎ𝑥𝜑)
Theorem	nf5d 2056	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
1.4.6  Existential uniqueness
Syntax	weu 2057	Extend wff definition to include existential uniqueness ("there exists a unique 𝑥 such that 𝜑").
wff ∃!𝑥𝜑
Syntax	wmo 2058	Extend wff definition to include uniqueness ("there exists at most one 𝑥 such that 𝜑").
wff ∃*𝑥𝜑
Theorem	eujust 2059*	A soundness justification theorem for df-eu 2060, showing that the definition is equivalent to itself with its dummy variable renamed. Note that 𝑦 and 𝑧 needn't be distinct variables. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
Definition	df-eu 2060*	Define existential uniqueness, i.e., "there exists exactly one 𝑥 such that 𝜑". Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2082, eu2 2102, eu3 2104, and eu5 2105 (which in some cases we show with a hypothesis 𝜑 → ∀𝑦𝜑 in place of a distinct variable condition on 𝑦 and 𝜑). Double uniqueness is tricky: ∃!𝑥∃!𝑦𝜑 does not mean "exactly one 𝑥 and one 𝑦 " (see 2eu4 2151). (Contributed by NM, 5-Aug-1993.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Definition	df-mo 2061	Define "there exists at most one 𝑥 such that 𝜑". Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2112. For another possible definition see mo4 2119. (Contributed by NM, 5-Aug-1993.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Theorem	euf 2062*	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	eubidh 2063	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	eubid 2064	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	eubidv 2065*	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	eubii 2066	Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
Theorem	hbeu1 2067	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
⊢ (∃!𝑥𝜑 → ∀𝑥∃!𝑥𝜑)
Theorem	nfeu1 2068	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃!𝑥𝜑
Theorem	nfmo1 2069	Bound-variable hypothesis builder for "at most one". (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃*𝑥𝜑
Theorem	sb8eu 2070	Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8mo 2071	Variable substitution for "at most one". (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)
Theorem	nfeudv 2072*	Deduction version of nfeu 2076. Similar to nfeud 2073 but has the additional constraint that 𝑥 and 𝑦 must be distinct. (Contributed by Jim Kingdon, 25-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfeud 2073	Deduction version of nfeu 2076. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 25-May-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfmod 2074	Bound-variable hypothesis builder for "at most one". (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfeuv 2075*	Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 2076 but has the additional condition that 𝑥 and 𝑦 must be distinct. (Contributed by Jim Kingdon, 23-May-2018.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦𝜑
Theorem	nfeu 2076	Bound-variable hypothesis builder for existential uniqueness. Note that 𝑥 and 𝑦 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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦𝜑
Theorem	nfmo 2077	Bound-variable hypothesis builder for "at most one". (Contributed by NM, 9-Mar-1995.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦𝜑
Theorem	hbeu 2078	Bound-variable hypothesis builder for uniqueness. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Proof rewritten by Jim Kingdon, 24-May-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃!𝑦𝜑 → ∀𝑥∃!𝑦𝜑)
Theorem	hbeud 2079	Deduction version of hbeu 2078. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 25-May-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (∃!𝑦𝜓 → ∀𝑥∃!𝑦𝜓))
Theorem	sb8euh 2080	Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)
Theorem	cbveu 2081	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓)
Theorem	eu1 2082*	An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)))
Theorem	euor 2083	Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 21-Oct-2005.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓))
Theorem	euorv 2084*	Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓))
Theorem	mo2n 2085*	There is at most one of something which does not exist. (Contributed by Jim Kingdon, 2-Jul-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	mon 2086	There is at most one of something which does not exist. (Contributed by Jim Kingdon, 5-Jul-2018.)
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑)
Theorem	euex 2087	Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
Theorem	eumo0 2088*	Existential uniqueness implies "at most one". (Contributed by NM, 8-Jul-1994.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ (∃!𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	eumo 2089	Existential uniqueness implies "at most one". (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)
Theorem	eumoi 2090	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
⊢ ∃!𝑥𝜑    ⇒   ⊢ ∃*𝑥𝜑
Theorem	mobidh 2091	Formula-building rule for "at most one" quantifier (deduction form). (Contributed by NM, 8-Mar-1995.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	mobid 2092	Formula-building rule for "at most one" quantifier (deduction form). (Contributed by NM, 8-Mar-1995.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	mobidv 2093*	Formula-building rule for "at most one" quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	mobii 2094	Formula-building rule for "at most one" quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Theorem	hbmo1 2095	Bound-variable hypothesis builder for "at most one". (Contributed by NM, 8-Mar-1995.)
⊢ (∃*𝑥𝜑 → ∀𝑥∃*𝑥𝜑)
Theorem	hbmo 2096	Bound-variable hypothesis builder for "at most one". (Contributed by NM, 9-Mar-1995.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃*𝑦𝜑 → ∀𝑥∃*𝑦𝜑)
Theorem	cbvmo 2097	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
Theorem	cbvmow 2098*	Rule used to change bound variables, using implicit substitution. Version of cbvmo 2097 with a disjoint variable condition. (Contributed by NM, 9-Mar-1995.) (Revised by GG, 23-May-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
Theorem	mo23 2099*	An implication between two definitions of "there exists at most one." (Contributed by Jim Kingdon, 25-Jun-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	mor 2100*	Converse of mo23 2099 with an additional ∃𝑥𝜑 condition. (Contributed by Jim Kingdon, 25-Jun-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))