P. 25 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 2401-2500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cbvald 2401*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2445. Usage of this theorem is discouraged because it depends on ax-13 2366. See cbvaldw 2329 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexd 2402*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2445. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvexdw 2330 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvaldva 2403*	Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvaldvaw 2034 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdva 2404*	Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvexdvaw 2035 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2 2405*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbval2v 2334 if possible. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2 2406*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvex2v 2335 if possible. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbval2vv 2407*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbval2vw 2036 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2130. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vv 2408*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvex2vw 2037 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2130. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4v 2409*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker cbvex4vw 2038 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	equs4 2410	Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sbalex 2231) or a nonfreeness hypothesis (equs45f 2453). Usage of this theorem is discouraged because it depends on ax-13 2366. See equs4v 1996 for a weaker version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	equsal 2411	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsalvw 2000 and equsalv 2254 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2412. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsex 2412	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsexvw 2001 and equsexv 2255 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2411. See equsexALT 2413 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	equsexALT 2413	Alternate proof of equsex 2412. This proves the result directly, instead of as a corollary of equsal 2411 via equs4 2410. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2366 is ax6e 2377. This proof mimics that of equsal 2411 (in particular, note that pm5.32i 573, exbii 1843, 19.41 2224, mpbiran 707 correspond respectively to pm5.74i 270, albii 1814, 19.23 2200, a1bi 361). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	equsalh 2414	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsalhw 2281 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexh 2415	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See equsexhv 2282 for a version with a disjoint variable condition which does not require ax-13 2366. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	axc15 2416	Derivation of set.mm's original ax-c15 38600 from ax-c11n 38599 and the shorter ax-12 2167 that has replaced it. Theorem ax12 2417 shows the reverse derivation of ax-12 2167 from ax-c15 38600. Normally, axc15 2416 should be used rather than ax-c15 38600, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12 2417	Rederivation of Axiom ax-12 2167 from ax12v 2168 (used only via sp 2172), axc11r 2360, and axc15 2416 (on top of Tarski's FOL). Since this version depends on ax-13 2366, usage of the weaker ax12v 2168, ax12w 2122, ax12i 1963 are preferred. (Contributed by NM, 22-Jan-2007.) Proof uses contemporary axioms. (Revised by Wolf Lammen, 8-Aug-2020.) (Proof shortened by BJ, 4-Jul-2021.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax12b 2418	A bidirectional version of axc15 2416. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13ALT 2419	Alternate proof of ax13 2369 from FOL, sp 2172, and axc9 2376. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	axc11n 2420	Derive set.mm's original ax-c11n 38599 from others. Commutation law for identical variable specifiers. The antecedent and consequent are true when 𝑥 and 𝑦 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 𝑥 and 𝑦, then this becomes an instance of aevlem 2051. Use aecom 2421 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2366. (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.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦 𝑦 = 𝑥)
Theorem	aecom 2421	Commutation law for identical variable specifiers. Both sides of the biconditional are true when 𝑥 and 𝑦 are substituted with the same variable. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms 2422	A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	naecoms 2423	A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	axc11 2424	Show that ax-c11 38598 can be derived from ax-c11n 38599 in the form of axc11n 2420. Normally, axc11 2424 should be used rather than ax-c11 38598, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker axc11v 2251 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	hbae 2425	All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker hbaev 2055 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	hbnae 2426	All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker hbnaev 2058 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	nfae 2427	All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
Theorem	nfnae 2428	All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker nfnaew 2138 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Theorem	hbnaes 2429	Rule that applies hbnae 2426 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)
Theorem	axc16i 2430*	Inference with axc16 2248 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use axc16 2248 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16nfALT 2431*	Alternate proof of axc16nf 2250, shorter but requiring ax-11 2147 and ax-13 2366. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	dral2 2432	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2366. Usage of albidv 1916 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2433. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	dral1 2433	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker dral1v 2361 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2147. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	dral1ALT 2434	Alternate proof of dral1 2433, shorter but requiring ax-11 2147. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	drex1 2435	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker drex1v 2363 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	drex2 2436	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2366. Usage of exbidv 1917 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓))
Theorem	drnf1 2437	Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use drnf1v 2364 instead. (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
Theorem	drnf2 2438	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.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use nfbidv 1918 instead. (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	nfald2 2439	Variation on nfald 2317 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use nfald 2317 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	nfexd2 2440	Variation on nfexd 2318 which adds the hypothesis that 𝑥 and 𝑦 are distinct in the inner subproof. (Contributed by Mario Carneiro, 8-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use nfexd 2318 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	exdistrf 2441	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.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use exdistr 1951 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	dvelimf 2442	Version of dvelimv 2446 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dvelimdf 2443	Deduction form of dvelimf 2442. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑧𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    &   ⊢ (𝜑 → Ⅎ𝑧𝜒)    &   ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))
Theorem	dvelimh 2444	Version of dvelim 2445 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out dvelimhw 2336 for a version requiring fewer axioms. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelim 2445*	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 2443. Other variants of this theorem are dvelimh 2444 (with no distinct variable restrictions) and dvelimhw 2336 (that avoids ax-13 2366). Usage of this theorem is discouraged because it depends on ax-13 2366. Check out dvelimhw 2336 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimv 2446*	Similar to dvelim 2445 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out dvelimhw 2336 for a version requiring fewer axioms. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (New usage is discouraged.)
⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimnf 2447*	Version of dvelim 2445 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dveeq2ALT 2448*	Alternate proof of dveeq2 2372, shorter but requiring ax-11 2147. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	equvini 2449	A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require 𝑧 to be distinct from 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2366. See equvinv 2025 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, 16-Sep-2023.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑧 = 𝑦))
Theorem	equvel 2450	A variable elimination law for equality with no distinct variable requirements. Compare equvini 2449. Usage of this theorem is discouraged because it depends on ax-13 2366. Use equvelv 2027 when possible. (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.)
⊢ (∀𝑧(𝑧 = 𝑥 ↔ 𝑧 = 𝑦) → 𝑥 = 𝑦)
Theorem	equs5a 2451	A property related to substitution that unlike equs5 2454 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. This proof uses ax12 2417, see equs5aALT 2358 for an alternative one using ax-12 2167 but not ax13 2369. Usage of the weaker equs5av 2266 is preferred, which uses ax12v2 2169, but not ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5e 2452	A property related to substitution that unlike equs5 2454 does not require a distinctor antecedent. This proof uses ax12 2417, see equs5eALT 2359 for an alternative one using ax-12 2167 but not ax13 2369. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	equs45f 2453	Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2410 and does not require the nonfreeness hypothesis. Theorem sbalex 2231 replaces the nonfreeness hypothesis with a disjoint variable condition and equs5 2454 replaces it with a distinctor antecedent. (Contributed by NM, 25-Apr-2008.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use sbalex 2231 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5 2454	Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sbalex 2231 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2453 can be used. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dveel1 2455*	Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧))
Theorem	dveel2 2456*	Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	axc14 2457	Axiom ax-c14 38602 is redundant if we assume ax-5 1906. 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 2456 and ax-5 1906. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	sb6x 2458	Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2366. Usage of sb6 2081 is preferred, which requires fewer axioms. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sbequ5 2459	Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	sbequ6 2460	Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	sb5rf 2461	Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥]𝜑))
Theorem	sb6rf 2462	Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv 2348. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sb6rfv 2348 if possible. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))
Theorem	ax12vALT 2463*	Alternate proof of ax12v2 2169, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	2ax6elem 2464	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2377 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 44271. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦))
Theorem	2ax6e 2465*	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2464 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.)
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)
Theorem	2sb5rf 2466*	Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove distinct variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    ⇒   ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	2sb6rf 2467*	Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 3-Feb-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) Remove variable constraints. (Revised by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 13-Apr-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑))
Theorem	sbel2x 2468*	Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑))
Theorem	sb4b 2469	Simplified definition of substitution when variables are distinct. Version of sb6 2081 with a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 27-May-1997.) Revise df-sb 2061. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	sb3b 2470	Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2471. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2471. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	sb3 2471	One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
Theorem	sb1 2472	One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2263) or a nonfreeness hypothesis (sb5f 2492). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sb1v 2083 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2061. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sb2 2473	One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2081) or a nonfreeness hypothesis (sb6f 2491). Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 13-May-1993.) Revise df-sb 2061. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
Theorem	sb4a 2474	A version of one implication of sb4b 2469 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sb4av 2232 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2061. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	dfsb1 2475	Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2061. Note that it does not require dummy variables in its definiens; this is done by having 𝑥 free in the first conjunct and bound in the second. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2061. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	hbsb2 2476	Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	nfsb2 2477	Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	hbsb2a 2478	Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	sb4e 2479	One direction of a simplified definition of substitution that unlike sb4b 2469 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	hbsb2e 2480	Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑)
Theorem	hbsb3 2481	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out bj-hbsb3v 36533 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1 2482	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out nfs1v 2146 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	axc16ALT 2483*	Alternate proof of axc16 2248, shorter but requiring ax-10 2130, ax-11 2147, ax-13 2366 and using df-nf 1779 and df-sb 2061. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gALT 2484*	Alternate proof of axc16g 2247 that uses df-sb 2061 and requires ax-10 2130, ax-11 2147, ax-13 2366. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	equsb1 2485	Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker equsb1v 2096 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ [𝑦 / 𝑥]𝑥 = 𝑦
Theorem	equsb2 2486	Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2366. Check out equsb1v 2096 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ [𝑦 / 𝑥]𝑦 = 𝑥
Theorem	dfsb2 2487	An alternate definition of proper substitution that, like dfsb1 2475, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb3 2488	An alternate definition of proper substitution df-sb 2061 that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	drsb1 2489	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑))
Theorem	sb2ae 2490*	In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑))
Theorem	sb6f 2491	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2473 and does not require the nonfreeness hypothesis. Theorem sb6 2081 replaces the nonfreeness hypothesis with a disjoint variable condition on 𝑥, 𝑦 and requires fewer axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5f 2492	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2472 and does not require the nonfreeness hypothesis. Theorem sb5 2263 replaces the nonfreeness hypothesis with a disjoint variable condition on 𝑥, 𝑦 and requires fewer axioms. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	nfsb4t 2493	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2494). Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑))
Theorem	nfsb4 2494	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t 2493). Theorem nfsb 2517 replaces the distinctor antecedent with a disjoint variable condition. See nfsbv 2319 for a weaker version of nfsb 2517 not requiring ax-13 2366. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Usage of this theorem is discouraged because it depends on ax-13 2366. Use nfsbv 2319 instead. (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbequ8 2495	Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2061. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑))
Theorem	sbie 2496	Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2304 and sbievw 2088. Usage of this theorem is discouraged because it depends on ax-13 2366. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbied 2497	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2496) Usage of this theorem is discouraged because it depends on ax-13 2366. See sbiedw 2305, sbiedvw 2089 for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	sbiedv 2498*	Conversion of implicit substitution to explicit substitution (deduction version of sbie 2496). Usage of this theorem is discouraged because it depends on ax-13 2366. Use the weaker sbiedvw 2089 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	2sbiev 2499*	Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2366. See 2sbievw 2090 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓)
Theorem	sbcom3 2500	Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2366. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2091. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2147. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.)
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑)