P. 21 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 2001-2100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	equvin 2001*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y ↔ ∃z(x = z ∧ z = y))
Theorem	cbvalv 2002*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∀xφ ↔ ∀yψ)
Theorem	cbvexv 2003*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ (∃xφ ↔ ∃yψ)
Theorem	cbval2 2004*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎzφ    &   ⊢ Ⅎwφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ (∀x∀yφ ↔ ∀z∀wψ)
Theorem	cbvex2 2005*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎzφ    &   ⊢ Ⅎwφ    &   ⊢ Ⅎxψ    &   ⊢ Ⅎyψ    &   ⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ (∃x∃yφ ↔ ∃z∃wψ)
Theorem	cbval2v 2006*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.)
⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ (∀x∀yφ ↔ ∀z∀wψ)
Theorem	cbvex2v 2007*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
⊢ ((x = z ∧ y = w) → (φ ↔ ψ))    ⇒   ⊢ (∃x∃yφ ↔ ∃z∃wψ)
Theorem	cbvald 2008*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2016. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎyψ)    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → (∀xψ ↔ ∀yχ))
Theorem	cbvexd 2009*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2016. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    &   ⊢ (φ → Ⅎyψ)    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → (∃xψ ↔ ∃yχ))
Theorem	cbvaldva 2010*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((φ ∧ x = y) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∀xψ ↔ ∀yχ))
Theorem	cbvexdva 2011*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
⊢ ((φ ∧ x = y) → (ψ ↔ χ))    ⇒   ⊢ (φ → (∃xψ ↔ ∃yχ))
Theorem	cbvex4v 2012*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
⊢ ((x = v ∧ y = u) → (φ ↔ ψ))    &   ⊢ ((z = f ∧ w = g) → (ψ ↔ χ))    ⇒   ⊢ (∃x∃y∃z∃wφ ↔ ∃v∃u∃f∃gχ)
Theorem	chvarv 2013*	Implicit substitution of y for x into a theorem. (Contributed by NM, 20-Apr-1994.)
⊢ (x = y → (φ ↔ ψ))    &   ⊢ φ    ⇒   ⊢ ψ
Theorem	cleljust 2014*	When the class variables in definition df-clel 2349 are replaced with setvar variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the setvar variables in wel 1711 with the class variables in wcel 1710. Note: This proof is referenced on the Metamath Proof Explorer Home Page and shouldn't be changed. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.)
⊢ (x ∈ y ↔ ∃z(z = x ∧ z ∈ y))
Theorem	cleljustALT 2015*	When the class variables in definition df-clel 2349 are replaced with setvar variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the setvar variables in wel 1711 with the class variables in wcel 1710. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) (Revised by Mario Carneiro, 21-Dec-2016.)
⊢ (x ∈ y ↔ ∃z(z = x ∧ z ∈ y))
Theorem	dvelim 2016*	This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" ¬ ∀xx = y as an antecedent. φ normally has z free and can be read φ(z), and ψ substitutes y for z and can be read φ(y). We don't require that x and y 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 ∀x∀z, conjoin them, and apply dvelimdf 2082. Other variants of this theorem are dvelimh 1964 (with no distinct variable restrictions), dvelimhw 1849 (that avoids ax-12 1925), and dvelimALT 2133 (that avoids ax-10 2140). (Contributed by NM, 23-Nov-1994.)
⊢ (φ → ∀xφ)    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → (ψ → ∀xψ))
Theorem	dvelimnf 2017*	Version of dvelim 2016 using "not free" notation. (Contributed by Mario Carneiro, 9-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (z = y → (φ ↔ ψ))    ⇒   ⊢ (¬ ∀x x = y → Ⅎxψ)
Theorem	dveeq1 2018*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀x x = y → (y = z → ∀x y = z))
Theorem	dveel1 2019*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀x x = y → (y ∈ z → ∀x y ∈ z))
Theorem	dveel2 2020*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀x x = y → (z ∈ y → ∀x z ∈ y))
Theorem	ax15 2021	Axiom ax-15 2143 is redundant if we assume ax-17 1616. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'. Note that w is a dummy variable introduced in the proof. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 2020 and ax-17 1616. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.)
⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))
Theorem	drsb1 2022	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, 5-Aug-1993.)
⊢ (∀x x = y → ([z / x]φ ↔ [z / y]φ))
Theorem	sb2 2023	One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x(x = y → φ) → [y / x]φ)
Theorem	stdpc4 2024	The specialization axiom of standard predicate calculus. It states that if a statement φ holds for all x, then it also holds for the specific case of y (properly) substituted for x. Translated to traditional notation, it can be read: "∀xφ(x) → φ(y), provided that y is free for x in φ(x)." Axiom 4 of [Mendelson] p. 69. See also spsbc 3059 and rspsbc 3125. (Contributed by NM, 5-Aug-1993.)
⊢ (∀xφ → [y / x]φ)
Theorem	sbft 2025	Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.)
⊢ (Ⅎxφ → ([y / x]φ ↔ φ))
Theorem	sbf 2026	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxφ    ⇒   ⊢ ([y / x]φ ↔ φ)
Theorem	sbh 2027	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀xφ)    ⇒   ⊢ ([y / x]φ ↔ φ)
Theorem	sbf2 2028	Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
⊢ ([y / x]∀xφ ↔ ∀xφ)
Theorem	sb6x 2029	Equivalence involving substitution for a variable not free. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxφ    ⇒   ⊢ ([y / x]φ ↔ ∀x(x = y → φ))
Theorem	nfs1f 2030	If x is not free in φ, it is not free in [y / x]φ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎxφ    ⇒   ⊢ Ⅎx[y / x]φ
Theorem	sbequ5 2031	Substitution does not change an identical variable specifier. (Contributed by NM, 5-Aug-1993.)
⊢ ([w / z]∀x x = y ↔ ∀x x = y)
Theorem	sbequ6 2032	Substitution does not change a distinctor. (Contributed by NM, 5-Aug-1993.)
⊢ ([w / z] ¬ ∀x x = y ↔ ¬ ∀x x = y)
Theorem	sbt 2033	A substitution into a theorem remains true. (See chvar 1986 and chvarv 2013 for versions using implicit substitution.) (Contributed by NM, 21-Jan-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ φ    ⇒   ⊢ [y / x]φ
Theorem	equsb1 2034	Substitution applied to an atomic wff. (Contributed by NM, 5-Aug-1993.)
⊢ [y / x]x = y
Theorem	equsb2 2035	Substitution applied to an atomic wff. (Contributed by NM, 5-Aug-1993.)
⊢ [y / x]y = x
Theorem	sbied 2036	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2038). (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ (φ → Ⅎxχ)    &   ⊢ (φ → (x = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → ([y / x]ψ ↔ χ))
Theorem	sbiedv 2037*	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2038). (Contributed by NM, 7-Jan-2017.)
⊢ ((φ ∧ x = y) → (ψ ↔ χ))    ⇒   ⊢ (φ → ([y / x]ψ ↔ χ))
Theorem	sbie 2038	Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxψ    &   ⊢ (x = y → (φ ↔ ψ))    ⇒   ⊢ ([y / x]φ ↔ ψ)
Theorem	sb6f 2039	Equivalence for substitution when y is not free in φ. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ ([y / x]φ ↔ ∀x(x = y → φ))
Theorem	sb5f 2040	Equivalence for substitution when y is not free in φ. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ ([y / x]φ ↔ ∃x(x = y ∧ φ))
Theorem	hbsb2a 2041	Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.)
⊢ ([y / x]∀yφ → ∀x[y / x]φ)
Theorem	hbsb2e 2042	Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.)
⊢ ([y / x]φ → ∀x[y / x]∃yφ)
Theorem	hbsb3 2043	If y is not free in φ, x is not free in [y / x]φ. (Contributed by NM, 5-Aug-1993.)
⊢ (φ → ∀yφ)    ⇒   ⊢ ([y / x]φ → ∀x[y / x]φ)
Theorem	nfs1 2044	If y is not free in φ, x is not free in [y / x]φ. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎyφ    ⇒   ⊢ Ⅎx[y / x]φ
Theorem	ax16 2045*	Proof of older axiom ax-16 2144. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.)
⊢ (∀x x = y → (φ → ∀xφ))
Theorem	ax16i 2046*	Inference with ax16 2045 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.)
⊢ (x = z → (φ ↔ ψ))    &   ⊢ (ψ → ∀xψ)    ⇒   ⊢ (∀x x = y → (φ → ∀xφ))
Theorem	ax16ALT 2047*	Alternate proof of ax16 2045. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀x x = y → (φ → ∀xφ))
Theorem	ax16ALT2 2048*	Alternate proof of ax16 2045. (Contributed by NM, 8-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀x x = y → (φ → ∀xφ))
Theorem	a16gALT 2049*	A generalization of Axiom ax-16 2144. Alternate proof of a16g 1945 that uses df-sb 1649. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀x x = y → (φ → ∀zφ))
Theorem	a16gb 2050*	A generalization of Axiom ax-16 2144. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x x = y → (φ ↔ ∀zφ))
Theorem	a16nf 2051*	If dtru in set.mm is false, then there is only one element in the universe, so everything satisfies Ⅎ. (Contributed by Mario Carneiro, 7-Oct-2016.)
⊢ (∀x x = y → Ⅎzφ)
Theorem	sb3 2052	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀x x = y → (∃x(x = y ∧ φ) → [y / x]φ))
Theorem	sb4 2053	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀x x = y → ([y / x]φ → ∀x(x = y → φ)))
Theorem	sb4b 2054	Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.)
⊢ (¬ ∀x x = y → ([y / x]φ ↔ ∀x(x = y → φ)))
Theorem	dfsb2 2055	An alternate definition of proper substitution that, like df-sb 1649, mixes free and bound variables to avoid distinct variable requirements. (Contributed by NM, 17-Feb-2005.)
⊢ ([y / x]φ ↔ ((x = y ∧ φ) ∨ ∀x(x = y → φ)))
Theorem	dfsb3 2056	An alternate definition of proper substitution df-sb 1649 that uses only primitive connectives (no defined terms) on the right-hand side. (Contributed by NM, 6-Mar-2007.)
⊢ ([y / x]φ ↔ ((x = y → ¬ φ) → ∀x(x = y → φ)))
Theorem	hbsb2 2057	Bound-variable hypothesis builder for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀x x = y → ([y / x]φ → ∀x[y / x]φ))
Theorem	nfsb2 2058	Bound-variable hypothesis builder for substitution. (Contributed by Mario Carneiro, 4-Oct-2016.)
⊢ (¬ ∀x x = y → Ⅎx[y / x]φ)
Theorem	sbequi 2059	An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → ([x / z]φ → [y / z]φ))
Theorem	sbequ 2060	An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → ([x / z]φ ↔ [y / z]φ))
Theorem	drsb2 2061	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 / z]φ ↔ [y / z]φ))
Theorem	sbn 2062	Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x] ¬ φ ↔ ¬ [y / x]φ)
Theorem	sbi1 2063	Removal of implication from substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x](φ → ψ) → ([y / x]φ → [y / x]ψ))
Theorem	sbi2 2064	Introduction of implication into substitution. (Contributed by NM, 5-Aug-1993.)
⊢ (([y / x]φ → [y / x]ψ) → [y / x](φ → ψ))
Theorem	sbim 2065	Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x](φ → ψ) ↔ ([y / x]φ → [y / x]ψ))
Theorem	sbor 2066	Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.)
⊢ ([y / x](φ ∨ ψ) ↔ ([y / x]φ ∨ [y / x]ψ))
Theorem	sbrim 2067	Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxφ    ⇒   ⊢ ([y / x](φ → ψ) ↔ (φ → [y / x]ψ))
Theorem	sblim 2068	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.)
⊢ Ⅎxψ    ⇒   ⊢ ([y / x](φ → ψ) ↔ ([y / x]φ → ψ))
Theorem	sban 2069	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x](φ ∧ ψ) ↔ ([y / x]φ ∧ [y / x]ψ))
Theorem	sb3an 2070	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
⊢ ([y / x](φ ∧ ψ ∧ χ) ↔ ([y / x]φ ∧ [y / x]ψ ∧ [y / x]χ))
Theorem	sbbi 2071	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x](φ ↔ ψ) ↔ ([y / x]φ ↔ [y / x]ψ))
Theorem	sblbis 2072	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
⊢ ([y / x]φ ↔ ψ)    ⇒   ⊢ ([y / x](χ ↔ φ) ↔ ([y / x]χ ↔ ψ))
Theorem	sbrbis 2073	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([y / x]φ ↔ ψ)    ⇒   ⊢ ([y / x](φ ↔ χ) ↔ (ψ ↔ [y / x]χ))
Theorem	sbrbif 2074	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎxχ    &   ⊢ ([y / x]φ ↔ ψ)    ⇒   ⊢ ([y / x](φ ↔ χ) ↔ (ψ ↔ χ))
Theorem	spsbe 2075	A specialization theorem. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x]φ → ∃xφ)
Theorem	spsbim 2076	Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∀x(φ → ψ) → ([y / x]φ → [y / x]ψ))
Theorem	spsbbi 2077	Specialization of biconditional. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x(φ ↔ ψ) → ([y / x]φ ↔ [y / x]ψ))
Theorem	sbbid 2078	Deduction substituting both sides of a biconditional. (Contributed by NM, 5-Aug-1993.)
⊢ Ⅎxφ    &   ⊢ (φ → (ψ ↔ χ))    ⇒   ⊢ (φ → ([y / x]ψ ↔ [y / x]χ))
Theorem	sbequ8 2079	Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x]φ ↔ [y / x](x = y → φ))
Theorem	nfsb4t 2080	A variable not free remains so after substitution with a distinct variable (closed form of nfsb4 2081). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ (∀xℲzφ → (¬ ∀z z = y → Ⅎz[y / x]φ))
Theorem	nfsb4 2081	A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎzφ    ⇒   ⊢ (¬ ∀z z = y → Ⅎz[y / x]φ)
Theorem	dvelimdf 2082	Deduction form of dvelimf 1997. This version may be useful if we want to avoid ax-17 1616 and use ax-16 2144 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎzφ    &   ⊢ (φ → Ⅎxψ)    &   ⊢ (φ → Ⅎzχ)    &   ⊢ (φ → (z = y → (ψ ↔ χ)))    ⇒   ⊢ (φ → (¬ ∀x x = y → Ⅎxχ))
Theorem	sbco 2083	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([y / x][x / y]φ ↔ [y / x]φ)
Theorem	sbid2 2084	An identity law for substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎxφ    ⇒   ⊢ ([y / x][x / y]φ ↔ φ)
Theorem	sbidm 2085	An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ ([y / x][y / x]φ ↔ [y / x]φ)
Theorem	sbco2 2086	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎzφ    ⇒   ⊢ ([y / z][z / x]φ ↔ [y / x]φ)
Theorem	sbco2d 2087	A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎxφ    &   ⊢ Ⅎzφ    &   ⊢ (φ → Ⅎzψ)    ⇒   ⊢ (φ → ([y / z][z / x]ψ ↔ [y / x]ψ))
Theorem	sbco3 2088	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
⊢ ([z / y][y / x]φ ↔ [z / x][x / y]φ)
Theorem	sbcom 2089	A commutativity law for substitution. (Contributed by NM, 27-May-1997.)
⊢ ([y / z][y / x]φ ↔ [y / x][y / z]φ)
Theorem	sb5rf 2090	Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ (φ ↔ ∃y(y = x ∧ [y / x]φ))
Theorem	sb6rf 2091	Reversed substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ (φ ↔ ∀y(y = x → [y / x]φ))
Theorem	sb8 2092	Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ (∀xφ ↔ ∀y[y / x]φ)
Theorem	sb8e 2093	Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎyφ    ⇒   ⊢ (∃xφ ↔ ∃y[y / x]φ)
Theorem	sb9i 2094	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x[x / y]φ → ∀y[y / x]φ)
Theorem	sb9 2095	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.)
⊢ (∀x[x / y]φ ↔ ∀y[y / x]φ)
Theorem	ax11v 2096*	This is a version of ax-11o 2141 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See Theorem ax11v2 1992 for the rederivation of ax-11o 2141 from this theorem. (Contributed by NM, 5-Aug-1993.)
⊢ (x = y → (φ → ∀x(x = y → φ)))
Theorem	ax11vALT 2097*	Alternate proof of ax11v 2096 that avoids Theorem ax16 2045 and is proved directly from ax-11 1746 rather than via ax11o 1994. (Contributed by Jim Kingdon, 15-Dec-2017.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (x = y → (φ → ∀x(x = y → φ)))
Theorem	sb56 2098*	Two equivalent ways of expressing the proper substitution of y for x in φ, when x and y are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1649. (Contributed by NM, 14-Apr-2008.)
⊢ (∃x(x = y ∧ φ) ↔ ∀x(x = y → φ))
Theorem	sb6 2099*	Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. (Contributed by NM, 18-Aug-1993.)
⊢ ([y / x]φ ↔ ∀x(x = y → φ))
Theorem	sb5 2100*	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. (Contributed by NM, 18-Aug-1993.)
⊢ ([y / x]φ ↔ ∃x(x = y ∧ φ))