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	sbbi 2401	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
|- ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )
Theorem	spsbbi 2402	Specialization of biconditional. (Contributed by NM, 2-Jun-1993.)
|- ( A. x ( ph <-> ps ) -> ( [ y / x ] ph <-> [ y / x ] ps ) )
Theorem	sbbid 2403	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [ y / x ] ps <-> [ y / x ] ch ) )
Theorem	sblbis 2404	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> ps ) )
Theorem	sbrbis 2405	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> [ y / x ] ch ) )
Theorem	sbrbif 2406	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ x ch   &    |- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> ch ) )
Theorem	sbequ8ALT 2407	Alternate proof of sbequ8 1885, shorter but requiring more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( [ y / x ] ph <-> [ y / x ] ( x = y -> ph ) )
Theorem	sbie 2408	Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.)
|- F/ x ps   &    |- ( x = y -> ( ph <-> ps ) )   =>    |- ( [ y / x ] ph <-> ps )
Theorem	sbied 2409	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2408). (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.)
|- F/ x ph   &    |- ( ph -> F/ x ch )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( [ y / x ] ps <-> ch ) )
Theorem	sbiedv 2410*	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2408). (Contributed by NM, 7-Jan-2017.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( [ y / x ] ps <-> ch ) )
Theorem	sbcom3 2411	Substituting y for x and then z for y is equivalent to substituting z for both x and y. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph )
Theorem	sbco 2412	A composition law for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
|- ( [ y / x ] [ x / y ] ph <-> [ y / x ] ph )
Theorem	sbid2 2413	An identity law for substitution. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ x ph   =>    |- ( [ y / x ] [ x / y ] ph <-> ph )
Theorem	sbidm 2414	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.)
|- ( [ y / x ] [ y / x ] ph <-> [ y / x ] ph )
Theorem	sbco2 2415	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.)
|- F/ z ph   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	sbco2d 2416	A composition law for substitution. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ x ph   &    |- F/ z ph   &    |- ( ph -> F/ z ps )   =>    |- ( ph -> ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps ) )
Theorem	sbco3 2417	A composition law for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )
Theorem	sbcom 2418	A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 20-Sep-2018.)
|- ( [ y / z ] [ y / x ] ph <-> [ y / x ] [ y / z ] ph )
Theorem	sbt 2419	A substitution into a theorem yields a theorem. (See chvar 2262 and chvarv 2263 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.)
|- ph   =>    |- [ y / x ] ph
Theorem	sbtrt 2420	Partially closed form of sbtr 2421. (Contributed by BJ, 4-Jun-2019.)
|- F/ y ph   =>    |- ( A. y [ y / x ] ph -> ph )
Theorem	sbtr 2421	A partial converse to sbt 2419. 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.)
|- F/ y ph   &    |- [ y / x ] ph   =>    |- ph
Theorem	sb5rf 2422	Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.)
|- F/ y ph   =>    |- ( ph <-> E. y ( y = x /\ [ y / x ] ph ) )
Theorem	sb6rf 2423	Reversed substitution. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
|- F/ y ph   =>    |- ( ph <-> A. y ( y = x -> [ y / x ] ph ) )
Theorem	sb8 2424	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.)
|- F/ y ph   =>    |- ( A. x ph <-> A. y [ y / x ] ph )
Theorem	sb8e 2425	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.)
|- F/ y ph   =>    |- ( E. x ph <-> E. y [ y / x ] ph )
Theorem	sb9 2426	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2427. (Revised by Wolf Lammen, 15-Jun-2019.)
|- ( A. x [ x / y ] ph <-> A. y [ y / x ] ph )
Theorem	sb9i 2427	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.)
|- ( A. x [ x / y ] ph -> A. y [ y / x ] ph )
Theorem	ax12vALT 2428*	Alternate proof of ax12v2 2049, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) )
Theorem	sb6 2429*	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 2352 and does not require any dv condition. Theorem sb6f 2385 replaces the dv condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
Theorem	sb5 2430*	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1 1883 and does not require any dv condition. Theorem sb5f 2386 replaces the dv condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.)
|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
Theorem	equsb3lem 2431*	Lemma for equsb3 2432. (Contributed by Raph Levien and FL, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ x / y ] y = z <-> x = z )
Theorem	equsb3 2432*	Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 21-Sep-2018.)
|- ( [ x / y ] y = z <-> x = z )
Theorem	equsb3ALT 2433*	Alternate proof of equsb3 2432, shorter but requiring ax-11 2034. (Contributed by Raph Levien and FL, 4-Dec-2005.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( [ x / y ] y = z <-> x = z )
Theorem	elsb3 2434*	Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ x / y ] y e. z <-> x e. z )
Theorem	elsb4 2435*	Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ x / y ] z e. y <-> z e. x )
Theorem	hbs1 2436*	The setvar x is not free in [ y / x ] ph when x and y are distinct. (Contributed by NM, 26-May-1993.)
|- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	nfs1v 2437*	The setvar x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x [ y / x ] ph
Theorem	sbhb 2438*	Two ways of expressing " x is (effectively) not free in ph." (Contributed by NM, 29-May-2009.)
|- ( ( ph -> A. x ph ) <-> A. y ( ph -> [ y / x ] ph ) )
Theorem	sbnf2 2439*	Two ways of expressing " x is (effectively) not free in ph." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Sep-2018.)
|- ( F/ x ph <-> A. y A. z ( [ y / x ] ph <-> [ z / x ] ph ) )
Theorem	nfsb 2440*	If z is not free in ph, it is not free in [ y / x ] ph when y and z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ z ph   =>    |- F/ z [ y / x ] ph
Theorem	hbsb 2441*	If z is not free in ph, it is not free in [ y / x ] ph when y and z are distinct. (Contributed by NM, 12-Aug-1993.)
|- ( ph -> A. z ph )   =>    |- ( [ y / x ] ph -> A. z [ y / x ] ph )
Theorem	nfsbd 2442*	Deduction version of nfsb 2440. (Contributed by NM, 15-Feb-2013.)
|- F/ x ph   &    |- ( ph -> F/ z ps )   =>    |- ( ph -> F/ z [ y / x ] ps )
Theorem	2sb5 2443*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( [ z / x ] [ w / y ] ph <-> E. x E. y ( ( x = z /\ y = w ) /\ ph ) )
Theorem	2sb6 2444*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( [ z / x ] [ w / y ] ph <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
Theorem	sbcom2 2445*	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.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sbcom4 2446*	Commutativity law for substitution. This theorem was incorrectly used as our previous version of pm11.07 2447 but may still be useful. (Contributed by Andrew Salmon, 17-Jun-2011.) (Proof shortened by Jim Kingdon, 22-Jan-2018.)
|- ( [ w / x ] [ y / z ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	pm11.07 2447	Axiom *11.07 in [WhiteheadRussell] p. 159. The original reads: *11.07 "Whatever possible argument x may be, ph ( x , y ) is true whatever possible argument y may be" implies the corresponding statement with x and y interchanged except in " ph ( x , y )". Under our formalism this appears to correspond to idi 2 and not to sbcom4 2446 as earlier thought. See https://groups.google.com/d/msg/metamath/iS0fOvSemC8/M1zTH8wxCAAJ. (Contributed by BJ, 16-Sep-2018.) (New usage is discouraged.)
|- ph   =>    |- ph
Theorem	sb6a 2448*	Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.)
|- ( [ y / x ] ph <-> A. x ( x = y -> [ x / y ] ph ) )
Theorem	2ax6elem 2449	We can always find values matching x and y, as long as they are represented by distinct variables. This theorem merges two ax6e 2250 instances E. z z = x and E. w w = y into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 38774. (Contributed by Wolf Lammen, 27-Sep-2018.)
|- ( -. A. w w = z -> E. z E. w ( z = x /\ w = y ) )
Theorem	2ax6e 2450*	We can always find values matching x and y, as long as they are represented by distinct variables. Version of 2ax6elem 2449 with a distinct variable constraint. (Contributed by Wolf Lammen, 28-Sep-2018.)
|- E. z E. w ( z = x /\ w = y )
Theorem	2sb5rf 2451*	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.)
|- F/ z ph   &    |- F/ w ph   =>    |- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )
Theorem	2sb6rf 2452*	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.)
|- F/ z ph   &    |- F/ w ph   =>    |- ( ph <-> A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) )
Theorem	sb7f 2453*	This version of dfsb7 2455 does not require that ph and z be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1839 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1881 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.)
|- F/ z ph   =>    |- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb7h 2454*	This version of dfsb7 2455 does not require that ph and z be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1839 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1881 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.)
|- ( ph -> A. z ph )   =>    |- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	dfsb7 2455*	An alternate definition of proper substitution df-sb 1881. By introducing a dummy variable z in the definiens, we are able to eliminate any distinct variable restrictions among the variables x, y, and ph of the definiendum. No distinct variable conflicts arise because z effectively insulates x from y. To achieve this, we use a chain of two substitutions in the form of sb5 2430, first z for x then y for z. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2609. Theorem sb7h 2454 provides a version where ph and z don't have to be distinct. (Contributed by NM, 28-Jan-2004.)
|- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb10f 2456*	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.)
|- F/ x ph   =>    |- ( [ y / z ] ph <-> E. x ( x = y /\ [ x / z ] ph ) )
Theorem	sbid2v 2457*	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.)
|- ( [ y / x ] [ x / y ] ph <-> ph )
Theorem	sbelx 2458*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> E. x ( x = y /\ [ x / y ] ph ) )
Theorem	sbel2x 2459*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
|- ( ph <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
Theorem	sbal1 2460*	A theorem used in elimination of disjoint variable restriction on x and y by replacing it with a distinctor -. A. x x = z. (Contributed by NM, 15-May-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2018.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbal2 2461*	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.)
|- ( -. A. x x = y -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbal 2462*	Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.)
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
Theorem	sbex 2463*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.)
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
Theorem	sbalv 2464*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] A. z ph <-> A. z ps )
Theorem	sbco4lem 2465*	Lemma for sbco4 2466. It replaces the temporary variable v with another temporary variable w. (Contributed by Jim Kingdon, 26-Sep-2018.)
|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
Theorem	sbco4 2466*	Two ways of exchanging two variables. Both sides of the biconditional exchange x and y, either via two temporary variables u and v, or a single temporary w. (Contributed by Jim Kingdon, 25-Sep-2018.)
|- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
Theorem	2sb8e 2467*	An equivalent expression for double existence. (Contributed by Wolf Lammen, 2-Nov-2019.)
|- ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )
Theorem	exsb 2468*	An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
|- ( E. x ph <-> E. y A. x ( x = y -> ph ) )
Theorem	2exsb 2469*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
|- ( E. x E. y ph <-> E. z E. w A. x A. y ( ( x = z /\ y = w ) -> ph ) )
1.6  Existential uniqueness
Syntax	weu 2470	Extend wff definition to include existential uniqueness ("there exists a unique x such that ph").
wff E! x ph
Syntax	wmo 2471	Extend wff definition to include uniqueness ("there exists at most one x such that ph").
wff E* x ph
Theorem	eujust 2472*	A soundness justification theorem for df-eu 2474, showing that the definition is equivalent to itself with its dummy variable renamed. Note that y and z needn't be distinct variables. See eujustALT 2473 for a proof that provides an example of how it can be achieved through the use of dvelim 2337. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
|- ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) )
Theorem	eujustALT 2473*	Alternate proof of eujust 2472 illustrating the use of dvelim 2337. (Contributed by NM, 11-Mar-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( E. y A. x ( ph <-> x = y ) <-> E. z A. x ( ph <-> x = z ) )
Definition	df-eu 2474*	Define existential uniqueness, i.e. "there exists exactly one x such that ph." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 2510, eu2 2509, eu3v 2498, and eu5 2496 (which in some cases we show with a hypothesis ph -> A. y ph in place of a distinct variable condition on y and ph). Double uniqueness is tricky: E! x E! y ph does not mean "exactly one x and one y " (see 2eu4 2556). (Contributed by NM, 12-Aug-1993.)
|- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Definition	df-mo 2475	Define "there exists at most one x such that ph." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 2507. For other possible definitions see mo2 2479 and mo4 2517. (Contributed by NM, 8-Mar-1995.)
|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
Theorem	euequ1 2476*	Equality has existential uniqueness. Special case of eueq1 3379 proved using only predicate calculus. The proof needs y = z be free of x. This is ensured by having x and y be distinct. Alternately, a distinctor -. A. x x = y could have been used instead. (Contributed by Stefan Allan, 4-Dec-2008.) (Proof shortened by Wolf Lammen, 8-Sep-2019.)
|- E! x x = y
Theorem	mo2v 2477*	Alternate definition of "at most one." Unlike mo2 2479, which is slightly more general, it does not depend on ax-11 2034 and ax-13 2246, 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.)
|- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
Theorem	euf 2478*	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.)
|- F/ y ph   =>    |- ( E! x ph <-> E. y A. x ( ph <-> x = y ) )
Theorem	mo2 2479*	Alternate definition of "at most one." (Contributed by NM, 8-Mar-1995.) Restrict dummy variable z. (Revised by Wolf Lammen, 28-May-2019.)
|- F/ y ph   =>    |- ( E* x ph <-> E. y A. x ( ph -> x = y ) )
Theorem	nfeu1 2480	Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x E! x ph
Theorem	nfmo1 2481	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x E* x ph
Theorem	nfeud2 2482	Bound-variable hypothesis builder for uniqueness. (Contributed by Mario Carneiro, 14-Nov-2016.) (Proof shortened by Wolf Lammen, 4-Oct-2018.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/ x E! y ps )
Theorem	nfmod2 2483	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/ x E* y ps )
Theorem	nfeud 2484	Deduction version of nfeu 2486. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E! y ps )
Theorem	nfmod 2485	Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.)
|- F/ y ph   &    |- ( ph -> F/ x ps )   =>    |- ( ph -> F/ x E* y ps )
Theorem	nfeu 2486	Bound-variable hypothesis builder for uniqueness. Note that x and y needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.)
|- F/ x ph   =>    |- F/ x E! y ph
Theorem	nfmo 2487	Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
|- F/ x ph   =>    |- F/ x E* y ph
Theorem	eubid 2488	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	mobid 2489	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	eubidv 2490*	Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E! x ps <-> E! x ch ) )
Theorem	mobidv 2491*	Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E* x ps <-> E* x ch ) )
Theorem	eubii 2492	Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- ( ph <-> ps )   =>    |- ( E! x ph <-> E! x ps )
Theorem	mobii 2493	Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
|- ( ps <-> ch )   =>    |- ( E* x ps <-> E* x ch )
Theorem	euex 2494	Existential uniqueness implies existence. For a shorter proof using more axioms, see euexALT 2511. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.)
|- ( E! x ph -> E. x ph )
Theorem	exmo 2495	Something exists or at most one exists. (Contributed by NM, 8-Mar-1995.)
|- ( E. x ph \/ E* x ph )
Theorem	eu5 2496	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.)
|- ( E! x ph <-> ( E. x ph /\ E* x ph ) )
Theorem	exmoeu2 2497	Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
|- ( E. x ph -> ( E* x ph <-> E! x ph ) )
Theorem	eu3v 2498*	An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) Add a distinct variable condition on ph. (Revised by Wolf Lammen, 29-May-2019.)
|- ( E! x ph <-> ( E. x ph /\ E. y A. x ( ph -> x = y ) ) )
Theorem	eumo 2499	Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.)
|- ( E! x ph -> E* x ph )
Theorem	eumoi 2500	"At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
|- E! x ph   =>    |- E* x ph