HomeHome Intuitionistic Logic Explorer
Theorem List (p. 20 of 131)
< 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
 
Theoremsbn 1901 Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 |-  ( [ y  /  x ]  -.  ph  <->  -.  [ y  /  x ] ph )
 
Theoremsbim 1902 Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 |-  ( [ y  /  x ] ( ph  ->  ps )  <->  ( [ y  /  x ] ph  ->  [ y  /  x ] ps ) )
 
Theoremsbor 1903 Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 |-  ( [ y  /  x ] ( ph  \/  ps )  <->  ( [ y  /  x ] ph  \/  [ y  /  x ] ps ) )
 
Theoremsban 1904 Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
 |-  ( [ y  /  x ] ( ph  /\  ps ) 
 <->  ( [ y  /  x ] ph  /\  [
 y  /  x ] ps ) )
 
Theoremsbrim 1905 Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( [ y  /  x ] ( ph  ->  ps )  <->  ( ph  ->  [ y  /  x ] ps ) )
 
Theoremsblim 1906 Substitution with a variable not free in consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario Carneiro, 4-Oct-2016.)
 |- 
 F/ x ps   =>    |-  ( [ y  /  x ] ( ph  ->  ps )  <->  ( [ y  /  x ] ph  ->  ps ) )
 
Theoremsb3an 1907 Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
 |-  ( [ y  /  x ] ( ph  /\  ps  /\ 
 ch )  <->  ( [ y  /  x ] ph  /\  [
 y  /  x ] ps  /\  [ y  /  x ] ch ) )
 
Theoremsbbi 1908 Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
 |-  ( [ y  /  x ] ( ph  <->  ps )  <->  ( [ y  /  x ] ph  <->  [ y  /  x ] ps ) )
 
Theoremsblbis 1909 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 ) )
 
Theoremsbrbis 1910 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 ) )
 
Theoremsbrbif 1911 Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
 |-  ( ch  ->  A. x ch )   &    |-  ( [ y  /  x ] ph  <->  ps )   =>    |-  ( [ y  /  x ] ( ph  <->  ch )  <->  ( ps  <->  ch ) )
 
Theoremsbco2yz 1912* This is a version of sbco2 1914 where  z is distinct from 
y. It is a lemma on the way to proving sbco2 1914 which has no distinct variable constraints. (Contributed by Jim Kingdon, 19-Mar-2018.)
 |- 
 F/ z ph   =>    |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
 
Theoremsbco2h 1913 A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
 |-  ( ph  ->  A. z ph )   =>    |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
 
Theoremsbco2 1914 A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
 |- 
 F/ z ph   =>    |-  ( [ y  /  z ] [ z  /  x ] ph  <->  [ y  /  x ] ph )
 
Theoremsbco2d 1915 A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  A. z ph )   &    |-  ( ph  ->  ( ps  ->  A. z ps ) )   =>    |-  ( ph  ->  ( [
 y  /  z ] [ z  /  x ] ps  <->  [ y  /  x ] ps ) )
 
Theoremsbco2vd 1916* Version of sbco2d 1915 with a distinct variable constraint between  x and  z. (Contributed by Jim Kingdon, 19-Feb-2018.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  A. z ph )   &    |-  ( ph  ->  ( ps  ->  A. z ps ) )   =>    |-  ( ph  ->  ( [
 y  /  z ] [ z  /  x ] ps  <->  [ y  /  x ] ps ) )
 
Theoremsbco 1917 A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( [ y  /  x ] [ x  /  y ] ph  <->  [ y  /  x ] ph )
 
Theoremsbco3v 1918* Version of sbco3 1923 with a distinct variable constraint between  x and  y. (Contributed by Jim Kingdon, 19-Feb-2018.)
 |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  x ] [ x  /  y ] ph )
 
Theoremsbcocom 1919 Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.)
 |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  y ] [ z  /  x ] ph )
 
Theoremsbcomv 1920* Version of sbcom 1924 with a distinct variable constraint between  x and  z. (Contributed by Jim Kingdon, 28-Feb-2018.)
 |-  ( [ y  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ y  /  z ] ph )
 
Theoremsbcomxyyz 1921* Version of sbcom 1924 with distinct variable constraints between  x and  y, and  y and  z. (Contributed by Jim Kingdon, 21-Mar-2018.)
 |-  ( [ y  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ y  /  z ] ph )
 
Theoremsbco3xzyz 1922* Version of sbco3 1923 with distinct variable constraints between  x and  z, and  y and  z. Lemma for proving sbco3 1923. (Contributed by Jim Kingdon, 22-Mar-2018.)
 |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  x ] [ x  /  y ] ph )
 
Theoremsbco3 1923 A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
 |-  ( [ z  /  y ] [ y  /  x ] ph  <->  [ z  /  x ] [ x  /  y ] ph )
 
Theoremsbcom 1924 A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
 |-  ( [ y  /  z ] [ y  /  x ] ph  <->  [ y  /  x ] [ y  /  z ] ph )
 
Theoremnfsbt 1925* Closed form of nfsb 1897. (Contributed by Jim Kingdon, 9-May-2018.)
 |-  ( A. x F/ z ph  ->  F/ z [ y  /  x ] ph )
 
Theoremnfsbd 1926* Deduction version of nfsb 1897. (Contributed by NM, 15-Feb-2013.)
 |- 
 F/ x ph   &    |-  ( ph  ->  F/ z ps )   =>    |-  ( ph  ->  F/ z [ y  /  x ] ps )
 
Theoremelsb3 1927* Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 |-  ( [ y  /  x ] x  e.  z  <->  y  e.  z )
 
Theoremelsb4 1928* Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 |-  ( [ y  /  x ] z  e.  x  <->  z  e.  y )
 
Theoremsb9v 1929* Like sb9 1930 but with a distinct variable constraint between  x and  y. (Contributed by Jim Kingdon, 28-Feb-2018.)
 |-  ( A. x [ x  /  y ] ph  <->  A. y [ y  /  x ] ph )
 
Theoremsb9 1930 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 )
 
Theoremsb9i 1931 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 1932* 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 1933* Deduction version of hbsb 1898. (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 1934* 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 1935* 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 1936* Lemma for proving sbcom2 1938. It is the same as sbcom2 1938 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 1937* Lemma for proving sbcom2 1938. It is the same as sbcom2v 1936 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 1938* 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 1939* Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( [ y  /  x ] ph  <->  A. x ( x  =  y  ->  [ x  /  y ] ph )
 )
 
Theorem2sb5rf 1940* 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 1941* 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 1942* An alternate definition of proper substitution df-sb 1719. 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 1841, first  z for  x then  y for  z. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1943 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 1943* This version of dfsb7 1942 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 1489 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1719 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 1944* An alternate definition of proper substitution df-sb 1719. Similar to dfsb7a 1945 but does not require that  ph and  z be distinct. Similar to sb7f 1943 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 1945* An alternate definition of proper substitution df-sb 1719. Similar to dfsb7 1942 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 1944. (Contributed by Jim Kingdon, 5-Feb-2018.)
 |-  ( [ y  /  x ] ph  <->  A. z ( z  =  y  ->  A. x ( x  =  z  -> 
 ph ) ) )
 
Theoremsb10f 1946* 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 1947* 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 1948* Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
 |-  ( ph  <->  E. x ( x  =  y  /\  [ x  /  y ] ph ) )
 
Theoremsbel2x 1949* 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 1950* Move universal quantifier in and out of substitution. Identical to sbal 1951 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 1951* 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 1952* Lemma for proving sbal1 1953. Same as sbal1 1953 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 1953* 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 1954* Move existential quantifier in and out of substitution. Identical to sbex 1955 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 1955* 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 1956* 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 1957* Lemma for sbco4 1958. 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 1958* 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 1959* An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.)
 |-  ( E. x ph  <->  E. y A. x ( x  =  y  ->  ph )
 )
 
Theorem2exsb 1960* 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 1961* Version of dvelim 1968 that doesn't use ax-10 1466. Because it has different distinct variable constraints than dvelim 1968 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 1962* Like dvelimf 1966 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 1963 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 1964 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1963). (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 1965 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1963). (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 1966 Version of dvelim 1968 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 1967 Deduction form of dvelimf 1966. This version may be useful if we want to avoid ax-17 1489 and use ax-16 1768 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 1968* 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 1967.

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

 |-  ( ph  ->  A. x ph )   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremdvelimor 1969* 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 1970* 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 1971* 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 1972* 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 1973* 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 1974 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 1975 Extend wff definition to include existential uniqueness ("there exists a unique  x such that  ph").
 wff  E! x ph
 
Syntaxwmo 1976 Extend wff definition to include uniqueness ("there exists at most one  x such that  ph").
 wff  E* x ph
 
Theoremeujust 1977* A soundness justification theorem for df-eu 1978, 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 1978* 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 2000, eu2 2019, eu3 2021, and eu5 2022 (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 2068). (Contributed by NM, 5-Aug-1993.)
 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
 
Definitiondf-mo 1979 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 2029. For another possible definition see mo4 2036. (Contributed by NM, 5-Aug-1993.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
 
Theoremeuf 1980* 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 1981 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 1982 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 1983* 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 1984 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 1985 Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
 |-  ( E! x ph  ->  A. x E! x ph )
 
Theoremnfeu1 1986 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 1987 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 1988 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 1989 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 1990* Deduction version of nfeu 1994. Similar to nfeud 1991 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 1991 Deduction version of nfeu 1994. (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 1992 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 1993* Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1994 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 1994 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 1995 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
 |- 
 F/ x ph   =>    |- 
 F/ x E* y ph
 
Theoremhbeu 1996 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 1997 Deduction version of hbeu 1996. (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 1998 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 1999 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 2000* 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 ) ) )
    < 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-13088
  Copyright terms: Public domain < Previous  Next >