P. 19 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1801-1900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	equs5 1801	Lemma used in proofs of substitution properties. (Contributed by NM, 5-Aug-1993.)
|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) -> A. x ( x = y -> ph ) ) )
Theorem	equs5or 1802	Lemma used in proofs of substitution properties. Like equs5 1801 but, in intuitionistic logic, replacing negation and implication with disjunction makes this a stronger result. (Contributed by Jim Kingdon, 2-Feb-2018.)
|- ( A. x x = y \/ ( E. x ( x = y /\ ph ) -> A. x ( x = y -> ph ) ) )
Theorem	sb3 1803	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) -> [ y / x ] ph ) )
Theorem	sb4 1804	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
|- ( -. A. x x = y -> ( [ y / x ] ph -> A. x ( x = y -> ph ) ) )
Theorem	sb4or 1805	One direction of a simplified definition of substitution when variables are distinct. Similar to sb4 1804 but stronger in intuitionistic logic. (Contributed by Jim Kingdon, 2-Feb-2018.)
|- ( A. x x = y \/ A. x ( [ y / x ] ph -> A. x ( x = y -> ph ) ) )
Theorem	sb4b 1806	Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.)
|- ( -. A. x x = y -> ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) )
Theorem	sb4bor 1807	Simplified definition of substitution when variables are distinct, expressed via disjunction. (Contributed by Jim Kingdon, 18-Mar-2018.)
|- ( A. x x = y \/ A. x ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) )
Theorem	hbsb2 1808	Bound-variable hypothesis builder for substitution. (Contributed by NM, 5-Aug-1993.)
|- ( -. A. x x = y -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
Theorem	nfsb2or 1809	Bound-variable hypothesis builder for substitution. Similar to hbsb2 1808 but in intuitionistic logic a disjunction is stronger than an implication. (Contributed by Jim Kingdon, 2-Feb-2018.)
|- ( A. x x = y \/ F/ x [ y / x ] ph )
Theorem	sbequilem 1810	Propositional logic lemma used in the sbequi 1811 proof. (Contributed by Jim Kingdon, 1-Feb-2018.)
|- ( ph \/ ( ps -> ( ch -> th ) ) )   &    |- ( ta \/ ( ps -> ( th -> et ) ) )   =>    |- ( ph \/ ( ta \/ ( ps -> ( ch -> et ) ) ) )
Theorem	sbequi 1811	An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof modified by Jim Kingdon, 1-Feb-2018.)
|- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
Theorem	sbequ 1812	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 ] ph <-> [ y / z ] ph ) )
Theorem	drsb2 1813	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.)
|- ( A. x x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )
Theorem	spsbe 1814	A specialization theorem, mostly the same as Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 29-Dec-2017.)
|- ( [ y / x ] ph -> E. x ph )
Theorem	spsbim 1815	Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	spsbbi 1816	Specialization of biconditional. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
|- ( A. x ( ph <-> ps ) -> ( [ y / x ] ph <-> [ y / x ] ps ) )
Theorem	sbbidh 1817	Deduction substituting both sides of a biconditional. New proofs should use sbbid 1818 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
|- ( ph -> A. x ph )   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [ y / x ] ps <-> [ y / x ] ch ) )
Theorem	sbbid 1818	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.)
|- F/ x ph   &    |- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( [ y / x ] ps <-> [ y / x ] ch ) )
Theorem	sbequ8 1819	Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) (Proof revised by Jim Kingdon, 20-Jan-2018.)
|- ( [ y / x ] ph <-> [ y / x ] ( x = y -> ph ) )
Theorem	sbft 1820	Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.)
|- ( F/ x ph -> ( [ y / x ] ph <-> ph ) )
Theorem	sbid2h 1821	An identity law for substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( [ y / x ] [ x / y ] ph <-> ph )
Theorem	sbid2 1822	An identity law for substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ x ph   =>    |- ( [ y / x ] [ x / y ] ph <-> ph )
Theorem	sbidm 1823	An idempotent law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 21-Jan-2018.)
|- ( [ y / x ] [ y / x ] ph <-> [ y / x ] ph )
Theorem	sb5rf 1824	Reversed substitution. (Contributed by NM, 3-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A. y ph )   =>    |- ( ph <-> E. y ( y = x /\ [ y / x ] ph ) )
Theorem	sb6rf 1825	Reversed substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A. y ph )   =>    |- ( ph <-> A. y ( y = x -> [ y / x ] ph ) )
Theorem	sb8h 1826	Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
|- ( ph -> A. y ph )   =>    |- ( A. x ph <-> A. y [ y / x ] ph )
Theorem	sb8eh 1827	Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 15-Jan-2018.)
|- ( ph -> A. y ph )   =>    |- ( E. x ph <-> E. y [ y / x ] ph )
Theorem	sb8 1828	Substitution of variable in universal quantifier. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
|- F/ y ph   =>    |- ( A. x ph <-> A. y [ y / x ] ph )
Theorem	sb8e 1829	Substitution of variable in existential quantifier. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.)
|- F/ y ph   =>    |- ( E. x ph <-> E. y [ y / x ] ph )
1.4.4  Predicate calculus with distinct variables (cont.)
Theorem	ax16i 1830*	Inference with ax-16 1786 as its conclusion, that doesn't require ax-10 1483, ax-11 1484, or ax-12 1489 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. (Contributed by NM, 20-May-2008.)
|- ( x = z -> ( ph <-> ps ) )   &    |- ( ps -> A. x ps )   =>    |- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	ax16ALT 1831*	Version of ax16 1785 that doesn't require ax-10 1483 or ax-12 1489 for its proof. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	spv 1832*	Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	spimev 1833*	Distinct-variable version of spime 1719. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( ph -> ps ) )   =>    |- ( ph -> E. x ps )
Theorem	speiv 1834*	Inference from existential specialization, using implicit substitition. (Contributed by NM, 19-Aug-1993.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ps   =>    |- E. x ph
Theorem	equvin 1835*	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 5-Aug-1993.)
|- ( x = y <-> E. z ( x = z /\ z = y ) )
Theorem	a16g 1836*	A generalization of axiom ax-16 1786. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	a16gb 1837*	A generalization of axiom ax-16 1786. (Contributed by NM, 5-Aug-1993.)
|- ( A. x x = y -> ( ph <-> A. z ph ) )
Theorem	a16nf 1838*	If there is only one element in the universe, then everything satisfies F/. (Contributed by Mario Carneiro, 7-Oct-2016.)
|- ( A. x x = y -> F/ z ph )
Theorem	2albidv 1839*	Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 4-Mar-1997.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x A. y ps <-> A. x A. y ch ) )
Theorem	2exbidv 1840*	Formula-building rule for 2 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x E. y ps <-> E. x E. y ch ) )
Theorem	3exbidv 1841*	Formula-building rule for 3 existential quantifiers (deduction form). (Contributed by NM, 1-May-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x E. y E. z ps <-> E. x E. y E. z ch ) )
Theorem	4exbidv 1842*	Formula-building rule for 4 existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995.)
|- ( ph -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x E. y E. z E. w ps <-> E. x E. y E. z E. w ch ) )
Theorem	19.9v 1843*	Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 21-May-2007.)
|- ( E. x ph <-> ph )
Theorem	exlimdd 1844	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.)
|- F/ x ph   &    |- F/ x ch   &    |- ( ph -> E. x ps )   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ( ph -> ch )
Theorem	19.21v 1845*	Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as ( ph -> A. x ph ) in 19.21 1562 via the use of distinct variable conditions combined with ax-17 1506. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g., euf 2004 derived from df-eu 2002. The "f" stands for "not free in" which is less restrictive than "does not occur in". (Contributed by NM, 5-Aug-1993.)
|- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
Theorem	alrimiv 1846*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> ps )   =>    |- ( ph -> A. x ps )
Theorem	alrimivv 1847*	Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
|- ( ph -> ps )   =>    |- ( ph -> A. x A. y ps )
Theorem	alrimdv 1848*	Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 10-Feb-1997.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( ps -> A. x ch ) )
Theorem	nfdv 1849*	Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- ( ph -> ( ps -> A. x ps ) )   =>    |- ( ph -> F/ x ps )
Theorem	2ax17 1850*	Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
|- ( ph -> A. x A. y ph )
Theorem	alimdv 1851*	Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x ps -> A. x ch ) )
Theorem	eximdv 1852*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x ps -> E. x ch ) )
Theorem	2alimdv 1853*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-2004.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( A. x A. y ps -> A. x A. y ch ) )
Theorem	2eximdv 1854*	Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 3-Aug-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x E. y ps -> E. x E. y ch ) )
Theorem	19.23v 1855*	Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)
|- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )
Theorem	19.23vv 1856*	Theorem 19.23 of [Margaris] p. 90 extended to two variables. (Contributed by NM, 10-Aug-2004.)
|- ( A. x A. y ( ph -> ps ) <-> ( E. x E. y ph -> ps ) )
Theorem	sb56 1857*	Two equivalent ways of expressing the proper substitution of y for x in ph, when x and y are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1736. (Contributed by NM, 14-Apr-2008.)
|- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
Theorem	sb6 1858*	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.) (Revised by NM, 14-Apr-2008.)
|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
Theorem	sb5 1859*	Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. (Contributed by NM, 18-Aug-1993.) (Revised by NM, 14-Apr-2008.)
|- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
Theorem	sbnv 1860*	Version of sbn 1925 where x and y are distinct. (Contributed by Jim Kingdon, 18-Dec-2017.)
|- ( [ y / x ] -. ph <-> -. [ y / x ] ph )
Theorem	sbanv 1861*	Version of sban 1928 where x and y are distinct. (Contributed by Jim Kingdon, 24-Dec-2017.)
|- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
Theorem	sborv 1862*	Version of sbor 1927 where x and y are distinct. (Contributed by Jim Kingdon, 3-Feb-2018.)
|- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )
Theorem	sbi1v 1863*	Forward direction of sbimv 1865. (Contributed by Jim Kingdon, 25-Dec-2017.)
|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	sbi2v 1864*	Reverse direction of sbimv 1865. (Contributed by Jim Kingdon, 18-Jan-2018.)
|- ( ( [ y / x ] ph -> [ y / x ] ps ) -> [ y / x ] ( ph -> ps ) )
Theorem	sbimv 1865*	Intuitionistic proof of sbim 1926 where x and y are distinct. (Contributed by Jim Kingdon, 18-Jan-2018.)
|- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	sblimv 1866*	Version of sblim 1930 where x and y are distinct. (Contributed by Jim Kingdon, 19-Jan-2018.)
|- ( ps -> A. x ps )   =>    |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) )
Theorem	pm11.53 1867*	Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
|- ( A. x A. y ( ph -> ps ) <-> ( E. x ph -> A. y ps ) )
Theorem	exlimivv 1868*	Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
|- ( ph -> ps )   =>    |- ( E. x E. y ph -> ps )
Theorem	exlimdvv 1869*	Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
|- ( ph -> ( ps -> ch ) )   =>    |- ( ph -> ( E. x E. y ps -> ch ) )
Theorem	exlimddv 1870*	Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
|- ( ph -> E. x ps )   &    |- ( ( ph /\ ps ) -> ch )   =>    |- ( ph -> ch )
Theorem	19.27v 1871*	Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 3-Jun-2004.)
|- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) )
Theorem	19.28v 1872*	Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 25-Mar-2004.)
|- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) )
Theorem	19.36aiv 1873*	Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- E. x ( ph -> ps )   =>    |- ( A. x ph -> ps )
Theorem	19.41v 1874*	Special case of Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) )
Theorem	19.41vv 1875*	Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 30-Apr-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x E. y ph /\ ps ) )
Theorem	19.41vvv 1876*	Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 30-Apr-1995.)
|- ( E. x E. y E. z ( ph /\ ps ) <-> ( E. x E. y E. z ph /\ ps ) )
Theorem	19.41vvvv 1877*	Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
|- ( E. w E. x E. y E. z ( ph /\ ps ) <-> ( E. w E. x E. y E. z ph /\ ps ) )
Theorem	19.42v 1878*	Special case of Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
|- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) )
Theorem	spvv 1879*	Version of spv 1832 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph -> ps )
Theorem	chvarvv 1880*	Version of chvarv 1909 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	exdistr 1881*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
Theorem	exdistrv 1882*	Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1874 and 19.42v 1878. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 1904. (Contributed by BJ, 30-Sep-2022.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	19.42vv 1883*	Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. (Contributed by NM, 16-Mar-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> ( ph /\ E. x E. y ps ) )
Theorem	19.42vvv 1884*	Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. (Contributed by NM, 21-Sep-2011.)
|- ( E. x E. y E. z ( ph /\ ps ) <-> ( ph /\ E. x E. y E. z ps ) )
Theorem	19.42vvvv 1885*	Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ( E. w E. x E. y E. z ( ph /\ ps ) <-> ( ph /\ E. w E. x E. y E. z ps ) )
Theorem	exdistr2 1886*	Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.)
|- ( E. x E. y E. z ( ph /\ ps ) <-> E. x ( ph /\ E. y E. z ps ) )
Theorem	3exdistr 1887*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( E. x E. y E. z ( ph /\ ps /\ ch ) <-> E. x ( ph /\ E. y ( ps /\ E. z ch ) ) )
Theorem	4exdistr 1888*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y E. z E. w ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> E. x ( ph /\ E. y ( ps /\ E. z ( ch /\ E. w th ) ) ) )
Theorem	cbvalv 1889*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvexv 1890*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	cbvalvw 1891*	Change bound variable. See cbvalv 1889 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvexvw 1892*	Change bound variable. See cbvexv 1890 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	cbval2 1893*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	cbvex2 1894*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ z ph   &    |- F/ w ph   &    |- F/ x ps   &    |- F/ y ps   &    |- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	cbval2v 1895*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( A. x A. y ph <-> A. z A. w ps )
Theorem	cbvex2v 1896*	Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.)
|- ( ( x = z /\ y = w ) -> ( ph <-> ps ) )   =>    |- ( E. x E. y ph <-> E. z E. w ps )
Theorem	cbvald 1897*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 1992. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)
|- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )
Theorem	cbvexdh 1898*	Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1992. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 30-Dec-2017.)
|- ( ph -> A. y ph )   &    |- ( ph -> ( ps -> A. y ps ) )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	cbvexd 1899*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 1992. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof rewritten by Jim Kingdon, 10-Jun-2018.)
|- F/ y ph   &    |- ( ph -> F/ y ps )   &    |- ( ph -> ( x = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	cbvaldva 1900*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( A. x ps <-> A. y ch ) )