P. 20 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 1901-2000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	chvarvv 1901*	Version of chvarv 1930 with a disjoint variable condition. (Contributed by BJ, 31-May-2019.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
Theorem	exdistr 1902*	Distribution of existential quantifiers. (Contributed by NM, 9-Mar-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> E. x ( ph /\ E. y ps ) )
Theorem	exdistrv 1903*	Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1895 and 19.42v 1899. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 1925. (Contributed by BJ, 30-Sep-2022.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	19.42vv 1904*	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 1905*	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 1906*	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 1907*	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 1908*	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 1909*	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 1910*	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 1911*	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 1912*	Change bound variable. See cbvalv 1910 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( A. x ph <-> A. y ps )
Theorem	cbvexvw 1913*	Change bound variable. See cbvexv 1911 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.)
|- ( x = y -> ( ph <-> ps ) )   =>    |- ( E. x ph <-> E. y ps )
Theorem	cbval2 1914*	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 1915*	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 1916*	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 1917*	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 1918*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2010. (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 1919*	Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 2010. (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 1920*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2010. (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 1921*	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 ) )
Theorem	cbvexdva 1922*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.)
|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )   =>    |- ( ph -> ( E. x ps <-> E. y ch ) )
Theorem	cbvex4v 1923*	Rule used to change bound variables, using implicit substitition. (Contributed by NM, 26-Jul-1995.)
|- ( ( x = v /\ y = u ) -> ( ph <-> ps ) )   &    |- ( ( z = f /\ w = g ) -> ( ps <-> ch ) )   =>    |- ( E. x E. y E. z E. w ph <-> E. v E. u E. f E. g ch )
Theorem	eean 1924	Rearrange existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	eeanv 1925*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)
|- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )
Theorem	eeeanv 1926*	Rearrange existential quantifiers. (Contributed by NM, 26-Jul-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	ee4anv 1927*	Rearrange existential quantifiers. (Contributed by NM, 31-Jul-1995.)
|- ( E. x E. y E. z E. w ( ph /\ ps ) <-> ( E. x E. y ph /\ E. z E. w ps ) )
Theorem	ee8anv 1928*	Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.)
|- ( E. x E. y E. z E. w E. v E. u E. t E. s ( ph /\ ps ) <-> ( E. x E. y E. z E. w ph /\ E. v E. u E. t E. s ps ) )
Theorem	nexdv 1929*	Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> -. ps )   =>    |- ( ph -> -. E. x ps )
Theorem	chvarv 1930*	Implicit substitution of y for x into a theorem. (Contributed by NM, 20-Apr-1994.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ph   =>    |- ps
1.4.5  More substitution theorems
Theorem	hbs1 1931*	x is not free in [ y / x ] ph when x and y are distinct. (Contributed by NM, 5-Aug-1993.) (Proof by Jim Kingdon, 16-Dec-2017.) (New usage is discouraged.)
|- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	nfs1v 1932*	x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x [ y / x ] ph
Theorem	sbhb 1933*	Two ways of expressing " x is (effectively) not free in ph." (Contributed by NM, 29-May-2009.)
|- ( ( ph -> A. x ph ) <-> A. y ( ph -> [ y / x ] ph ) )
Theorem	hbsbv 1934*	This is a version of hbsb 1942 with an extra distinct variable constraint, on z and x. (Contributed by Jim Kingdon, 25-Dec-2017.)
|- ( ph -> A. z ph )   =>    |- ( [ y / x ] ph -> A. z [ y / x ] ph )
Theorem	nfsbxy 1935*	Similar to hbsb 1942 but with an extra distinct variable constraint, on x and y. (Contributed by Jim Kingdon, 19-Mar-2018.)
|- F/ z ph   =>    |- F/ z [ y / x ] ph
Theorem	nfsbxyt 1936*	Closed form of nfsbxy 1935. (Contributed by Jim Kingdon, 9-May-2018.)
|- ( A. x F/ z ph -> F/ z [ y / x ] ph )
Theorem	sbco2vlem 1937*	This is a version of sbco2 1958 where z is distinct from x and from y. It is a lemma on the way to proving sbco2v 1941 which only requires that z and x be distinct. (Contributed by Jim Kingdon, 25-Dec-2017.) Remove one disjoint variable condition. (Revised by Jim Kingdon, 3-Feb-2018.)
|- ( ph -> A. z ph )   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	sbco2vh 1938*	This is a version of sbco2 1958 where z is distinct from x. (Contributed by Jim Kingdon, 12-Feb-2018.)
|- ( ph -> A. z ph )   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	nfsb 1939*	If z is not free in ph, it is not free in [ y / x ] ph when y and z are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
|- F/ z ph   =>    |- F/ z [ y / x ] ph
Theorem	nfsbv 1940*	If z is not free in ph, it is not free in [ y / x ] ph when z is distinct from x and y. Version of nfsb 1939 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on x , y. (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.)
|- F/ z ph   =>    |- F/ z [ y / x ] ph
Theorem	sbco2v 1941*	Version of sbco2 1958 with disjoint variable conditions. (Contributed by Wolf Lammen, 29-Apr-2023.)
|- F/ z ph   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	hbsb 1942*	If z is not free in ph, it is not free in [ y / x ] ph when y and z are distinct. (Contributed by NM, 12-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
|- ( ph -> A. z ph )   =>    |- ( [ y / x ] ph -> A. z [ y / x ] ph )
Theorem	equsb3lem 1943*	Lemma for equsb3 1944. (Contributed by NM, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
|- ( [ y / x ] x = z <-> y = z )
Theorem	equsb3 1944*	Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.)
|- ( [ y / x ] x = z <-> y = z )
Theorem	sbn 1945	Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
|- ( [ y / x ] -. ph <-> -. [ y / x ] ph )
Theorem	sbim 1946	Implication inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
|- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	sbor 1947	Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
|- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )
Theorem	sban 1948	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 3-Feb-2018.)
|- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
Theorem	sbrim 1949	Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   =>    |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )
Theorem	sblim 1950	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.)
|- F/ x ps   =>    |- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> ps ) )
Theorem	sb3an 1951	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
|- ( [ y / x ] ( ph /\ ps /\ ch ) <-> ( [ y / x ] ph /\ [ y / x ] ps /\ [ y / x ] ch ) )
Theorem	sbbi 1952	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 5-Aug-1993.)
|- ( [ y / x ] ( ph <-> ps ) <-> ( [ y / x ] ph <-> [ y / x ] ps ) )
Theorem	sblbis 1953	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] ( ch <-> ph ) <-> ( [ y / x ] ch <-> ps ) )
Theorem	sbrbis 1954	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> [ y / x ] ch ) )
Theorem	sbrbif 1955	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
|- ( ch -> A. x ch )   &    |- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] ( ph <-> ch ) <-> ( ps <-> ch ) )
Theorem	sbco2yz 1956*	This is a version of sbco2 1958 where z is distinct from y. It is a lemma on the way to proving sbco2 1958 which has no distinct variable constraints. (Contributed by Jim Kingdon, 19-Mar-2018.)
|- F/ z ph   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	sbco2h 1957	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Proof rewritten by Jim Kingdon, 19-Mar-2018.)
|- ( ph -> A. z ph )   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	sbco2 1958	A composition law for substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- F/ z ph   =>    |- ( [ y / z ] [ z / x ] ph <-> [ y / x ] ph )
Theorem	sbco2d 1959	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph -> A. x ph )   &    |- ( ph -> A. z ph )   &    |- ( ph -> ( ps -> A. z ps ) )   =>    |- ( ph -> ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps ) )
Theorem	sbco2vd 1960*	Version of sbco2d 1959 with a distinct variable constraint between x and z. (Contributed by Jim Kingdon, 19-Feb-2018.)
|- ( ph -> A. x ph )   &    |- ( ph -> A. z ph )   &    |- ( ph -> ( ps -> A. z ps ) )   =>    |- ( ph -> ( [ y / z ] [ z / x ] ps <-> [ y / x ] ps ) )
Theorem	sbco 1961	A composition law for substitution. (Contributed by NM, 5-Aug-1993.)
|- ( [ y / x ] [ x / y ] ph <-> [ y / x ] ph )
Theorem	sbco3v 1962*	Version of sbco3 1967 with a distinct variable constraint between x and y. (Contributed by Jim Kingdon, 19-Feb-2018.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )
Theorem	sbcocom 1963	Relationship between composition and commutativity for substitution. (Contributed by Jim Kingdon, 28-Feb-2018.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / y ] [ z / x ] ph )
Theorem	sbcomv 1964*	Version of sbcom 1968 with a distinct variable constraint between x and z. (Contributed by Jim Kingdon, 28-Feb-2018.)
|- ( [ y / z ] [ y / x ] ph <-> [ y / x ] [ y / z ] ph )
Theorem	sbcomxyyz 1965*	Version of sbcom 1968 with distinct variable constraints between x and y, and y and z. (Contributed by Jim Kingdon, 21-Mar-2018.)
|- ( [ y / z ] [ y / x ] ph <-> [ y / x ] [ y / z ] ph )
Theorem	sbco3xzyz 1966*	Version of sbco3 1967 with distinct variable constraints between x and z, and y and z. Lemma for proving sbco3 1967. (Contributed by Jim Kingdon, 22-Mar-2018.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )
Theorem	sbco3 1967	A composition law for substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
|- ( [ z / y ] [ y / x ] ph <-> [ z / x ] [ x / y ] ph )
Theorem	sbcom 1968	A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof rewritten by Jim Kingdon, 22-Mar-2018.)
|- ( [ y / z ] [ y / x ] ph <-> [ y / x ] [ y / z ] ph )
Theorem	nfsbt 1969*	Closed form of nfsb 1939. (Contributed by Jim Kingdon, 9-May-2018.)
|- ( A. x F/ z ph -> F/ z [ y / x ] ph )
Theorem	nfsbd 1970*	Deduction version of nfsb 1939. (Contributed by NM, 15-Feb-2013.)
|- F/ x ph   &    |- ( ph -> F/ z ps )   =>    |- ( ph -> F/ z [ y / x ] ps )
Theorem	sb9v 1971*	Like sb9 1972 but with a distinct variable constraint between x and y. (Contributed by Jim Kingdon, 28-Feb-2018.)
|- ( A. x [ x / y ] ph <-> A. y [ y / x ] ph )
Theorem	sb9 1972	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|- ( A. x [ x / y ] ph <-> A. y [ y / x ] ph )
Theorem	sb9i 1973	Commutation of quantification and substitution variables. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|- ( A. x [ x / y ] ph -> A. y [ y / x ] ph )
Theorem	sbnf2 1974*	Two ways of expressing " x is (effectively) not free in ph." (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.)
|- ( F/ x ph <-> A. y A. z ( [ y / x ] ph <-> [ z / x ] ph ) )
Theorem	hbsbd 1975*	Deduction version of hbsb 1942. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.)
|- ( ph -> A. x ph )   &    |- ( ph -> A. z ph )   &    |- ( ph -> ( ps -> A. z ps ) )   =>    |- ( ph -> ( [ y / x ] ps -> A. z [ y / x ] ps ) )
Theorem	2sb5 1976*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( [ z / x ] [ w / y ] ph <-> E. x E. y ( ( x = z /\ y = w ) /\ ph ) )
Theorem	2sb6 1977*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( [ z / x ] [ w / y ] ph <-> A. x A. y ( ( x = z /\ y = w ) -> ph ) )
Theorem	sbcom2v 1978*	Lemma for proving sbcom2 1980. It is the same as sbcom2 1980 but with additional distinct variable constraints on x and y, and on w and z. (Contributed by Jim Kingdon, 19-Feb-2018.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sbcom2v2 1979*	Lemma for proving sbcom2 1980. It is the same as sbcom2v 1978 but removes the distinct variable constraint on x and y. (Contributed by Jim Kingdon, 19-Feb-2018.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sbcom2 1980*	Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.)
|- ( [ w / z ] [ y / x ] ph <-> [ y / x ] [ w / z ] ph )
Theorem	sb6a 1981*	Equivalence for substitution. (Contributed by NM, 5-Aug-1993.)
|- ( [ y / x ] ph <-> A. x ( x = y -> [ x / y ] ph ) )
Theorem	2sb5rf 1982*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( ph -> A. z ph )   &    |- ( ph -> A. w ph )   =>    |- ( ph <-> E. z E. w ( ( z = x /\ w = y ) /\ [ z / x ] [ w / y ] ph ) )
Theorem	2sb6rf 1983*	Reversed double substitution. (Contributed by NM, 3-Feb-2005.)
|- ( ph -> A. z ph )   &    |- ( ph -> A. w ph )   =>    |- ( ph <-> A. z A. w ( ( z = x /\ w = y ) -> [ z / x ] [ w / y ] ph ) )
Theorem	dfsb7 1984*	An alternate definition of proper substitution df-sb 1756. By introducing a dummy variable z in the definiens, we are able to eliminate any distinct variable restrictions among the variables x, y, and ph of the definiendum. No distinct variable conflicts arise because z effectively insulates x from y. To achieve this, we use a chain of two substitutions in the form of sb5 1880, first z for x then y for z. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1985 provides a version where ph and z don't have to be distinct. (Contributed by NM, 28-Jan-2004.)
|- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb7f 1985*	This version of dfsb7 1984 does not require that ph and z be disjoint. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1519, i.e., that does not have the concept of a variable not occurring in a formula. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( ph -> A. z ph )   =>    |- ( [ y / x ] ph <-> E. z ( z = y /\ E. x ( x = z /\ ph ) ) )
Theorem	sb7af 1986*	An alternate definition of proper substitution df-sb 1756. Similar to dfsb7a 1987 but does not require that ph and z be distinct. Similar to sb7f 1985 in that it involves a dummy variable z, but expressed in terms of A. rather than E.. (Contributed by Jim Kingdon, 5-Feb-2018.)
|- F/ z ph   =>    |- ( [ y / x ] ph <-> A. z ( z = y -> A. x ( x = z -> ph ) ) )
Theorem	dfsb7a 1987*	An alternate definition of proper substitution df-sb 1756. Similar to dfsb7 1984 in that it involves a dummy variable z, but expressed in terms of A. rather than E.. For a version which only requires F/ z ph rather than z and ph being distinct, see sb7af 1986. (Contributed by Jim Kingdon, 5-Feb-2018.)
|- ( [ y / x ] ph <-> A. z ( z = y -> A. x ( x = z -> ph ) ) )
Theorem	sb10f 1988*	Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. (Contributed by NM, 9-May-2005.)
|- ( ph -> A. x ph )   =>    |- ( [ y / z ] ph <-> E. x ( x = y /\ [ x / z ] ph ) )
Theorem	sbid2v 1989*	An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.)
|- ( [ y / x ] [ x / y ] ph <-> ph )
Theorem	sbelx 1990*	Elimination of substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> E. x ( x = y /\ [ x / y ] ph ) )
Theorem	sbel2x 1991*	Elimination of double substitution. (Contributed by NM, 5-Aug-1993.)
|- ( ph <-> E. x E. y ( ( x = z /\ y = w ) /\ [ y / w ] [ x / z ] ph ) )
Theorem	sbalyz 1992*	Move universal quantifier in and out of substitution. Identical to sbal 1993 except that it has an additional distinct variable constraint on y and z. (Contributed by Jim Kingdon, 29-Dec-2017.)
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
Theorem	sbal 1993*	Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
|- ( [ z / y ] A. x ph <-> A. x [ z / y ] ph )
Theorem	sbal1yz 1994*	Lemma for proving sbal1 1995. Same as sbal1 1995 but with an additional disjoint variable condition on y , z. (Contributed by Jim Kingdon, 23-Feb-2018.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbal1 1995*	A theorem used in elimination of disjoint variable conditions on x , y by replacing it with a distinctor -. A. x x = z. (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.)
|- ( -. A. x x = z -> ( [ z / y ] A. x ph <-> A. x [ z / y ] ph ) )
Theorem	sbexyz 1996*	Move existential quantifier in and out of substitution. Identical to sbex 1997 except that it has an additional disjoint variable condition on y , z. (Contributed by Jim Kingdon, 29-Dec-2017.)
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
Theorem	sbex 1997*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.)
|- ( [ z / y ] E. x ph <-> E. x [ z / y ] ph )
Theorem	sbalv 1998*	Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.)
|- ( [ y / x ] ph <-> ps )   =>    |- ( [ y / x ] A. z ph <-> A. z ps )
Theorem	sbco4lem 1999*	Lemma for sbco4 2000. It replaces the temporary variable v with another temporary variable w. (Contributed by Jim Kingdon, 26-Sep-2018.)
|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
Theorem	sbco4 2000*	Two ways of exchanging two variables. Both sides of the biconditional exchange x and y, either via two temporary variables u and v, or a single temporary w. (Contributed by Jim Kingdon, 25-Sep-2018.)
|- ( [ y / u ] [ x / v ] [ u / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )