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	cbv2 2401	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbv2w 2333 with disjoint variable conditions, not depending on ax-13 2370. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style, avoid ax-10 2137. (Revised by Wolf Lammen, 10-Sep-2023.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbv3h 2402	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbv3hv 2336 if possible. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbv1h 2403	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	cbv2h 2404	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 11-May-1993.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvald 2405*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2449. Usage of this theorem is discouraged because it depends on ax-13 2370. See cbvaldw 2334 for a version with 𝑥, 𝑦 disjoint, not depending on ax-13 2370. (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 2406*	Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2449. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvexdw 2335 if possible. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbvaldva 2407*	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 2370. Use the weaker cbvaldvaw 2041 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdva 2408*	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 2370. Use the weaker cbvexdvaw 2042 if possible. (Contributed by David Moews, 1-May-2017.) (New usage is discouraged.)
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbval2 2409*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbval2v 2339 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 2410*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvex2v 2340 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 2411*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbval2vw 2043 if possible. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2137. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2vv 2412*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvex2vw 2044 if possible. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2137. (Revised by Wolf Lammen, 18-Jul-2021.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	cbvex4v 2413*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker cbvex4vw 2045 if possible. (Contributed by NM, 26-Jul-1995.) (New usage is discouraged.)
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓))    &   ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒))    ⇒   ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒)
Theorem	equs4 2414	Lemma used in proofs of implicit substitution properties. The converse requires either a disjoint variable condition (sbalex 2235) or a nonfreeness hypothesis (equs45f 2457). Usage of this theorem is discouraged because it depends on ax-13 2370. See equs4v 2003 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 2415	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See equsalvw 2007 and equsalv 2258 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsex 2416. (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 2416	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See equsexvw 2008 and equsexv 2259 for versions with disjoint variable conditions proved from fewer axioms. See also the dual form equsal 2415. See equsexALT 2417 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 2417	Alternate proof of equsex 2416. This proves the result directly, instead of as a corollary of equsal 2415 via equs4 2414. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2370 is ax6e 2381. This proof mimics that of equsal 2415 (in particular, note that pm5.32i 575, exbii 1850, 19.41 2228, mpbiran 707 correspond respectively to pm5.74i 270, albii 1821, 19.23 2204, a1bi 362). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	equsalh 2418	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See equsalhw 2287 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexh 2419	An equivalence related to implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. See equsexhv 2288 for a version with a disjoint variable condition which does not require ax-13 2370. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	axc15 2420	Derivation of set.mm's original ax-c15 37424 from ax-c11n 37423 and the shorter ax-12 2171 that has replaced it. Theorem ax12 2421 shows the reverse derivation of ax-12 2171 from ax-c15 37424. Normally, axc15 2420 should be used rather than ax-c15 37424, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 26-Mar-2023.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))))
Theorem	ax12 2421	Rederivation of Axiom ax-12 2171 from ax12v 2172 (used only via sp 2176), axc11r 2364, and axc15 2420 (on top of Tarski's FOL). Since this version depends on ax-13 2370, usage of the weaker ax12v 2172, ax12w 2129, ax12i 1970 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 2422	A bidirectional version of axc15 2420. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	ax13ALT 2423	Alternate proof of ax13 2373 from FOL, sp 2176, and axc9 2380. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	axc11n 2424	Derive set.mm's original ax-c11n 37423 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 2058. Use aecom 2425 instead when this does not lengthen the proof. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2425	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 2370. (Contributed by NM, 10-May-1993.) Change to a biconditional. (Revised by BJ, 26-Sep-2019.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥)
Theorem	aecoms 2426	A commutation rule for identical variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	naecoms 2427	A commutation rule for distinct variable specifiers. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → 𝜑)
Theorem	axc11 2428	Show that ax-c11 37422 can be derived from ax-c11n 37423 in the form of axc11n 2424. Normally, axc11 2428 should be used rather than ax-c11 37422, except by theorems specifically studying the latter's properties. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker axc11v 2255 when possible. (Contributed by NM, 16-May-2008.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	hbae 2429	All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker hbaev 2062 when possible. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 21-Apr-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
Theorem	hbnae 2430	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 2370. Use the weaker hbnaev 2065 when possible. (Contributed by NM, 13-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	nfae 2431	All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
Theorem	nfnae 2432	All variables are effectively bound in a distinct variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker nfnaew 2145 when possible. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
Theorem	hbnaes 2433	Rule that applies hbnae 2430 to antecedent. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)
⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → 𝜑)
Theorem	axc16i 2434*	Inference with axc16 2252 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 2370. Use axc16 2252 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16nfALT 2435*	Alternate proof of axc16nf 2254, shorter but requiring ax-11 2154 and ax-13 2370. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	dral2 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 2370. Usage of albidv 1923 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) Allow a shortening of dral1 2437. (Revised by Wolf Lammen, 4-Mar-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧𝜑 ↔ ∀𝑧𝜓))
Theorem	dral1 2437	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 2370. Use the weaker dral1v 2365 if possible. (Contributed by NM, 24-Nov-1994.) Remove dependency on ax-11 2154. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	dral1ALT 2438	Alternate proof of dral1 2437, shorter but requiring ax-11 2154. (Contributed by NM, 24-Nov-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	drex1 2439	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 2370. Use the weaker drex1v 2367 if possible. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	drex2 2440	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 2370. Usage of exbidv 1924 is preferred, which requires fewer axioms. (Contributed by NM, 27-Feb-2005.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑧𝜑 ↔ ∃𝑧𝜓))
Theorem	drnf1 2441	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 2370. Use drnf1v 2368 instead. (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
Theorem	drnf2 2442	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 2370. Use nfbidv 1925 instead. (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑧𝜑 ↔ Ⅎ𝑧𝜓))
Theorem	nfald2 2443	Variation on nfald 2321 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 2370. Use nfald 2321 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	nfexd2 2444	Variation on nfexd 2322 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 2370. Use nfexd 2322 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ ((𝜑 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	exdistrf 2445	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 2370. Use exdistr 1958 instead. (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) → ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
Theorem	dvelimf 2446	Version of dvelimv 2450 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2447	Deduction form of dvelimf 2446. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2448	Version of dvelim 2449 without any variable restrictions. Usage of this theorem is discouraged because it depends on ax-13 2370. Check out dvelimhw 2341 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 2449*	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 2447. Other variants of this theorem are dvelimh 2448 (with no distinct variable restrictions) and dvelimhw 2341 (that avoids ax-13 2370). Usage of this theorem is discouraged because it depends on ax-13 2370. Check out dvelimhw 2341 for a version requiring fewer axioms. (Contributed by NM, 23-Nov-1994.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	dvelimv 2450*	Similar to dvelim 2449 with first hypothesis replaced by a distinct variable condition. Usage of this theorem is discouraged because it depends on ax-13 2370. Check out dvelimhw 2341 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 2451*	Version of dvelim 2449 using "not free" notation. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by Mario Carneiro, 9-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
Theorem	dveeq2ALT 2452*	Alternate proof of dveeq2 2376, shorter but requiring ax-11 2154. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	equvini 2453	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 2370. See equvinv 2032 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 2454	A variable elimination law for equality with no distinct variable requirements. Compare equvini 2453. Usage of this theorem is discouraged because it depends on ax-13 2370. Use equvelv 2034 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 2455	A property related to substitution that unlike equs5 2458 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2370. This proof uses ax12 2421, see equs5aALT 2362 for an alternative one using ax-12 2171 but not ax13 2373. Usage of the weaker equs5av 2270 is preferred, which uses ax12v2 2173, but not ax-13 2370. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5e 2456	A property related to substitution that unlike equs5 2458 does not require a distinctor antecedent. This proof uses ax12 2421, see equs5eALT 2363 for an alternative one using ax-12 2171 but not ax13 2373. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	equs45f 2457	Two ways of expressing substitution when 𝑦 is not free in 𝜑. The implication "to the left" is equs4 2414 and does not require the nonfreeness hypothesis. Theorem sbalex 2235 replaces the nonfreeness hypothesis with a disjoint variable condition and equs5 2458 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 2370. Use sbalex 2235 instead. (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5 2458	Lemma used in proofs of substitution properties. If there is a disjoint variable condition on 𝑥, 𝑦, then sbalex 2235 can be used instead; if 𝑦 is not free in 𝜑, then equs45f 2457 can be used. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 14-May-1993.) (Revised by BJ, 1-Oct-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dveel1 2459*	Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧))
Theorem	dveel2 2460*	Quantifier introduction when one pair of variables is disjoint. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Jan-2002.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
Theorem	axc14 2461	Axiom ax-c14 37426 is redundant if we assume ax-5 1913. 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 2460 and ax-5 1913. 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 2370. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 ∈ 𝑦 → ∀𝑧 𝑥 ∈ 𝑦)))
Theorem	sb6x 2462	Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 2370. Usage of sb6 2088 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 2463	Substitution does not change an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 15-May-1993.) (New usage is discouraged.)
⊢ ([𝑤 / 𝑧]∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	sbequ6 2464	Substitution does not change a distinctor. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
⊢ ([𝑤 / 𝑧] ¬ ∀𝑥 𝑥 = 𝑦 ↔ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	sb5rf 2465	Reversed substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2466	Reversed substitution. For a version requiring disjoint variables, but fewer axioms, see sb6rfv 2353. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker sb6rfv 2353 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 2467*	Alternate proof of ax12v2 2173, shorter, but depending on more axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	2ax6elem 2468	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. This theorem merges two ax6e 2381 instances ∃𝑧𝑧 = 𝑥 and ∃𝑤𝑤 = 𝑦 into a common expression. Alan Sare contributed a variant of this theorem with distinct variable conditions before, see ax6e2nd 42962. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by Wolf Lammen, 27-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑤 𝑤 = 𝑧 → ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦))
Theorem	2ax6e 2469*	We can always find values matching 𝑥 and 𝑦, as long as they are represented by distinct variables. Version of 2ax6elem 2468 with a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by Wolf Lammen, 28-Sep-2018.) (Proof shortened by Wolf Lammen, 3-Oct-2023.) (New usage is discouraged.)
⊢ ∃𝑧∃𝑤(𝑧 = 𝑥 ∧ 𝑤 = 𝑦)
Theorem	2sb5rf 2470*	Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2471*	Reversed double substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2472*	Elimination of double substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.)
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑))
Theorem	sb4b 2473	Simplified definition of substitution when variables are distinct. Version of sb6 2088 with a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 27-May-1997.) Revise df-sb 2068. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)))
Theorem	sb3b 2474	Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2475. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2475. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	sb3 2475	One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
Theorem	sb1 2476	One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2267) or a nonfreeness hypothesis (sb5f 2496). Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker sb1v 2090 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2068. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	sb2 2477	One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2088) or a nonfreeness hypothesis (sb6f 2495). Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 13-May-1993.) Revise df-sb 2068. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑)
Theorem	sb4a 2478	A version of one implication of sb4b 2473 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker sb4av 2236 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2068. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑))
Theorem	dfsb1 2479	Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2068. 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 2370. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2068. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	hbsb2 2480	Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑))
Theorem	nfsb2 2481	Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	hbsb2a 2482	Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	sb4e 2483	One direction of a simplified definition of substitution that unlike sb4b 2473 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	hbsb2e 2484	Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑)
Theorem	hbsb3 2485	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2370. Check out bj-hbsb3v 35356 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑦𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1 2486	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2370. Check out nfs1v 2153 for a version requiring fewer axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	axc16ALT 2487*	Alternate proof of axc16 2252, shorter but requiring ax-10 2137, ax-11 2154, ax-13 2370 and using df-nf 1786 and df-sb 2068. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑))
Theorem	axc16gALT 2488*	Alternate proof of axc16g 2251 that uses df-sb 2068 and requires ax-10 2137, ax-11 2154, ax-13 2370. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑))
Theorem	equsb1 2489	Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2370. Use the weaker equsb1v 2103 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ [𝑦 / 𝑥]𝑥 = 𝑦
Theorem	equsb2 2490	Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2370. Check out equsb1v 2103 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.)
⊢ [𝑦 / 𝑥]𝑦 = 𝑥
Theorem	dfsb2 2491	An alternate definition of proper substitution that, like dfsb1 2479, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	dfsb3 2492	An alternate definition of proper substitution df-sb 2068 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 2370. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	drsb1 2493	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 2370. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑))
Theorem	sb2ae 2494*	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 2370. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑))
Theorem	sb6f 2495	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2477 and does not require the nonfreeness hypothesis. Theorem sb6 2088 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 2370. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	sb5f 2496	Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2476 and does not require the nonfreeness hypothesis. Theorem sb5 2267 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 2370. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	nfsb4t 2497	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2498). Usage of this theorem is discouraged because it depends on ax-13 2370. (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 2498	A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (inference associated with nfsb4t 2497). Theorem nfsb 2521 replaces the distinctor antecedent with a disjoint variable condition. See nfsbv 2323 for a weaker version of nfsb 2521 not requiring ax-13 2370. (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 2370. Use nfsbv 2323 instead. (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbequ8 2499	Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2370. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2068. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑))
Theorem	sbie 2500	Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2308 and sbievw 2095. Usage of this theorem is discouraged because it depends on ax-13 2370. (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.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)