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