P. 26 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2501-2600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ax12vALT 2501*	Alternate proof of ax12v2 2215, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	2ax6elem 2502	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2415 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 45247. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦))
Theorem	2ax6e 2503*	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2502 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.)
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)
Theorem	2sb5rf 2504*	Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    ⇒   ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	2sb6rf 2505*	Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 13-Apr-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	sbel2x 2506*	Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑))
Theorem	sb4b 2507	Simplified definition of substitution when variables are distinct. Version of sb6 2119 with a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 27-May-1997.) Revise df-sb 2097. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	sb3b 2508	Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2509. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2509. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	sb3 2509	One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
Theorem	sb1 2510	One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2311) or a nonfreeness hypothesis (sb5f 2530). Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker sb1v 2121 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2097. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sb2 2511	One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2119) or a nonfreeness hypothesis (sb6f 2529). Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 13-May-1993.) Revise df-sb 2097. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
Theorem	sb4a 2512	A version of one implication of sb4b 2507 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker sb4av 2280 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2097. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	dfsb1 2513	Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2097. Note that it does not require dummy variables in its definiens; this is done by having 𝑥 free in the first conjunct and bound in the second. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2097. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	hbsb2 2514	Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	nfsb2 2515	Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. Use nfs1v 2191 when sufficient. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	hbsb2a 2516	Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	sb4e 2517	One direction of a simplified definition of substitution that unlike sb4b 2507 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	hbsb2e 2518	Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑)
Theorem	hbsb3 2519	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2404. Check out bj-hbsb3v 37428 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1 2520	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2404. Check out nfs1v 2191 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	axc16ALT 2521*	Alternate proof of axc16 2297, shorter but requiring ax-10 2176, ax-11 2192, ax-13 2404 and using df-nf 1814 and df-sb 2097. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gALT 2522*	Alternate proof of axc16g 2296 that uses df-sb 2097 and requires ax-10 2176, ax-11 2192, ax-13 2404. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	equsb1 2523	Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker equsb1v 2140 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ [𝑦 / 𝑥]𝑥 = 𝑦
Theorem	equsb2 2524	Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2404. Check out equsb1v 2140 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ [𝑦 / 𝑥]𝑦 = 𝑥
Theorem	dfsb2 2525	An alternate definition of proper substitution that, like dfsb1 2513, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb3 2526	An alternate definition of proper substitution df-sb 2097 that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	drsb1 2527	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑))
Theorem	sb2ae 2528*	In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑))
Theorem	sb6f 2529	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2511 and does not require the nonfreeness hypothesis. Theorem sb6 2119 replaces the nonfreeness hypothesis with a disjoint variable condition on 𝑥, 𝑦 and requires fewer axioms. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5f 2530	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2510 and does not require the nonfreeness hypothesis. Theorem sb5 2311 replaces the nonfreeness hypothesis with a disjoint variable condition on 𝑥, 𝑦 and requires fewer axioms. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	nfsb4t 2531	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2532). Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑))
Theorem	nfsb4 2532	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t 2531). Theorem nfsb 2555 replaces the distinctor antecedent with a disjoint variable condition. See nfsbv 2363 for a weaker version of nfsb 2555 not requiring ax-13 2404. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2404. Use nfsbv 2363 instead. (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbequ8 2533	Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2097. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑))
Theorem	sbie 2534	Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2347 and sbievw 2128. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbied 2535	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2534) Usage of this theorem is discouraged because it depends on ax-13 2404. See sbiedw 2349, sbiedvw 2130 for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	sbiedv 2536*	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2534). Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker sbiedvw 2130 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	2sbiev 2537*	Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. See 2sbievw 2131 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓)
Theorem	sbcom3 2538	Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2404. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2132. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2192. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑)
Theorem	sbco 2539	A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. See sbcov 2292 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbid2 2540	An identity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. Check out sbid2vw 2295 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbid2v 2541*	An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). Usage of this theorem is discouraged because it depends on ax-13 2404. See sbid2vw 2295 for a version with an extra disjoint variable condition requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbidm 2542	An idempotent law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2 2543	A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2364 and sbco2vv 2134. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	sbco2d 2544	A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco3 2545	A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbcom 2546	A commutativity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2404. Check out sbcom3vv 2132 for a version requiring fewer axioms. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑)
Theorem	sbtrt 2547	Partially closed form of sbtr 2548. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BJ, 4-Jun-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑦[𝑦 / 𝑥]𝜑 → 𝜑)
Theorem	sbtr 2548	A partial converse to sbt 2100. If the substitution of a variable for a nonfree one in a wff gives a theorem, then the original wff is a theorem. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by BJ, 15-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ [𝑦 / 𝑥]𝜑    ⇒   ⊢ 𝜑
Theorem	sb8 2549	Substitution of variable in universal quantifier. Usage of this theorem is discouraged because it depends on ax-13 2404. For a version requiring disjoint variables, but fewer axioms, see sb8f 2386. (Contributed by NM, 16-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8e 2550	Substitution of variable in existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2404. For a version requiring disjoint variables, but fewer axioms, see sb8ef 2387. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9 2551	Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2552. (Revised by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9i 2552	Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sbhb 2553*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑". Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 29-May-2009.) (New usage is discouraged.)
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))
Theorem	nfsbd 2554*	Deduction version of nfsb 2555. (Contributed by NM, 15-Feb-2013.) Usage of this theorem is discouraged because it depends on ax-13 2404. Use nfsbv 2363 instead. (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓)
Theorem	nfsb 2555*	If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2363 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2404. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) Usage of this theorem is discouraged because it depends on ax-13 2404. Use nfsbv 2363 instead. (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	hbsb 2556*	If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. (Contributed by NM, 12-Aug-1993.) Usage of this theorem is discouraged because it depends on ax-13 2404. Use hbsbw 2206 instead. (New usage is discouraged.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	sb7f 2557*	This version of dfsb7 2314 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-5 1940, i.e., that does not have the concept of a variable not occurring in a formula. (Definition dfsb1 2513 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7h 2558*	This version of dfsb7 2314 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-5 1940, i.e., that does not have the concept of a variable not occurring in a formula. (Definition dfsb1 2513 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb10f 2559*	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. Usage of this theorem is discouraged because it depends on ax-13 2404. (Contributed by NM, 9-May-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑))
Theorem	sbal1 2560*	Check out sbal 2204 for a version not dependent on ax-13 2404. 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.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	sbal2 2561*	Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022.) (Proof shortened by Wolf Lammen, 23-Sep-2023.) Usage of this theorem is discouraged because it depends on ax-13 2404. Use sbal 2204 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	2sb8e 2562*	An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 2404. For a version requiring more disjoint variables, but fewer axioms, see 2sb8ef 2388. (Contributed by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
1.6  Uniqueness and unique existence
Theorem	dfmoeu 2563*	An elementary proof of moeu 2611 in disguise, connecting an expression characterizing uniqueness (df-mo 2567) to that of existential uniqueness (eu6 2602). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2564. (Contributed by Wolf Lammen, 27-May-2019.)
⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	dfeumo 2564*	An elementary proof showing the reverse direction of dfmoeu 2563. Here the characterizing expression of existential uniqueness (eu6 2602) is derived from that of uniqueness (df-mo 2567). (Contributed by Wolf Lammen, 3-Oct-2023.)
⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
1.6.1  Uniqueness: the at-most-one quantifier
Syntax	wmo 2565	Extend wff definition to include the at-most-one quantifier ("there exists at most one 𝑥 such that 𝜑").
wff ∃*𝑥𝜑
Theorem	mojust 2566*	Soundness justification theorem for df-mo 2567. (Contributed by NM, 11-Mar-2010.) Added this theorem by adapting the proof of eujust 2599. (Revised by BJ, 30-Sep-2022.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
Definition	df-mo 2567*	Define the at-most-one quantifier. The expression ∃*𝑥𝜑 is read "there exists at most one 𝑥 such that 𝜑". This is also called the "uniqueness quantifier" but that expression is also used for the unique existential quantifier df-eu 2597, therefore we avoid that ambiguous name. Notation of [BellMachover] p. 460, whose definition we show as mo3 2592. For other possible definitions see moeu 2611 and mo4 2594. Note that the definiens does not express "at-most-one" in the empty domain. Since the hypothesis relies on ax-6 1997, this case is excluded anyway. Nevertheless, it was suggested to begin with the definition of uniqueness (eu6 2602) and then define the at-most-one quantifier via moeu 2611. Both eu6 2602 and moeu 2611 remain valid in the empty domain. The hypothesis asserts that the definition is independent of the particular choice of the dummy variable 𝑦. Without this hypothesis, mojust 2566 would be derivable from propositional axioms alone: one could apply the definiens for ∃*𝑥𝜑 twice, using different dummy variables 𝑦 and 𝑧, and then invoke bitr3i 280 to establish their equivalence. This would jeopardize the independence of axioms, as demonstrated in an analoguous situation involving df-ss 3923 to prove ax-8 2145 (see in-ax8 36714). Prefer dfmo 2568 unless you can prove the hypothesis from fewer axioms in special cases. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2611, while this definition was then proved as dfmo 2568). (Revised by BJ, 30-Sep-2022.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	dfmo 2568*	Simplify definition df-mo 2567 by removing its provable hypothesis. (Contributed by Wolf Lammen, 15-Feb-2026.)
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	nexmo 2569	Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022.) Avoid ax-11 2192. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑)
Theorem	exmo 2570	Any proposition holds for some 𝑥 or holds for at most one 𝑥. (Contributed by NM, 8-Mar-1995.) Shorten proof and avoid df-eu 2597. (Revised by BJ, 14-Oct-2022.)
⊢ (∃𝑥𝜑 ∨ ∃*𝑥𝜑)
Theorem	moabs 2571	Absorption of existence condition by uniqueness. (Contributed by NM, 4-Nov-2002.) Shorten proof and avoid df-eu 2597. (Revised by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
Theorem	moim 2572	The at-most-one quantifier reverses implication. (Contributed by NM, 22-Apr-1995.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
Theorem	moimi 2573	The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)
Theorem	moimdv 2574*	The at-most-one quantifier reverses implication, deduction form. (Contributed by Thierry Arnoux, 25-Feb-2017.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜒 → ∃*𝑥𝜓))
Theorem	mobi 2575	Equivalence theorem for the at-most-one quantifier. (Contributed by BJ, 7-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃*𝑥𝜑 ↔ ∃*𝑥𝜓))
Theorem	mobii 2576	Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Theorem	mobidv 2577*	Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	mobid 2578	Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by NM, 8-Mar-1995.) Remove dependency on ax-10 2176, ax-11 2192, ax-13 2404. (Revised by BJ, 14-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	moa1 2579	If an implication holds for at most one value, then its consequent holds for at most one value. See also ala1 1843 and exa1 1868. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.)
⊢ (∃*𝑥(𝜑 → 𝜓) → ∃*𝑥𝜓)
Theorem	moan 2580	"At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
⊢ (∃*𝑥𝜑 → ∃*𝑥(𝜓 ∧ 𝜑))
Theorem	moani 2581	"At most one" is still true when a conjunct is added, inference form. (Contributed by NM, 9-Mar-1995.)
⊢ ∃*𝑥𝜑    ⇒   ⊢ ∃*𝑥(𝜓 ∧ 𝜑)
Theorem	moor 2582	"At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → ∃*𝑥𝜑)
Theorem	mooran1 2583	"At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ((∃*𝑥𝜑 ∨ ∃*𝑥𝜓) → ∃*𝑥(𝜑 ∧ 𝜓))
Theorem	mooran2 2584	"At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → (∃*𝑥𝜑 ∧ ∃*𝑥𝜓))
Theorem	nfmo1 2585	Bound-variable hypothesis builder for the at-most-one quantifier. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) Adapt to new definition. (Revised by BJ, 1-Oct-2022.)
⊢ Ⅎ𝑥∃*𝑥𝜑
Theorem	nfmod2 2586	Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 2404. See nfmodv 2587 for a version replacing the distinctor with a disjoint variable condition, not requiring ax-13 2404. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid df-eu 2597. (Revised by BJ, 14-Oct-2022.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfmodv 2587*	Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod 2589 for a version without disjoint variable conditions but requiring ax-13 2404. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by BJ, 28-Jan-2023.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfmov 2588*	Bound-variable hypothesis builder for the at-most-one quantifier. See nfmo 2590 for a version without disjoint variable conditions but requiring ax-13 2404. (Contributed by NM, 9-Mar-1995.) (Revised by Wolf Lammen, 2-Oct-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦𝜑
Theorem	nfmod 2589	Bound-variable hypothesis builder for the at-most-one quantifier. Deduction version of nfmo 2590. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker nfmodv 2587 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfmo 2590	Bound-variable hypothesis builder for the at-most-one quantifier. Note that 𝑥 and 𝑦 need not be disjoint. Usage of this theorem is discouraged because it depends on ax-13 2404. Use the weaker nfmov 2588 when possible. (Contributed by NM, 9-Mar-1995.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦𝜑
Theorem	mof 2591*	Version of df-mo 2567 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995.) Extract dfmo 2568 from this proof, and prove mof 2591 from it (as of 30-Sep-2022, directly from df-mo 2567). (Revised by Wolf Lammen, 28-May-2019.) Avoid ax-13 2404. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	mo3 2592*	Alternate definition of the at-most-one quantifier. 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.) Remove dependency on ax-13 2404. (Revised by BJ and WL, 29-Jan-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	mo 2593*	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	mo4 2594*	At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2595, but this proof is based on fewer axioms. By the way, swapping 𝑥, 𝑦 and 𝜑, 𝜓 leads to an expression for ∃*𝑦𝜓, which is equivalent to ∃*𝑥𝜑 (is a proof line), so the right hand side is a rare instance of an expression where swapping the quantifiers can be done without ax-11 2192. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
Theorem	mo4f 2595*	At-most-one quantifier expressed using implicit substitution. Note that the disjoint variable condition on 𝑦, 𝜑 can be replaced by the nonfreeness hypothesis ⊢ Ⅎ𝑦𝜑 with essentially the same proof. (Contributed by NM, 10-Apr-2004.) Remove dependency on ax-13 2404. (Revised by Wolf Lammen, 19-Jan-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
1.6.2  Unique existence: the unique existential quantifier
Syntax	weu 2596	Extend wff definition to include the unique existential quantifier ("there exists a unique 𝑥 such that 𝜑").
wff ∃!𝑥𝜑
Definition	df-eu 2597	Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1810) and uniqueness (df-mo 2567). The expression ∃!𝑥𝜑 is read "there exists exactly one 𝑥 such that 𝜑 " or "there exists a unique 𝑥 such that 𝜑". This is also called the "uniqueness quantifier" but that expression is also used for the at-most-one quantifier df-mo 2567, therefore we avoid that ambiguous name. Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2638, eu2 2637, eu3v 2598, and eu6 2602. As for double unique existence, beware that the expression ∃!𝑥∃!𝑦𝜑 means "there exists a unique 𝑥 such that there exists a unique 𝑦 such that 𝜑 " which is a weaker property than "there exists exactly one 𝑥 and one 𝑦 such that 𝜑 " (see 2eu4 2682). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2602, while this definition was then proved as dfeu 2623). (Revised by BJ, 30-Sep-2022.)
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Theorem	eu3v 2598*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) Replace a nonfreeness hypothesis with a disjoint variable condition on 𝜑, 𝑦 to reduce axiom usage. (Revised by Wolf Lammen, 29-May-2019.)
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	eujust 2599*	Soundness justification theorem for eu6 2602 when this was the definition of the unique existential quantifier (note that 𝑦 and 𝑧 need not be disjoint, although the weaker theorem with that disjoint variable condition added would be enough to justify the soundness of the definition). See eujustALT 2600 for a proof that provides an example of how it can be achieved through the use of dvelim 2483. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
Theorem	eujustALT 2600*	Alternate proof of eujust 2599 illustrating the use of dvelim 2483. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))