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-spae 37501	Prove an instance of sp 2180 from ax-13 2374 and Tarski's FOL only, without distinct variable conditions. The antecedent ∀𝑥𝑥 = 𝑦 holds in a multi-object universe only if 𝑦 is substituted for 𝑥, or vice versa, i.e. both variables are effectively the same. The converse ¬ ∀𝑥𝑥 = 𝑦 indicates that both variables are distinct, and it so provides a simple translation of a distinct variable condition to a logical term. In case studies ∀𝑥𝑥 = 𝑦 and ¬ ∀𝑥𝑥 = 𝑦 can help eliminating distinct variable conditions. The antecedent ∀𝑥𝑥 = 𝑦 is expressed in the theorem's name by the abbreviation ae standing for 'all equal'. Note that we cannot provide a logical predicate telling us directly whether a logical expression contains a particular variable, as such a construct would usually contradict ax-12 2174. Note that this theorem is also provable from ax-12 2174 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1978 and spaev 2049 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
Theorem	wl-speqv 37502*	Under the assumption ¬ 𝑥 = 𝑦 a specialized version of sp 2180 is provable from Tarski's FOL and ax13v 2375 only. Note that this reverts the implication in ax13lem1 2376, so in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (∀𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦))
Theorem	wl-19.8eqv 37503*	Under the assumption ¬ 𝑥 = 𝑦 a specialized version of 19.8a 2178 is provable from Tarski's FOL and ax13v 2375 only. Note that this reverts the implication in ax13lem2 2378, so in fact (¬ 𝑥 = 𝑦 → (∃𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∃𝑥 𝑧 = 𝑦))
Theorem	wl-19.2reqv 37504*	Under the assumption ¬ 𝑥 = 𝑦 the reverse direction of 19.2 1973 is provable from Tarski's FOL and ax13v 2375 only. Note that in conjunction with 19.2 1973 in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ ∃𝑥𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	wl-nfalv 37505*	If 𝑥 is not present in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Wolf Lammen, 11-Jan-2020.)
⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	wl-nfimf1 37506	An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim 1893 in dvelimdf 2451 to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018.)
⊢ (∀𝑥𝜑 → (Ⅎ𝑥(𝜑 → 𝜓) ↔ Ⅎ𝑥𝜓))
Theorem	wl-nfae1 37507	Unlike nfae 2435, this specialized theorem avoids ax-11 2154. (Contributed by Wolf Lammen, 26-Jun-2019.)
⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑥
Theorem	wl-nfnae1 37508	Unlike nfnae 2436, this specialized theorem avoids ax-11 2154. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑥
Theorem	wl-aetr 37509	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑧))
Theorem	wl-axc11r 37510	Same as axc11r 2368, but using ax12 2425 instead of ax-12 2174 directly. This better reflects axiom usage in theorems dependent on it. (Contributed by NM, 25-Jul-2015.) Avoid direct use of ax-12 2174. (Revised by Wolf Lammen, 30-Mar-2024.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	wl-dral1d 37511	A version of dral1 2441 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 37524 and nf5di 2283 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)))
Theorem	wl-cbvalnaed 37512	wl-cbvalnae 37513 with a context. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜓))    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	wl-cbvalnae 37513	A more general version of cbval 2400 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 2450, nfsb2 2485 or dveeq1 2382. (Contributed by Wolf Lammen, 4-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	wl-exeq 37514	The semantics of ∃𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-aleq 37515	The semantics of ∀𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)))
Theorem	wl-nfeqfb 37516	Extend nfeqf 2383 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.)
⊢ (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-nfs1t 37517	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Closed form of nfs1 2490. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	wl-equsalvw 37518*	Version of equsalv 2264 with a disjoint variable condition, and of equsal 2419 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2001. 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 2021 and cbvalvw 2032 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 37519	Deduction version of equsal 2419. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	wl-equsaldv 37520*	Deduction version of equsal 2419. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	wl-equsal 37521	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 37519 first, and then deriving more specialized versions wl-equsal 37521 and wl-equsal1t 37522 then is more efficient than the other way round, which is possible, too. See also equsal 2419. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	wl-equsal1t 37522	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 2419, spimt 2388 or sbft 2267, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	wl-equsalcom 37523	This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑))
Theorem	wl-equsal1i 37524	The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑)    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	wl-sbid2ft 37525*	A more general version of sbid2vw 2256. (Contributed by Wolf Lammen, 14-May-2019.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑))
Theorem	wl-cbvalsbi 37526*	Change bounded variables in a special case. The reverse direction seems to involve ax-11 2154. My hope is that I will in some future be able to prove mo3 2561 with reversed quantifiers not using ax-11 2154. See also the remark in mo4 2563, which lead me to this effort. (Contributed by Wolf Lammen, 5-Mar-2024.)
⊢ (∀𝑥𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	wl-sbrimt 37527	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2302. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)))
Theorem	wl-sblimt 37528	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2302. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)))
Theorem	wl-sb9v 37529*	Commutation of quantification and substitution variables based on fewer axioms than sb9 2521. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	wl-sb8ft 37530*	Substitution of variable in universal quantifier. Closed form of sb8f 2353. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8eft 37531*	Substitution of variable in existentialal quantifier. Closed form of sb8ef 2355. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8t 37532	Substitution of variable in universal quantifier. Closed form of sb8 2519. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8et 37533	Substitution of variable in universal quantifier. Closed form of sb8e 2520. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sbhbt 37534	Closed form of sbhb 2523. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-sbnf1 37535	Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2358. Note: This theorem shows that sbnf2 2358 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-equsb3 37536	equsb3 2100 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧))
Theorem	wl-equsb4 37537	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 37538	Version of 2sb6 2083 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
Theorem	wl-sbcom2d-lem1 37539*	Lemma used to prove wl-sbcom2d 37541. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)))
Theorem	wl-sbcom2d-lem2 37540*	Lemma used to prove wl-sbcom2d 37541. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑)))
Theorem	wl-sbcom2d 37541	Version of sbcom2 2170 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦)    ⇒   ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
Theorem	wl-sbalnae 37542	A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal1 37543*	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 37542 now. See also sbal1 2530. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal2 37544*	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 37542 now. See also sbal2 2531. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-2spsbbi 37545	spsbbi 2070 applied twice. (Contributed by Wolf Lammen, 5-Aug-2023.)
⊢ (∀𝑎∀𝑏(𝜑 ↔ 𝜓) → ([𝑦 / 𝑏][𝑥 / 𝑎]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜓))
Theorem	wl-lem-exsb 37546*	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	wl-lem-nexmo 37547	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧))
Theorem	wl-lem-moexsb 37548*	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 37549	This theorem extends alanimi 1812 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
Theorem	wl-mo2df 37550	Version of mof 2560 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 37551	Closed form of mof 2560 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-eudf 37552	Version of eu6 2571 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 37553	Closed form of eu6 2571 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
Theorem	wl-euequf 37554	euequ 2594 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦)
Theorem	wl-mo2t 37555*	Closed form of mof 2560. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-mo3t 37556*	Closed form of mo3 2561. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Theorem	wl-nfsbtv 37557*	Closed form of nfsbv 2328. (Contributed by Wolf Lammen, 2-May-2025.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	wl-sb8eut 37558	Substitution of variable in universal quantifier. Closed form of sb8eu 2597. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8eutv 37559*	Substitution of variable in universal quantifier. Closed form of sb8euv 2596. (Contributed by Wolf Lammen, 3-May-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8mot 37560	Substitution of variable in universal quantifier. Closed form of sb8mo 2598. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8motv 37561*	Substitution of variable in universal quantifier. Closed form of sb8mo 2598 without ax-13 2374, but requiring 𝑥 and 𝑦 being disjoint. This theorem relates to wl-mo3t 37556, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2267 and sbco 2509. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 37556 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 37556 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 37562	A closed form of issetf 3494. The proof here is a modification of a subproof in vtoclgft 3551, where it could be used to shorten the proof. (Contributed by Wolf Lammen, 25-Jan-2025.)
⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴))
Theorem	wl-axc11rc11 37563	Proving axc11r 2368 from axc11 2432. The hypotheses are two instances of axc11 2432 used in the proof here. Some systems introduce axc11 2432 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf 2432. By contrast, this database sees the variant axc11r 2368, directly derived from ax-12 2174, as foundational. Later axc11 2432 is proven somewhat trickily, requiring ax-10 2138 and ax-13 2374, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥))    &   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-wl-11v 37564*	Version of ax-11 2154 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2154. It will later be converted into a theorem directly based on ax-11 2154. (Contributed by Wolf Lammen, 28-Jun-2019.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	wl-ax11-lem1 37565	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧))
Theorem	wl-ax11-lem2 37566*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦)
Theorem	wl-ax11-lem3 37567*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦)
Theorem	wl-ax11-lem4 37568*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-ax11-lem5 37569	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑))
Theorem	wl-ax11-lem6 37570*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem7 37571	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑))
Theorem	wl-ax11-lem8 37572*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑))
Theorem	wl-ax11-lem9 37573	The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem10 37574*	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 37573 to eliminate the second antecedent. Missing is something along the lines of ax-6 1964, 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 37575*	Variant of df-clab 2712, 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 2705, df-clel 2813 and df-cleq 2726. 𝑥 ∈ 𝐴 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 2107, ax-9 2115, or df-clel 2813. Theorem cleljust 2114 shows that a possible choice does not matter. The original df-clab 2712 can be rederived, see wl-dfclab 37576. 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 37576	Rederive df-clab 2712 from wl-clabv 37575. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	wl-clabtv 37577*	Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 37578. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
Theorem	wl-clabt 37578	Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 37577. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
21.23  Mathbox for Brendan Leahy
Theorem	rabiun 37579*	Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.)
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑}
Theorem	iundif1 37580*	Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.)
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶)
Theorem	imadifss 37581	The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵))
Theorem	cureq 37582	Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵)
Theorem	unceq 37583	Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵)
Theorem	curf 37584	Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑m 𝐵))
Theorem	uncf 37585	Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (𝐹:𝐴⟶(𝐶 ↑m 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶)
Theorem	curfv 37586	Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵))
Theorem	uncov 37587	Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵))
Theorem	curunc 37588	Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.)
⊢ ((𝐹:𝐴⟶(𝐶 ↑m 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹)
Theorem	unccur 37589	Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.)
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹)
Theorem	phpreu 37590*	Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.)
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶))
Theorem	finixpnum 37591*	A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.)
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card)
Theorem	fin2solem 37592*	Lemma for fin2so 37593. (Contributed by Brendan Leahy, 29-Jun-2019.)
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧}))
Theorem	fin2so 37593	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 37594	Theorem to move the floor function across a strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((⌊‘𝐴) < 𝐵 ↔ 𝐴 < -(⌊‘-𝐵)))
Theorem	leceifl 37595	Theorem to move the floor function across a non-strict inequality. (Contributed by Brendan Leahy, 25-Oct-2017.)
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-(⌊‘-𝐴) ≤ 𝐵 ↔ 𝐴 ≤ (⌊‘𝐵)))
Theorem	sin2h 37596	Half-angle rule for sine. (Contributed by Brendan Leahy, 3-Aug-2018.)
⊢ (𝐴 ∈ (0[,](2 · π)) → (sin‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / 2)))
Theorem	cos2h 37597	Half-angle rule for cosine. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (-π[,]π) → (cos‘(𝐴 / 2)) = (√‘((1 + (cos‘𝐴)) / 2)))
Theorem	tan2h 37598	Half-angle rule for tangent. (Contributed by Brendan Leahy, 4-Aug-2018.)
⊢ (𝐴 ∈ (0[,)π) → (tan‘(𝐴 / 2)) = (√‘((1 − (cos‘𝐴)) / (1 + (cos‘𝐴)))))
Theorem	lindsadd 37599	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 37600	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 𝐼))) → 𝑋 ≼ 𝐼)