 Home New Foundations ExplorerTheorem List (p. 20 of 64) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 1901-2000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorem19.41v 1901* Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
(x(φ ψ) ↔ (xφ ψ))

Theorem19.41vv 1902* Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
(xy(φ ψ) ↔ (xyφ ψ))

Theorem19.41vvv 1903* Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
(xyz(φ ψ) ↔ (xyzφ ψ))

Theorem19.41vvvv 1904* Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
(wxyz(φ ψ) ↔ (wxyzφ ψ))

Theorem19.42v 1905* Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
(x(φ ψ) ↔ (φ xψ))

Theoremexdistr 1906* Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
(xy(φ ψ) ↔ x(φ yψ))

Theorem19.42vv 1907* Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
(xy(φ ψ) ↔ (φ xyψ))

Theorem19.42vvv 1908* Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.)
(xyz(φ ψ) ↔ (φ xyzψ))

Theoremexdistr2 1909* Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
(xyz(φ ψ) ↔ x(φ yzψ))

Theorem3exdistr 1910* Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(xyz(φ ψ χ) ↔ x(φ y(ψ zχ)))

Theorem4exdistr 1911* Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
(xyzw((φ ψ) (χ θ)) ↔ x(φ y(ψ z(χ wθ))))

Theoremeean 1912 Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
yφ    &   xψ       (xy(φ ψ) ↔ (xφ yψ))

Theoremeeanv 1913* Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
(xy(φ ψ) ↔ (xφ yψ))

Theoremeeeanv 1914* Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(xyz(φ ψ χ) ↔ (xφ yψ zχ))

Theoremee4anv 1915* Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
(xyzw(φ ψ) ↔ (xyφ zwψ))

Theoremnexdv 1916* Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
(φ → ¬ ψ)       (φ → ¬ xψ)

Theoremstdpc7 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: "x = y → (φ(x, x) → φ(x, y)), provided that y is free for x in φ(x, x)." Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.)
(x = y → ([x / y]φφ))

Theoremsbequ1 1918 An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
(x = y → (φ → [y / x]φ))

Theoremsbequ12 1919 An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
(x = y → (φ ↔ [y / x]φ))

Theoremsbequ12r 1920 An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
(x = y → ([x / y]φφ))

Theoremsbequ12a 1921 An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
(x = y → ([y / x]φ ↔ [x / y]φ))

Theoremsbid 1922 An identity theorem for substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by NM, 5-Aug-1993.)
([x / x]φφ)

Theoremsb4a 1923 A version of sb4 2053 that doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
([y / x]yφx(x = yφ))

Theoremsb4e 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.)
([y / x]φx(x = yyφ))

1.5.4  Axiom scheme ax-12 (Quantified Equality)

Axiomax-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 x = y → (¬ x = z → (y = zxy = z))) (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 ¬ x = y to hold, x and y must have different values and thus cannot be the same object-language variable. Similarly, x and z cannot be the same object-language variable. Therefore, x will not occur in the wff y = z when the first two antecedents hold, so analogous to ax-17 1616, the conclusion (y = zxy = z) 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 x on y = z even when x and y are substituted with the same variable. In this case, the first antecedent becomes ¬ x = x 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 ¬ xx = y.

This axiom can be weakened if desired by adding distinct variable restrictions on pairs x, z and y, z. 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.)

x = y → (y = zx y = z))

Theoremax12v 1926* A weaker version of ax-12 1925 with distinct variable restrictions on pairs x, z and y, z. 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.)
x = y → (y = zx y = z))

Theoremax12olem1 1927* Lemma for ax12o 1934. Similar to equvin 2001 but with a negated equality. (Contributed by NM, 24-Dec-2015.)
(w(y = w ¬ z = w) ↔ ¬ y = z)

Theoremax12olem2 1928* Lemma for ax12o 1934. Negate the equalities in ax-12 1925, shown as the hypothesis. (Contributed by NM, 24-Dec-2015.)
x = y → (y = wx y = w))       x = y → (¬ y = zx ¬ y = z))

Theoremax12olem3 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.)
((¬ x = y → (¬ x ¬ y = zx y = z)) ↔ ((¬ x = y → (y = zx y = z)) x = y → (¬ y = zx ¬ y = z))))

Theoremax12olem4 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.)
x = y → (y = zx y = z))    &   x = y → (y = wx y = w))       x = y → (¬ x ¬ y = zx y = z))

Theoremax12olem5 1931 Lemma for ax12o 1934. See ax12olem6 1932 for derivation of ax12o 1934 from the conclusion. (Contributed by NM, 24-Dec-2015.)
x = y → (¬ x ¬ y = zx y = z))       x x = y → (y = zx y = z))

Theoremax12olem6 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.)
x x = z → (z = wx z = w))    &   x x = y → (y = wx y = w))       x x = y → (¬ x x = z → (y = zx y = z)))

Theoremax12olem7 1933* Lemma for ax12o 1934. Derivation of ax12o 1934 from the hypotheses, without using ax12o 1934. (Contributed by NM, 24-Dec-2015.)
x = z → (¬ x ¬ z = wx z = w))    &   x = y → (¬ x ¬ y = wx y = w))       x x = y → (¬ x x = z → (y = zx y = z)))

Theoremax12o 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.)
z z = x → (¬ z z = y → (x = yz x = y)))

Theoremax12 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.)
x = y → (y = zx y = z))

Theoremax10lem1 1936* Lemma for ax10 1944. Change bound variable. (Contributed by NM, 22-Jul-2015.)
(x x = wy y = w)

Theoremax10lem2 1937* Lemma for ax10 1944. Change free variable. (Contributed by NM, 25-Jul-2015.)
(x x = yx x = z)

Theoremax10lem3 1938* Lemma for ax10 1944. Similar to ax-10 2140 but with distinct variables. (Contributed by NM, 25-Jul-2015.)
(x x = yy y = x)

Theoremdvelimv 1939* Similar to dvelim 2016 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.)
(z = y → (φψ))       x x = y → (ψxψ))

Theoremdveeq2 1940* Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.)
x x = y → (z = yx z = y))

Theoremax10lem4 1941* Lemma for ax10 1944. Change bound variable. (Contributed by NM, 8-Jul-2016.)
(x x = wy y = x)

Theoremax10lem5 1942* Lemma for ax10 1944. Change free and bound variables. (Contributed by NM, 22-Jul-2015.)
(z z = wy y = x)

Theoremax10lem6 1943 Lemma for ax10 1944. Similar to ax10o 1952 but with reversed antecedent. (Contributed by NM, 25-Jul-2015.)
(y y = x → (xφyφ))

Theoremax10 1944 Derive set.mm's original ax-10 2140 from others. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 7-Nov-2015.)
(x x = yy y = x)

Theorema16g 1945* Generalization of ax16 2045. (Contributed by NM, 25-Jul-2015.)
(x x = y → (φzφ))

Theoremaecom 1946 Commutation law for identical variable specifiers. The antecedent and consequent are true when x and y are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.)
(x x = yy y = x)

Theoremaecoms 1947 A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.)
(x x = yφ)       (y y = xφ)

Theoremnaecoms 1948 A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.)
x x = yφ)       y y = xφ)

Theoremax9 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.)

¬ x ¬ x = y

Theoremax9o 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.)

(x(x = yxφ) → φ)

Theorema9e 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.)
x x = y

Theoremax10o 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.)
(x x = y → (xφyφ))

Theoremhbae 1953 All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.)
(x x = yzx x = y)

Theoremnfae 1954 All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
zx x = y

Theoremhbnae 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.)
x x = yz ¬ x x = y)

Theoremnfnae 1956 All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
z ¬ x x = y

Theoremhbnaes 1957 Rule that applies hbnae 1955 to antecedent. (Contributed by NM, 5-Aug-1993.)
(z ¬ x x = yφ)       x x = yφ)

Theoremnfeqf 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.)
((¬ z z = x ¬ z z = y) → Ⅎz x = y)

Theoremequs4 1959 Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.)
(x(x = yφ) → x(x = y φ))

Theoremequsal 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.)
xψ    &   (x = y → (φψ))       (x(x = yφ) ↔ ψ)

Theoremequsalh 1961 A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.)
(ψxψ)    &   (x = y → (φψ))       (x(x = yφ) ↔ ψ)

Theoremequsex 1962 A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
xψ    &   (x = y → (φψ))       (x(x = y φ) ↔ ψ)

Theoremequsexh 1963 A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.)
(ψxψ)    &   (x = y → (φψ))       (x(x = y φ) ↔ ψ)

Theoremdvelimh 1964 Version of dvelim 2016 without any variable restrictions. (Contributed by NM, 1-Oct-2002.)
(φxφ)    &   (ψzψ)    &   (z = y → (φψ))       x x = y → (ψxψ))

Theoremdral1 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.)
(x x = y → (φψ))       (x x = y → (xφyψ))

Theoremdral2 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.)
(x x = y → (φψ))       (x x = y → (zφzψ))

Theoremdrex1 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.)
(x x = y → (φψ))       (x x = y → (xφyψ))

Theoremdrex2 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.)
(x x = y → (φψ))       (x x = y → (zφzψ))

Theoremdrnf1 1969 Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.)
(x x = y → (φψ))       (x x = y → (Ⅎxφ ↔ Ⅎyψ))

Theoremdrnf2 1970 Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.)
(x x = y → (φψ))       (x x = y → (Ⅎzφ ↔ Ⅎzψ))

Theoremexdistrf 1971 Distribution of existential quantifiers, with a bound-variable hypothesis saying that y is not free in φ, but x can be free in φ (and there is no distinct variable condition on x and y). (Contributed by Mario Carneiro, 20-Mar-2013.)
x x = y → Ⅎyφ)       (xy(φ ψ) → x(φ yψ))

Theoremnfald2 1972 Variation on nfald 1852 which adds the hypothesis that x and y are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.)
yφ    &   ((φ ¬ x x = y) → Ⅎxψ)       (φ → Ⅎxyψ)

Theoremnfexd2 1973 Variation on nfexd 1854 which adds the hypothesis that x and y are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.)
yφ    &   ((φ ¬ x x = y) → Ⅎxψ)       (φ → Ⅎxyψ)

Theoremspimt 1974 Closed theorem form of spim 1975. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.)
((Ⅎxψ x(x = y → (φψ))) → (xφψ))

Theoremspim 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.)
xψ    &   (x = y → (φψ))       (xφψ)

Theoremspime 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.)
xφ    &   (x = y → (φψ))       (φxψ)

Theoremspimed 1977 Deduction version of spime 1976. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
(χ → Ⅎxφ)    &   (x = y → (φψ))       (χ → (φxψ))

Theoremcbv1h 1978 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
(φ → (ψyψ))    &   (φ → (χxχ))    &   (φ → (x = y → (ψχ)))       (xyφ → (xψyχ))

Theoremcbv1 1979 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
(φ → Ⅎyψ)    &   (φ → Ⅎxχ)    &   (φ → (x = y → (ψχ)))       (xyφ → (xψyχ))

Theoremcbv2h 1980 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
(φ → (ψyψ))    &   (φ → (χxχ))    &   (φ → (x = y → (ψχ)))       (xyφ → (xψyχ))

Theoremcbv2 1981 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
(φ → Ⅎyψ)    &   (φ → Ⅎxχ)    &   (φ → (x = y → (ψχ)))       (xyφ → (xψyχ))

Theoremcbv3 1982 Rule used to change bound variables, using implicit substitution, that does not use ax-12o 2142. (Contributed by NM, 5-Aug-1993.)
yφ    &   xψ    &   (x = y → (φψ))       (xφyψ)

Theoremcbv3h 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.)
(φyφ)    &   (ψxψ)    &   (x = y → (φψ))       (xφyψ)

Theoremcbval 1984 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
yφ    &   xψ    &   (x = y → (φψ))       (xφyψ)

Theoremcbvex 1985 Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
yφ    &   xψ    &   (x = y → (φψ))       (xφyψ)

Theoremchvar 1986 Implicit substitution of y for x into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.)
xψ    &   (x = y → (φψ))    &   φ       ψ

Theoremequvini 1987 A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require z to be distinct from x and y (making the proof longer). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
(x = yz(x = z z = y))

Theoremequveli 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.)
(z(z = xz = y) → x = y)

Theoremequs45f 1989 Two ways of expressing substitution when y is not free in φ. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.)
yφ       (x(x = y φ) ↔ x(x = yφ))

Theoremspimv 1990* A version of spim 1975 with a distinct variable requirement instead of a bound variable hypothesis. (Contributed by NM, 5-Aug-1993.)
(x = y → (φψ))       (xφψ)

Theoremaev 1991* A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.)
(x x = yz w = v)

Theoremax11v2 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.)
(x = z → (φx(x = zφ)))       x x = y → (x = y → (φx(x = yφ))))

Theoremax11a2 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.)
(x = z → (zφx(x = zφ)))       x x = y → (x = y → (φx(x = yφ))))

Theoremax11o 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.)

x x = y → (x = y → (φx(x = yφ))))

Theoremax11b 1995 A bidirectional version of ax11o 1994. (Contributed by NM, 30-Jun-2006.)
((¬ x x = y x = y) → (φx(x = yφ)))

Theoremequs5 1996 Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.)
x x = y → (x(x = y φ) → x(x = yφ)))

Theoremdvelimf 1997 Version of dvelimv 1939 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.)
xφ    &   zψ    &   (z = y → (φψ))       x x = y → Ⅎxψ)

Theoremspv 1998* Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)
(x = y → (φψ))       (xφψ)

Theoremspimev 1999* Distinct-variable version of spime 1976. (Contributed by NM, 5-Aug-1993.)
(x = y → (φψ))       (φxψ)

Theoremspeiv 2000* Inference from existential specialization, using implicit substitution. (Contributed by NM, 19-Aug-1993.)
(x = y → (φψ))    &   ψ       xφ

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-6336
 Copyright terms: Public domain < Previous  Next >