P. 25 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sbid2 2401	An identity law for substitution. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbidm 2402	An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jul-2019.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2 2403	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2d 2404	A composition law for substitution. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco3 2405	A composition law for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbcom 2406	A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 20-Sep-2018.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	sbt 2407	A substitution into a theorem yields a theorem. (See chvar 2250 and chvarv 2251 for versions using implicit substitution.) (Contributed by NM, 21-Jan-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 20-Jul-2018.)
⊢ 𝜑    ⇒   ⊢ [𝑦 / 𝑥]𝜑
Theorem	sbtrt 2408	Partially closed form of sbtr 2409. (Contributed by BJ, 4-Jun-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑦[𝑦 / 𝑥]𝜑 → 𝜑)
Theorem	sbtr 2409	A partial converse to sbt 2407. If the substitution of a variable for a non-free one in a wff gives a theorem, then the original wff is a theorem. (Contributed by BJ, 15-Sep-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ [𝑦 / 𝑥]𝜑    ⇒   ⊢ 𝜑
Theorem	sb5rf 2410	Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑))
Theorem	sb6rf 2411	Reversed substitution. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))
Theorem	sb8 2412	Substitution of variable in universal quantifier. (Contributed by NM, 16-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8e 2413	Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9 2414	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2415. (Revised by Wolf Lammen, 15-Jun-2019.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9i 2415	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	ax12vALT 2416*	Alternate proof of ax12v2 2036, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb6 2417*	Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left" is sb2 2340 and does not require any dv condition. Theorem sb6f 2373 replaces the dv condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5 2418*	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1 1870 and does not require any dv condition. Theorem sb5f 2374 replaces the dv condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	equsb3lem 2419*	Lemma for equsb3 2420. (Contributed by Raph Levien and FL, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧)
Theorem	equsb3 2420*	Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.) Remove dependency on ax-11 2021. (Revised by Wolf Lammen, 21-Sep-2018.)
⊢ ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧)
Theorem	equsb3ALT 2421*	Alternate proof of equsb3 2420, shorter but requiring ax-11 2021. (Contributed by Raph Levien and FL, 4-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧)
Theorem	elsb3 2422*	Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑥 / 𝑦]𝑦 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧)
Theorem	elsb4 2423*	Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
⊢ ([𝑥 / 𝑦]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑥)
Theorem	hbs1 2424*	The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1v 2425*	The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sbhb 2426*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑." (Contributed by NM, 29-May-2009.)
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))
Theorem	sbnf2 2427*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Sep-2018.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
Theorem	nfsb 2428*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	hbsb 2429*	If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by NM, 12-Aug-1993.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	nfsbd 2430*	Deduction version of nfsb 2428. (Contributed by NM, 15-Feb-2013.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓)
Theorem	2sb5 2431*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑))
Theorem	2sb6 2432*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	sbcom2 2433*	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 shortened by Wolf Lammen, 24-Sep-2018.)
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	sbcom4 2434*	Commutativity law for substitution. This theorem was incorrectly used as our previous version of pm11.07 2435 but may still be useful. (Contributed by Andrew Salmon, 17-Jun-2011.) (Proof shortened by Jim Kingdon, 22-Jan-2018.)
⊢ ([𝑤 / 𝑥][𝑦 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)
Theorem	pm11.07 2435	Axiom *11.07 in [WhiteheadRussell] p. 159. The original reads: *11.07 "Whatever possible argument 𝑥 may be, 𝜑(𝑥, 𝑦) is true whatever possible argument 𝑦 may be" implies the corresponding statement with 𝑥 and 𝑦 interchanged except in "𝜑(𝑥, 𝑦)". Under our formalism this appears to correspond to idi 2 and not to sbcom4 2434 as earlier thought. See https://groups.google.com/d/msg/metamath/iS0fOvSemC8/M1zTH8wxCAAJ. (Contributed by BJ, 16-Sep-2018.) (New usage is discouraged.)
⊢ 𝜑    ⇒   ⊢ 𝜑
Theorem	sb6a 2436*	Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))
Theorem	2ax6elem 2437	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2238 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 37795. (Contributed by Wolf Lammen, 27-Sep-2018.)
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦))
Theorem	2ax6e 2438*	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2437 with a distinct variable constraint. (Contributed by Wolf Lammen, 28-Sep-2018.)
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)
Theorem	2sb5rf 2439*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    ⇒   ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	2sb6rf 2440*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	sb7f 2441*	This version of dfsb7 2443 does not require that 𝜑 and 𝑧 be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1827 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1868 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7h 2442*	This version of dfsb7 2443 does not require that 𝜑 and 𝑧 be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1827 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1868 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	dfsb7 2443*	An alternate definition of proper substitution df-sb 1868. 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 2418, first 𝑧 for 𝑥 then 𝑦 for 𝑧. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2597. Theorem sb7h 2442 provides a version where 𝜑 and 𝑧 don't have to be distinct. (Contributed by NM, 28-Jan-2004.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb10f 2444*	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.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑))
Theorem	sbid2v 2445*	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 2446*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑))
Theorem	sbel2x 2447*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑))
Theorem	sbal1 2448*	A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 15-May-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	sbal2 2449*	Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 3-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	sbal 2450*	Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbex 2451*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.)
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbalv 2452*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥]∀𝑧𝜑 ↔ ∀𝑧𝜓)
Theorem	sbco4lem 2453*	Lemma for sbco4 2454. It replaces the temporary variable 𝑣 with another temporary variable 𝑤. (Contributed by Jim Kingdon, 26-Sep-2018.)
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sbco4 2454*	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	2sb8e 2455*	An equivalent expression for double existence. (Contributed by Wolf Lammen, 2-Nov-2019.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	exsb 2456*	An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2exsb 2457*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
1.6  Existential uniqueness
Syntax	weu 2458	Extend wff definition to include existential uniqueness ("there exists a unique 𝑥 such that 𝜑").
wff ∃!𝑥𝜑
Syntax	wmo 2459	Extend wff definition to include uniqueness ("there exists at most one 𝑥 such that 𝜑").
wff ∃*𝑥𝜑
Theorem	eujust 2460*	A soundness justification theorem for df-eu 2462, showing that the definition is equivalent to itself with its dummy variable renamed. Note that 𝑦 and 𝑧 needn't be distinct variables. See eujustALT 2461 for a proof that provides an example of how it can be achieved through the use of dvelim 2325. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
Theorem	eujustALT 2461*	Alternate proof of eujust 2460 illustrating the use of dvelim 2325. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
Definition	df-eu 2462*	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 2498, eu2 2497, eu3v 2486, and eu5 2484 (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 2544). (Contributed by NM, 12-Aug-1993.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Definition	df-mo 2463	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 2495. For other possible definitions see mo2 2467 and mo4 2505. (Contributed by NM, 8-Mar-1995.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Theorem	euequ1 2464*	Equality has existential uniqueness. Special case of eueq1 3346 proved using only predicate calculus. The proof needs 𝑦 = 𝑧 be free of 𝑥. This is ensured by having 𝑥 and 𝑦 be distinct. Alternatively, a distinctor ¬ ∀𝑥𝑥 = 𝑦 could have been used instead. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof shortened by Wolf Lammen, 8-Sep-2019.)
⊢ ∃!𝑥 𝑥 = 𝑦
Theorem	mo2v 2465*	Alternate definition of "at most one." Unlike mo2 2467, which is slightly more general, it does not depend on ax-11 2021 and ax-13 2234, whence it is preferable within predicate logic. Elsewhere, most theorems depend on these axioms anyway, so this advantage is no longer important. (Contributed by Wolf Lammen, 27-May-2019.) (Proof shortened by Wolf Lammen, 10-Nov-2019.)
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	euf 2466*	A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2018.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	mo2 2467*	Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.) Restrict dummy variable z. (Revised by Wolf Lammen, 28-May-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	nfeu1 2468	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃!𝑥𝜑
Theorem	nfmo1 2469	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃*𝑥𝜑
Theorem	nfeud2 2470	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by Wolf Lammen, 4-Oct-2018.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfmod2 2471	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfeud 2472	Deduction version of nfeu 2474. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfmod 2473	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfeu 2474	Bound-variable hypothesis builder for uniqueness. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦𝜑
Theorem	nfmo 2475	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦𝜑
Theorem	eubid 2476	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	mobid 2477	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	eubidv 2478*	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	mobidv 2479*	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	eubii 2480	Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
Theorem	mobii 2481	Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Theorem	euex 2482	Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2499. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)
⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
Theorem	exmo 2483	Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)
⊢ (∃𝑥𝜑 ∨ ∃*𝑥𝜑)
Theorem	eu5 2484	Uniqueness in terms of "at most one." Revised to reduce dependencies on axioms. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.)
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Theorem	exmoeu2 2485	Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	eu3v 2486*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) Add a distinct variable condition on 𝜑. (Revised by Wolf Lammen, 29-May-2019.)
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	eumo 2487	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)
Theorem	eumoi 2488	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
⊢ ∃!𝑥𝜑    ⇒   ⊢ ∃*𝑥𝜑
Theorem	moabs 2489	Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
Theorem	exmoeu 2490	Existence in terms of "at most one" and uniqueness. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Wolf Lammen, 5-Dec-2018.)
⊢ (∃𝑥𝜑 ↔ (∃*𝑥𝜑 → ∃!𝑥𝜑))
Theorem	sb8eu 2491	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.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8mo 2492	Variable substitution for "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑)
Theorem	cbveu 2493	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓)
Theorem	cbvmo 2494	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓)
Theorem	mo3 2495*	Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that 𝑦 not occur in 𝜑 in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Aug-2019.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	mo 2496*	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.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	eu2 2497*	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.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Theorem	eu1 2498*	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.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦)))
Theorem	euexALT 2499	Alternate proof of euex 2482. 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.)
⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
Theorem	euor 2500	Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓))