P. 376 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37501-37600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wl-nfnae1 37501	Unlike nfnae 2432, this specialized theorem avoids ax-11 2158. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑥
Theorem	wl-aetr 37502	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑧))
Theorem	wl-axc11r 37503	Same as axc11r 2366, but using ax12 2421 instead of ax-12 2178 directly. This better reflects axiom usage in theorems dependent on it. (Contributed by NM, 25-Jul-2015.) Avoid direct use of ax-12 2178. (Revised by Wolf Lammen, 30-Mar-2024.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	wl-dral1d 37504	A version of dral1 2437 with a context. Note: At first glance one might be tempted to generalize this (or a similar) theorem by weakening the first two hypotheses adding a 𝑥 = 𝑦, ∀𝑥𝑥 = 𝑦 or 𝜑 antecedent. wl-equsal1i 37517 and nf5di 2285 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)))
Theorem	wl-cbvalnaed 37505	wl-cbvalnae 37506 with a context. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜓))    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	wl-cbvalnae 37506	A more general version of cbval 2396 when nonfree properties depend on a distinctor. Such expressions arise in proofs aiming at the elimination of distinct variable constraints, specifically in application of dvelimf 2446, nfsb2 2481 or dveeq1 2378. (Contributed by Wolf Lammen, 4-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	wl-exeq 37507	The semantics of ∃𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-aleq 37508	The semantics of ∀𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)))
Theorem	wl-nfeqfb 37509	Extend nfeqf 2379 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.)
⊢ (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-nfs1t 37510	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Closed form of nfs1 2486. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	wl-equsalvw 37511*	Version of equsalv 2268 with a disjoint variable condition, and of equsal 2415 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2005. This theorem lays the foundation to a transformation of expressions called substitution of set variables in a wff. Only in this particular context we additionally assume 𝜑 and 𝑦 disjoint, stated here as 𝜑(𝑥). Similarly the disjointness of 𝜓 and 𝑥 is expressed by 𝜓(𝑦). Both 𝜑 and 𝜓 may still depend on other set variables, but that is irrelevant here. We want to transform 𝜑(𝑥) into 𝜓(𝑦) such that 𝜓 depends on 𝑦 the same way as 𝜑 depends on 𝑥. This dependency is expressed in our hypothesis (called implicit substitution): (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)). For primitive enough 𝜑 a sort of textual substitution of 𝑥 by 𝑦 is sufficient for such transformation. But note: 𝜑 must not contain wff variables, and the substitution is no proper textual substitution either. We still need grammar information to not accidently replace the x in a token 'x.' denoting multiplication, but only catch set variables 𝑥. Our current stage of development allows only equations and quantifiers make up such primitives. Thanks to equequ1 2025 and cbvalvw 2036 we can then prove in a mechanical way that in fact the implicit substitution holds for each instance. If 𝜑 contains wff variables we cannot use textual transformation any longer, since we don't know how to replace 𝑦 for 𝑥 in placeholders of unknown structure. Our theorem now states, that the generic expression ∀𝑥(𝑥 = 𝑦 → 𝜑) formally behaves as if such a substitution was possible and made. (Contributed by BJ, 31-May-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	wl-equsald 37512	Deduction version of equsal 2415. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	wl-equsaldv 37513*	Deduction version of equsal 2415. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	wl-equsal 37514	A useful equivalence related to substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) It seems proving wl-equsald 37512 first, and then deriving more specialized versions wl-equsal 37514 and wl-equsal1t 37515 then is more efficient than the other way round, which is possible, too. See also equsal 2415. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	wl-equsal1t 37515	The expression 𝑥 = 𝑦 in antecedent position plays an important role in predicate logic, namely in implicit substitution. However, occasionally it is irrelevant, and can safely be dropped. A sufficient condition for this is when 𝑥 (or 𝑦 or both) is not free in 𝜑. This theorem is more fundamental than equsal 2415, spimt 2384 or sbft 2270, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	wl-equsalcom 37516	This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑))
Theorem	wl-equsal1i 37517	The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑)    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	wl-sbid2ft 37518*	A more general version of sbid2vw 2260. (Contributed by Wolf Lammen, 14-May-2019.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑))
Theorem	wl-cbvalsbi 37519*	Change bounded variables in a special case. The reverse direction seems to involve ax-11 2158. My hope is that I will in some future be able to prove mo3 2557 with reversed quantifiers not using ax-11 2158. See also the remark in mo4 2559, which lead me to this effort. (Contributed by Wolf Lammen, 5-Mar-2024.)
⊢ (∀𝑥𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	wl-sbrimt 37520	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2304. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)))
Theorem	wl-sblimt 37521	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2304. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)))
Theorem	wl-sb9v 37522*	Commutation of quantification and substitution variables based on fewer axioms than sb9 2517. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	wl-sb8ft 37523*	Substitution of variable in universal quantifier. Closed form of sb8f 2352. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8eft 37524*	Substitution of variable in existentialal quantifier. Closed form of sb8ef 2353. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8t 37525	Substitution of variable in universal quantifier. Closed form of sb8 2515. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8et 37526	Substitution of variable in universal quantifier. Closed form of sb8e 2516. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sbhbt 37527	Closed form of sbhb 2519. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-sbnf1 37528	Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2356. Note: This theorem shows that sbnf2 2356 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-equsb3 37529	equsb3 2104 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧))
Theorem	wl-equsb4 37530	Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable condition. (Contributed by Wolf Lammen, 26-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑦 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	wl-2sb6d 37531	Version of 2sb6 2087 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
Theorem	wl-sbcom2d-lem1 37532*	Lemma used to prove wl-sbcom2d 37534. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)))
Theorem	wl-sbcom2d-lem2 37533*	Lemma used to prove wl-sbcom2d 37534. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑)))
Theorem	wl-sbcom2d 37534	Version of sbcom2 2174 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦)    ⇒   ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
Theorem	wl-sbalnae 37535	A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal1 37536*	A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 15-May-1993.) Proof is based on wl-sbalnae 37535 now. See also sbal1 2526. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal2 37537*	Move quantifier in and out of substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 2-Jan-2002.) Proof is based on wl-sbalnae 37535 now. See also sbal2 2527. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-2spsbbi 37538	spsbbi 2074 applied twice. (Contributed by Wolf Lammen, 5-Aug-2023.)
⊢ (∀𝑎∀𝑏(𝜑 ↔ 𝜓) → ([𝑦 / 𝑏][𝑥 / 𝑎]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜓))
Theorem	wl-lem-exsb 37539*	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	wl-lem-nexmo 37540	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧))
Theorem	wl-lem-moexsb 37541*	The antecedent ∀𝑥(𝜑 → 𝑥 = 𝑧) relates to ∃*𝑥𝜑, but is better suited for usage in proofs. Note that no distinct variable restriction is placed on 𝜑. This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (∀𝑥(𝜑 → 𝑥 = 𝑧) → (∃𝑥𝜑 ↔ [𝑧 / 𝑥]𝜑))
Theorem	wl-alanbii 37542	This theorem extends alanimi 1816 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
Theorem	wl-mo2df 37543	Version of mof 2556 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    ⇒   ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦)))
Theorem	wl-mo2tf 37544	Closed form of mof 2556 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-eudf 37545	Version of eu6 2567 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate disjoint variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦)    &   ⊢ (𝜑 → Ⅎ𝑦𝜓)    ⇒   ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑦)))
Theorem	wl-eutf 37546	Closed form of eu6 2567 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
Theorem	wl-euequf 37547	euequ 2590 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦)
Theorem	wl-mo2t 37548*	Closed form of mof 2556. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-mo3t 37549*	Closed form of mo3 2557. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Theorem	wl-nfsbtv 37550*	Closed form of nfsbv 2329. (Contributed by Wolf Lammen, 2-May-2025.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	wl-sb8eut 37551	Substitution of variable in universal quantifier. Closed form of sb8eu 2593. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8eutv 37552*	Substitution of variable in universal quantifier. Closed form of sb8euv 2592. (Contributed by Wolf Lammen, 3-May-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8mot 37553	Substitution of variable in universal quantifier. Closed form of sb8mo 2594. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8motv 37554*	Substitution of variable in universal quantifier. Closed form of sb8mo 2594 without ax-13 2370, but requiring 𝑥 and 𝑦 being disjoint. This theorem relates to wl-mo3t 37549, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2270 and sbco 2505. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 37549 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 37549 to be more fundamental, as it hints how the "at most one" objects on both sides of the biconditional correlate (they are the same), if they exist at all, and then prove this theorem from it. (Contributed by Wolf Lammen, 3-May-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-issetft 37555	A closed form of issetf 3455. The proof here is a modification of a subproof in vtoclgft 3509, where it could be used to shorten the proof. (Contributed by Wolf Lammen, 25-Jan-2025.)
⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴))
Theorem	wl-axc11rc11 37556	Proving axc11r 2366 from axc11 2428. The hypotheses are two instances of axc11 2428 used in the proof here. Some systems introduce axc11 2428 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf 2428. By contrast, this database sees the variant axc11r 2366, directly derived from ax-12 2178, as foundational. Later axc11 2428 is proven somewhat trickily, requiring ax-10 2142 and ax-13 2370, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥))    &   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-wl-11v 37557*	Version of ax-11 2158 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2158. It will later be converted into a theorem directly based on ax-11 2158. (Contributed by Wolf Lammen, 28-Jun-2019.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	wl-ax11-lem1 37558	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧))
Theorem	wl-ax11-lem2 37559*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦)
Theorem	wl-ax11-lem3 37560*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦)
Theorem	wl-ax11-lem4 37561*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-ax11-lem5 37562	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑))
Theorem	wl-ax11-lem6 37563*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem7 37564	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑))
Theorem	wl-ax11-lem8 37565*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑))
Theorem	wl-ax11-lem9 37566	The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem10 37567*	We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 192 can be used in conjunction with wl-ax11-lem9 37566 to eliminate the second antecedent. Missing is something along the lines of ax-6 1967, so we could remove the first antecedent. But the Metamath axioms cannot accomplish this. Such a rule must reside one abstraction level higher than all others: It says that a distinctor implies a distinct variable condition on its contained setvar. This is only needed if such conditions are required, as ax-11v does. The result of this study is for me, that you cannot introduce a setvar capturing this condition, and hope to eliminate it later. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑦 𝑦 = 𝑢 → (¬ ∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 → ∀𝑥∀𝑦𝜑)))
Theorem	wl-clabv 37568*	Variant of df-clab 2708, where the element 𝑥 is required to be disjoint from the class it is taken from. This restriction meets similar ones found in other definitions and axioms like ax-ext 2701, df-clel 2803 and df-cleq 2721. 𝑥 ∈ 𝐴 with 𝐴 depending on 𝑥 can be the source of side effects, that you rather want to be aware of. So here we eliminate one possible way of letting this slip in instead. An expression 𝑥 ∈ 𝐴 with 𝑥, 𝐴 not disjoint, is now only introduced either via ax-8 2111, ax-9 2119, or df-clel 2803. Theorem cleljust 2118 shows that a possible choice does not matter. The original df-clab 2708 can be rederived, see wl-dfclab 37569. In an implementation this theorem is the only user of df-clab. (Contributed by NM, 26-May-1993.) Element and class are disjoint. (Revised by Wolf Lammen, 31-May-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	wl-dfclab 37569	Rederive df-clab 2708 from wl-clabv 37568. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	wl-clabtv 37570*	Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 37571. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
Theorem	wl-clabt 37571	Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 37570. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
21.23  Mathbox for Brendan Leahy
Theorem	rabiun 37572*	Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.)
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	iundif1 37573*	Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶)
Theorem	imadifss 37574	The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵))
Theorem	cureq 37575	Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵)
Theorem	unceq 37576	Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵)
Theorem	curf 37577	Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵))
Theorem	uncf 37578	Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶)
Theorem	curfv 37579	Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵))
Theorem	uncov 37580	Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵))
Theorem	curunc 37581	Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹)
Theorem	unccur 37582	Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.)
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹)
Theorem	phpreu 37583*	Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))
Theorem	finixpnum 37584*	A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card)
Theorem	fin2solem 37585*	Lemma for fin2so 37586. (Contributed by Brendan Leahy, 29-Jun-2019.)
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
Theorem	fin2so 37586	Any totally ordered Tarski-finite set is finite; in particular, no amorphous set can be ordered. Theorem 2 of [Levy58]] p. 4. (Contributed by Brendan Leahy, 28-Jun-2019.)
⊢ ((𝐴 ∈ FinII ∧ 𝑅 Or 𝐴) → 𝐴 ∈ Fin)
Theorem	ltflcei 37587	Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ 𝐴 < -(⌊‘-𝐵)))
Theorem	leceifl 37588	Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (⌊‘𝐵)))
Theorem	sin2h 37589	Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.)
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2)))
Theorem	cos2h 37590	Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2)))
Theorem	tan2h 37591	Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))
Theorem	lindsadd 37592	In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023.)
⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))
Theorem	lindsdom 37593	A linearly independent set in a free linear module of finite dimension over a division ring is smaller than the dimension of the module. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) → 𝑋 ≼ 𝐼)
Theorem	lindsenlbs 37594	A maximal linearly independent set in a free module of finite dimension over a division ring is a basis. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (((𝑅 ∈ DivRing ∧ 𝐼 ∈ Fin ∧ 𝑋 ∈ (LIndS‘(𝑅 freeLMod 𝐼))) ∧ 𝑋 ≈ 𝐼) → 𝑋 ∈ (LBasis‘(𝑅 freeLMod 𝐼)))
Theorem	matunitlindflem1 37595	One direction of matunitlindf 37597. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (((𝑅 ∈ Field ∧ 𝑀:(𝐼 × 𝐼)⟶(Base‘𝑅)) ∧ 𝐼 ∈ (Fin ∖ {∅})) → (¬ curry 𝑀 LIndF (𝑅 freeLMod 𝐼) → ((𝐼 maDet 𝑅)‘𝑀) = (0g‘𝑅)))
Theorem	matunitlindflem2 37596	One direction of matunitlindf 37597. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) ∧ 𝐼 ≠ ∅) ∧ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)) → ((𝐼 maDet 𝑅)‘𝑀) ∈ (Unit‘𝑅))
Theorem	matunitlindf 37597	A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝑅 ∈ Field ∧ 𝑀 ∈ (Base‘(𝐼 Mat 𝑅))) → (𝑀 ∈ (Unit‘(𝐼 Mat 𝑅)) ↔ curry 𝑀 LIndF (𝑅 freeLMod 𝐼)))
Theorem	ptrest 37598*	Expressing a restriction of a product topology as a product topology. (Contributed by Brendan Leahy, 24-Mar-2019.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:𝐴⟶Top)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑆 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ((∏t‘𝐹) ↾t X𝑘 ∈ 𝐴 𝑆) = (∏t‘(𝑘 ∈ 𝐴 ↦ ((𝐹‘𝑘) ↾t 𝑆))))
Theorem	ptrecube 37599*	Any point in an open set of N-space is surrounded by an open cube within that set. (Contributed by Brendan Leahy, 21-Aug-2020.) (Proof shortened by AV, 28-Sep-2020.)
⊢ 𝑅 = (∏t‘((1...𝑁) × {(topGen‘ran (,))}))    &   ⊢ 𝐷 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)
Theorem	poimirlem1 37600*	Lemma for poimir 37632- the vertices on either side of a skipped vertex differ in at least two dimensions. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐹 = (𝑦 ∈ (0...(𝑁 − 1)) ↦ ⦋if(𝑦 < 𝑀, 𝑦, (𝑦 + 1)) / 𝑗⦌(𝑇 ∘f + (((𝑈 “ (1...𝑗)) × {1}) ∪ ((𝑈 “ ((𝑗 + 1)...𝑁)) × {0})))))    &   ⊢ (𝜑 → 𝑇:(1...𝑁)⟶ℤ)    &   ⊢ (𝜑 → 𝑈:(1...𝑁)–1-1-onto→(1...𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1)))    ⇒   ⊢ (𝜑 → ¬ ∃*𝑛 ∈ (1...𝑁)((𝐹‘(𝑀 − 1))‘𝑛) ≠ ((𝐹‘𝑀)‘𝑛))