P. 340 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33901-34000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wl-moae 33901*	Two ways to express "at most one thing exists" or, in this context equivalently, "exactly one thing exists" . The equivalence results from the presence of ax-6 2021 in the proof, that ensures "at least one thing exists". For other equivalences see wl-euae 33902 and exists1 2692. Gerard Lang pointed out, that ∃𝑦∀𝑥𝑥 = 𝑦 with disjoint 𝑥 and 𝑦 (df-mo 2551, trut 1608) also means "exactly one thing exists" . (Contributed by NM, 5-Apr-2004.) State the theorem using truth constant ⊤. (Revised by BJ, 7-Oct-2022.) Reduce axiom dependencies, and use ∃*. (Revised by Wolf Lammen, 7-Mar-2023.)
⊢ (∃*𝑥⊤ ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-euae 33902*	Two ways to express "exactly one thing exists" . (Contributed by Wolf Lammen, 5-Mar-2023.)
⊢ (∃!𝑥⊤ ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-nax6im 33903*	The following series of theorems are centered around the empty domain, where no set exists. As a consequence, a set variable like 𝑥 has no instance to assign to. An expression like 𝑥 = 𝑦 is not really meaningful then. What does it evaluate to, true or false? In fact, the grammar extension weq 2005 requires us to formally assign a boolean value to an equation, say always false, unless you want to give up on exmid 881, for example. Whatever it is, we start out with the contraposition of ax-6 2021, that guarantees the existence of at least one set. Our hypothesis here expresses tentatively it might not hold. We can simplify the antecedent then, to the point where we do not need equation any more. This suggests what a decent characterization of the empty domain could be. (Contributed by Wolf Lammen, 12-Mar-2023.)
⊢ (¬ ∃𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∃𝑥⊤ → 𝜑)
Theorem	wl-nax6al 33904	In an empty domain the for-all operator always holds, even when applied to a false expression. This theorem actually shows that ax-5 1953 is provable there. Also we cannot assume that sp 2167 generally holds, except of course in the form of sptruw 1850. Without the support of an sp 2167 like theorem it seems difficult, if not impossible, to arrive at a theorem allowing to change the bounded variable in the antecedent. Additional axioms need to be postulated to further strengthen this result. A consequence of this result is that ∃𝑥𝜑 is not true for any 𝜑. In particular, ∃*𝑥𝜑 does not hold either, a somewhat counterintuitive result. (Contributed by Wolf Lammen, 12-Mar-2023.)
⊢ (¬ ∃𝑥⊤ → ∀𝑥𝜑)
Theorem	wl-nax6nfr 33905	All expressions are free of the variable used in the antecedent. (Contributed by Wolf Lammen, 12-Mar-2023.)
⊢ (¬ ∃𝑥⊤ → Ⅎ𝑥𝜑)
Theorem	wl-naev 33906*	If some set variables can assume different values, then any two distinct set variables cannot always be the same. (Contributed by Wolf Lammen, 10-Aug-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑢 𝑢 = 𝑣)
Theorem	wl-hbae1 33907	This specialization of hbae 2397 does not depend on ax-11 2150. (Contributed by Wolf Lammen, 8-Aug-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦∀𝑥 𝑥 = 𝑦)
Theorem	wl-naevhba1v 33908*	An instance of hbn1w 2091 applied to equality. (Contributed by Wolf Lammen, 7-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-spae 33909	Prove an instance of sp 2167 from ax-13 2334 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 2163. Note that this theorem is also provable from ax-12 2163 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 2031 and spaev 2095 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
Theorem	wl-speqv 33910*	Under the assumption ¬ 𝑥 = 𝑦 a specialized version of sp 2167 is provable from Tarski's FOL and ax13v 2335 only. Note that this reverts the implication in ax13lem1 2336, so in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (∀𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦))
Theorem	wl-19.8eqv 33911*	Under the assumption ¬ 𝑥 = 𝑦 a specialized version of 19.8a 2166 is provable from Tarski's FOL and ax13v 2335 only. Note that this reverts the implication in ax13lem2 2338, so in fact (¬ 𝑥 = 𝑦 → (∃𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∃𝑥 𝑧 = 𝑦))
Theorem	wl-19.2reqv 33912*	Under the assumption ¬ 𝑥 = 𝑦 the reverse direction of 19.2 2026 is provable from Tarski's FOL and ax13v 2335 only. Note that in conjunction with 19.2 2026 in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ ∃𝑥𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	wl-nfalv 33913*	If 𝑥 is not present in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Wolf Lammen, 11-Jan-2020.)
⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	wl-nfimf1 33914	An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim 1943 in dvelimdf 2415 to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018.)
⊢ (∀𝑥𝜑 → (Ⅎ𝑥(𝜑 → 𝜓) ↔ Ⅎ𝑥𝜓))
Theorem	wl-nfnbi 33915	Being free does not depend on an outside negation in an expression. This theorem is slightly more general than nfn 1902 or nfnd 1903. (Contributed by Wolf Lammen, 5-May-2018.)
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑)
Theorem	wl-nfae1 33916	Unlike nfae 2398, this specialized theorem avoids ax-11 2150. (Contributed by Wolf Lammen, 26-Jun-2019.)
⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑥
Theorem	wl-nfnae1 33917	Unlike nfnae 2400, this specialized theorem avoids ax-11 2150. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑥
Theorem	wl-aetr 33918	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑧))
Theorem	wl-dral1d 33919	A version of dral1 2405 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 33930 and nf5di 2259 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)))
Theorem	wl-cbvalnaed 33920	wl-cbvalnae 33921 with a context. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜓))    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	wl-cbvalnae 33921	A more general version of cbval 2368 when non-free properties depend on a distinctor. Such expressions arise in proofs aiming at the elimination of distinct variable constraints, specifically in application of dvelimf 2414, nfsb2 2436 or dveeq1 2344. (Contributed by Wolf Lammen, 4-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	wl-exeq 33922	The semantics of ∃𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-aleq 33923	The semantics of ∀𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)))
Theorem	wl-nfeqfb 33924	Extend nfeqf 2345 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.)
⊢ (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-nfs1t 33925	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Closed form of nfs1 2441. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	wl-equsald 33926	Deduction version of equsal 2382. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	wl-equsal 33927	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 33926 first, and then deriving more specialized versions wl-equsal 33927 and wl-equsal1t 33928 then is more efficient than the other way round, which is possible, too. See also equsal 2382. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	wl-equsal1t 33928	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 2382, spimt 2350 or sbft 2455, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	wl-equsalcom 33929	This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑))
Theorem	wl-equsal1i 33930	The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑)    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	wl-dv-sb 33931*	Substitution for 𝑥 has no effect on 𝜑 not containing 𝑥. See also sbf 2456. (Contributed by Wolf Lammen, 4-Sep-2022.)
⊢ (𝜑 ↔ [𝑦 / 𝑥]𝜑)
Theorem	wl-sb6rft 33932	A specialization of wl-equsal1t 33928. Closed form of sb6rf 2500. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)))
Theorem	wl-sbrimt 33933	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2472. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)))
Theorem	wl-sblimt 33934	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2472. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)))
Theorem	wl-sb8t 33935	Substitution of variable in universal quantifier. Closed form of sb8 2501. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8et 33936	Substitution of variable in universal quantifier. Closed form of sb8e 2502. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sbhbt 33937	Closed form of sbhb 2518. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-sbnf1 33938	Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2326. Note: This theorem shows that sbnf2 2326 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-equsb3 33939	equsb3 2510 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧))
Theorem	wl-equsb4 33940	Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable constraint. (Contributed by Wolf Lammen, 26-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑦 / 𝑥]𝑦 = 𝑧 ↔ 𝑦 = 𝑧))
Theorem	wl-sb6nae 33941	Version of sb6 2250 suitable for elimination of unnecessary disjoint variable conditions. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	wl-2sb6d 33942	Version of 2sb6 2253 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
Theorem	wl-sbcom2d-lem1 33943*	Lemma used to prove wl-sbcom2d 33945. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)))
Theorem	wl-sbcom2d-lem2 33944*	Lemma used to prove wl-sbcom2d 33945. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑)))
Theorem	wl-sbcom2d 33945	Version of sbcom2 2523 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦)    ⇒   ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
Theorem	wl-sbalnae 33946	A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal1 33947*	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 33946 now. See also sbal1 2539. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal2 33948*	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 33946 now. See also sbal2 2540. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-lem-exsb 33949*	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	wl-lem-nexmo 33950	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧))
Theorem	wl-lem-moexsb 33951*	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 33952	This theorem extends alanimi 1860 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
Theorem	wl-mo2df 33953	Version of mof 2578 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 33954	Closed form of mof 2578 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-eudf 33955	Version of eu6 2592 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 33956	Closed form of eu6 2592 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
Theorem	wl-euequf 33957	euequ 2616 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦)
Theorem	wl-mo2t 33958*	Closed form of mof 2578. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-mo3t 33959*	Closed form of mo3 2580. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Theorem	wl-sb8eut 33960	Substitution of variable in universal quantifier. Closed form of sb8eu 2635. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8mot 33961	Substitution of variable in universal quantifier. Closed form of sb8mo 2636. This theorem relates to wl-mo3t 33959, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2455 and sbco 2488. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 33959 in a simple fashion, unfortunately only if 𝑥 and 𝑦 are known to be distinct. To avoid any hassle with distinctors, we prefer to derive this theorem independently, ignoring the close connection between both theorems. From an educational standpoint, one would assume wl-mo3t 33959 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, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Axiom	ax-wl-11v 33962*	Version of ax-11 2150 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2150. It will later be converted into a theorem directly based on ax-11 2150. (Contributed by Wolf Lammen, 28-Jun-2019.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	wl-ax11-lem1 33963	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧))
Theorem	wl-ax11-lem2 33964*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦)
Theorem	wl-ax11-lem3 33965*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦)
Theorem	wl-ax11-lem4 33966*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-ax11-lem5 33967	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑))
Theorem	wl-ax11-lem6 33968*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem7 33969	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑))
Theorem	wl-ax11-lem8 33970*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑))
Theorem	wl-ax11-lem9 33971	The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem10 33972*	We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 184 can be used in conjunction with wl-ax11-lem9 33971 to eliminate the second antecedent. Missing is something along the lines of ax-6 2021, 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 33973*	Variant of df-clab 2764, 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 2754, df-clel 2774 and df-cleq 2770. 𝑥 ∈ 𝐴 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 2109, ax-9 2116, or df-clel 2774. Theorem cleljust 2115 shows that a possible choice does not matter. The original df-clab 2764 can be rederived, see wl-dfclab 33974. 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 33974	Rederive df-clab 2764 from wl-clabv 33973. (Contributed by Wolf Lammen, 31-May-2023.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	wl-clabtv 33975*	Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 33976. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
Theorem	wl-clabt 33976	Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 33975. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
20.17.5  1. Restricted Quantifiers
Syntax	wl-ral 33977	Redefine the restricted universal quantifier context to avoid overloading and syntax check errors in mmj2. This operator does not require 𝑥 and 𝐵 disjoint.
wff ∀𝑥 in 𝐵𝜑
Syntax	wl-rex 33978	Redefine the restricted existential quantifier context to avoid overloading and syntax check errors in mmj2. This operator does not require 𝑥 and 𝐵 disjoint.
wff ∃𝑥 in 𝐵𝜑
Syntax	wl-rmo 33979	Redefine the restricted "at most one" quantifier context to avoid overloading and syntax check errors in mmj2. This operator does not require 𝑥 and 𝐵 disjoint.
wff ∃*𝑥 in 𝐵𝜑
Syntax	wl-reu 33980	Redefine the restricted existential uniqueness context to avoid overloading and syntax check errors in mmj2. This operator does not require 𝑥 and 𝐵 disjoint.
wff ∃!𝑥 in 𝐵𝜑
Syntax	wl-crab 33981	Redefine extended class notation to include the restricted class abstraction (class builder).
class {𝑥 in 𝐴 ∣ 𝜑}
Definition	df-wl-ral 33982*	Define an improved restricted universal quantifier. This version does not interpret elementhood verbatim in ∀𝑥 in 𝐴𝜑. Assuming a real elementhood leads to awkward consequences should the class 𝐴 depend on 𝑥. Instead a dummy variable 𝑦, disjoint from all other variables, is introduced to describe an element in 𝐴. The subexpression ∀𝑥(𝑥 = 𝑦 → 𝜑) is [𝑦 / 𝑥]𝜑 in disguise (see wl-dfralsb 33983). This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurences in 𝜑 are fully honored. If 𝑥 is not free in 𝐴, a simplification is possible ( see wl-dfralf 33985, wl-dfralv 33987). (Contributed by NM, 19-Aug-1993.) Isolate x from A, idea of Mario Carneiro. (Revised by Wolf Lammen, 21-May-2023.)
⊢ (∀𝑥 in 𝐴𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	wl-dfralsb 33983*	An alternate definition of restricted universal quantification (df-wl-ral 33982) using substitution. (Contributed by Wolf Lammen, 25-May-2023.)
⊢ (∀𝑥 in 𝐴𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → [𝑦 / 𝑥]𝜑))
Theorem	wl-dfralflem 33984*	Lemma for wl-dfralf 33985 and wl-dfralv . (Contributed by Wolf Lammen, 23-May-2023.)
⊢ (∀𝑦∀𝑥(𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	wl-dfralf 33985	Restricted universal quantification (df-wl-ral 33982) allows a simplification, if we can assume all appearences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 23-May-2023.)
⊢ (Ⅎ𝑥𝐴 → (∀𝑥 in 𝐴𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)))
Theorem	wl-dfralfi 33986	Restricted universal quantification (df-wl-ral 33982) allows allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 26-May-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∀𝑥 in 𝐴𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Theorem	wl-dfralv 33987*	Alternate definition of restricted universal quantification (df-wl-ral ) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 23-May-2023.)
⊢ (∀𝑥 in 𝐴𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
Definition	df-wl-rex 33988	Define an improved restricted existential quantifier. This version does not interpret elementhood verbatim in ∃𝑥 in 𝐴𝜑. Assuming a real elementhood leads to awkward consequences should the class 𝐴 depend on 𝑥. Instead we base the definiton on df-wl-ral 33982, where this is already cleanly handled. Alternate definitions are wl-dfrexsb 33993 and wl-dfrexex 33992. If 𝑥 is not free in 𝐴, the defining expression can be simplified (see wl-dfrexf 33989, wl-dfrexv 33991). This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurences in 𝜑 are fully honored. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 25-May-2023.)
⊢ (∃𝑥 in 𝐴𝜑 ↔ ¬ ∀𝑥 in 𝐴 ¬ 𝜑)
Theorem	wl-dfrexf 33989	Restricted existential quantification (df-wl-rex 33988) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 25-May-2023.)
⊢ (Ⅎ𝑥𝐴 → (∃𝑥 in 𝐴𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
Theorem	wl-dfrexfi 33990	Restricted universal quantification (df-wl-rex 33988) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 26-May-2023.)
⊢ Ⅎ𝑥𝐴    ⇒   ⊢ (∃𝑥 in 𝐴𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	wl-dfrexv 33991*	Alternate definition of restricted universal quantification (df-wl-rex 33988) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 25-May-2023.)
⊢ (∃𝑥 in 𝐴𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	wl-dfrexex 33992*	Alternate definition of the restricted existential quantification (df-wl-rex 33988), according to the pattern given in df-wl-ral 33982. (Contributed by Wolf Lammen, 25-May-2023.)
⊢ (∃𝑥 in 𝐴𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
Theorem	wl-dfrexsb 33993*	An alternate definition of restricted existential quantification (df-wl-rex 33988) using substitution. (Contributed by Wolf Lammen, 25-May-2023.)
⊢ (∃𝑥 in 𝐴𝜑 ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑))
Definition	df-wl-rmo 33994*	Define an improved restricted "at most one". This version does not interpret elementhood verbatim in ∃*𝑥 in 𝐴𝜑. Assuming a real elementhood leads to awkward consequences should the class 𝐴 depend on 𝑥. Instead we base the definiton on df-wl-ral 33982, where this is already cleanly handled. This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurences in 𝜑 are fully honored. Alternate definitions are given in wl-dfrmosb 33995 and, if 𝑥 is not free in 𝐴, wl-dfrmov 33996 and wl-dfrmof 33997. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 26-May-2023.)
⊢ (∃*𝑥 in 𝐴𝜑 ↔ ∃𝑦∀𝑥 in 𝐴(𝜑 → 𝑥 = 𝑦))
Theorem	wl-dfrmosb 33995*	An alternate definition of restricted "at most one" (df-wl-rmo 33994) using substitution. (Contributed by Wolf Lammen, 27-May-2023.)
⊢ (∃*𝑥 in 𝐴𝜑 ↔ ∃*𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑))
Theorem	wl-dfrmov 33996*	Alternate definition of restricted "at most one" (df-wl-rmo 33994) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 28-May-2023.)
⊢ (∃*𝑥 in 𝐴𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
Theorem	wl-dfrmof 33997	Restricted "at most one" (df-wl-rmo 33994) allows a simplification, if we can assume all occurrences of 𝑥 in 𝐴 are bounded. (Contributed by Wolf Lammen, 28-May-2023.)
⊢ (Ⅎ𝑥𝐴 → (∃*𝑥 in 𝐴𝜑 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)))
Definition	df-wl-reu 33998	Define an improved restricted existential uniqueness. This version does not interpret elementhood verbatim in ∃!𝑥 in 𝐴𝜑. Assuming a real elementhood leads to awkward consequences should the class 𝐴 depend on 𝑥. Instead we base the definiton on df-wl-ral 33982, where this is already cleanly handled. This definition lets 𝑥 appear as a formal parameter with no connection to 𝐴, but occurences in 𝜑 are fully honored. Alternate definitions are given in wl-dfreusb 33999 and, if 𝑥 is not free in 𝐴, wl-dfreuv 34000 and wl-dfreuf 34001. (Contributed by NM, 30-Aug-1993.) Isolate x from A. (Revised by Wolf Lammen, 28-May-2023.)
⊢ (∃!𝑥 in 𝐴𝜑 ↔ (∃𝑥 in 𝐴𝜑 ∧ ∃*𝑥 in 𝐴𝜑))
Theorem	wl-dfreusb 33999*	An alternate definition of restricted existential uniqueness (df-wl-reu 33998) using substitution. (Contributed by Wolf Lammen, 28-May-2023.)
⊢ (∃!𝑥 in 𝐴𝜑 ↔ ∃!𝑦(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑))
Theorem	wl-dfreuv 34000*	Alternate definition of restricted existential uniqueness (df-wl-reu 33998) when 𝑥 and 𝐴 are disjoint. (Contributed by Wolf Lammen, 28-May-2023.)
⊢ (∃!𝑥 in 𝐴𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))