P. 20 of Theorem List - New Foundations Explorer

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

Type	Label	Description
Statement
Theorem	19.41v 1901*	Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃x(φ ∧ ψ) ↔ (∃xφ ∧ ψ))
Theorem	19.41vv 1902*	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃x∃y(φ ∧ ψ) ↔ (∃x∃yφ ∧ ψ))
Theorem	19.41vvv 1903*	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
⊢ (∃x∃y∃z(φ ∧ ψ) ↔ (∃x∃y∃zφ ∧ ψ))
Theorem	19.41vvvv 1904*	Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
⊢ (∃w∃x∃y∃z(φ ∧ ψ) ↔ (∃w∃x∃y∃zφ ∧ ψ))
Theorem	19.42v 1905*	Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
⊢ (∃x(φ ∧ ψ) ↔ (φ ∧ ∃xψ))
Theorem	exdistr 1906*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃x∃y(φ ∧ ψ) ↔ ∃x(φ ∧ ∃yψ))
Theorem	19.42vv 1907*	Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
⊢ (∃x∃y(φ ∧ ψ) ↔ (φ ∧ ∃x∃yψ))
Theorem	19.42vvv 1908*	Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.)
⊢ (∃x∃y∃z(φ ∧ ψ) ↔ (φ ∧ ∃x∃y∃zψ))
Theorem	exdistr2 1909*	Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
⊢ (∃x∃y∃z(φ ∧ ψ) ↔ ∃x(φ ∧ ∃y∃zψ))
Theorem	3exdistr 1910*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃x∃y∃z(φ ∧ ψ ∧ χ) ↔ ∃x(φ ∧ ∃y(ψ ∧ ∃zχ)))
Theorem	4exdistr 1911*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
⊢ (∃x∃y∃z∃w((φ ∧ ψ) ∧ (χ ∧ θ)) ↔ ∃x(φ ∧ ∃y(ψ ∧ ∃z(χ ∧ ∃wθ))))
Theorem	eean 1912	Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    ⇒   ⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ))
Theorem	eeanv 1913*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ))
Theorem	eeeanv 1914*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∃x∃y∃z(φ ∧ ψ ∧ χ) ↔ (∃xφ ∧ ∃yψ ∧ ∃zχ))
Theorem	ee4anv 1915*	Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
⊢ (∃x∃y∃z∃w(φ ∧ ψ) ↔ (∃x∃yφ ∧ ∃z∃wψ))
Theorem	nexdv 1916*	Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ¬ ψ)    ⇒   ⊢ (φ → ¬ ∃xψ)
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: "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]φ → φ))
Theorem	sbequ1 1918	An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → (φ → [y / x]φ))
Theorem	sbequ12 1919	An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → (φ ↔ [y / x]φ))
Theorem	sbequ12r 1920	An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
⊢ (x = y → ([x / y]φ ↔ φ))
Theorem	sbequ12a 1921	An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → ([y / x]φ ↔ [x / y]φ))
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.)
⊢ ([x / x]φ ↔ φ)
Theorem	sb4a 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 → φ))
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.)
⊢ ([y / x]φ → ∀x(x = y → ∃yφ))
1.5.4  Axiom scheme ax-12 (Quantified Equality)
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 (¬ x = y → (¬ x = z → (y = z → ∀xy = 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 = z → ∀xy = 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 = z → ∀x y = z))
Theorem	ax12v 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 = z → ∀x y = z))
Theorem	ax12olem1 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)
Theorem	ax12olem2 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 = w → ∀x y = w))    ⇒   ⊢ (¬ x = y → (¬ y = z → ∀x ¬ y = z))
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.)
⊢ ((¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z)) ↔ ((¬ x = y → (y = z → ∀x y = z)) ∧ (¬ x = y → (¬ y = z → ∀x ¬ y = z))))
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.)
⊢ (¬ x = y → (y = z → ∀x y = z))    &   ⊢ (¬ x = y → (y = w → ∀x y = w))    ⇒   ⊢ (¬ x = y → (¬ ∀x ¬ y = z → ∀x y = z))
Theorem	ax12olem5 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 = z → ∀x y = z))    ⇒   ⊢ (¬ ∀x x = y → (y = z → ∀x y = z))
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.)
⊢ (¬ ∀x x = z → (z = w → ∀x z = w))    &   ⊢ (¬ ∀x x = y → (y = w → ∀x y = w))    ⇒   ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (y = z → ∀x y = z)))
Theorem	ax12olem7 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 = w → ∀x z = w))    &   ⊢ (¬ x = y → (¬ ∀x ¬ y = w → ∀x y = w))    ⇒   ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (y = z → ∀x y = z)))
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.)
⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
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.)
⊢ (¬ x = y → (y = z → ∀x y = z))
Theorem	ax10lem1 1936*	Lemma for ax10 1944. Change bound variable. (Contributed by NM, 22-Jul-2015.)
⊢ (∀x x = w → ∀y y = w)
Theorem	ax10lem2 1937*	Lemma for ax10 1944. Change free variable. (Contributed by NM, 25-Jul-2015.)
⊢ (∀x x = y → ∀x x = z)
Theorem	ax10lem3 1938*	Lemma for ax10 1944. Similar to ax-10 2140 but with distinct variables. (Contributed by NM, 25-Jul-2015.)
⊢ (∀x x = y → ∀y y = x)
Theorem	dvelimv 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ψ))
Theorem	dveeq2 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 = y → ∀x z = y))
Theorem	ax10lem4 1941*	Lemma for ax10 1944. Change bound variable. (Contributed by NM, 8-Jul-2016.)
⊢ (∀x x = w → ∀y y = x)
Theorem	ax10lem5 1942*	Lemma for ax10 1944. Change free and bound variables. (Contributed by NM, 22-Jul-2015.)
⊢ (∀z z = w → ∀y y = x)
Theorem	ax10lem6 1943	Lemma for ax10 1944. Similar to ax10o 1952 but with reversed antecedent. (Contributed by NM, 25-Jul-2015.)
⊢ (∀y y = x → (∀xφ → ∀yφ))
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.)
⊢ (∀x x = y → ∀y y = x)
Theorem	a16g 1945*	Generalization of ax16 2045. (Contributed by NM, 25-Jul-2015.)
⊢ (∀x x = y → (φ → ∀zφ))
Theorem	aecom 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 = y → ∀y y = x)
Theorem	aecoms 1947	A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x x = y → φ)    ⇒   ⊢ (∀y y = x → φ)
Theorem	naecoms 1948	A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀x x = y → φ)    ⇒   ⊢ (¬ ∀y y = x → φ)
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.)
⊢ ¬ ∀x ¬ x = y
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.)
⊢ (∀x(x = y → ∀xφ) → φ)
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.)
⊢ ∃x x = y
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.)
⊢ (∀x x = y → (∀xφ → ∀yφ))
Theorem	hbae 1953	All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x x = y → ∀z∀x x = y)
Theorem	nfae 1954	All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎz∀x x = y
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.)
⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
Theorem	nfnae 1956	All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎz ¬ ∀x x = y
Theorem	hbnaes 1957	Rule that applies hbnae 1955 to antecedent. (Contributed by NM, 5-Aug-1993.)
⊢ (∀z ¬ ∀x x = y → φ)    ⇒   ⊢ (¬ ∀x x = y → φ)
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.)
⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → Ⅎz x = y)
Theorem	equs4 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 ∧ φ))
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.)
⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x(x = y → φ) ↔ ψ)
Theorem	equsalh 1961	A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x(x = y → φ) ↔ ψ)
Theorem	equsex 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 ∧ φ) ↔ ψ)
Theorem	equsexh 1963	A useful equivalence related to substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃x(x = y ∧ φ) ↔ ψ)
Theorem	dvelimh 1964	Version of dvelim 2016 without any variable restrictions. (Contributed by NM, 1-Oct-2002.)
⊢ (φ → ∀xφ)    &   ⊢ (ψ → ∀zψ)    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
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.)
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∀xφ ↔ ∀yψ))
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.)
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∀zφ ↔ ∀zψ))
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.)
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∃xφ ↔ ∃yψ))
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.)
⊢ (∀x x = y → (φ ↔ ψ))    ⇒   ⊢ (∀x x = y → (∃zφ ↔ ∃zψ))
Theorem	drnf1 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ψ))
Theorem	drnf2 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ψ))
Theorem	exdistrf 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φ)    ⇒   ⊢ (∃x∃y(φ ∧ ψ) → ∃x(φ ∧ ∃yψ))
Theorem	nfald2 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ψ)    ⇒   ⊢ (φ → Ⅎx∀yψ)
Theorem	nfexd2 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ψ)    ⇒   ⊢ (φ → Ⅎx∃yψ)
Theorem	spimt 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φ → ψ))
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.)
⊢ Ⅎxψ    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ψ)
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.)
⊢ Ⅎxφ    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (φ → ∃xψ)
Theorem	spimed 1977	Deduction version of spime 1976. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)
⊢ (χ → Ⅎxφ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (χ → (φ → ∃xψ))
Theorem	cbv1h 1978	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → ∀yψ))    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ → χ)))    ⇒   ⊢ (∀x∀yφ → (∀xψ → ∀yχ))
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.)
⊢ (φ → Ⅎyψ)    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → (x = y → (ψ → χ)))    ⇒   ⊢ (∀x∀yφ → (∀xψ → ∀yχ))
Theorem	cbv2h 1980	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → (ψ → ∀yψ))    &   ⊢ (φ → (χ → ∀xχ))    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (∀x∀yφ → (∀xψ ↔ ∀yχ))
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.)
⊢ (φ → Ⅎyψ)    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (∀x∀yφ → (∀xψ ↔ ∀yχ))
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.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ∀yψ)
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.)
⊢ (φ → ∀yφ)    &   ⊢ (ψ → ∀xψ)    &   ⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ∀yψ)
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.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀xφ ↔ ∀yψ)
Theorem	cbvex 1985	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎyφ    &   ⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃xφ ↔ ∃yψ)
Theorem	chvar 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 → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	equvini 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 = y → ∃z(x = z ∧ z = y))
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.)
⊢ (∀z(z = x ↔ z = y) → x = y)
Theorem	equs45f 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 → φ))
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.)
⊢ (x = y → (φ → ψ))    ⇒   ⊢ (∀xφ → ψ)
Theorem	aev 1991*	A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.)
⊢ (∀x x = y → ∀z w = v)
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.)
⊢ (x = z → (φ → ∀x(x = z → φ)))    ⇒   ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
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.)
⊢ (x = z → (∀zφ → ∀x(x = z → φ)))    ⇒   ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
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.)
⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
Theorem	ax11b 1995	A bidirectional version of ax11o 1994. (Contributed by NM, 30-Jun-2006.)
⊢ ((¬ ∀x x = y ∧ x = y) → (φ ↔ ∀x(x = y → φ)))
Theorem	equs5 1996	Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀x x = y → (∃x(x = y ∧ φ) → ∀x(x = y → φ)))
Theorem	dvelimf 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ψ)
Theorem	spv 1998*	Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀xφ → ψ)
Theorem	spimev 1999*	Distinct-variable version of spime 1976. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → (φ → ψ))    ⇒   ⊢ (φ → ∃xψ)
Theorem	speiv 2000*	Inference from existential specialization, using implicit substitution. (Contributed by NM, 19-Aug-1993.)
⊢ (x = y → (φ ↔ ψ))    &   ⊢ ψ    ⇒   ⊢ ∃xφ