P. 24 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2301-2400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nfeqf 2301	A variable is effectively not free in an equality if it is not either of the involved variables. F/ version of ax-c9 34175. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 6-Sep-2018.)
|- ( ( -. A. z z = x /\ -. A. z z = y ) -> F/ z x = y )
Theorem	axc9 2302	Derive set.mm's original ax-c9 34175 from the shorter ax-13 2246. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
Theorem	axc15 2303	Derivation of set.mm's original ax-c15 34174 from ax-c11n 34173 and the shorter ax-12 2047 that has replaced it. Theorem ax12 2304 shows the reverse derivation of ax-12 2047 from ax-c15 34174. Normally, axc15 2303 should be used rather than ax-c15 34174, except by theorems specifically studying the latter's properties. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 21-Apr-2018.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	ax12 2304	Rederivation of axiom ax-12 2047 from ax12v 2048 (used only via sp 2053) , axc11r 2187, and axc15 2303 (on top of Tarski's FOL). (Contributed by NM, 22-Jan-2007.) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof shortened by BJ, 4-Jul-2021.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
Theorem	ax13ALT 2305	Alternate proof of ax13 2249 from FOL, sp 2053, and axc9 2302. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. x = y -> ( y = z -> A. x y = z ) )
Theorem	axc11nlemALT 2306*	Alternate version of axc11nlemOLD2 1988 used in an older proof. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = w -> A. y y = x )
Theorem	axc11n 2307	Derive set.mm's original ax-c11n 34173 from others. 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). If a disjoint variable condition is added on x and y, then this becomes an instance of aevlem 1981. Use aecom 2311 instead when this does not lengthen the proof. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 2-Jul-2021.)
|- ( A. x x = y -> A. y y = x )
Theorem	axc11nOLD 2308	Obsolete proof of axc11n 2307 as of 2-Jul-2021. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Revised by Wolf Lammen, 30-Nov-2019.) (Proof shortened by BJ, 29-Mar-2021.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	axc11nOLDOLD 2309	Old proof of axc11n 2307. Obsolete as of 29-Mar-2021. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) Adapt to a modification of axc11nlemOLD2 1988. (Revised by Wolf Lammen, 30-Nov-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	axc11nALT 2310	Alternate proof of axc11n 2307 from axc11nlemALT 2306. (Contributed by NM, 10-May-1993.) (Revised by NM, 7-Nov-2015.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> A. y y = x )
Theorem	aecom 2311	Commutation law for identical variable specifiers. Both sides of the biconditional are true when x and y are substituted with the same variable. (Contributed by NM, 10-May-1993.) Changed to a biconditional. (Revised by BJ, 26-Sep-2019.)
|- ( A. x x = y <-> A. y y = x )
Theorem	aecoms 2312	A commutation rule for identical variable specifiers. (Contributed by NM, 10-May-1993.)
|- ( A. x x = y -> ph )   =>    |- ( A. y y = x -> ph )
Theorem	naecoms 2313	A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. x x = y -> ph )   =>    |- ( -. A. y y = x -> ph )
Theorem	axc11 2314	Show that ax-c11 34172 can be derived from ax-c11n 34173 in the form of axc11n 2307. Normally, axc11 2314 should be used rather than ax-c11 34172, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.)
|- ( A. x x = y -> ( A. x ph -> A. y ph ) )
Theorem	hbae 2315	All variables are effectively bound in an identical variable specifier. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.)
|- ( A. x x = y -> A. z A. x x = y )
Theorem	nfae 2316	All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ z A. x x = y
Theorem	hbnae 2317	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 13-May-1993.)
|- ( -. A. x x = y -> A. z -. A. x x = y )
Theorem	nfnae 2318	All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ z -. A. x x = y
Theorem	hbnaes 2319	Rule that applies hbnae 2317 to antecedent. (Contributed by NM, 15-May-1993.)
|- ( A. z -. A. x x = y -> ph )   =>    |- ( -. A. x x = y -> ph )
Theorem	aevlemALTOLD 2320*	Older alternate version of aevlem 1981. Obsolete as of 30-Mar-2021. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. z z = w -> A. y y = x )
Theorem	aevALTOLD 2321*	Older alternate proof of aev 1983. Obsolete as of 30-Mar-2021. (Contributed by NM, 8-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x x = y -> A. z w = v )
Theorem	axc16i 2322*	Inference with axc16 2135 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.)
|- ( x = z -> ( ph <-> ps ) )   &    |- ( ps -> A. x ps )   =>    |- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	axc16nfALT 2323*	Alternate proof of axc16nf 2137, shorter but requiring ax-11 2034 and ax-13 2246. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> F/ z ph )
Theorem	dral2 2324	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.) Allow a shortening of dral1 2325. (Revised by Wolf Lammen, 4-Mar-2018.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( A. z ph <-> A. z ps ) )
Theorem	dral1 2325	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.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 6-Sep-2018.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( A. x ph <-> A. y ps ) )
Theorem	dral1ALT 2326	Alternate proof of dral1 2325, shorter but requiring ax-11 2034. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( A. x ph <-> A. y ps ) )
Theorem	drex1 2327	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 -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( E. x ph <-> E. y ps ) )
Theorem	drex2 2328	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 -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( E. z ph <-> E. z ps ) )
Theorem	drnf1 2329	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( F/ x ph <-> F/ y ps ) )
Theorem	drnf2 2330	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.)
|- ( A. x x = y -> ( ph <-> ps ) )   =>    |- ( A. x x = y -> ( F/ z ph <-> F/ z ps ) )
Theorem	nfald2 2331	Variation on nfald 2165 which adds the hypothesis that x and y are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/ x A. y ps )
Theorem	nfexd2 2332	Variation on nfexd 2167 which adds the hypothesis that x and y are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.)
|- F/ y ph   &    |- ( ( ph /\ -. A. x x = y ) -> F/ x ps )   =>    |- ( ph -> F/ x E. y ps )
Theorem	exdistrf 2333	Distribution of existential quantifiers, with a bound-variable hypothesis saying that y is not free in ph, but x can be free in ph (and there is no distinct variable condition on x and y). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.)
|- ( -. A. x x = y -> F/ y ph )   =>    |- ( E. x E. y ( ph /\ ps ) -> E. x ( ph /\ E. y ps ) )
Theorem	dvelimf 2334	Version of dvelimv 2338 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
|- F/ x ph   &    |- F/ z ps   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> F/ x ps )
Theorem	dvelimdf 2335	Deduction form of dvelimf 2334. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
|- F/ x ph   &    |- F/ z ph   &    |- ( ph -> F/ x ps )   &    |- ( ph -> F/ z ch )   &    |- ( ph -> ( z = y -> ( ps <-> ch ) ) )   =>    |- ( ph -> ( -. A. x x = y -> F/ x ch ) )
Theorem	dvelimh 2336	Version of dvelim 2337 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.)
|- ( ph -> A. x ph )   &    |- ( ps -> A. z ps )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelim 2337*	This theorem can be used to eliminate a distinct variable restriction on x and z and replace it with the "distinctor" -. A. x x = y as an antecedent. ph normally has z free and can be read ph ( z ), and ps substitutes y for z and can be read ph ( y ). We do not require that x and y be distinct: if they are not, 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 A. x A. z, conjoin them, and apply dvelimdf 2335. Other variants of this theorem are dvelimh 2336 (with no distinct variable restrictions) and dvelimhw 2173 (that avoids ax-13 2246). (Contributed by NM, 23-Nov-1994.)
|- ( ph -> A. x ph )   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelimv 2338*	Similar to dvelim 2337 with first hypothesis replaced by a distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.)
|- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> ( ps -> A. x ps ) )
Theorem	dvelimnf 2339*	Version of dvelim 2337 using "not free" notation. (Contributed by Mario Carneiro, 9-Oct-2016.)
|- F/ x ph   &    |- ( z = y -> ( ph <-> ps ) )   =>    |- ( -. A. x x = y -> F/ x ps )
Theorem	dveeq2ALT 2340*	Alternate proof of dveeq2 2298, shorter but requiring ax-11 2034. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( -. A. x x = y -> ( z = y -> A. x z = y ) )
Theorem	ax12OLD 2341	Obsolete proof of ax12 2304 as of 4-Jul-2021 . Rederivation of axiom ax-12 2047 from ax12v 2048, axc11r 2187, and other axioms. (Contributed by NM, 22-Jan-2007.) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = y -> ( A. y ph -> A. x ( x = y -> ph ) ) )
Theorem	ax12v2OLD 2342*	Obsolete proof of ax12v 2048 as of 24-Mar-2021. (Contributed by NM, 12-Feb-2007.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( x = z -> ( ph -> A. x ( x = z -> ph ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	ax12a2OLD 2343*	Obsolete proof of ax12v 2048 as of 24-Mar-2021. (Contributed by NM, 12-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( x = z -> ( A. z ph -> A. x ( x = z -> ph ) ) )   =>    |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	axc15OLD 2344	Obsolete proof of axc15 2303 as of 24-Mar-2021. (Contributed by NM, 3-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Theorem	ax12b 2345	A bidirectional version of axc15 2303. (Contributed by NM, 30-Jun-2006.)
|- ( ( -. A. x x = y /\ x = y ) -> ( ph <-> A. x ( x = y -> ph ) ) )
Theorem	equvini 2346	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. See equvinv 1959 for a shorter proof requiring fewer axioms when z is required to be distinct from x and y. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 15-Sep-2018.)
|- ( x = y -> E. z ( x = z /\ z = y ) )
Theorem	equvel 2347	A variable elimination law for equality with no distinct variable requirements. Compare equvini 2346. (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.)
|- ( A. z ( z = x <-> z = y ) -> x = y )
Theorem	equs5a 2348	A property related to substitution that unlike equs5 2351 does not require a distinctor antecedent. See equs5aALT 2177 for an alternate proof using ax-12 2047 but not ax13 2249. (Contributed by NM, 2-Feb-2007.)
|- ( E. x ( x = y /\ A. y ph ) -> A. x ( x = y -> ph ) )
Theorem	equs5e 2349	A property related to substitution that unlike equs5 2351 does not require a distinctor antecedent. See equs5eALT 2178 for an alternate proof using ax-12 2047 but not ax13 2249. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.)
|- ( E. x ( x = y /\ ph ) -> A. x ( x = y -> E. y ph ) )
Theorem	equs45f 2350	Two ways of expressing substitution when y is not free in ph. The implication "to the left" is equs4 2290 and does not require the non-freeness hypothesis. Theorem sb56 2150 replaces the non-freeness hypothesis with a dv condition and equs5 2351 replaces it with a distinctor as antecedent. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ y ph   =>    |- ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) )
Theorem	equs5 2351	Lemma used in proofs of substitution properties. If there is a dv condition on x , y, then sb56 2150 can be used instead; if y is not free in ph, then equs45f 2350 can be used. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.)
|- ( -. A. x x = y -> ( E. x ( x = y /\ ph ) <-> A. x ( x = y -> ph ) ) )
Theorem	sb2 2352	One direction of a simplified definition of substitution. The converse requires either a dv condition (sb6 2429) or a non-freeness hypothesis (sb6f 2385). (Contributed by NM, 13-May-1993.)
|- ( A. x ( x = y -> ph ) -> [ y / x ] ph )
Theorem	stdpc4 2353	The specialization axiom of standard predicate calculus. It states that if a statement ph 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: " A. x ph ( x ) -> ph ( y ), provided that y is free for x in ph ( x )." Axiom 4 of [Mendelson] p. 69. See also spsbc 3448 and rspsbc 3518. (Contributed by NM, 14-May-1993.)
|- ( A. x ph -> [ y / x ] ph )
Theorem	2stdpc4 2354	A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 2353 for the analogous single specialization. See 2sp 2056 for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.) (Revised by BJ, 21-Oct-2018.)
|- ( A. x A. y ph -> [ z / x ] [ w / y ] ph )
Theorem	sb3 2355	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 2356	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993.)
|- ( -. A. x x = y -> ( [ y / x ] ph -> A. x ( x = y -> ph ) ) )
Theorem	sb4a 2357	A version of sb4 2356 that doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
|- ( [ y / x ] A. y ph -> A. x ( x = y -> ph ) )
Theorem	sb4b 2358	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	hbsb2 2359	Bound-variable hypothesis builder for substitution. (Contributed by NM, 14-May-1993.)
|- ( -. A. x x = y -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
Theorem	nfsb2 2360	Bound-variable hypothesis builder for substitution. (Contributed by Mario Carneiro, 4-Oct-2016.)
|- ( -. A. x x = y -> F/ x [ y / x ] ph )
Theorem	hbsb2a 2361	Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.)
|- ( [ y / x ] A. y ph -> A. x [ y / x ] ph )
Theorem	sb4e 2362	One direction of a simplified definition of substitution that unlike sb4 2356 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
|- ( [ y / x ] ph -> A. x ( x = y -> E. y ph ) )
Theorem	hbsb2e 2363	Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.)
|- ( [ y / x ] ph -> A. x [ y / x ] E. y ph )
Theorem	hbsb3 2364	If y is not free in ph, x is not free in [ y / x ] ph. (Contributed by NM, 14-May-1993.)
|- ( ph -> A. y ph )   =>    |- ( [ y / x ] ph -> A. x [ y / x ] ph )
Theorem	nfs1 2365	If y is not free in ph, x is not free in [ y / x ] ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ y ph   =>    |- F/ x [ y / x ] ph
Theorem	axc16ALT 2366*	Alternate proof of axc16 2135, shorter but requiring ax-10 2019, ax-11 2034, ax-13 2246 and using df-nf 1710 and df-sb 1881. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph -> A. x ph ) )
Theorem	axc16gALT 2367*	Alternate proof of axc16g 2134 that uses df-sb 1881 and requires ax-10 2019, ax-11 2034, ax-13 2246. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A. x x = y -> ( ph -> A. z ph ) )
Theorem	equsb1 2368	Substitution applied to an atomic wff. (Contributed by NM, 10-May-1993.)
|- [ y / x ] x = y
Theorem	equsb2 2369	Substitution applied to an atomic wff. (Contributed by NM, 10-May-1993.)
|- [ y / x ] y = x
Theorem	dveel1 2370*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. x x = y -> ( y e. z -> A. x y e. z ) )
Theorem	dveel2 2371*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
|- ( -. A. x x = y -> ( z e. y -> A. x z e. y ) )
Theorem	axc14 2372	Axiom ax-c14 34176 is redundant if we assume ax-5 1839. 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. Its purpose is to satisfy the distinct variable requirements of dveel2 2371 and ax-5 1839. 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.)
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )
Theorem	dfsb2 2373	An alternate definition of proper substitution that, like df-sb 1881, mixes free and bound variables to avoid distinct variable requirements. (Contributed by NM, 17-Feb-2005.)
|- ( [ y / x ] ph <-> ( ( x = y /\ ph ) \/ A. x ( x = y -> ph ) ) )
Theorem	dfsb3 2374	An alternate definition of proper substitution df-sb 1881 that uses only primitive connectives (no defined terms) on the right-hand side. (Contributed by NM, 6-Mar-2007.)
|- ( [ y / x ] ph <-> ( ( x = y -> -. ph ) -> A. x ( x = y -> ph ) ) )
Theorem	sbequi 2375	An equality theorem for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.)
|- ( x = y -> ( [ x / z ] ph -> [ y / z ] ph ) )
Theorem	sbequ 2376	An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.)
|- ( x = y -> ( [ x / z ] ph <-> [ y / z ] ph ) )
Theorem	drsb1 2377	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, 2-Jun-1993.)
|- ( A. x x = y -> ( [ z / x ] ph <-> [ z / y ] ph ) )
Theorem	drsb2 2378	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	sbft 2379	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	sbf 2380	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ x ph   =>    |- ( [ y / x ] ph <-> ph )
Theorem	sbh 2381	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.)
|- ( ph -> A. x ph )   =>    |- ( [ y / x ] ph <-> ph )
Theorem	sbf2 2382	Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
|- ( [ y / x ] A. x ph <-> A. x ph )
Theorem	nfs1f 2383	If x is not free in ph, it is not free in [ y / x ] ph. (Contributed by Mario Carneiro, 11-Aug-2016.)
|- F/ x ph   =>    |- F/ x [ y / x ] ph
Theorem	sb6x 2384	Equivalence involving substitution for a variable not free. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ x ph   =>    |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
Theorem	sb6f 2385	Equivalence for substitution when y is not free in ph. The implication "to the left" is sb2 2352 and does not require the non-freeness hypothesis. Theorem sb6 2429 replaces the non-freeness hypothesis with a dv condition. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ y ph   =>    |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
Theorem	sb5f 2386	Equivalence for substitution when y is not free in ph. The implication "to the right" is sb1 1883 and does not require the non-freeness hypothesis. Theorem sb5 2430 replaces the non-freeness hypothesis with a dv condition. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ y ph   =>    |- ( [ y / x ] ph <-> E. x ( x = y /\ ph ) )
Theorem	sbequ5 2387	Substitution does not change an identical variable specifier. (Contributed by NM, 15-May-1993.)
|- ( [ w / z ] A. x x = y <-> A. x x = y )
Theorem	sbequ6 2388	Substitution does not change a distinctor. (Contributed by NM, 5-Aug-1993.)
|- ( [ w / z ] -. A. x x = y <-> -. A. x x = y )
Theorem	nfsb4t 2389	A variable not free remains so after substitution with a distinct variable (closed form of nfsb4 2390). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
|- ( A. x F/ z ph -> ( -. A. z z = y -> F/ z [ y / x ] ph ) )
Theorem	nfsb4 2390	A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ z ph   =>    |- ( -. A. z z = y -> F/ z [ y / x ] ph )
Theorem	sbn 2391	Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.)
|- ( [ y / x ] -. ph <-> -. [ y / x ] ph )
Theorem	sbi1 2392	Removal of implication from substitution. (Contributed by NM, 14-May-1993.)
|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	sbi2 2393	Introduction of implication into substitution. (Contributed by NM, 14-May-1993.)
|- ( ( [ y / x ] ph -> [ y / x ] ps ) -> [ y / x ] ( ph -> ps ) )
Theorem	spsbim 2394	Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
|- ( A. x ( ph -> ps ) -> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	sbim 2395	Implication inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.)
|- ( [ y / x ] ( ph -> ps ) <-> ( [ y / x ] ph -> [ y / x ] ps ) )
Theorem	sbrim 2396	Substitution with a variable not free in antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
|- F/ x ph   =>    |- ( [ y / x ] ( ph -> ps ) <-> ( ph -> [ y / x ] ps ) )
Theorem	sblim 2397	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	sbor 2398	Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.)
|- ( [ y / x ] ( ph \/ ps ) <-> ( [ y / x ] ph \/ [ y / x ] ps ) )
Theorem	sban 2399	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
|- ( [ y / x ] ( ph /\ ps ) <-> ( [ y / x ] ph /\ [ y / x ] ps ) )
Theorem	sb3an 2400	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 ) )