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	naecoms 2301	A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	axc11 2302	Show that ax-c11 33190 can be derived from ax-c11n 33191 in the form of axc11n 2295. Normally, axc11 2302 should be used rather than ax-c11 33190, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	hbae 2303	All variables are effectively bound in an identical variable specifier. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	nfae 2304	All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
Theorem	hbnae 2305	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.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	nfnae 2306	All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Theorem	hbnaes 2307	Rule that applies hbnae 2305 to antecedent. (Contributed by NM, 15-May-1993.)
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)
Theorem	aevlemALTOLD 2308*	Older alternate version of aevlem 1968. 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.)
⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑦 𝑦 = 𝑥)
Theorem	aevALTOLD 2309*	Older alternate proof of aev 1970. Obsolete as of 30-Mar-2021. (Contributed by NM, 8-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑤 = 𝑣)
Theorem	axc16i 2310*	Inference with axc16 2120 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16nfALT 2311*	Alternate proof of axc16nf 2122, shorter but requiring ax-11 2021 and ax-13 2234. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	dral2 2312	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 2313. (Revised by Wolf Lammen, 4-Mar-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	dral1 2313	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 2021. (Revised by Wolf Lammen, 6-Sep-2018.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	dral1ALT 2314	Alternate proof of dral1 2313, shorter but requiring ax-11 2021. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	drex1 2315	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.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	drex2 2316	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.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓))
Theorem	drnf1 2317	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
Theorem	drnf2 2318	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.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	nfald2 2319	Variation on nfald 2151 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	nfexd2 2320	Variation on nfexd 2153 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	exdistrf 2321	Distribution of existential quantifiers, with a bound-variable hypothesis saying that 𝑦 is not free in 𝜑, but 𝑥 can be free in 𝜑 (and there is no distinct variable condition on 𝑥 and 𝑦). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	dvelimf 2322	Version of dvelimv 2326 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.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dvelimdf 2323	Deduction form of dvelimf 2322. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑧𝜒)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))
Theorem	dvelimh 2324	Version of dvelim 2325 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelim 2325*	This theorem can be used to eliminate a distinct variable restriction on 𝑥 and 𝑧 and replace it with the "distinctor" ¬ ∀𝑥𝑥 = 𝑦 as an antecedent. 𝜑 normally has 𝑧 free and can be read 𝜑(𝑧), and 𝜓 substitutes 𝑦 for 𝑧 and can be read 𝜑(𝑦). We do not require that 𝑥 and 𝑦 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 ∀𝑥∀𝑧, conjoin them, and apply dvelimdf 2323. Other variants of this theorem are dvelimh 2324 (with no distinct variable restrictions) and dvelimhw 2159 (that avoids ax-13 2234). (Contributed by NM, 23-Nov-1994.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimv 2326*	Similar to dvelim 2325 with first hypothesis replaced by a distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.)
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimnf 2327*	Version of dvelim 2325 using "not free" notation. (Contributed by Mario Carneiro, 9-Oct-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dveeq2ALT 2328*	Alternate proof of dveeq2 2286, shorter but requiring ax-11 2021. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	ax12OLD 2329	Obsolete proof of ax12 2292 as of 4-Jul-2021 . Rederivation of axiom ax-12 2034 from ax12v 2035, axc11r 2175, 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.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12v2OLD 2330*	Obsolete proof of ax12v 2035 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.)
⊢ (𝑥 = 𝑧 → (𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12a2OLD 2331*	Obsolete proof of ax12v 2035 as of 24-Mar-2021. (Contributed by NM, 12-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (∀𝑧𝜑 → ∀𝑥(𝑥 = 𝑧 → 𝜑)))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	axc15OLD 2332	Obsolete proof of axc15 2291 as of 24-Mar-2021. (Contributed by NM, 3-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12b 2333	A bidirectional version of axc15 2291. (Contributed by NM, 30-Jun-2006.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	equvini 2334	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require 𝑧 to be distinct from 𝑥 and 𝑦. See equvinv 1946 for a shorter proof requiring fewer axioms when 𝑧 is required to be distinct from 𝑥 and 𝑦. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 15-Sep-2018.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦))
Theorem	equvel 2335	A variable elimination law for equality with no distinct variable requirements. Compare equvini 2334. (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.)
⊢ (∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦)
Theorem	equs5a 2336	A property related to substitution that unlike equs5 2339 does not require a distinctor antecedent. See equs5aALT 2165 for an alternate proof using ax-12 2034 but not ax13 2237. (Contributed by NM, 2-Feb-2007.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5e 2337	A property related to substitution that unlike equs5 2339 does not require a distinctor antecedent. See equs5eALT 2166 for an alternate proof using ax-12 2034 but not ax13 2237. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	equs45f 2338	Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2278 and does not require the non-freeness hypothesis. Theorem sb56 2136 replaces the non-freeness hypothesis with a dv condition and equs5 2339 replaces it with a distinctor as antecedent. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5 2339	Lemma used in proofs of substitution properties. If there is a dv condition on 𝑥, 𝑦, then sb56 2136 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2338 can be used. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb2 2340	One direction of a simplified definition of substitution. The converse requires either a dv condition (sb6 2417) or a non-freeness hypothesis (sb6f 2373). (Contributed by NM, 13-May-1993.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
Theorem	stdpc4 2341	The specialization axiom of standard predicate calculus. It states that if a statement 𝜑 holds for all 𝑥, then it also holds for the specific case of 𝑦 (properly) substituted for 𝑥. Translated to traditional notation, it can be read: "∀𝑥𝜑(𝑥) → 𝜑(𝑦), provided that 𝑦 is free for 𝑥 in 𝜑(𝑥)." Axiom 4 of [Mendelson] p. 69. See also spsbc 3415 and rspsbc 3484. (Contributed by NM, 14-May-1993.)
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑)
Theorem	2stdpc4 2342	A double specialization using explicit substitution. This is Theorem PM*11.1 in [WhiteheadRussell] p. 159. See stdpc4 2341 for the analogous single specialization. See 2sp 2044 for another double specialization. (Contributed by Andrew Salmon, 24-May-2011.) (Revised by BJ, 21-Oct-2018.)
⊢ (∀𝑥∀𝑦𝜑 → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sb3 2343	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 5-Aug-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
Theorem	sb4 2344	One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sb4a 2345	A version of sb4 2344 that doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb4b 2346	Simplified definition of substitution when variables are distinct. (Contributed by NM, 27-May-1997.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	hbsb2 2347	Bound-variable hypothesis builder for substitution. (Contributed by NM, 14-May-1993.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	nfsb2 2348	Bound-variable hypothesis builder for substitution. (Contributed by Mario Carneiro, 4-Oct-2016.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	hbsb2a 2349	Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	sb4e 2350	One direction of a simplified definition of substitution that unlike sb4 2344 doesn't require a distinctor antecedent. (Contributed by NM, 2-Feb-2007.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	hbsb2e 2351	Special case of a bound-variable hypothesis builder for substitution. (Contributed by NM, 2-Feb-2007.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑)
Theorem	hbsb3 2352	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1 2353	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	axc16ALT 2354*	Alternate proof of axc16 2120, shorter but requiring ax-10 2006, ax-11 2021, ax-13 2234 and using df-nf 1701 and df-sb 1868. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gALT 2355*	Alternate proof of axc16g 2119 that uses df-sb 1868 and requires ax-10 2006, ax-11 2021, ax-13 2234. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	equsb1 2356	Substitution applied to an atomic wff. (Contributed by NM, 10-May-1993.)
⊢ [𝑦 / 𝑥]𝑥 = 𝑦
Theorem	equsb2 2357	Substitution applied to an atomic wff. (Contributed by NM, 10-May-1993.)
⊢ [𝑦 / 𝑥]𝑦 = 𝑥
Theorem	dveel1 2358*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧))
Theorem	dveel2 2359*	Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	axc14 2360	Axiom ax-c14 33194 is redundant if we assume ax-5 1827. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'. Note that 𝑤 is a dummy variable introduced in the proof. Its purpose is to satisfy the distinct variable requirements of dveel2 2359 and ax-5 1827. 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.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	dfsb2 2361	An alternate definition of proper substitution that, like df-sb 1868, mixes free and bound variables to avoid distinct variable requirements. (Contributed by NM, 17-Feb-2005.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb3 2362	An alternate definition of proper substitution df-sb 1868 that uses only primitive connectives (no defined terms) on the right-hand side. (Contributed by NM, 6-Mar-2007.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	sbequi 2363	An equality theorem for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑))
Theorem	sbequ 2364	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.)
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	drsb1 2365	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.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑))
Theorem	drsb2 2366	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.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	sbft 2367	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.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbf 2368	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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbh 2369	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbf2 2370	Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	nfs1f 2371	If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sb6x 2372	Equivalence involving substitution for a variable not free. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb6f 2373	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2340 and does not require the non-freeness hypothesis. Theorem sb6 2417 replaces the non-freeness hypothesis with a dv condition. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5f 2374	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 1870 and does not require the non-freeness hypothesis. Theorem sb5 2418 replaces the non-freeness hypothesis with a dv condition. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sbequ5 2375	Substitution does not change an identical variable specifier. (Contributed by NM, 15-May-1993.)
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	sbequ6 2376	Substitution does not change a distinctor. (Contributed by NM, 5-Aug-1993.)
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	nfsb4t 2377	A variable not free remains so after substitution with a distinct variable (closed form of nfsb4 2378). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑))
Theorem	nfsb4 2378	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.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbn 2379	Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.)
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
Theorem	sbi1 2380	Removal of implication from substitution. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbi2 2381	Introduction of implication into substitution. (Contributed by NM, 14-May-1993.)
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓))
Theorem	spsbim 2382	Specialization of implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbim 2383	Implication inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbrim 2384	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.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblim 2385	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.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	sbor 2386	Logical OR inside and outside of substitution are equivalent. (Contributed by NM, 29-Sep-2002.)
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
Theorem	sban 2387	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓))
Theorem	sb3an 2388	Conjunction inside and outside of a substitution are equivalent. (Contributed by NM, 14-Dec-2006.)
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓 ∧ [𝑦 / 𝑥]𝜒))
Theorem	sbbi 2389	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	spsbbi 2390	Specialization of biconditional. (Contributed by NM, 2-Jun-1993.)
⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sbbid 2391	Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sblbis 2392	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓))
Theorem	sbrbis 2393	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbrbif 2394	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜒    &   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	sbequ8ALT 2395	Alternate proof of sbequ8 1872, shorter but requiring more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑))
Theorem	sbie 2396	Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbied 2397	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2396). (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	sbiedv 2398*	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2396). (Contributed by NM, 7-Jan-2017.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	sbcom3 2399	Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2021. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑)
Theorem	sbco 2400	A composition law for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.)
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑)