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	sb6f 2501	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2480 and does not require the nonfreeness hypothesis. Theorem sb6 2089 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 2372. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5f 2502	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2479 and does not require the nonfreeness hypothesis. Theorem sb5 2271 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 2372. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	nfsb4t 2503	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2504). Usage of this theorem is discouraged because it depends on ax-13 2372. (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 2504	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t 2503). Theorem nfsb 2527 replaces the distinctor antecedent with a disjoint variable condition. See nfsbv 2328 for a weaker version of nfsb 2527 not requiring ax-13 2372. (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 2372. Use nfsbv 2328 instead. (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbequ8 2505	Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2069. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑))
Theorem	sbie 2506	Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2312 and sbievw 2097. Usage of this theorem is discouraged because it depends on ax-13 2372. (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 2507	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2506) Usage of this theorem is discouraged because it depends on ax-13 2372. See sbiedw 2313, sbiedvw 2098 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 2508*	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2506). Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker sbiedvw 2098 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	2sbiev 2509*	Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. See 2sbievw 2099 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓)
Theorem	sbcom3 2510	Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2372. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2100. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2156. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑)
Theorem	sbco 2511	A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. See sbcov 2252 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 2512	An identity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Check out sbid2vw 2254 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 2513*	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 2372. See sbid2vw 2254 for a version with an extra disjoint variable condition requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑)
Theorem	sbidm 2514	An idempotent law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. (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 2515	A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2331 and sbco2vv 2102. Usage of this theorem is discouraged because it depends on ax-13 2372. (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 2516	A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbco3 2517	A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑)
Theorem	sbcom 2518	A commutativity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Check out sbcom3vv 2100 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 2519	Partially closed form of sbtr 2520. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by BJ, 4-Jun-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑦[𝑦 / 𝑥]𝜑 → 𝜑)
Theorem	sbtr 2520	A partial converse to sbt 2070. 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 2372. (Contributed by BJ, 15-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ [𝑦 / 𝑥]𝜑    ⇒   ⊢ 𝜑
Theorem	sb8 2521	Substitution of variable in universal quantifier. Usage of this theorem is discouraged because it depends on ax-13 2372. For a version requiring disjoint variables, but fewer axioms, see sb8v 2352. (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 2522	Substitution of variable in existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2372. For a version requiring disjoint variables, but fewer axioms, see sb8ev 2353. (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 2523	Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2524. (Revised by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb9i 2524	Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sbhb 2525*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑". Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 29-May-2009.) (New usage is discouraged.)
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))
Theorem	nfsbd 2526*	Deduction version of nfsb 2527. (Contributed by NM, 15-Feb-2013.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use nfsbv 2328 instead. (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑧𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓)
Theorem	nfsb 2527*	If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. See nfsbv 2328 for a version with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2372. (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 2372. Use nfsbv 2328 instead. (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	nfsbOLD 2528*	Obsolete version of nfsb 2527 as of 25-Feb-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	hbsb 2529*	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 2372. Use hbsbw 2171 instead. (New usage is discouraged.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	sb7f 2530*	This version of dfsb7 2279 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 1914, i.e., that does not have the concept of a variable not occurring in a formula. (Definition dfsb1 2485 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 2372. (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb7h 2531*	This version of dfsb7 2279 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 1914, i.e., that does not have the concept of a variable not occurring in a formula. (Definition dfsb1 2485 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 2372. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑)))
Theorem	sb10f 2532*	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 2372. (Contributed by NM, 9-May-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑))
Theorem	sbal1 2533*	Check out sbal 2161 for a version not dependent on ax-13 2372. 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 2534*	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 2372. Use sbal 2161 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	2sb8e 2535*	An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 2372. For a version requiring more disjoint variables, but fewer axioms, see 2sb8ev 2354. (Contributed by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
1.6  Uniqueness and unique existence
Theorem	dfmoeu 2536*	An elementary proof of moeu 2583 in disguise, connecting an expression characterizing uniqueness (df-mo 2540) to that of existential uniqueness (eu6 2574). No particular order of definition is required, as one can be derived from the other. This is shown here and in dfeumo 2537. (Contributed by Wolf Lammen, 27-May-2019.)
⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	dfeumo 2537*	An elementary proof showing the reverse direction of dfmoeu 2536. Here the characterizing expression of existential uniqueness (eu6 2574) is derived from that of uniqueness (df-mo 2540). (Contributed by Wolf Lammen, 3-Oct-2023.)
⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
1.6.1  Uniqueness: the at-most-one quantifier
Syntax	wmo 2538	Extend wff definition to include the at-most-one quantifier ("there exists at most one 𝑥 such that 𝜑").
wff ∃*𝑥𝜑
Theorem	mojust 2539*	Soundness justification theorem for df-mo 2540 (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). (Contributed by NM, 11-Mar-2010.) Added this theorem by adapting the proof of eujust 2571. (Revised by BJ, 30-Sep-2022.)
⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧))
Definition	df-mo 2540*	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 2569, therefore we avoid that ambiguous name. Notation of [BellMachover] p. 460, whose definition we show as mo3 2564. For other possible definitions see moeu 2583 and mo4 2566. (Contributed by Wolf Lammen, 27-May-2019.) Make this the definition (which used to be moeu 2583, while this definition was then proved as dfmo 2596). (Revised by BJ, 30-Sep-2022.)
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	nexmo 2541	Nonexistence implies uniqueness. (Contributed by BJ, 30-Sep-2022.) Avoid ax-11 2156. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑)
Theorem	exmo 2542	Any proposition holds for some 𝑥 or holds for at most one 𝑥. (Contributed by NM, 8-Mar-1995.) Shorten proof and avoid df-eu 2569. (Revised by BJ, 14-Oct-2022.)
⊢ (∃𝑥𝜑 ∨ ∃*𝑥𝜑)
Theorem	moabs 2543	Absorption of existence condition by uniqueness. (Contributed by NM, 4-Nov-2002.) Shorten proof and avoid df-eu 2569. (Revised by BJ, 14-Oct-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑))
Theorem	moim 2544	The at-most-one quantifier reverses implication. (Contributed by NM, 22-Apr-1995.)
⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
Theorem	moimi 2545	The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1914. (Revised by Steven Nguyen, 9-May-2023.)
⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)
Theorem	moimdv 2546*	The at-most-one quantifier reverses implication, deduction form. (Contributed by Thierry Arnoux, 25-Feb-2017.)
⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜒 → ∃*𝑥𝜓))
Theorem	mobi 2547	Equivalence theorem for the at-most-one quantifier. (Contributed by BJ, 7-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃*𝑥𝜑 ↔ ∃*𝑥𝜓))
Theorem	mobii 2548	Formula-building rule for the at-most-one quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) Avoid ax-5 1914. (Revised by Wolf Lammen, 24-Sep-2023.)
⊢ (𝜓 ↔ 𝜒)    ⇒   ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)
Theorem	mobidv 2549*	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 2550	Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by NM, 8-Mar-1995.) Remove dependency on ax-10 2139, ax-11 2156, ax-13 2372. (Revised by BJ, 14-Oct-2022.) (Proof shortened by Wolf Lammen, 18-Feb-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Theorem	moa1 2551	If an implication holds for at most one value, then its consequent holds for at most one value. See also ala1 1817 and exa1 1841. (Contributed by NM, 28-Jul-1995.) (Proof shortened by Wolf Lammen, 22-Dec-2018.) (Revised by BJ, 29-Mar-2021.)
⊢ (∃*𝑥(𝜑 → 𝜓) → ∃*𝑥𝜓)
Theorem	moan 2552	"At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
⊢ (∃*𝑥𝜑 → ∃*𝑥(𝜓 ∧ 𝜑))
Theorem	moani 2553	"At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
⊢ ∃*𝑥𝜑    ⇒   ⊢ ∃*𝑥(𝜓 ∧ 𝜑)
Theorem	moor 2554	"At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → ∃*𝑥𝜑)
Theorem	mooran1 2555	"At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ ((∃*𝑥𝜑 ∨ ∃*𝑥𝜓) → ∃*𝑥(𝜑 ∧ 𝜓))
Theorem	mooran2 2556	"At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃*𝑥(𝜑 ∨ 𝜓) → (∃*𝑥𝜑 ∧ ∃*𝑥𝜓))
Theorem	nfmo1 2557	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 2558	Bound-variable hypothesis builder for the at-most-one quantifier. Usage of this theorem is discouraged because it depends on ax-13 2372. See nfmodv 2559 for a version replacing the distinctor with a disjoint variable condition, not requiring ax-13 2372. (Contributed by Mario Carneiro, 14-Nov-2016.) Avoid df-eu 2569. (Revised by BJ, 14-Oct-2022.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfmodv 2559*	Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod 2561 for a version without disjoint variable conditions but requiring ax-13 2372. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by BJ, 28-Jan-2023.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfmov 2560*	Bound-variable hypothesis builder for the at-most-one quantifier. See nfmo 2562 for a version without disjoint variable conditions but requiring ax-13 2372. (Contributed by NM, 9-Mar-1995.) (Revised by Wolf Lammen, 2-Oct-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦𝜑
Theorem	nfmod 2561	Bound-variable hypothesis builder for the at-most-one quantifier. Deduction version of nfmo 2562. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfmodv 2559 when possible. (Contributed by Mario Carneiro, 14-Nov-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓)
Theorem	nfmo 2562	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 2372. Use the weaker nfmov 2560 when possible. (Contributed by NM, 9-Mar-1995.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃*𝑦𝜑
Theorem	mof 2563*	Version of df-mo 2540 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 8-Mar-1995.) Extract dfmo 2596 from this proof, and prove mof 2563 from it (as of 30-Sep-2022, directly from df-mo 2540). (Revised by Wolf Lammen, 28-May-2019.) Avoid ax-13 2372. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	mo3 2564*	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 2372. (Revised by BJ and WL, 29-Jan-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))
Theorem	mo 2565*	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 2566*	At-most-one quantifier expressed using implicit substitution. This theorem is also a direct consequence of mo4f 2567, 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 2156. (Contributed by NM, 26-Jul-1995.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2023.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
Theorem	mo4f 2567*	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 2372. (Revised by Wolf Lammen, 19-Jan-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ 𝜓) → 𝑥 = 𝑦))
1.6.2  Unique existence: the unique existential quantifier
Syntax	weu 2568	Extend wff definition to include the unique existential quantifier ("there exists a unique 𝑥 such that 𝜑").
wff ∃!𝑥𝜑
Definition	df-eu 2569	Define the existential uniqueness quantifier. This expresses unique existence, or existential uniqueness, which is the conjunction of existence (df-ex 1784) and uniqueness (df-mo 2540). 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 2540, 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 2612, eu2 2611, eu3v 2570, and eu6 2574. 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 2656). (Contributed by NM, 12-Aug-1993.) Make this the definition (which used to be eu6 2574, while this definition was then proved as dfeu 2595). (Revised by BJ, 30-Sep-2022.)
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Theorem	eu3v 2570*	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 2571*	Soundness justification theorem for eu6 2574 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 2572 for a proof that provides an example of how it can be achieved through the use of dvelim 2451. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
Theorem	eujustALT 2572*	Alternate proof of eujust 2571 illustrating the use of dvelim 2451. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧))
Theorem	eu6lem 2573*	Lemma of eu6im 2575. A dissection of an idiom characterizing existential uniqueness. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2569 was then proved as dfeu 2595. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Extract common proof lines. (Revised by Wolf Lammen, 3-Mar-2023.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
Theorem	eu6 2574*	Alternate definition of the unique existential quantifier df-eu 2569 not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2569 was then proved as dfeu 2595. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2156. (Revised by SN, 21-Sep-2023.)
⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	eu6im 2575*	One direction of eu6 2574 needs fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.)
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃!𝑥𝜑)
Theorem	euf 2576*	Version of eu6 2574 with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2018.) Avoid ax-13 2372. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
Theorem	euex 2577	Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.)
⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)
Theorem	eumo 2578	Existential uniqueness implies uniqueness. (Contributed by NM, 23-Mar-1995.)
⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑)
Theorem	eumoi 2579	Uniqueness inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
⊢ ∃!𝑥𝜑    ⇒   ⊢ ∃*𝑥𝜑
Theorem	exmoeub 2580	Existence implies that uniqueness is equivalent to unique existence. (Contributed by NM, 5-Apr-2004.)
⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	exmoeu 2581	Existence is equivalent to uniqueness implying existential uniqueness. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Wolf Lammen, 5-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.)
⊢ (∃𝑥𝜑 ↔ (∃*𝑥𝜑 → ∃!𝑥𝜑))
Theorem	moeuex 2582	Uniqueness implies that existence is equivalent to unique existence. (Contributed by BJ, 7-Oct-2022.)
⊢ (∃*𝑥𝜑 → (∃𝑥𝜑 ↔ ∃!𝑥𝜑))
Theorem	moeu 2583	Uniqueness is equivalent to existence implying unique existence. Alternate definition of the at-most-one quantifier, in terms of the existential quantifier and the unique existential quantifier. (Contributed by NM, 8-Mar-1995.) This used to be the definition of the at-most-one quantifier, while df-mo 2540 was then proved as dfmo 2596. (Revised by BJ, 30-Sep-2022.)
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
Theorem	eubi 2584	Equivalence theorem for the unique existential quantifier. Theorem *14.271 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) Reduce dependencies on axioms. (Revised by BJ, 7-Oct-2022.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∃!𝑥𝜑 ↔ ∃!𝑥𝜓))
Theorem	eubii 2585	Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) Avoid ax-5 1914. (Revised by Wolf Lammen, 27-Sep-2023.)
⊢ (𝜑 ↔ 𝜓)    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓)
Theorem	eubidv 2586*	Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)
⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	eubid 2587	Formula-building rule for the unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) (Proof shortened by Wolf Lammen, 19-Feb-2023.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒))
Theorem	nfeu1 2588	Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2589. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
⊢ Ⅎ𝑥∃!𝑥𝜑
Theorem	nfeu1ALT 2589	Alternate proof of nfeu1 2588. This illustrates the systematic way of proving nonfreeness in a defined expression: consider the definiens as a tree whose nodes are its subformulas, and prove by tree-induction nonfreeness of each node, starting from the leaves (generally using nfv 1918 or nf* theorems for previously defined expressions) and up to the root. Here, the definiens is a conjunction of two previously defined expressions, which automatically yields the present proof. (Contributed by BJ, 2-Oct-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥∃!𝑥𝜑
Theorem	nfeud2 2590	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by Wolf Lammen, 4-Oct-2018.) (Proof shortened by BJ, 14-Oct-2022.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use nfeudw 2591 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfeudw 2591*	Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu 2594. Version of nfeud 2592 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 15-Feb-2013.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfeud 2592	Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu 2594. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfeudw 2591 when possible. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓)
Theorem	nfeuw 2593*	Bound-variable hypothesis builder for the unique existential quantifier. Version of nfeu 2594 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 8-Mar-1995.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦𝜑
Theorem	nfeu 2594	Bound-variable hypothesis builder for the unique existential quantifier. Note that 𝑥 and 𝑦 need not be disjoint. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker nfeuw 2593 when possible. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃!𝑦𝜑
Theorem	dfeu 2595	Rederive df-eu 2569 from the old definition eu6 2574. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 25-May-2019.) (Proof shortened by BJ, 7-Oct-2022.) (Proof modification is discouraged.) Use df-eu 2569 instead. (New usage is discouraged.)
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
Theorem	dfmo 2596*	Rederive df-mo 2540 from the old definition moeu 2583. (Contributed by Wolf Lammen, 27-May-2019.) (Proof modification is discouraged.) Use df-mo 2540 instead. (New usage is discouraged.)
⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
Theorem	euequ 2597*	There exists a unique set equal to a given set. Special case of eueqi 3639 proved using only predicate calculus. The proof needs 𝑦 = 𝑧 be free of 𝑥. This is ensured by having 𝑥 and 𝑦 be distinct. Alternately, a distinctor ¬ ∀𝑥𝑥 = 𝑦 could have been used instead. See eueq 3638 and eueqi 3639 for classes. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof shortened by Wolf Lammen, 8-Sep-2019.) Reduce axiom usage. (Revised by Wolf Lammen, 1-Mar-2023.)
⊢ ∃!𝑥 𝑥 = 𝑦
Theorem	sb8eulem 2598*	Lemma. Factor out the common proof skeleton of sb8euv 2599 and sb8eu 2600. Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Aug-2019.) Factor out common proof lines. (Revised by Wolf Lammen, 9-Feb-2023.)
⊢ Ⅎ𝑦[𝑤 / 𝑥]𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8euv 2599*	Variable substitution in unique existential quantifier. Version of sb8eu 2600 requiring more disjoint variables, but fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Wolf Lammen, 7-Feb-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8eu 2600	Variable substitution in unique existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2372. For a version requiring more disjoint variables, but fewer axioms, see sb8euv 2599. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Aug-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)