Home | New
Foundations Explorer Theorem List (p. 20 of 64) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > NFE Home Page > Theorem List Contents This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.41v 1901* | Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.41vv 1902* | Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.) |
Theorem | 19.41vvv 1903* | Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.) |
Theorem | 19.41vvvv 1904* | Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.) |
Theorem | 19.42v 1905* | Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exdistr 1906* | Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
Theorem | 19.42vv 1907* | Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.) |
Theorem | 19.42vvv 1908* | Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.) |
Theorem | exdistr2 1909* | Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
Theorem | 3exdistr 1910* | Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | 4exdistr 1911* | Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
Theorem | eean 1912 | Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | eeanv 1913* | Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) |
Theorem | eeeanv 1914* | Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | ee4anv 1915* | Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.) |
Theorem | nexdv 1916* | Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.) |
Theorem | stdpc7 1917 | One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 1687.) Translated to traditional notation, it can be read: " , provided that is free for in ." Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.) |
Theorem | sbequ1 1918 | An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbequ12 1919 | An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbequ12r 1920 | An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
Theorem | sbequ12a 1921 | An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | sbid 1922 | An identity theorem for substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | sb4a 1923 | A version of sb4 2053 that doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.) |
Theorem | sb4e 1924 | One direction of a simplified definition of substitution that unlike sb4 2053 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.) |
Axiom | ax-12 1925 |
Axiom of Quantified Equality. One of the equality and substitution axioms
of predicate calculus with equality.
An equivalent way to express this axiom that may be easier to understand is (see ax12b 1689). Recall that in the intended interpretation, our variables are metavariables ranging over the variables of predicate calculus (the object language). In order for the first antecedent to hold, and must have different values and thus cannot be the same object-language variable. Similarly, and cannot be the same object-language variable. Therefore, will not occur in the wff when the first two antecedents hold, so analogous to ax-17 1616, the conclusion follows. The original version of this axiom was ax-12o 2142 and was replaced with this shorter ax-12 1925 in December 2015. The old axiom is proved from this one as theorem ax12o 1934. Conversely, this axiom is proved from ax-12o 2142 as theorem ax12 1935. The primary purpose of this axiom is to provide a way to introduce the quantifier on even when and are substituted with the same variable. In this case, the first antecedent becomes and the axiom still holds. Although this version is shorter, the original version ax12o 1934 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of ax12o 1934 is in dvelimh 1964 which converts a distinct variable pair to the distinctor antecendent . This axiom can be weakened if desired by adding distinct variable restrictions on pairs and . To show that, we add these restrictions to theorem ax12v 1926 and use only ax12v 1926 for further derivations. Thus, ax12v 1926 should be the only theorem referencing this axiom. Other theorems can reference either ax12v 1926 or ax12o 1934. This axiom scheme is logically redundant (see ax12w 1724) but is used as an auxiliary axiom to achieve metalogical completeness. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.) |
Theorem | ax12v 1926* | A weaker version of ax-12 1925 with distinct variable restrictions on pairs and . In order to show that this weakening is adequate, this should be the only theorem referencing ax-12 1925 directly. (Contributed by NM, 30-Jun-2016.) |
Theorem | ax12olem1 1927* | Lemma for ax12o 1934. Similar to equvin 2001 but with a negated equality. (Contributed by NM, 24-Dec-2015.) |
Theorem | ax12olem2 1928* | Lemma for ax12o 1934. Negate the equalities in ax-12 1925, shown as the hypothesis. (Contributed by NM, 24-Dec-2015.) |
Theorem | ax12olem3 1929 | Lemma for ax12o 1934. Show the equivalence of an intermediate equivalent to ax12o 1934 with the conjunction of ax-12 1925 and a variant with negated equalities. (Contributed by NM, 24-Dec-2015.) |
Theorem | ax12olem4 1930* | Lemma for ax12o 1934. Construct an intermediate equivalent to ax-12 1925 from two instances of ax-12 1925. (Contributed by NM, 24-Dec-2015.) |
Theorem | ax12olem5 1931 | Lemma for ax12o 1934. See ax12olem6 1932 for derivation of ax12o 1934 from the conclusion. (Contributed by NM, 24-Dec-2015.) |
Theorem | ax12olem6 1932* | Lemma for ax12o 1934. Derivation of ax12o 1934 from the hypotheses, without using ax12o 1934. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 24-Dec-2015.) |
Theorem | ax12olem7 1933* | Lemma for ax12o 1934. Derivation of ax12o 1934 from the hypotheses, without using ax12o 1934. (Contributed by NM, 24-Dec-2015.) |
Theorem | ax12o 1934 | Derive set.mm's original ax-12o 2142 from the shorter ax-12 1925. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) |
Theorem | ax12 1935 | Derive ax-12 1925 from ax12v 1926 via ax12o 1934. This shows that the weakening in ax12v 1926 is still sufficient for a complete system. (Contributed by NM, 21-Dec-2015.) |
Theorem | ax10lem1 1936* | Lemma for ax10 1944. Change bound variable. (Contributed by NM, 22-Jul-2015.) |
Theorem | ax10lem2 1937* | Lemma for ax10 1944. Change free variable. (Contributed by NM, 25-Jul-2015.) |
Theorem | ax10lem3 1938* | Lemma for ax10 1944. Similar to ax-10 2140 but with distinct variables. (Contributed by NM, 25-Jul-2015.) |
Theorem | dvelimv 1939* | Similar to dvelim 2016 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.) |
Theorem | dveeq2 1940* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) |
Theorem | ax10lem4 1941* | Lemma for ax10 1944. Change bound variable. (Contributed by NM, 8-Jul-2016.) |
Theorem | ax10lem5 1942* | Lemma for ax10 1944. Change free and bound variables. (Contributed by NM, 22-Jul-2015.) |
Theorem | ax10lem6 1943 | Lemma for ax10 1944. Similar to ax10o 1952 but with reversed antecedent. (Contributed by NM, 25-Jul-2015.) |
Theorem | ax10 1944 | Derive set.mm's original ax-10 2140 from others. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 7-Nov-2015.) |
Theorem | a16g 1945* | Generalization of ax16 2045. (Contributed by NM, 25-Jul-2015.) |
Theorem | aecom 1946 | Commutation law for identical variable specifiers. The antecedent and consequent are true when and are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | aecoms 1947 | A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.) |
Theorem | naecoms 1948 | A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) |
Theorem | ax9 1949 |
Theorem showing that ax-9 1654 follows from the weaker version ax9v 1655.
(Even though this theorem depends on ax-9 1654,
all references of ax-9 1654
are made via ax9v 1655. An earlier version stated ax9v 1655
as a separate
axiom, but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-9 1654 so that all proofs can be traced back to ax9v 1655. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) |
Theorem | ax9o 1950 |
Show that the original axiom ax-9o 2138 can be derived from ax9 1949
and
others. See ax9from9o 2148 for the rederivation of ax9 1949
from ax-9o 2138.
Normally, ax9o 1950 should be used rather than ax-9o 2138, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) |
Theorem | a9e 1951 | At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1557 through ax-14 1714 and ax-17 1616, all axioms other than ax9 1949 are believed to be theorems of free logic, although the system without ax9 1949 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) |
Theorem | ax10o 1952 | Show that ax-10o 2139 can be derived from ax-10 2140 in the form of ax10 1944. Normally, ax10o 1952 should be used rather than ax-10o 2139, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof modification is discouraged.) |
Theorem | hbae 1953 | All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfae 1954 | All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbnae 1955 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | nfnae 1956 | All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbnaes 1957 | Rule that applies hbnae 1955 to antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfeqf 1958 | A variable is effectively not free in an equality if it is not either of the involved variables. version of ax-12o 2142. (Contributed by Mario Carneiro, 6-Oct-2016.) |
Theorem | equs4 1959 | Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) |
Theorem | equsal 1960 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | equsalh 1961 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | equsex 1962 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | equsexh 1963 | A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | dvelimh 1964 | Version of dvelim 2016 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) |
Theorem | dral1 1965 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 24-Nov-1994.) |
Theorem | dral2 1966 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
Theorem | drex1 1967 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
Theorem | drex2 1968 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
Theorem | drnf1 1969 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) |
Theorem | drnf2 1970 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) |
Theorem | exdistrf 1971 | Distribution of existential quantifiers, with a bound-variable hypothesis saying that is not free in , but can be free in (and there is no distinct variable condition on and ). (Contributed by Mario Carneiro, 20-Mar-2013.) |
Theorem | nfald2 1972 | Variation on nfald 1852 which adds the hypothesis that and are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | nfexd2 1973 | Variation on nfexd 1854 which adds the hypothesis that and are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) |
Theorem | spimt 1974 | Closed theorem form of spim 1975. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) |
Theorem | spim 1975 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 1975 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | spime 1976 | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | spimed 1977 | Deduction version of spime 1976. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | cbv1h 1978 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | cbv1 1979 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | cbv2h 1980 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | cbv2 1981 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | cbv3 1982 | Rule used to change bound variables, using implicit substitution, that does not use ax-12o 2142. (Contributed by NM, 5-Aug-1993.) |
Theorem | cbv3h 1983 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) |
Theorem | cbval 1984 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | cbvex 1985 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) |
Theorem | chvar 1986 | Implicit substitution of for into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) |
Theorem | equvini 1987 | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require to be distinct from and (making the proof longer). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | equveli 1988 | A variable elimination law for equality with no distinct variable requirements. (Compare equvini 1987.) (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) |
Theorem | equs45f 1989 | Two ways of expressing substitution when is not free in . (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) |
Theorem | spimv 1990* | A version of spim 1975 with a distinct variable requirement instead of a bound variable hypothesis. (Contributed by NM, 5-Aug-1993.) |
Theorem | aev 1991* | A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) |
Theorem | ax11v2 1992* | Recovery of ax-11o 2141 from ax11v 2096. This proof uses ax-10 2140 and ax-11 1746. TODO: figure out if this is useful, or if it should be simplified or eliminated. (Contributed by NM, 2-Feb-2007.) |
Theorem | ax11a2 1993* | Derive ax-11o 2141 from a hypothesis in the form of ax-11 1746. ax-10 2140 and ax-11 1746 are used by the proof, but not ax-10o 2139 or ax-11o 2141. TODO: figure out if this is useful, or if it should be simplified or eliminated. (Contributed by NM, 2-Feb-2007.) |
Theorem | ax11o 1994 |
Derivation of set.mm's original ax-11o 2141 from ax-10 2140 and the shorter
ax-11 1746 that has replaced it.
An open problem is whether this theorem can be proved without relying on ax-16 2144 or ax-17 1616 (given all of the original and new versions of sp 1747 through ax-15 2143). Another open problem is whether this theorem can be proved without relying on ax12o 1934. Theorem ax11 2155 shows the reverse derivation of ax-11 1746 from ax-11o 2141. Normally, ax11o 1994 should be used rather than ax-11o 2141, except by theorems specifically studying the latter's properties. (Contributed by NM, 3-Feb-2007.) |
Theorem | ax11b 1995 | A bidirectional version of ax11o 1994. (Contributed by NM, 30-Jun-2006.) |
Theorem | equs5 1996 | Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.) |
Theorem | dvelimf 1997 | Version of dvelimv 1939 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) |
Theorem | spv 1998* | Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.) |
Theorem | spimev 1999* | Distinct-variable version of spime 1976. (Contributed by NM, 5-Aug-1993.) |
Theorem | speiv 2000* | Inference from existential specialization, using implicit substitution. (Contributed by NM, 19-Aug-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |