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	axc16nf 2301*	If dtru 5410 is false, then there is only one element in the universe, so everything satisfies Ⅎ. (Contributed by Mario Carneiro, 7-Oct-2016.) Remove dependency on ax-11 2197. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2180. (Revised by Wolf Lammen, 12-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑)
Theorem	axc11v 2302*	Version of axc11 2462 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2043 }, from ax12v 2217 (contrary to axc11 2462 which seems to require the full ax-12 2216 and ax-13 2404). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	axc11rv 2303*	Version of axc11r 2400 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2043 }, from ax12v 2217 (contrary to axc11 2462 which seems to require the full ax-12 2216 and ax-13 2404, and to axc11r 2400 which seems to require the full ax-12 2216). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑))
Theorem	drsb2 2304	Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.)
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Theorem	equsalv 2305*	An equivalence related to implicit substitution. Version of equsal 2449 with a disjoint variable condition, which does not require ax-13 2404. See equsalvw 2039 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2306. (Contributed by NM, 2-Jun-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexv 2306*	An equivalence related to implicit substitution. Version of equsex 2450 with a disjoint variable condition, which does not require ax-13 2404. See equsexvw 2040 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2305. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid ax-10 2180. (Revised by GG, 18-Nov-2024.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	sbft 2307	Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑))
Theorem	sbf 2308	Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2127. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	sbf2 2309	Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.)
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑)
Theorem	sbh 2310	Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
Theorem	hbs1 2311*	The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.)
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
Theorem	nfs1f 2312	If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
Theorem	sb5 2313*	Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v 2126 and even needs no disjoint variable condition, see sb1 2510. Theorem sb5f 2530 replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Revised by Wolf Lammen, 4-Sep-2023.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
Theorem	equs5av 2314*	A property related to substitution that replaces the distinctor from equs5 2492 to a disjoint variable condition. Version of equs5a 2489 with a disjoint variable condition, which does not require ax-13 2404. See also sbalex 2282. (Contributed by NM, 2-Feb-2007.) (Revised by GG, 15-Dec-2023.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2sb5 2315*	Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.)
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑))
Theorem	dfsb7 2316*	An alternate definition of proper substitution df-sb 2102. By introducing a dummy variable 𝑦 in the definiens, we are able to eliminate any distinct variable restrictions among the variables 𝑡, 𝑥, and 𝜑 of the definiendum. No distinct variable conflicts arise because 𝑦 effectively insulates 𝑡 from 𝑥. To achieve this, we use a chain of two substitutions in the form of sb5 2313, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2742. Theorem sb7h 2558 provides a version where 𝜑 and 𝑦 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2102. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.)
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	sbn 2317	Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) Revise df-sb 2102. (Revised by BJ, 25-Dec-2020.)
⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑)
Theorem	sbex 2318*	Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.)
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑)
Theorem	nf5 2319	Alternate definition of df-nf 1817. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1817 changed. (Revised by Wolf Lammen, 11-Sep-2021.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
Theorem	nf6 2320	An alternate definition of df-nf 1817. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑))
Theorem	nf5d 2321	Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → Ⅎ𝑥𝜓)
Theorem	nf5diOLD 2322	Obsolete version of nf5di 2184 as of 23-Oct-2026. (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → Ⅎ𝑥𝜑)    ⇒   ⊢ Ⅎ𝑥𝜑
Theorem	19.9h 2323	A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 5-Jan-2018.) (Proof shortened by Wolf Lammen, 14-Jul-2020.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑥𝜑 ↔ 𝜑)
Theorem	19.21h 2324	Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2247 and 19.21v 1974. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
Theorem	19.23h 2325	Theorem 19.23 of [Margaris] p. 90. See 19.23 2251. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))
Theorem	exlimih 2326	Inference associated with 19.23 2251. See exlimiv 1965 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜑 → 𝜓)    ⇒   ⊢ (∃𝑥𝜑 → 𝜓)
Theorem	exlimdh 2327	Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜒 → ∀𝑥𝜒)    &   ⊢ (𝜑 → (𝜓 → 𝜒))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
Theorem	equsalhw 2328*	Version of equsalh 2452 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	equsexhv 2329*	An equivalence related to implicit substitution. Version of equsexh 2453 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓)
Theorem	hba1 2330	The setvar 𝑥 is not free in ∀𝑥𝜑. This corresponds to the axiom (4) of modal logic. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Oct-2021.)
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑)
Theorem	hbnt 2331	Closed theorem version of bound-variable hypothesis builder hbn 2332. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑))
Theorem	hbn 2332	If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Dec-2017.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑)
Theorem	hbnd 2333	Deduction form of bound-variable hypothesis builder hbn 2332. (Contributed by NM, 3-Jan-2002.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓))
Theorem	hbim1 2334	A closed form of hbim 2336. (Contributed by NM, 2-Jun-1993.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	hbimd 2335	Deduction form of bound-variable hypothesis builder hbim 2336. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓))    &   ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒))    ⇒   ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒)))
Theorem	hbim 2336	If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 → 𝜓). (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓))
Theorem	hbanOLD 2337	Obsolete version of hban 1906 as of 22-Oct-2026. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓))
Theorem	hb3anOLD 2338	Obsolete version of hb3an 1907 as of 23-Oct-2026. (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → ∀𝑥𝜑)    &   ⊢ (𝜓 → ∀𝑥𝜓)    &   ⊢ (𝜒 → ∀𝑥𝜒)    ⇒   ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒))
Theorem	sbi2 2339	Introduction of implication into substitution. (Contributed by NM, 14-May-1993.)
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓))
Theorem	sbim 2340	Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sbrim 2341	Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Avoid ax-10 2180. (Revised by GG, 20-Nov-2024.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))
Theorem	sblim 2342	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 2343	Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002.)
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓))
Theorem	sbbi 2344	Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.)
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
Theorem	sblbis 2345	Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓))
Theorem	sbrbis 2346	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.)
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒))
Theorem	sbrbif 2347	Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.)
⊢ Ⅎ𝑥𝜒    &   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)    ⇒   ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒))
Theorem	sbnf 2348*	Move nonfree predicate in and out of substitution; see sbal 2209 and sbex 2318. (Contributed by BJ, 2-May-2019.) (Proof shortened by Wolf Lammen, 2-May-2025.)
⊢ ([𝑧 / 𝑦]Ⅎ𝑥𝜑 ↔ Ⅎ𝑥[𝑧 / 𝑦]𝜑)
Theorem	sbiev 2349*	Conversion of implicit substitution to explicit substitution. Version of sbie 2534 with a disjoint variable condition, not requiring ax-13 2404. See sbievw 2133 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 2180 and shorten proof. (Revised by BJ, 18-Jul-2023.) (Proof shortened by SN, 24-Jul-2025.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
Theorem	sbiedw 2350*	Conversion of implicit substitution to explicit substitution (deduction version of sbiev 2349). Version of sbied 2535 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) Avoid ax-13 2404. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒))
Theorem	axc7 2351	Show that the original axiom ax-c7 40145 can be derived from ax-10 2180 (hbn1 2181), sp 2223 and propositional calculus. See ax10fromc7 40155 for the rederivation of ax-10 2180 from ax-c7 40145. Normally, axc7 2351 should be used rather than ax-c7 40145, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.)
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑)
Theorem	axc7e 2352	Abbreviated version of axc7 2351 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 2353	The analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.)
⊢ (𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑)
Theorem	19.9ht 2354	A closed version of 19.9h 2323. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.)
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑))
Theorem	axc4 2355	Show that the original axiom ax-c4 40144 can be derived from ax-4 1842 (alim 1843), ax-10 2180 (hbn1 2181), sp 2223 and propositional calculus. See ax4fromc4 40154 for the rederivation of ax-4 1842 from ax-c4 40144. 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 2356	Inference version of axc4 2355. (Contributed by NM, 3-Jan-1993.)
⊢ (∀𝑥𝜑 → 𝜓)    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑥𝜓)
Theorem	nfal 2357	If 𝑥 is not free in 𝜑, then it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	nfex 2358	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 2358, hbex 2359. (Revised by Wolf Lammen, 16-Oct-2021.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ Ⅎ𝑥∃𝑦𝜑
Theorem	hbex 2359	If 𝑥 is not free in 𝜑, then it is not free in ∃𝑦𝜑. (Contributed by NM, 12-Mar-1993.) Reduce symbol count in nfex 2358, hbex 2359. (Revised by Wolf Lammen, 16-Oct-2021.)
⊢ (𝜑 → ∀𝑥𝜑)    ⇒   ⊢ (∃𝑦𝜑 → ∀𝑥∃𝑦𝜑)
Theorem	nfnf 2360	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 2361	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 2380 and r19.12sn 4681. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.)
⊢ (∃𝑥∀𝑦𝜑 → ∀𝑦∃𝑥𝜑)
Theorem	nfald 2362	Deduction form of nfal 2357. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 16-Oct-2021.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∀𝑦𝜓)
Theorem	nfexd 2363	If 𝑥 is not free in 𝜓, then it is not free in ∃𝑦𝜓. (Contributed by Mario Carneiro, 24-Sep-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜓)    ⇒   ⊢ (𝜑 → Ⅎ𝑥∃𝑦𝜓)
Theorem	nfsbv 2364*	If 𝑧 is not free in 𝜑, then it is not free in [𝑦 / 𝑥]𝜑 when 𝑧 is disjoint from both 𝑥 and 𝑦. Version of nfsb 2555 with an additional disjoint variable condition on 𝑥, 𝑧 but not requiring ax-13 2404. (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	sbco2v 2365*	A composition law for substitution. Version of sbco2 2543 with disjoint variable conditions but not requiring ax-13 2404. (Contributed by NM, 30-Jun-1994.) (Revised by Wolf Lammen, 29-Apr-2023.)
⊢ Ⅎ𝑧𝜑    ⇒   ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	aaan 2366	Distribute universal quantifiers. (Contributed by NM, 12-Aug-1993.) Avoid ax-10 2180. (Revised by GG, 21-Nov-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑥∀𝑦(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ ∀𝑦𝜓))
Theorem	eeor 2367	Distribute existential quantifiers. (Contributed by NM, 8-Aug-1994.) Avoid ax-10 2180. (Revised by GG, 21-Nov-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ ∃𝑦𝜓))
Theorem	cbv3v 2368*	Rule used to change bound variables, using implicit substitution. Version of cbv3 2429 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))    ⇒   ⊢ (∀𝑥𝜑 → ∀𝑦𝜓)
Theorem	cbv1v 2369*	Rule used to change bound variables, using implicit substitution. Version of cbv1 2434 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 16-Jun-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒))
Theorem	cbv2w 2370*	Rule used to change bound variables, using implicit substitution. Version of cbv2 2435 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2404. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvaldw 2371*	Deduction used to change bound variables, using implicit substitution. Version of cbvald 2439 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 2-Jan-2002.) Avoid ax-13 2404. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	cbvexdw 2372*	Deduction used to change bound variables, using implicit substitution. Version of cbvexd 2440 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 2-Jan-2002.) Avoid ax-13 2404. (Revised by GG, 10-Jan-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒))
Theorem	cbv3hv 2373*	Rule used to change bound variables, using implicit substitution. Version of cbv3h 2436 with a disjoint variable condition on 𝑥, 𝑦, which does not require ax-13 2404. Was used in a proof of axc11n 2458 (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 2374*	Rule used to change bound variables, using implicit substitution. Version of cbval 2430 with a disjoint variable condition, which does not require ax-13 2404. See cbvalvw 2071 for a version with two more disjoint variable conditions, requiring fewer axioms, and cbvalv 2432 for another variant. (Contributed by NM, 13-May-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	cbvexv1 2375*	Rule used to change bound variables, using implicit substitution. Version of cbvex 2431 with a disjoint variable condition, which does not require ax-13 2404. See cbvexvw 2072 for a version with two disjoint variable conditions, requiring fewer axioms, and cbvexv 2433 for another variant. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 31-May-2019.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓)
Theorem	cbval2v 2376*	Rule used to change bound variables, using implicit substitution. Version of cbval2 2443 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 22-Dec-2003.) (Revised by BJ, 16-Jun-2019.) (Proof shortened by GG, 10-Jan-2024.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓)
Theorem	cbvex2v 2377*	Rule used to change bound variables, using implicit substitution. Version of cbvex2 2444 with a disjoint variable condition, which does not require ax-13 2404. (Contributed by NM, 14-Sep-2003.) (Revised by BJ, 16-Jun-2019.)
⊢ Ⅎ𝑧𝜑    &   ⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ Ⅎ𝑦𝜓    &   ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓)
Theorem	dvelimhw 2378*	Proof of dvelimh 2482 without using ax-13 2404 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 2379*	Theorem *11.53 in [WhiteheadRussell] p. 164. See pm11.53v 1979 for a version requiring fewer axioms. (Contributed by Andrew Salmon, 24-May-2011.)
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → ∀𝑦𝜓))
Theorem	19.12vv 2380*	Special case of 19.12 2361 where its converse holds. See 19.12vvv 2029 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 2381	Distribute existential quantifiers. (Contributed by NM, 27-Oct-2010.) (Revised by Mario Carneiro, 6-Oct-2016.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeanv 2382*	Distribute a pair of existential quantifiers over a conjunction. Combination of 19.41v 1984 and 19.42v 1988. For a version requiring fewer axioms but with additional disjoint variable conditions, see exdistrv 1990. (Contributed by NM, 26-Jul-1995.)
⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Theorem	eeeanv 2383*	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 2384*	Distribute two pairs of existential quantifiers over a conjunction. For a version requiring fewer axioms but with additional disjoint variable conditions, see 4exdistrv 1991. (Contributed by NM, 31-Jul-1995.) Remove disjoint variable conditions on 𝑦, 𝑧 and 𝑥, 𝑤. (Revised by Eric Schmidt, 26-Oct-2025.)
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤(𝜑 ∧ 𝜓) ↔ (∃𝑥∃𝑦𝜑 ∧ ∃𝑧∃𝑤𝜓))
Theorem	sb8v 2385*	Substitution of variable in universal quantifier. Version of sb8f 2386 with a disjoint variable condition replacing the nonfree hypothesis Ⅎ𝑦𝜑, not requiring ax-12 2216. (Contributed by SN, 5-Dec-2024.)
⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8f 2386*	Substitution of variable in universal quantifier. Version of sb8 2549 with a disjoint variable condition, not requiring ax-10 2180 or ax-13 2404. (Contributed by NM, 16-May-1993.) (Revised by Wolf Lammen, 19-Jan-2023.) Avoid ax-10 2180. (Revised by SN, 5-Dec-2024.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	sb8ef 2387*	Substitution of variable in existential quantifier. Version of sb8e 2550 with a disjoint variable condition, not requiring ax-13 2404. (Contributed by NM, 12-Aug-1993.) (Revised by Wolf Lammen, 19-Jan-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)
Theorem	2sb8ef 2388*	An equivalent expression for double existence. Version of 2sb8e 2562 with more disjoint variable conditions, not requiring ax-13 2404. (Contributed by Wolf Lammen, 28-Jan-2023.)
⊢ Ⅎ𝑤𝜑    &   ⊢ Ⅎ𝑧𝜑    ⇒   ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑)
Theorem	sb6rfv 2389*	Reversed substitution. Version of sb6rf 2500 requiring disjoint variables, but fewer axioms. (Contributed by NM, 1-Aug-1993.) (Revised by Wolf Lammen, 7-Feb-2023.)
⊢ Ⅎ𝑦𝜑    ⇒   ⊢ (𝜑 ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥]𝜑))
Theorem	sbnf2 2390*	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 2404. (Revised by Wolf Lammen, 30-Jan-2023.)
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑))
Theorem	exsb 2391*	An equivalent expression for existence. One direction (exsbim 2037) needs fewer axioms. (Contributed by NM, 2-Feb-2005.) Avoid ax-13 2404. (Revised by Wolf Lammen, 16-Oct-2022.)
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	2exsb 2392*	An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) (Proof shortened by Wolf Lammen, 30-Sep-2018.)
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑))
Theorem	sbbib 2393*	Reversal of substitution. (Contributed by AV, 6-Aug-2023.) (Proof shortened by Wolf Lammen, 4-Sep-2023.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    ⇒   ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
Theorem	sbbibvv 2394*	Reversal of substitution. (Contributed by AV, 6-Aug-2023.)
⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓))
Theorem	cbvsbvf 2395*	Change the bound variable (i.e. the substituted one) in wff's linked by implicit substitution. The proof was part of a former cbvabw 2835 version. (Contributed by GG and WL, 26-Oct-2024.)
⊢ Ⅎ𝑦𝜑    &   ⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
Theorem	cleljustALT 2396*	Alternate proof of cleljust 2156. 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 2397*	Alternate proof of cleljust 2156. Compared with cleljustALT 2396, it uses nfv 1949 followed by equsexv 2306 instead of ax-5 1945 followed by equsexhv 2329, 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 2398	Alternate proof of equs5a 2489. Uses ax-12 2216 but not ax-13 2404. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
Theorem	equs5eALT 2399	Alternate proof of equs5e 2490. Uses ax-12 2216 but not ax-13 2404. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Wolf Lammen, 15-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑))
Theorem	axc11r 2400	Same as axc11 2462 but with reversed antecedent. Note the use of ax-12 2216 (and not merely ax12v 2217 as in axc11rv 2303). This theorem is mostly used to eliminate conditions requiring set variables be distinct (cf. cbvaev 2090 and aecom 2459, 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 2404 only, and like that, it should be applied only in niches where indispensable. (Contributed by NM, 25-Jul-2015.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))