HomeHome Intuitionistic Logic Explorer
Theorem List (p. 20 of 114)
< 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 - 1901-2000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsb9i 1901 Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
 |-  ( A. x [ x  /  y ] ph  ->  A. y [ y  /  x ] ph )
 
Theoremsbnf2 1902* 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.)
 |-  ( F/ x ph  <->  A. y A. z ( [
 y  /  x ] ph 
 <->  [ z  /  x ] ph ) )
 
Theoremhbsbd 1903* Deduction version of hbsb 1868. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  A. z ph )   &    |-  ( ph  ->  ( ps  ->  A. z ps ) )   =>    |-  ( ph  ->  ( [
 y  /  x ] ps  ->  A. z [ y  /  x ] ps )
 )
 
Theorem2sb5 1904* Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
 |-  ( [ z  /  x ] [ w  /  y ] ph  <->  E. x E. y
 ( ( x  =  z  /\  y  =  w )  /\  ph )
 )
 
Theorem2sb6 1905* Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
 |-  ( [ z  /  x ] [ w  /  y ] ph  <->  A. x A. y
 ( ( x  =  z  /\  y  =  w )  ->  ph )
 )
 
Theoremsbcom2v 1906* Lemma for proving sbcom2 1908. It is the same as sbcom2 1908 but with additional distinct variable constraints on  x and  y, and on  w and  z. (Contributed by Jim Kingdon, 19-Feb-2018.)
 |-  ( [ w  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ w  /  z ] ph )
 
Theoremsbcom2v2 1907* Lemma for proving sbcom2 1908. It is the same as sbcom2v 1906 but removes the distinct variable constraint on  x and  y. (Contributed by Jim Kingdon, 19-Feb-2018.)
 |-  ( [ w  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ w  /  z ] ph )
 
Theoremsbcom2 1908* 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 modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.)
 |-  ( [ w  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ w  /  z ] ph )
 
Theoremsb6a 1909* Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( [ y  /  x ] ph  <->  A. x ( x  =  y  ->  [ x  /  y ] ph )
 )
 
Theorem2sb5rf 1910* 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 1911* 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 1912* An alternate definition of proper substitution df-sb 1690. 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 1812, first  z for  x then  y for  z. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1913 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 1913* This version of dfsb7 1912 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-17 1462 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1690 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 )
 ) )
 
Theoremsb7af 1914* An alternate definition of proper substitution df-sb 1690. Similar to dfsb7a 1915 but does not require that  ph and  z be distinct. Similar to sb7f 1913 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 1915* An alternate definition of proper substitution df-sb 1690. Similar to dfsb7 1912 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 1914. (Contributed by Jim Kingdon, 5-Feb-2018.)
 |-  ( [ y  /  x ] ph  <->  A. z ( z  =  y  ->  A. x ( x  =  z  -> 
 ph ) ) )
 
Theoremsb10f 1916* 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 1917* 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 1918* Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  <->  E. x ( x  =  y  /\  [ x  /  y ] ph ) )
 
Theoremsbel2x 1919* 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 1920* Move universal quantifier in and out of substitution. Identical to sbal 1921 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 1921* 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 1922* Lemma for proving sbal1 1923. Same as sbal1 1923 but with an additional distinct variable constraint on  y and  z. (Contributed by Jim Kingdon, 23-Feb-2018.)
 |-  ( -.  A. x  x  =  z  ->  ( [ z  /  y ] A. x ph  <->  A. x [ z  /  y ] ph )
 )
 
Theoremsbal1 1923* 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, 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 1924* Move existential quantifier in and out of substitution. Identical to sbex 1925 except that it has an additional distinct variable constraint on  y and  z. (Contributed by Jim Kingdon, 29-Dec-2017.)
 |-  ( [ z  /  y ] E. x ph  <->  E. x [ z  /  y ] ph )
 
Theoremsbex 1925* 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 1926* 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 1927* Lemma for sbco4 1928. 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 1928* 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 1929* An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
 |-  ( E. x ph  <->  E. y A. x ( x  =  y  ->  ph )
 )
 
Theorem2exsb 1930* 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 1931* Version of dvelim 1938 that doesn't use ax-10 1439. Because it has different distinct variable constraints than dvelim 1938 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 1932* Like dvelimf 1936 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 1933 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 1934 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1933). (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 1935 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1933). (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 1936 Version of dvelim 1938 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 1937 Deduction form of dvelimf 1936. This version may be useful if we want to avoid ax-17 1462 and use ax-16 1739 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 1938* 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 1937.

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

 |-  ( ph  ->  A. x ph )   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremdvelimor 1939* 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 1940* 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 ) )
 
Theoremdveel1 1941* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
 |-  ( -.  A. x  x  =  y  ->  ( y  e.  z  ->  A. x  y  e.  z ) )
 
Theoremdveel2 1942* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
 |-  ( -.  A. x  x  =  y  ->  ( z  e.  y  ->  A. x  z  e.  y ) )
 
Theoremsbal2 1943* 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 1944 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 )
 
1.4.6  Existential uniqueness
 
Syntaxweu 1945 Extend wff definition to include existential uniqueness ("there exists a unique  x such that  ph").
 wff  E! x ph
 
Syntaxwmo 1946 Extend wff definition to include uniqueness ("there exists at most one  x such that  ph").
 wff  E* x ph
 
Theoremeujust 1947* A soundness justification theorem for df-eu 1948, 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 1948* 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 1970, eu2 1989, eu3 1991, and eu5 1992 (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 2038). (Contributed by NM, 5-Aug-1993.)
 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
 
Definitiondf-mo 1949 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 1999. For another possible definition see mo4 2006. (Contributed by NM, 5-Aug-1993.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
 
Theoremeuf 1950* 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 1951 Formula-building rule for unique existential quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubid 1952 Formula-building rule for unique existential quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
 |- 
 F/ x ph   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubidv 1953* Formula-building rule for unique existential quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubii 1954 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 1955 Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
 |-  ( E! x ph  ->  A. x E! x ph )
 
Theoremnfeu1 1956 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 1957 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 1958 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 1959 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 1960* Deduction version of nfeu 1964. Similar to nfeud 1961 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 1961 Deduction version of nfeu 1964. (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 1962 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 1963* Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1964 but has the additional constraint that  x and  y must be distinct. (Contributed by Jim Kingdon, 23-May-2018.)
 |- 
 F/ x ph   =>    |- 
 F/ x E! y ph
 
Theoremnfeu 1964 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 1965 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
 |- 
 F/ x ph   =>    |- 
 F/ x E* y ph
 
Theoremhbeu 1966 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 1967 Deduction version of hbeu 1966. (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 1968 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 1969 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 1970* 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 1971 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 1972* Introduce a disjunct into a unique existential quantifier. (Contributed by NM, 23-Mar-1995.)
 |-  ( ( -.  ph  /\ 
 E! x ps )  ->  E! x ( ph  \/  ps ) )
 
Theoremmo2n 1973* 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 1974 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 1975 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 1976* 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 1977 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 1978 "At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
 |- 
 E! x ph   =>    |- 
 E* x ph
 
Theoremmobidh 1979 Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E* x ps  <->  E* x ch )
 )
 
Theoremmobid 1980 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 )
 )
 
Theoremmobidv 1981* 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 )
 )
 
Theoremmobii 1982 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 )
 
Theoremhbmo1 1983 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.)
 |-  ( E* x ph  ->  A. x E* x ph )
 
Theoremhbmo 1984 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 1985 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 1986* 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 1987* Converse of mo23 1986 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 1988* 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 1989* 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 1990* 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 1991* 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 1992 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 1993 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 1994 Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E* x ph ) )
 
Theoremexmodc 1995 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 1996 There is at most one of something which does not exist. Unlike exmodc 1995 there is no decidability condition. (Contributed by Jim Kingdon, 22-Sep-2018.)
 |-  ( -.  E. x ph 
 ->  E* x ph )
 
Theoremmo2r 1997* 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 1998* 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 1999* 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 2000* 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 ) ) )
    < 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-11363
  Copyright terms: Public domain < Previous  Next >