Home | 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2exsb 1901* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) |
Theorem | dvelimALT 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.) |
Theorem | dvelimfv 1903* | Like dvelimf 1907 but with a distinct variable constraint on and . (Contributed by Jim Kingdon, 6-Mar-2018.) |
Theorem | hbsb4 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.) |
Theorem | hbsb4t 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.) |
Theorem | nfsb4t 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.) |
Theorem | dvelimf 1907 | Version of dvelim 1909 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) |
Theorem | dvelimdf 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.) |
Theorem | dvelim 1909* |
This theorem can be used to eliminate a distinct variable restriction on
and and replace it with the
"distinctor"
as an antecedent. normally has free and can be read
, and
substitutes for and can be read
. We don't require that and 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 , 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.) |
Theorem | dvelimor 1910* | Disjunctive distinct variable constraint elimination. A user of this theorem starts with a formula (containing ) and a distinct variable constraint between and . The theorem makes it possible to replace the distinct variable constraint with the disjunct ( is just a version of with substituted for ). (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | dveeq1 1911* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.) |
Theorem | dveel1 1912* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
Theorem | dveel2 1913* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
Theorem | sbal2 1914* | Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) |
Theorem | nfsb4or 1915 | A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.) |
Syntax | weu 1916 | Extend wff definition to include existential uniqueness ("there exists a unique such that "). |
Syntax | wmo 1917 | Extend wff definition to include uniqueness ("there exists at most one such that "). |
Theorem | eujust 1918* | A soundness justification theorem for df-eu 1919, showing that the definition is equivalent to itself with its dummy variable renamed. Note that and needn't be distinct variables. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Definition | df-eu 1919* | Define existential uniqueness, i.e. "there exists exactly one such that ." 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 in place of a distinct variable condition on and ). Double uniqueness is tricky: does not mean "exactly one and one " (see 2eu4 2009). (Contributed by NM, 5-Aug-1993.) |
Definition | df-mo 1920 | Define "there exists at most one such that ." 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.) |
Theorem | euf 1921* | A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.) |
Theorem | eubidh 1922 | Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
Theorem | eubid 1923 | Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
Theorem | eubidv 1924* | Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
Theorem | eubii 1925 | Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | hbeu1 1926 | Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) |
Theorem | nfeu1 1927 | Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfmo1 1928 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | sb8eu 1929 | Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | sb8mo 1930 | Variable substitution for "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | nfeudv 1931* | Deduction version of nfeu 1935. Similar to nfeud 1932 but has the additional constraint that and must be distinct. (Contributed by Jim Kingdon, 25-May-2018.) |
Theorem | nfeud 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.) |
Theorem | nfmod 1933 | Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.) |
Theorem | nfeuv 1934* | Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1935 but has the additional constraint that and must be distinct. (Contributed by Jim Kingdon, 23-May-2018.) |
Theorem | nfeu 1935 | Bound-variable hypothesis builder for existential uniqueness. Note that and 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.) |
Theorem | nfmo 1936 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.) |
Theorem | hbeu 1937 | Bound-variable hypothesis builder for uniqueness. Note that and needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Proof rewritten by Jim Kingdon, 24-May-2018.) |
Theorem | hbeud 1938 | Deduction version of hbeu 1937. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 25-May-2018.) |
Theorem | sb8euh 1939 | Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.) |
Theorem | cbveu 1940 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | eu1 1941* | An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) |
Theorem | euor 1942 | Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) |
Theorem | euorv 1943* | Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.) |
Theorem | mo2n 1944* | There is at most one of something which does not exist. (Contributed by Jim Kingdon, 2-Jul-2018.) |
Theorem | mon 1945 | There is at most one of something which does not exist. (Contributed by Jim Kingdon, 5-Jul-2018.) |
Theorem | euex 1946 | Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | eumo0 1947* | Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.) |
Theorem | eumo 1948 | Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.) |
Theorem | eumoi 1949 | "At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.) |
Theorem | mobidh 1950 | Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.) |
Theorem | mobid 1951 | Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.) |
Theorem | mobidv 1952* | Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | mobii 1953 | Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) |
Theorem | hbmo1 1954 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) |
Theorem | hbmo 1955 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.) |
Theorem | cbvmo 1956 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.) |
Theorem | mo23 1957* | An implication between two definitions of "there exists at most one." (Contributed by Jim Kingdon, 25-Jun-2018.) |
Theorem | mor 1958* | Converse of mo23 1957 with an additional condition. (Contributed by Jim Kingdon, 25-Jun-2018.) |
Theorem | modc 1959* | Equivalent definitions of "there exists at most one," given decidable existence. (Contributed by Jim Kingdon, 1-Jul-2018.) |
DECID | ||
Theorem | eu2 1960* | An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.) |
Theorem | eu3h 1961* | An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) (New usage is discouraged.) |
Theorem | eu3 1962* | An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) |
Theorem | eu5 1963 | Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.) |
Theorem | exmoeu2 1964 | Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.) |
Theorem | moabs 1965 | Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.) |
Theorem | exmodc 1966 | If existence is decidable, something exists or at most one exists. (Contributed by Jim Kingdon, 30-Jun-2018.) |
DECID | ||
Theorem | exmonim 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.) |
Theorem | mo2r 1968* | A condition which implies "at most one." (Contributed by Jim Kingdon, 2-Jul-2018.) |
Theorem | mo3h 1969* | Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that not occur in in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (New usage is discouraged.) |
Theorem | mo3 1970* | Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that not occur in in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) |
Theorem | mo2dc 1971* | Alternate definition of "at most one" where existence is decidable. (Contributed by Jim Kingdon, 2-Jul-2018.) |
DECID | ||
Theorem | euan 1972 | Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | euanv 1973* | Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.) |
Theorem | euor2 1974 | Introduce or eliminate a disjunct in a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | sbmo 1975* | Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | mo4f 1976* | "At most one" expressed using implicit substitution. (Contributed by NM, 10-Apr-2004.) |
Theorem | mo4 1977* | "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
Theorem | eu4 1978* | Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
Theorem | exmoeudc 1979 | Existence in terms of "at most one" and uniqueness. (Contributed by Jim Kingdon, 3-Jul-2018.) |
DECID | ||
Theorem | moim 1980 | "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 22-Apr-1995.) |
Theorem | moimi 1981 | "At most one" is preserved through implication (notice wff reversal). (Contributed by NM, 15-Feb-2006.) |
Theorem | moimv 1982* | Move antecedent outside of "at most one." (Contributed by NM, 28-Jul-1995.) |
Theorem | euimmo 1983 | Uniqueness implies "at most one" through implication. (Contributed by NM, 22-Apr-1995.) |
Theorem | euim 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.) |
Theorem | moan 1985 | "At most one" is still the case when a conjunct is added. (Contributed by NM, 22-Apr-1995.) |
Theorem | moani 1986 | "At most one" is still true when a conjunct is added. (Contributed by NM, 9-Mar-1995.) |
Theorem | moor 1987 | "At most one" is still the case when a disjunct is removed. (Contributed by NM, 5-Apr-2004.) |
Theorem | mooran1 1988 | "At most one" imports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | mooran2 1989 | "At most one" exports disjunction to conjunction. (Contributed by NM, 5-Apr-2004.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
Theorem | moanim 1990 | Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 3-Dec-2001.) |
Theorem | moanimv 1991* | Introduction of a conjunct into "at most one" quantifier. (Contributed by NM, 23-Mar-1995.) |
Theorem | moaneu 1992 | Nested "at most one" and uniqueness quantifiers. (Contributed by NM, 25-Jan-2006.) |
Theorem | moanmo 1993 | Nested "at most one" quantifiers. (Contributed by NM, 25-Jan-2006.) |
Theorem | mopick 1994 | "At most one" picks a variable value, eliminating an existential quantifier. (Contributed by NM, 27-Jan-1997.) |
Theorem | eupick 1995 | Existential uniqueness "picks" a variable value for which another wff is true. If there is only one thing such that is true, and there is also an (actually the same one) such that and are both true, then implies regardless of . 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.) |
Theorem | eupicka 1996 | Version of eupick 1995 with closed formulas. (Contributed by NM, 6-Sep-2008.) |
Theorem | eupickb 1997 | Existential uniqueness "pick" showing wff equivalence. (Contributed by NM, 25-Nov-1994.) |
Theorem | eupickbi 1998 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
Theorem | mopick2 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.) |
Theorem | moexexdc 2000 | "At most one" double quantification. (Contributed by Jim Kingdon, 5-Jul-2018.) |
DECID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |