HomeHome Intuitionistic Logic Explorer
Theorem List (p. 20 of 106)
< 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
 
Theorem2exsb 1901* 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 1902* Version of dvelim 1909 that doesn't use ax-10 1412. Because it has different distinct variable constraints than dvelim 1909 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 1903* Like dvelimf 1907 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 1904 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 1905 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1904). (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 1906 A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1904). (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 1907 Version of dvelim 1909 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 1908 Deduction form of dvelimf 1907. This version may be useful if we want to avoid ax-17 1435 and use ax-16 1711 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 1909* 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 1908.

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

 |-  ( ph  ->  A. x ph )   &    |-  ( z  =  y  ->  ( ph  <->  ps ) )   =>    |-  ( -.  A. x  x  =  y  ->  ( ps  ->  A. x ps ) )
 
Theoremdvelimor 1910* 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 1911* 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 1912* 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 1913* 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 1914* 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 1915 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 1916 Extend wff definition to include existential uniqueness ("there exists a unique  x such that  ph").
 wff  E! x ph
 
Syntaxwmo 1917 Extend wff definition to include uniqueness ("there exists at most one  x such that  ph").
 wff  E* x ph
 
Theoremeujust 1918* A soundness justification theorem for df-eu 1919, 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 1919* 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 1941, eu2 1960, eu3 1962, and eu5 1963 (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 2009). (Contributed by NM, 5-Aug-1993.)
 |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
 
Definitiondf-mo 1920 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 1970. For another possible definition see mo4 1977. (Contributed by NM, 5-Aug-1993.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E! x ph ) )
 
Theoremeuf 1921* 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 1922 Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
 |-  ( ph  ->  A. x ph )   &    |-  ( ph  ->  ( ps  <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubid 1923 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 )
 )
 
Theoremeubidv 1924* Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.)
 |-  ( ph  ->  ( ps 
 <->  ch ) )   =>    |-  ( ph  ->  ( E! x ps  <->  E! x ch )
 )
 
Theoremeubii 1925 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 )
 
Theoremhbeu1 1926 Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.)
 |-  ( E! x ph  ->  A. x E! x ph )
 
Theoremnfeu1 1927 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 1928 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 1929 Variable substitution in uniqueness 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 1930 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 1931* Deduction version of nfeu 1935. Similar to nfeud 1932 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 1932 Deduction version of nfeu 1935. (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 1933 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 1934* Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1935 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 1935 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 1936 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.)
 |- 
 F/ x ph   =>    |- 
 F/ x E* y ph
 
Theoremhbeu 1937 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 1938 Deduction version of hbeu 1937. (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 1939 Variable substitution in uniqueness 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 1940 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 1941* 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 1942 Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.)
 |-  ( ph  ->  A. x ph )   =>    |-  ( ( -.  ph  /\ 
 E! x ps )  ->  E! x ( ph  \/  ps ) )
 
Theoremeuorv 1943* Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
 |-  ( ( -.  ph  /\ 
 E! x ps )  ->  E! x ( ph  \/  ps ) )
 
Theoremmo2n 1944* 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 1945 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 1946 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 1947* 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 1948 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 1949 "At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.)
 |- 
 E! x ph   =>    |- 
 E* x ph
 
Theoremmobidh 1950 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 1951 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 1952* 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 1953 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 1954 Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.)
 |-  ( E* x ph  ->  A. x E* x ph )
 
Theoremhbmo 1955 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 1956 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 1957* 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 1958* Converse of mo23 1957 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 1959* 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 1960* 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 1961* 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 1962* 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 1963 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 1964 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 1965 Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.)
 |-  ( E* x ph  <->  ( E. x ph  ->  E* x ph ) )
 
Theoremexmodc 1966 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 1967 There is at most one of something which does not exist. Unlike exmodc 1966 there is no decidability condition. (Contributed by Jim Kingdon, 22-Sep-2018.)
 |-  ( -.  E. x ph 
 ->  E* x ph )
 
Theoremmo2r 1968* 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 1969* 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 1970* 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 1971* 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 1972 Introduction of a conjunct into uniqueness 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 1973* Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.)
 |-  ( E! x (
 ph  /\  ps )  <->  (
 ph  /\  E! x ps ) )
 
Theoremeuor2 1974 Introduce or eliminate a disjunct in a uniqueness 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 1975* Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.)
 |-  ( [ y  /  x ] E* z ph  <->  E* z [ y  /  x ] ph )
 
Theoremmo4f 1976* "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 1977* "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 1978* 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 ) ) )
 
Theoremexmoeudc 1979 Existence in terms of "at most one" and uniqueness. (Contributed by Jim Kingdon, 3-Jul-2018.)
 |-  (DECID 
 E. x ph  ->  ( E. x ph  <->  ( E* x ph 
 ->  E! x ph )
 ) )
 
Theoremmoim 1980 "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.)
 |-  ( A. x (
 ph  ->  ps )  ->  ( E* x ps  ->  E* x ph ) )
 
Theoremmoimi 1981 "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.)
 |-  ( ph  ->  ps )   =>    |-  ( E* x ps  ->  E* x ph )
 
Theoremmoimv 1982* Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.)
 |-  ( E* x (
 ph  ->  ps )  ->  ( ph  ->  E* x ps )
 )
 
Theoremeuimmo 1983 Uniqueness implies "at most one" through implication. (Contributed by NM, 22-Apr-1995.)
 |-  ( A. x (
 ph  ->  ps )  ->  ( E! x ps  ->  E* x ph ) )
 
Theoremeuim 1984 Add existential uniqueness quantifiers to an implication. Note the reversed implication in the antecedent. (Contributed by NM, 19-Oct-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
 |-  ( ( E. x ph 
 /\  A. x ( ph  ->  ps ) )  ->  ( E! x ps  ->  E! x ph ) )
 
Theoremmoan 1985 "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.)
 |-  ( E* x ph  ->  E* x ( ps 
 /\  ph ) )
 
Theoremmoani 1986 "At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.)
 |- 
 E* x ph   =>    |- 
 E* x ( ps 
 /\  ph )
 
Theoremmoor 1987 "At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.)
 |-  ( E* x (
 ph  \/  ps )  ->  E* x ph )
 
Theoremmooran1 1988 "At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
 |-  ( ( E* x ph 
 \/  E* x ps )  ->  E* x ( ph  /\ 
 ps ) )
 
Theoremmooran2 1989 "At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
 |-  ( E* x (
 ph  \/  ps )  ->  ( E* x ph  /\ 
 E* x ps )
 )
 
Theoremmoanim 1990 Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 3-Dec-2001.)
 |- 
 F/ x ph   =>    |-  ( E* x (
 ph  /\  ps )  <->  (
 ph  ->  E* x ps )
 )
 
Theoremmoanimv 1991* Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.)
 |-  ( E* x (
 ph  /\  ps )  <->  (
 ph  ->  E* x ps )
 )
 
Theoremmoaneu 1992 Nested "at most one" and uniqueness quantifiers. (Contributed by NM, 25-Jan-2006.)
 |- 
 E* x ( ph  /\ 
 E! x ph )
 
Theoremmoanmo 1993 Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.)
 |- 
 E* x ( ph  /\ 
 E* x ph )
 
Theoremmopick 1994 "At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.)
 |-  ( ( E* x ph 
 /\  E. x ( ph  /\ 
 ps ) )  ->  ( ph  ->  ps )
 )
 
Theoremeupick 1995 Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing  x such that 
ph is true, and there is also an  x (actually the same one) such that  ph and  ps are both true, then  ph implies  ps regardless of  x. This theorem can be useful for eliminating existential quantifiers in a hypothesis. Compare Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by NM, 10-Jul-1994.)
 |-  ( ( E! x ph 
 /\  E. x ( ph  /\ 
 ps ) )  ->  ( ph  ->  ps )
 )
 
Theoremeupicka 1996 Version of eupick 1995 with closed formulas. (Contributed by NM, 6-Sep-2008.)
 |-  ( ( E! x ph 
 /\  E. x ( ph  /\ 
 ps ) )  ->  A. x ( ph  ->  ps ) )
 
Theoremeupickb 1997 Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.)
 |-  ( ( E! x ph 
 /\  E! x ps  /\  E. x ( ph  /\  ps ) )  ->  ( ph  <->  ps ) )
 
Theoremeupickbi 1998 Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.)
 |-  ( E! x ph  ->  ( E. x (
 ph  /\  ps )  <->  A. x ( ph  ->  ps ) ) )
 
Theoremmopick2 1999 "At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 1538. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
 |-  ( ( E* x ph 
 /\  E. x ( ph  /\ 
 ps )  /\  E. x ( ph  /\  ch ) )  ->  E. x ( ph  /\  ps  /\  ch ) )
 
Theoremmoexexdc 2000 "At most one" double quantification. (Contributed by Jim Kingdon, 5-Jul-2018.)
 |- 
 F/ y ph   =>    |-  (DECID 
 E. x ph  ->  ( ( E* x ph  /\ 
 A. x E* y ps )  ->  E* y E. x ( ph  /\  ps ) ) )
    < 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-10511
  Copyright terms: Public domain < Previous  Next >