P. 24 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	hb3an 2301	If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	sbi2 2302	Introduction of implication into substitution. (Contributed by NM, 14-May-1993.)
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓))
Theorem	sbim 2303	Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbrim 2304	Substitution in an implication with a variable not free in the antecedent affects only the consequent. See sbrimv 2305 for a version with disjoint variables not requiring ax-10 2139. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbrimv 2305*	Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2304 not depending on ax-10 2139, but with disjoint variables. (Contributed by Wolf Lammen, 28-Jan-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblim 2306	Substitution in an implication with a variable not free in the consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜓    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))
Theorem	sbor 2307	Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002.)
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
Theorem	sbbi 2308	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sblbis 2309	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓))
Theorem	sbrbis 2310	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbrbif 2311	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜒    &   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	sbiev 2312*	Conversion of implicit substitution to explicit substitution. Version of sbie 2506 with a disjoint variable condition, not requiring ax-13 2372. See sbievw 2097 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 18-Jan-2023.) Remove dependence on ax-10 2139 and shorten proof. (Revised by BJ, 18-Jul-2023.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbiedw 2313*	Conversion of implicit substitution to explicit substitution (deduction version of sbiev 2312). Version of sbied 2507 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Gino Giotto, 10-Jan-2024.) Avoid ax-10 2139. (Revised by Wolf Lammen, 28-Jan-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	sbiedwOLD 2314*	Obsolete version of sbiedw 2313 as of 28-Jan-2024. (Contributed by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	axc7 2315	Show that the original axiom ax-c7 36826 can be derived from ax-10 2139 (hbn1 2140) , sp 2178 and propositional calculus. See ax10fromc7 36836 for the rederivation of ax-10 2139 from ax-c7 36826. Normally, axc7 2315 should be used rather than ax-c7 36826, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc7e 2316	Abbreviated version of axc7 2315 using the existential quantifier. Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
⊢ (∃𝑥∀𝑥𝜑 → 𝜑)
Theorem	modal-b 2317	The analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.)
⊢ (𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑)
Theorem	19.9ht 2318	A closed version of 19.9h 2286. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑))
Theorem	axc4 2319	Show that the original axiom ax-c4 36825 can be derived from ax-4 1813 (alim 1814), ax-10 2139 (hbn1 2140), sp 2178 and propositional calculus. See ax4fromc4 36835 for the rederivation of ax-4 1813 from ax-c4 36825. Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114. (Contributed by NM, 21-May-2008.) (Proof modification is discouraged.)
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))
Theorem	axc4i 2320	Inference version of axc4 2319. (Contributed by NM, 3-Jan-1993.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	nfal 2321	If 𝑥 is not free in 𝜑, then it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfex 2322	If 𝑥 is not free in 𝜑, then it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex 2322, hbex 2323. (Revised by Wolf Lammen, 16-Oct-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	hbex 2323	If 𝑥 is not free in 𝜑, then it is not free in ∃𝑦𝜑. (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex 2322, hbex 2323. (Revised by Wolf Lammen, 16-Oct-2021.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)
Theorem	nfnf 2324	If 𝑥 is not free in 𝜑, then it is not free in Ⅎ𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥Ⅎ𝑦𝜑
Theorem	19.12 2325	Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 2347 and r19.12sn 4653. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	nfald 2326	Deduction form of nfal 2321. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	nfexd 2327	If 𝑥 is not free in 𝜓, then it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	nfsbv 2328*	If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2527 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2372. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof shortened by Wolf Lammen, 25-Oct-2024.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	nfsbvOLD 2329*	Obsolete version of nfsbv 2328 as of 25-Oct-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on 𝑥, 𝑦. (Revised by Steven Nguyen, 13-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑
Theorem	hbsbwOLD 2330*	Obsolete version of hbsbw 2171 as of 23-May-2024. (Contributed by NM, 12-Aug-1993.) (Revised by Gino Giotto, 10-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑧𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)
Theorem	sbco2v 2331*	A composition law for substitution. Version of sbco2 2515 with disjoint variable conditions but not requiring ax-13 2372. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 29-Apr-2023.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	aaan 2332	Distribute universal quantifiers. (Contributed by NM, 12-Aug-1993.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
Theorem	eeor 2333	Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
Theorem	cbv3v 2334*	Rule used to change bound variables, using implicit substitution. Version of cbv3 2397 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbv1v 2335*	Rule used to change bound variables, using implicit substitution. Version of cbv1 2402 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 16-Jun-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	cbv2w 2336*	Rule used to change bound variables, using implicit substitution. Version of cbv2 2403 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 5-Aug-1993.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvaldw 2337*	Deduction used to change bound variables, using implicit substitution. Version of cbvald 2407 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 2-Jan-2002.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdw 2338*	Deduction used to change bound variables, using implicit substitution. Version of cbvexd 2408 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 2-Jan-2002.) (Revised by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbv3hv 2339*	Rule used to change bound variables, using implicit substitution. Version of cbv3h 2404 with a disjoint variable condition on 𝑥, 𝑦, which does not require ax-13 2372. Was used in a proof of axc11n 2426 (but of independent interest). (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 29-Nov-2020.) (Proof shortened by BJ, 30-Nov-2020.)
⊢ (𝜑 → ∀𝑦𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbvalv1 2340*	Rule used to change bound variables, using implicit substitution. Version of cbval 2398 with a disjoint variable condition, which does not require ax-13 2372. See cbvalvw 2040 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2400 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexv1 2341*	Rule used to change bound variables, using implicit substitution. Version of cbvex 2399 with a disjoint variable condition, which does not require ax-13 2372. See cbvexvw 2041 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2401 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbval2v 2342*	Rule used to change bound variables, using implicit substitution. Version of cbval2 2411 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 22-Dec-2003.) (Revised by BJ, 16-Jun-2019.) (Proof shortened by Gino Giotto, 10-Jan-2024.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbval2vOLD 2343*	Obsolete version of cbval2v 2342 as of 14-Jan-2024. (Contributed by BJ, 16-Jan-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2v 2344*	Rule used to change bound variables, using implicit substitution. Version of cbvex2 2412 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 14-Sep-2003.) (Revised by BJ, 16-Jun-2019.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	dvelimhw 2345*	Proof of dvelimh 2450 without using ax-13 2372 but with additional distinct variable conditions. (Contributed by NM, 1-Oct-2002.) (Revised by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 23-Dec-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑧𝜓)    &   ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))    ⇒   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))
Theorem	pm11.53 2346*	Theorem *11.53 in [WhiteheadRussell] p. 164. See pm11.53v 1948 for a version requiring fewer axioms. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))
Theorem	19.12vv 2347*	Special case of 19.12 2325 where its converse holds. See 19.12vvv 1993 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 18-Jul-2001.) (Revised by Andrew Salmon, 11-Jul-2011.)
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓))
Theorem	eean 2348	Distribute existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeanv 2349*	Distribute a pair of existential quantifiers over a conjunction. Combination of 19.41v 1954 and 19.42v 1958. For a version requiring fewer axioms but with additional disjoint variable conditions, see exdistrv 1960. (Contributed by NM, 26-Jul-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeeanv 2350*	Distribute three existential quantifiers over a conjunction. (Contributed by NM, 26-Jul-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) Reduce distinct variable restrictions. (Revised by Wolf Lammen, 20-Jan-2018.)
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒))
Theorem	ee4anv 2351*	Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv 1961. (Contributed by NM, 31-Jul-1995.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓))
Theorem	sb8v 2352*	Substitution of variable in universal quantifier. Version of sb8 2521 with a disjoint variable condition, not requiring ax-13 2372. (Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8ev 2353*	Substitution of variable in existential quantifier. Version of sb8e 2522 with a disjoint variable condition, not requiring ax-13 2372. (Contributed by NM, 12-Aug-1993.) (Revised by Wolf Lammen, 19-Jan-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
Theorem	2sb8ev 2354*	An equivalent expression for double existence. Version of 2sb8e 2535 with more disjoint variable conditions, not requiring ax-13 2372. (Contributed by Wolf Lammen, 28-Jan-2023.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sb6rfv 2355*	Reversed substitution. Version of sb6rf 2468 requiring disjoint variables, but fewer axioms. (Contributed by NM, 1-Aug-1993.) (Revised by Wolf Lammen, 7-Feb-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))
Theorem	sbnf2 2356*	Two ways of expressing "𝑥 is (effectively) not free in 𝜑". (Contributed by Gérard Lang, 14-Nov-2013.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Sep-2018.) Avoid ax-13 2372. (Revised by Wolf Lammen, 30-Jan-2023.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
Theorem	exsb 2357*	An equivalent expression for existence. One direction (exsbim 2006) needs fewer axioms. (Contributed by NM, 2-Feb-2005.) Avoid ax-13 2372. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2exsb 2358*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	sbbib 2359*	Reversal of substitution. (Contributed by AV, 6-Aug-2023.) (Proof shortened by Wolf Lammen, 4-Sep-2023.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
Theorem	sbbibvv 2360*	Reversal of substitution. (Contributed by AV, 6-Aug-2023.)
⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
Theorem	sbievg 2361*	Substitution applied to expressions linked by implicit substitution. The proof was part of a former cbvabw 2813 version. (Contributed by GG and WL, 26-Oct-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
Theorem	cleljustALT 2362*	Alternate proof of cleljust 2117. It is kept here and should not be modified because it is referenced on the Metamath Proof Explorer Home Page (mmset.html) as an example of how disjoint variable conditions are inherited by substitutions. (Contributed by NM, 28-Jan-2004.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦))
Theorem	cleljustALT2 2363*	Alternate proof of cleljust 2117. Compared with cleljustALT 2362, it uses nfv 1918 followed by equsexv 2263 instead of ax-5 1914 followed by equsexhv 2292, so it uses the idiom Ⅎ𝑥𝜑 instead of 𝜑 → ∀𝑥𝜑 to express nonfreeness. This style is generally preferred for later theorems. (Contributed by NM, 28-Jan-2004.) (Revised by Mario Carneiro, 21-Dec-2016.) (Revised by BJ, 29-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 ∈ 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝑦))
Theorem	equs5aALT 2364	Alternate proof of equs5a 2457. Uses ax-12 2173 but not ax-13 2372. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5eALT 2365	Alternate proof of equs5e 2458. Uses ax-12 2173 but not ax-13 2372. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	axc11r 2366	Same as axc11 2430 but with reversed antecedent. Note the use of ax-12 2173 (and not merely ax12v 2174 as in axc11rv 2260). This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2057 and aecom 2427, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations. As of 2024, it is used in conjunction with ax-13 2372 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	dral1v 2367*	Formula-building lemma for use with the Distinctor Reduction Theorem. Version of dral1 2439 with a disjoint variable condition, which does not require ax-13 2372. Remark: the corresponding versions for dral2 2438 and drex2 2442 are instances of albidv 1924 and exbidv 1925 respectively. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v 2174. (Revised by Wolf Lammen, 30-Mar-2024.) Avoid ax-10 2139. (Revised by Gino Giotto, 18-Nov-2024.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	dral1vOLD 2368*	Obsolete version of dral1v 2367 as of 18-Nov-2024. (Contributed by NM, 24-Nov-1994.) (Revised by BJ, 17-Jun-2019.) Base the proof on ax12v 2174. (Revised by Wolf Lammen, 30-Mar-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 ↔ ∀𝑦𝜓))
Theorem	drex1v 2369*	Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drex1 2441 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 27-Feb-2005.) (Revised by BJ, 17-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥𝜑 ↔ ∃𝑦𝜓))
Theorem	drnf1v 2370*	Formula-building lemma for use with the Distinctor Reduction Theorem. Version of drnf1 2443 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) Avoid ax-10 2139. (Revised by Gino Giotto, 18-Nov-2024.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
Theorem	drnf1vOLD 2371*	Obsolete version of drnf1v 2370 as of 18-Nov-2024. (Contributed by Mario Carneiro, 4-Oct-2016.) (Revised by BJ, 17-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥 𝑥 = 𝑦 → (Ⅎ𝑥𝜑 ↔ Ⅎ𝑦𝜓))
1.5.4  Axiom scheme ax-13 (Quantified Equality)
Axiom	ax-13 2372	Axiom of Quantified Equality. One of the equality and substitution axioms of predicate calculus with equality. An equivalent way to express this axiom that may be easier to understand is (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧))) (see ax13b 2036). Recall that in the intended interpretation, our variables are metavariables ranging over the variables of predicate calculus (the object language). In order for the first antecedent ¬ 𝑥 = 𝑦 to hold, 𝑥 and 𝑦 must have different values and thus cannot be the same object-language variable (so they are effectively "distinct variables" even though no $d is present). Similarly, 𝑥 and 𝑧 cannot be the same object-language variable. Therefore, 𝑥 will not occur in the wff 𝑦 = 𝑧 when the first two antecedents hold, so analogous to ax-5 1914, the conclusion (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧) follows. Note that ax-5 1914 cannot prove this because its distinct variable ($d) requirement is not satisfied directly but only indirectly (outside of Metamath) by the argument above. The original version of this axiom was ax-c9 36831 and was replaced with this shorter ax-13 2372 in December 2015. The old axiom is proved from this one as Theorem axc9 2382. The primary purpose of this axiom is to provide a way to introduce the quantifier ∀𝑥 on 𝑦 = 𝑧 even when 𝑥 and 𝑦 are substituted with the same variable. In this case, the first antecedent becomes ¬ 𝑥 = 𝑥 and the axiom still holds. This axiom is mostly used to eliminate conditions requiring set variables be distinct (cf. ax6ev 1974 and ax6e 2383, for example) in proofs. In practice, theorems beyond elementary set theory do not really benefit from such eliminations, so direct or indirect application of this axiom is discouraged now. You need to explicitly confirm its use in case you see a sensible application in a niche. After some assisting contributions by others over the years, it was in particular the extensive work of Gino Giotto in 2024 that helped reducing dependencies on this axiom on a large scale. Although this version is shorter, the original version axc9 2382 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2382 is in dvelimh 2450 which converts a distinct variable pair to the distinctor antecedent ¬ ∀𝑥𝑥 = 𝑦. In particular, it is conjectured that it is not possible to prove ax6 2384 from ax6v 1973 without this axiom. This axiom can be weakened if desired by adding distinct variable restrictions on pairs 𝑥, 𝑧 and 𝑦, 𝑧. To show that, we add these restrictions to Theorem ax13v 2373 and use only ax13v 2373 for further derivations. Thus, ax13v 2373 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2373 (preferred) or ax13 2375 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2134) but is used as an auxiliary axiom scheme to achieve scheme completeness (i.e. so that all possible cases of bundling can be proved; see text linked at mmtheorems.html#ax6dgen 2134). It is not known whether this axiom can be derived from the others. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax13v 2373*	A weaker version of ax-13 2372 with distinct variable restrictions on pairs 𝑥, 𝑧 and 𝑦, 𝑧. In order to show (with ax13 2375) that this weakening is still adequate, this should be the only theorem referencing ax-13 2372 directly. Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1914. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. Preferably, use the version ax13w 2134 to avoid the propagation of ax-13 2372. (Contributed by NM, 30-Jun-2016.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax13lem1 2374*	A version of ax13v 2373 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. The proof of ax13 2375 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	ax13 2375	Derive ax-13 2372 from ax13v 2373 and Tarski's FOL. This shows that the weakening in ax13v 2373 is still sufficient for a complete system. Preferably, use the weaker ax13w 2134 to avoid the propagation of ax-13 2372. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 2-Jun-2021.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	ax13lem2 2376*	Lemma for nfeqf2 2377. This lemma is equivalent to ax13v 2373 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020.) (New usage is discouraged.)
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦))
Theorem	nfeqf2 2377*	An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by Wolf Lammen, 9-Jun-2019.) Remove dependency on ax-12 2173. (Revised by Wolf Lammen, 16-Dec-2022.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
Theorem	dveeq2 2378*	Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2156. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	nfeqf1 2379*	An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by Wolf Lammen, 10-Jun-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧)
Theorem	dveeq1 2380*	Quantifier introduction when one pair of variables is distinct. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by NM, 2-Jan-2002.) Remove dependency on ax-11 2156. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	nfeqf 2381	A variable is effectively not free in an equality if it is not either of the involved variables. Ⅎ version of ax-c9 36831. Usage of this theorem is discouraged because it depends on ax-13 2372. (Contributed by Mario Carneiro, 6-Oct-2016.) Remove dependency on ax-11 2156. (Revised by Wolf Lammen, 6-Sep-2018.) (New usage is discouraged.)
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → Ⅎ𝑧 𝑥 = 𝑦)
Theorem	axc9 2382	Derive set.mm's original ax-c9 36831 from the shorter ax-13 2372. Usage is discouraged to avoid uninformed ax-13 2372 propagation. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) (New usage is discouraged.)
⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (𝑥 = 𝑦 → ∀𝑧 𝑥 = 𝑦)))
Theorem	ax6e 2383	At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-4 1813 through ax-9 2118, all axioms other than ax-6 1972 are believed to be theorems of free logic, although the system without ax-6 1972 is not complete in free logic. Usage of this theorem is discouraged because it depends on ax-13 2372. It is preferred to use ax6ev 1974 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2374 became available. (Revised by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.)
⊢ ∃𝑥 𝑥 = 𝑦
Theorem	ax6 2384	Theorem showing that ax-6 1972 follows from the weaker version ax6v 1973. (Even though this theorem depends on ax-6 1972, all references of ax-6 1972 are made via ax6v 1973. An earlier version stated ax6v 1973 as a separate axiom, but having two axioms caused some confusion.) This theorem should be referenced in place of ax-6 1972 so that all proofs can be traced back to ax6v 1973. When possible, use the weaker ax6v 1973 rather than ax6 2384 since the ax6v 1973 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use ax6v 1973 instead. (New usage is discouraged.)
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦
Theorem	axc10 2385	Show that the original axiom ax-c10 36827 can be derived from ax6 2384 and axc7 2315 (on top of propositional calculus, ax-gen 1799, and ax-4 1813). See ax6fromc10 36837 for the rederivation of ax6 2384 from ax-c10 36827. Normally, axc10 2385 should be used rather than ax-c10 36827, except by theorems specifically studying the latter's properties. See bj-axc10v 34902 for a weaker version requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 2372. (New usage is discouraged.)
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑)
Theorem	spimt 2386	Closed theorem form of spim 2387. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 21-Mar-2023.) Usage of this theorem is discouraged because it depends on ax-13 2372. (New usage is discouraged.)
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓))
Theorem	spim 2387	Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2387 series of theorems requires that only one direction of the substitution hypothesis hold. Usage of this theorem is discouraged because it depends on ax-13 2372. See spimw 1975 for a version requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimed 2388	Deduction version of spime 2389. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use spimedv 2193 instead. (New usage is discouraged.)
⊢ (𝜒 → Ⅎ𝑥𝜑)    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓))
Theorem	spime 2389	Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. See spimew 1976 and spimevw 1999 for weaker versions requiring fewer axioms. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use spimefv 2194 instead. (New usage is discouraged.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spimv 2390*	A version of spim 2387 with a distinct variable requirement instead of a bound-variable hypothesis. See spimfv 2235 and spimvw 2000 for versions requiring fewer axioms. (Contributed by NM, 31-Jul-1993.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use spimvw 2000 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimvALT 2391*	Alternate proof of spimv 2390. Note that it requires only ax-1 6 through ax-5 1914 together with ax6e 2383. Currently, proofs derive from ax6v 1973, but if ax-6 1972 could be used instead, this proof would reduce axiom usage. (Contributed by NM, 31-Jul-1993.) Remove dependency on ax-10 2139. (Revised by BJ, 29-Nov-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spimev 2392*	Distinct-variable version of spime 2389. (Contributed by NM, 10-Jan-1993.) Usage of this theorem is discouraged because it depends on ax-13 2372. Use spimevw 1999 instead. (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (𝜑 → ∃𝑥𝜓)
Theorem	spv 2393*	Specialization, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker spvv 2001 if possible. (Contributed by NM, 30-Aug-1993.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → 𝜓)
Theorem	spei 2394	Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker speiv 1977 if possible. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜓    ⇒   ⊢ ∃𝑥𝜑
Theorem	chvar 2395	Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker chvarfv 2236 if possible. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	chvarv 2396*	Implicit substitution of 𝑦 for 𝑥 into a theorem. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker chvarvv 2003 if possible. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    &   ⊢ 𝜑    ⇒   ⊢ 𝜓
Theorem	cbv3 2397	Rule used to change bound variables, using implicit substitution, that does not use ax-c9 36831. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker cbv3v 2334 if possible. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbval 2398	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Check out cbvalw 2039, cbvalvw 2040, cbvalv1 2340 for versions requiring fewer axioms. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvex 2399	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. Check out cbvexvw 2041, cbvexv1 2341 for weaker versions requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbvalv 2400*	Rule used to change bound variables, using implicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2372. See cbvalvw 2040 for a version requiring fewer axioms, to be preferred when sufficient. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2139, shorten. (Revised by Wolf Lammen, 11-Sep-2023.) (New usage is discouraged.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)