Home | 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sbn 1901 | Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sbim 1902 | Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sbor 1903 | Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sban 1904 | Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.) |
Theorem | sbrim 1905 | Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | sblim 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.) |
Theorem | sb3an 1907 | Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.) |
Theorem | sbbi 1908 | Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) |
Theorem | sblbis 1909 | Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.) |
Theorem | sbrbis 1910 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
Theorem | sbrbif 1911 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
Theorem | sbco2yz 1912* | This is a version of sbco2 1914 where is distinct from . It is a lemma on the way to proving sbco2 1914 which has no distinct variable constraints. (Contributed by Jim Kingdon, 19-Mar-2018.) |
Theorem | sbco2h 1913 | A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.) |
Theorem | sbco2 1914 | A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | sbco2d 1915 | A composition law for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbco2vd 1916* | Version of sbco2d 1915 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbco 1917 | A composition law for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbco3v 1918* | Version of sbco3 1923 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbcocom 1919 | Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.) |
Theorem | sbcomv 1920* | Version of sbcom 1924 with a distinct variable constraint between and . (Contributed by Jim Kingdon, 28-Feb-2018.) |
Theorem | sbcomxyyz 1921* | Version of sbcom 1924 with distinct variable constraints between and , and and . (Contributed by Jim Kingdon, 21-Mar-2018.) |
Theorem | sbco3xzyz 1922* | Version of sbco3 1923 with distinct variable constraints between and , and and . Lemma for proving sbco3 1923. (Contributed by Jim Kingdon, 22-Mar-2018.) |
Theorem | sbco3 1923 | A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.) |
Theorem | sbcom 1924 | A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.) |
Theorem | nfsbt 1925* | Closed form of nfsb 1897. (Contributed by Jim Kingdon, 9-May-2018.) |
Theorem | nfsbd 1926* | Deduction version of nfsb 1897. (Contributed by NM, 15-Feb-2013.) |
Theorem | elsb3 1927* | Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | elsb4 1928* | Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | sb9v 1929* | Like sb9 1930 but with a distinct variable constraint between and . (Contributed by Jim Kingdon, 28-Feb-2018.) |
Theorem | sb9 1930 | Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | sb9i 1931 | Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | sbnf2 1932* | Two ways of expressing " is (effectively) not free in ." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | hbsbd 1933* | Deduction version of hbsb 1898. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
Theorem | 2sb5 1934* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | 2sb6 1935* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | sbcom2v 1936* | Lemma for proving sbcom2 1938. It is the same as sbcom2 1938 but with additional distinct variable constraints on and , and on and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbcom2v2 1937* | Lemma for proving sbcom2 1938. It is the same as sbcom2v 1936 but removes the distinct variable constraint on and . (Contributed by Jim Kingdon, 19-Feb-2018.) |
Theorem | sbcom2 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.) |
Theorem | sb6a 1939* | Equivalence for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2sb5rf 1940* | Reversed double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | 2sb6rf 1941* | Reversed double substitution. (Contributed by NM, 3-Feb-2005.) |
Theorem | dfsb7 1942* | An alternate definition of proper substitution df-sb 1719. By introducing a dummy variable in the definiens, we are able to eliminate any distinct variable restrictions among the variables , , and of the definiendum. No distinct variable conflicts arise because effectively insulates from . To achieve this, we use a chain of two substitutions in the form of sb5 1841, first for then for . Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1943 provides a version where and don't have to be distinct. (Contributed by NM, 28-Jan-2004.) |
Theorem | sb7f 1943* | This version of dfsb7 1942 does not require that and 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.) |
Theorem | sb7af 1944* | An alternate definition of proper substitution df-sb 1719. Similar to dfsb7a 1945 but does not require that and be distinct. Similar to sb7f 1943 in that it involves a dummy variable , but expressed in terms of rather than . (Contributed by Jim Kingdon, 5-Feb-2018.) |
Theorem | dfsb7a 1945* | An alternate definition of proper substitution df-sb 1719. Similar to dfsb7 1942 in that it involves a dummy variable , but expressed in terms of rather than . For a version which only requires rather than and being distinct, see sb7af 1944. (Contributed by Jim Kingdon, 5-Feb-2018.) |
Theorem | sb10f 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.) |
Theorem | sbid2v 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.) |
Theorem | sbelx 1948* | Elimination of substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbel2x 1949* | Elimination of double substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbalyz 1950* | Move universal quantifier in and out of substitution. Identical to sbal 1951 except that it has an additional distinct variable constraint on and . (Contributed by Jim Kingdon, 29-Dec-2017.) |
Theorem | sbal 1951* | Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.) |
Theorem | sbal1yz 1952* | Lemma for proving sbal1 1953. Same as sbal1 1953 but with an additional disjoint variable condition on . (Contributed by Jim Kingdon, 23-Feb-2018.) |
Theorem | sbal1 1953* | A theorem used in elimination of disjoint variable conditions on by replacing it with a distinctor . (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.) |
Theorem | sbexyz 1954* | Move existential quantifier in and out of substitution. Identical to sbex 1955 except that it has an additional disjoint variable condition on . (Contributed by Jim Kingdon, 29-Dec-2017.) |
Theorem | sbex 1955* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.) |
Theorem | sbalv 1956* | Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.) |
Theorem | sbco4lem 1957* | Lemma for sbco4 1958. It replaces the temporary variable with another temporary variable . (Contributed by Jim Kingdon, 26-Sep-2018.) |
Theorem | sbco4 1958* | Two ways of exchanging two variables. Both sides of the biconditional exchange and , either via two temporary variables and , or a single temporary . (Contributed by Jim Kingdon, 25-Sep-2018.) |
Theorem | exsb 1959* | An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.) |
Theorem | 2exsb 1960* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) |
Theorem | dvelimALT 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.) |
Theorem | dvelimfv 1962* | Like dvelimf 1966 but with a distinct variable constraint on and . (Contributed by Jim Kingdon, 6-Mar-2018.) |
Theorem | hbsb4 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.) |
Theorem | hbsb4t 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.) |
Theorem | nfsb4t 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.) |
Theorem | dvelimf 1966 | Version of dvelim 1968 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) |
Theorem | dvelimdf 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.) |
Theorem | dvelim 1968* |
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 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.) |
Theorem | dvelimor 1969* | 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 1970* | 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 1971* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
Theorem | dveel2 1972* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
Theorem | sbal2 1973* | Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) |
Theorem | nfsb4or 1974 | A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.) |
Syntax | weu 1975 | Extend wff definition to include existential uniqueness ("there exists a unique such that "). |
Syntax | wmo 1976 | Extend wff definition to include uniqueness ("there exists at most one such that "). |
Theorem | eujust 1977* | A soundness justification theorem for df-eu 1978, 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 1978* | 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 2000, eu2 2019, eu3 2021, and eu5 2022 (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 2068). (Contributed by NM, 5-Aug-1993.) |
Definition | df-mo 1979 | 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 2029. For another possible definition see mo4 2036. (Contributed by NM, 5-Aug-1993.) |
Theorem | euf 1980* | A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.) |
Theorem | eubidh 1981 | Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) |
Theorem | eubid 1982 | Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) |
Theorem | eubidv 1983* | Formula-building rule for unique existential quantifier (deduction form). (Contributed by NM, 9-Jul-1994.) |
Theorem | eubii 1984 | Introduce unique existential quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | hbeu1 1985 | Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) |
Theorem | nfeu1 1986 | Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | nfmo1 1987 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | sb8eu 1988 | Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | sb8mo 1989 | Variable substitution for "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
Theorem | nfeudv 1990* | Deduction version of nfeu 1994. Similar to nfeud 1991 but has the additional constraint that and must be distinct. (Contributed by Jim Kingdon, 25-May-2018.) |
Theorem | nfeud 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.) |
Theorem | nfmod 1992 | Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.) |
Theorem | nfeuv 1993* | Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1994 but has the additional constraint that and must be distinct. (Contributed by Jim Kingdon, 23-May-2018.) |
Theorem | nfeu 1994 | 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 1995 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.) |
Theorem | hbeu 1996 | 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 1997 | Deduction version of hbeu 1996. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 25-May-2018.) |
Theorem | sb8euh 1998 | Variable substitution in unique existential quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.) |
Theorem | cbveu 1999 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
Theorem | eu1 2000* | An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |