HomeHome Intuitionistic Logic Explorer
Theorem List (p. 21 of 154)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 2001-2100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem2sb5rf 2001* Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
 |-  ( ph  ->  A. z ph )   &    |-  ( ph  ->  A. w ph )   =>    |-  ( ph  <->  E. z E. w ( ( z  =  x  /\  w  =  y )  /\  [
 z  /  x ] [ w  /  y ] ph ) )
 
Theorem2sb6rf 2002* Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
 |-  ( ph  ->  A. z ph )   &    |-  ( ph  ->  A. w ph )   =>    |-  ( ph  <->  A. z A. w ( ( z  =  x  /\  w  =  y )  ->  [ z  /  x ] [ w  /  y ] ph )
 )
 
Theoremdfsb7 2003* An alternate definition of proper substitution df-sb 1774. 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 1899, first  z for  x then  y for  z. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 2004 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 )
 ) )
 
Theoremsb7f 2004* This version of dfsb7 2003 does not require that  ph and  z be disjoint. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1537, i.e., that does not have the concept of a variable not occurring in a formula. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( ph  ->  A. z ph )   =>    |-  ( [ y  /  x ] ph  <->  E. z ( z  =  y  /\  E. x ( x  =  z  /\  ph )
 ) )
 
Theoremsb7af 2005* An alternate definition of proper substitution df-sb 1774. Similar to dfsb7a 2006 but does not require that  ph and  z be distinct. Similar to sb7f 2004 in that it involves a dummy variable  z, but expressed in terms of  A. rather than  E.. (Contributed by Jim Kingdon, 5-Feb-2018.)
 |- 
 F/ z ph   =>    |-  ( [ y  /  x ] ph  <->  A. z ( z  =  y  ->  A. x ( x  =  z  -> 
 ph ) ) )
 
Theoremdfsb7a 2006* An alternate definition of proper substitution df-sb 1774. Similar to dfsb7 2003 in that it involves a dummy variable  z, but expressed in terms of  A. rather than  E.. For a version which only requires  F/ z ph rather than  z and  ph being distinct, see sb7af 2005. (Contributed by Jim Kingdon, 5-Feb-2018.)
 |-  ( [ y  /  x ] ph  <->  A. z ( z  =  y  ->  A. x ( x  =  z  -> 
 ph ) ) )
 
Theoremsb10f 2007* 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.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( [ y  /  z ] ph  <->  E. x ( x  =  y  /\  [ x  /  z ] ph ) )
 
Theoremsbid2v 2008* 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 )
 
Theoremsbelx 2009* Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  <->  E. x ( x  =  y  /\  [ x  /  y ] ph ) )
 
Theoremsbel2x 2010* Elimination of double substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  <->  E. x E. y
 ( ( x  =  z  /\  y  =  w )  /\  [
 y  /  w ] [ x  /  z ] ph ) )
 
Theoremsbalyz 2011* Move universal quantifier in and out of substitution. Identical to sbal 2012 except that it has an additional distinct variable constraint on  y and  z. (Contributed by Jim Kingdon, 29-Dec-2017.)
 |-  ( [ z  /  y ] A. x ph  <->  A. x [ z  /  y ] ph )
 
Theoremsbal 2012* Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
 |-  ( [ z  /  y ] A. x ph  <->  A. x [ z  /  y ] ph )
 
Theoremsbal1yz 2013* Lemma for proving sbal1 2014. Same as sbal1 2014 but with an additional disjoint variable condition on 
y ,  z. (Contributed by Jim Kingdon, 23-Feb-2018.)
 |-  ( -.  A. x  x  =  z  ->  ( [ z  /  y ] A. x ph  <->  A. x [ z  /  y ] ph )
 )
 
Theoremsbal1 2014* A theorem used in elimination of disjoint variable conditions on  x ,  y by replacing it with a distinctor  -.  A. x x  =  z. (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.)
 |-  ( -.  A. x  x  =  z  ->  ( [ z  /  y ] A. x ph  <->  A. x [ z  /  y ] ph )
 )
 
Theoremsbexyz 2015* Move existential quantifier in and out of substitution. Identical to sbex 2016 except that it has an additional disjoint variable condition on  y ,  z. (Contributed by Jim Kingdon, 29-Dec-2017.)
 |-  ( [ z  /  y ] E. x ph  <->  E. x [ z  /  y ] ph )
 
Theoremsbex 2016* Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
 |-  ( [ z  /  y ] E. x ph  <->  E. x [ z  /  y ] ph )
 
Theoremsbalv 2017* Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
 |-  ( [ y  /  x ] ph  <->  ps )   =>    |-  ( [ y  /  x ] A. z ph  <->  A. z ps )
 
Theoremsbco4lem 2018* Lemma for sbco4 2019. 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 )
 
Theoremsbco4 2019* 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 )
 
Theoremexsb 2020* An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
 |-  ( E. x ph  <->  E. y A. x ( x  =  y  ->  ph )
 )
 
Theorem2exsb 2021* An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.)
 |-  ( E. x E. y ph  <->  E. z E. w A. x A. y ( ( x  =  z 
 /\  y  =  w )  ->  ph ) )
 
TheoremdvelimALT 2022* Version of dvelim 2029 that doesn't use ax-10 1516. Because it has different distinct variable constraints than dvelim 2029 and is used in important proofs, it would be better if it had a name which does not end in ALT (ideally more close to set.mm naming). (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
 |-  ( ph  ->  A. x ph )   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremdvelimfv 2023* Like dvelimf 2027 but with a distinct variable constraint on  x and  z. (Contributed by Jim Kingdon, 6-Mar-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremhbsb4 2024 A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
 |-  ( ph  ->  A. z ph )   =>    |-  ( -.  A. z  z  =  y  ->  ( [ y  /  x ] ph  ->  A. z [
 y  /  x ] ph ) )
 
Theoremhbsb4t 2025 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 2024). (Contributed by NM, 7-Apr-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 |-  ( A. x A. z ( ph  ->  A. z ph )  ->  ( -.  A. z  z  =  y  ->  ( [ y  /  x ] ph  ->  A. z [
 y  /  x ] ph ) ) )
 
Theoremnfsb4t 2026 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 2024). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof rewritten by Jim Kingdon, 9-May-2018.)
 |-  ( A. x F/ z ph  ->  ( -.  A. z  z  =  y  ->  F/ z [ y  /  x ] ph ) )
 
Theoremdvelimf 2027 Version of dvelim 2029 without any variable restrictions. (Contributed by NM, 1-Oct-2002.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ps  ->  A. z ps )   &    |-  (
 z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremdvelimdf 2028 Deduction form of dvelimf 2027. This version may be useful if we want to avoid ax-17 1537 and use ax-16 1825 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
 |- 
 F/ x ph   &    |-  F/ z ph   &    |-  ( ph  ->  F/ x ps )   &    |-  ( ph  ->  F/ z ch )   &    |-  ( ph  ->  ( z  =  y  ->  ( ps  <->  ch ) ) )   =>    |-  ( ph  ->  ( -.  A. x  x  =  y 
 ->  F/ x ch )
 )
 
Theoremdvelim 2029* This theorem can be used to eliminate a distinct variable restriction on  x and  z and replace it with the "distinctor"  -.  A. x x  =  y as an antecedent.  ph normally has  z free and can be read  ph ( z ), and  ps substitutes  y for  z and can be read  ph ( y ). We don't require that 
x and  y be distinct: if they aren't, the distinctor will become false (in multiple-element domains of discourse) and "protect" the consequent.

To obtain a closed-theorem form of this inference, prefix the hypotheses with  A. x A. z, conjoin them, and apply dvelimdf 2028.

Other variants of this theorem are dvelimf 2027 (with no distinct variable restrictions) and dvelimALT 2022 (that avoids ax-10 1516). (Contributed by NM, 23-Nov-1994.)

 |-  ( ph  ->  A. x ph )   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremdvelimor 2030* Disjunctive distinct variable constraint elimination. A user of this theorem starts with a formula  ph (containing  z) and a distinct variable constraint between 
x and  z. The theorem makes it possible to replace the distinct variable constraint with the disjunct  A. x x  =  y ( ps is just a version of  ph with  y substituted for  z). (Contributed by Jim Kingdon, 11-May-2018.)
 |- 
 F/ x ph   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( A. x  x  =  y  \/  F/ x ps )
 
Theoremdveeq1 2031* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.)
 |-  ( -.  A. x  x  =  y  ->  ( y  =  z  ->  A. x  y  =  z ) )
 
Theoremsbal2 2032* Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.)
 |-  ( -.  A. x  x  =  y  ->  ( [ z  /  y ] A. x ph  <->  A. x [ z  /  y ] ph )
 )
 
Theoremnfsb4or 2033 A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.)
 |- 
 F/ z ph   =>    |-  ( A. z  z  =  y  \/  F/ z [ y  /  x ] ph )
 
Theoremnfd2 2034 Deduce that  x is not free in  ps in a context. (Contributed by Wolf Lammen, 16-Sep-2021.)
 |-  ( ph  ->  ( E. x ps  ->  A. x ps ) )   =>    |-  ( ph  ->  F/ x ps )
 
Theoremhbe1a 2035 Dual statement of hbe1 1506. (Contributed by Wolf Lammen, 15-Sep-2021.)
 |-  ( E. x A. x ph  ->  A. x ph )
 
Theoremnf5-1 2036 One direction of nf5 . (Contributed by Wolf Lammen, 16-Sep-2021.)
 |-  ( A. x (
 ph  ->  A. x ph )  ->  F/ x ph )
 
Theoremnf5d 2037 Deduce that  x is not free in  ps in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
 |- 
 F/ x ph   &    |-  ( ph  ->  ( ps  ->  A. x ps ) )   =>    |-  ( ph  ->  F/ x ps )
 
1.4.6  Existential uniqueness
 
Syntaxweu 2038 Extend wff definition to include existential uniqueness ("there exists a unique  x such that  ph").
 wff  E! x ph
 
Syntaxwmo 2039 Extend wff definition to include uniqueness ("there exists at most one  x such that  ph").
 wff  E* x ph
 
Theoremeujust 2040* A soundness justification theorem for df-eu 2041, showing that the definition is equivalent to itself with its dummy variable renamed. Note that  y and  z needn't be distinct variables. (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
 ) )
 
Definitiondf-eu 2041* 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 2063, eu2 2082, eu3 2084, and eu5 2085 (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 2131). (Contributed by NM, 5-Aug-1993.)
 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
 
Definitiondf-mo 2042 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 2092. For another possible definition see mo4 2099. (Contributed by NM, 5-Aug-1993.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
 
Theoremeuf 2043* A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.)
 |-  ( ph  ->  A. y ph )   =>    |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
 
Theoremeubidh 2044 Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubid 2045 Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
 |- 
 F/ x ph   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubidv 2046* Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubii 2047 Introduce unique existential 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 )
 
Theoremhbeu1 2048 Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
 |-  ( E! x ph  ->  A. x E! x ph )
 
Theoremnfeu1 2049 Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
 |- 
 F/ x E! x ph
 
Theoremnfmo1 2050 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
 
Theoremsb8eu 2051 Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
 |- 
 F/ y ph   =>    |-  ( E! x ph  <->  E! y [ y  /  x ] ph )
 
Theoremsb8mo 2052 Variable substitution for "at most one". (Contributed by Alexander van der Vekens, 17-Jun-2017.)
 |- 
 F/ y ph   =>    |-  ( E* x ph  <->  E* y [ y  /  x ] ph )
 
Theoremnfeudv 2053* Deduction version of nfeu 2057. Similar to nfeud 2054 but has the additional constraint that  x and  y must be distinct. (Contributed by Jim Kingdon, 25-May-2018.)
 |- 
 F/ y ph   &    |-  ( ph  ->  F/ x ps )   =>    |-  ( ph  ->  F/ x E! y ps )
 
Theoremnfeud 2054 Deduction version of nfeu 2057. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 25-May-2018.)
 |- 
 F/ y ph   &    |-  ( ph  ->  F/ x ps )   =>    |-  ( ph  ->  F/ x E! y ps )
 
Theoremnfmod 2055 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 )
 
Theoremnfeuv 2056* Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 2057 but has the additional condition that  x and  y must be distinct. (Contributed by Jim Kingdon, 23-May-2018.)
 |- 
 F/ x ph   =>    |- 
 F/ x E! y ph
 
Theoremnfeu 2057 Bound-variable hypothesis builder for existential uniqueness. Note that  x and  y needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 23-May-2018.)
 |- 
 F/ x ph   =>    |- 
 F/ x E! y ph
 
Theoremnfmo 2058 Bound-variable hypothesis builder for "at most one". (Contributed by NM, 9-Mar-1995.)
 |- 
 F/ x ph   =>    |- 
 F/ x E* y ph
 
Theoremhbeu 2059 Bound-variable hypothesis builder for uniqueness. Note that  x and  y needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Proof rewritten by Jim Kingdon, 24-May-2018.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( E! y ph  ->  A. x E! y ph )
 
Theoremhbeud 2060 Deduction version of hbeu 2059. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 25-May-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  A. y ph )   &    |-  ( ph  ->  ( ps  ->  A. x ps ) )   =>    |-  ( ph  ->  ( E! y ps  ->  A. x E! y ps ) )
 
Theoremsb8euh 2061 Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.)
 |-  ( ph  ->  A. y ph )   =>    |-  ( E! x ph  <->  E! y [ y  /  x ] ph )
 
Theoremcbveu 2062 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)
 |- 
 F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E! x ph  <->  E! y ps )
 
Theoremeu1 2063* An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.)
 |-  ( ph  ->  A. y ph )   =>    |-  ( E! x ph  <->  E. x ( ph  /\  A. y ( [ y  /  x ] ph  ->  x  =  y ) ) )
 
Theoremeuor 2064 Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 21-Oct-2005.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( ( -.  ph  /\ 
 E! x ps )  ->  E! x ( ph  \/  ps ) )
 
Theoremeuorv 2065* Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
 |-  ( ( -.  ph  /\ 
 E! x ps )  ->  E! x ( ph  \/  ps ) )
 
Theoremmo2n 2066* There is at most one of something which does not exist. (Contributed by Jim Kingdon, 2-Jul-2018.)
 |- 
 F/ y ph   =>    |-  ( -.  E. x ph 
 ->  E. y A. x ( ph  ->  x  =  y ) )
 
Theoremmon 2067 There is at most one of something which does not exist. (Contributed by Jim Kingdon, 5-Jul-2018.)
 |-  ( -.  E. x ph 
 ->  E* x ph )
 
Theoremeuex 2068 Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
 |-  ( E! x ph  ->  E. x ph )
 
Theoremeumo0 2069* Existential uniqueness implies "at most one". (Contributed by NM, 8-Jul-1994.)
 |-  ( ph  ->  A. y ph )   =>    |-  ( E! x ph  ->  E. y A. x ( ph  ->  x  =  y ) )
 
Theoremeumo 2070 Existential uniqueness implies "at most one". (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
 |-  ( E! x ph  ->  E* x ph )
 
Theoremeumoi 2071 "At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
 |- 
 E! x ph   =>    |- 
 E* x ph
 
Theoremmobidh 2072 Formula-building rule for "at most one" quantifier (deduction form). (Contributed by NM, 8-Mar-1995.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E* x ps  <->  E* x ch )
 )
 
Theoremmobid 2073 Formula-building rule for "at most one" quantifier (deduction form). (Contributed by NM, 8-Mar-1995.)
 |- 
 F/ x ph   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E* x ps  <->  E* x ch )
 )
 
Theoremmobidv 2074* Formula-building rule for "at most one" quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E* x ps  <->  E* x ch )
 )
 
Theoremmobii 2075 Formula-building rule for "at most one" quantifier (inference form). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.)
 |-  ( ps  <->  ch )   =>    |-  ( E* x ps  <->  E* x ch )
 
Theoremhbmo1 2076 Bound-variable hypothesis builder for "at most one". (Contributed by NM, 8-Mar-1995.)
 |-  ( E* x ph  ->  A. x E* x ph )
 
Theoremhbmo 2077 Bound-variable hypothesis builder for "at most one". (Contributed by NM, 9-Mar-1995.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( E* y ph  ->  A. x E* y ph )
 
Theoremcbvmo 2078 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.)
 |- 
 F/ y ph   &    |-  F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E* x ph  <->  E* y ps )
 
Theoremmo23 2079* An implication between two definitions of "there exists at most one." (Contributed by Jim Kingdon, 25-Jun-2018.)
 |- 
 F/ y ph   =>    |-  ( E. y A. x ( ph  ->  x  =  y )  ->  A. x A. y ( ( ph  /\  [
 y  /  x ] ph )  ->  x  =  y ) )
 
Theoremmor 2080* Converse of mo23 2079 with an additional  E. x ph condition. (Contributed by Jim Kingdon, 25-Jun-2018.)
 |- 
 F/ y ph   =>    |-  ( E. x ph  ->  ( A. x A. y ( ( ph  /\ 
 [ y  /  x ] ph )  ->  x  =  y )  ->  E. y A. x ( ph  ->  x  =  y ) ) )
 
Theoremmodc 2081* Equivalent definitions of "there exists at most one," given decidable existence. (Contributed by Jim Kingdon, 1-Jul-2018.)
 |- 
 F/ y ph   =>    |-  (DECID 
 E. x ph  ->  ( E. y A. x ( ph  ->  x  =  y )  <->  A. x A. y
 ( ( ph  /\  [
 y  /  x ] ph )  ->  x  =  y ) ) )
 
Theoremeu2 2082* An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.)
 |- 
 F/ y ph   =>    |-  ( E! x ph  <->  ( E. x ph  /\  A. x A. y ( (
 ph  /\  [ y  /  x ] ph )  ->  x  =  y ) ) )
 
Theoremeu3h 2083* An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) (New usage is discouraged.)
 |-  ( ph  ->  A. y ph )   =>    |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
 
Theoremeu3 2084* An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.)
 |- 
 F/ y ph   =>    |-  ( E! x ph  <->  ( E. x ph  /\  E. y A. x ( ph  ->  x  =  y ) ) )
 
Theoremeu5 2085 Uniqueness in terms of "at most one". (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.)
 |-  ( E! x ph  <->  ( E. x ph  /\  E* x ph ) )
 
Theoremexmoeu2 2086 Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.)
 |-  ( E. x ph  ->  ( E* x ph  <->  E! x ph ) )
 
Theoremmoabs 2087 Absorption of existence condition by "at most one". (Contributed by NM, 4-Nov-2002.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E* x ph ) )
 
Theoremexmodc 2088 If existence is decidable, something exists or at most one exists. (Contributed by Jim Kingdon, 30-Jun-2018.)
 |-  (DECID 
 E. x ph  ->  ( E. x ph  \/  E* x ph ) )
 
Theoremexmonim 2089 There is at most one of something which does not exist. Unlike exmodc 2088 there is no decidability condition. (Contributed by Jim Kingdon, 22-Sep-2018.)
 |-  ( -.  E. x ph 
 ->  E* x ph )
 
Theoremmo2r 2090* A condition which implies "at most one". (Contributed by Jim Kingdon, 2-Jul-2018.)
 |- 
 F/ y ph   =>    |-  ( E. y A. x ( ph  ->  x  =  y )  ->  E* x ph )
 
Theoremmo3h 2091* Alternate definition of "at most one". Definition of [BellMachover] p. 460, except that definition has the side condition that  y not occur in  ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (New usage is discouraged.)
 |-  ( ph  ->  A. y ph )   =>    |-  ( E* x ph  <->  A. x A. y ( (
 ph  /\  [ y  /  x ] ph )  ->  x  =  y ) )
 
Theoremmo3 2092* Alternate definition of "at most one". Definition of [BellMachover] p. 460, except that definition has the side condition that  y not occur in  ph in place of our hypothesis. (Contributed by NM, 8-Mar-1995.)
 |- 
 F/ y ph   =>    |-  ( E* x ph  <->  A. x A. y ( (
 ph  /\  [ y  /  x ] ph )  ->  x  =  y ) )
 
Theoremmo2dc 2093* Alternate definition of "at most one" where existence is decidable. (Contributed by Jim Kingdon, 2-Jul-2018.)
 |- 
 F/ y ph   =>    |-  (DECID 
 E. x ph  ->  ( E* x ph  <->  E. y A. x ( ph  ->  x  =  y ) ) )
 
Theoremeuan 2094 Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( E! x (
 ph  /\  ps )  <->  (
 ph  /\  E! x ps ) )
 
Theoremeuanv 2095* Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
 |-  ( E! x (
 ph  /\  ps )  <->  (
 ph  /\  E! x ps ) )
 
Theoremeuor2 2096 Introduce or eliminate a disjunct in a unique existential quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
 |-  ( -.  E. x ph 
 ->  ( E! x (
 ph  \/  ps )  <->  E! x ps ) )
 
Theoremsbmo 2097* Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
 |-  ( [ y  /  x ] E* z ph  <->  E* z [ y  /  x ] ph )
 
Theoremmo4f 2098* "At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.)
 |- 
 F/ x ps   &    |-  ( x  =  y  ->  (
 ph 
 <->  ps ) )   =>    |-  ( E* x ph  <->  A. x A. y ( ( ph  /\  ps )  ->  x  =  y ) )
 
Theoremmo4 2099* "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E* x ph  <->  A. x A. y ( ( ph  /\  ps )  ->  x  =  y ) )
 
Theoremeu4 2100* Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
 |-  ( x  =  y 
 ->  ( ph  <->  ps ) )   =>    |-  ( E! x ph  <->  ( E. x ph  /\  A. x A. y ( (
 ph  /\  ps )  ->  x  =  y ) ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15311
  Copyright terms: Public domain < Previous  Next >