P. 370 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36901-37000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wl-df3-3mintru2 36901	The adder carry in conjunctive normal form. An alternative highly symmetric definition emphasizing the independence of order of the inputs 𝜑, 𝜓 and 𝜒. Copy of cadan 1603. (Contributed by Mario Carneiro, 4-Sep-2016.) df-cad redefined. (Revised by Wolf Lammen, 18-Jun-2024.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜒)))
Theorem	wl-df4-3mintru2 36902	An alternative definition of the adder carry. Copy of df-cad 1601. (Contributed by Mario Carneiro, 4-Sep-2016.) df-cad redefined. (Revised by Wolf Lammen, 19-Jun-2024.)
⊢ (cadd(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (𝜒 ∧ (𝜑 ⊻ 𝜓))))
Theorem	wl-1mintru1 36903	Using the recursion formula: "(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" ) for "1-mintru-1" (meaning "at least 1 out of 1 input is true") by plugging in n = 0, m = 0, and simplifying. The expressions "0-mintru-0" and "0-mintru-1" are base cases of the recursion, meaning "in a sequence of zero inputs, at least 0 / 1 input is true", respectively equvalent to ⊤ / ⊥. Negating an "n-mintru1" operation means: All n inputs 𝜑.. 𝜃 are false. This is also conveniently expressed as ¬ (𝜑 ∨.. ∨ 𝜃). Applying this idea here (n = 1) yields the obvious result that in an input sequence of size 1 only then all will be false, if its single input is. (Contributed by Wolf Lammen, 10-May-2024.)
⊢ (if-(𝜒, ⊤, ⊥) ↔ 𝜒)
Theorem	wl-1mintru2 36904	Using the recursion formula: "(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" ) for "1-mintru-2" (meaning "at least 2 out of a single input are true") by plugging in n = 0, m = 1, and simplifying. The expressions "0-mintru-1" and "0-mintru-2" are base cases of the recursion, meaning "in a sequence of zero inputs at least 1 / 2 input is true", evaluate both to ⊥. Since no sequence of inputs has a longer subsequence of whatever property, the resulting ⊥ is to be expected. Negating a "n-mintru2" operation has an interesting interpretation: at most one input is true, so all inputs exclude each other mutually. Such an exclusion is expressed by a NAND operation (𝜑 ⊼ 𝜓), not by a XOR. Applying this idea here (n = 1) leads to the obvious "In a single input sequence 'at most one is true' always holds". (Contributed by Wolf Lammen, 10-May-2024.)
⊢ (if-(𝜒, ⊥, ⊥) ↔ ⊥)
Theorem	wl-2mintru1 36905	Using the recursion formula "(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" ) for "2-mintru-1" (meaning "at least 1 out of 2 inputs is true") by plugging in n = 1, m = 0, and simplifying. The expression "1-mintru-0" is a base case (meaning at least zero inputs out of 1 are true), evaluating to ⊤, and wl-1mintru1 36903 shows "1-mintru-1" is equivalent to the only input. Negating an "n-mintru1" operation means: All n inputs 𝜑.. 𝜃 are false. This is also conveniently expressed as ¬ (𝜑 ∨.. ∨ 𝜃), in accordance with the result here. (Contributed by Wolf Lammen, 10-May-2024.)
⊢ (if-(𝜓, ⊤, 𝜒) ↔ (𝜓 ∨ 𝜒))
Theorem	wl-2mintru2 36906	Using the recursion formula "(n+1)-mintru-(m+1)" ↔ if-(𝜑, "n-mintru-m" , "n-mintru-(m+1)" ) for "2-mintru-2" (meaning "2 out of 2 inputs are true") by plugging in n = 1, m = 1, and simplifying. See wl-1mintru1 36903 and wl-1mintru2 36904 to see that "1-mintru-1" / "1-mintru-2" evaluate to 𝜒 / ⊥ respectively. Negating a "n-mintru2" operation means 'at most one input is true', so all inputs exclude each other mutually. Such an exclusion is expressed by a NAND operation (𝜑 ⊼ 𝜓), not by a XOR. Applying this idea here (n = 2) yields the expected NAND in case of a pair of inputs. (Contributed by Wolf Lammen, 10-May-2024.)
⊢ (if-(𝜓, 𝜒, ⊥) ↔ (𝜓 ∧ 𝜒))
Theorem	wl-df3maxtru1 36907	Assuming "(n+1)-maxtru1" ↔ ¬ "(n+1)-mintru-2", we can deduce from the recursion formula given in wl-df-3mintru2 36899, that a similiar one "(n+1)-maxtru1" ↔ if-(𝜑,-. "n-mintru-1" , "n-maxtru1" ) is valid for expressing 'at most one input is true'. This can also be rephrased as a mutual exclusivity of propositional expressions (no two of a sequence of inputs can simultaniously be true). Of course, this suggests that all inputs depend on variables 𝜂, 𝜁... Whatever wellformed expression we plugin for these variables, it will render at most one of the inputs true. The here introduced mutual exclusivity is possibly useful for case studies, where we want the cases be sort of 'disjoint'. One can further imagine that a complete case scenario demands that the 'at most' is sharpened to 'exactly one'. This does not impose any difficulty here, as one of the inputs will then be the negation of all others be or'ed. As one input is determined, 'at most one' is sufficient to describe the general form here. Since cadd is an alias for 'at least 2 out of three are true', its negation is under focus here. (Contributed by Wolf Lammen, 23-Jun-2024.)
⊢ (¬ cadd(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, (𝜓 ⊽ 𝜒), (𝜓 ⊼ 𝜒)))
21.20.5  An alternative axiom ~ ax-13
Axiom	ax-wl-13v 36908*	A version of ax13v 2367 with a distinctor instead of a distinct variable condition. Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1906. So essentially this theorem states, that a distinct variable condition between set variables can be replaced with a distinctor expression. (Contributed by Wolf Lammen, 23-Jul-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧))
Theorem	wl-ax13lem1 36909*	A version of ax-wl-13v 36908 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. This proof bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 23-Jul-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
21.20.6  Other stuff
Theorem	wl-mps 36910	Replacing a nested consequent. A sort of modus ponens in antecedent position. (Contributed by Wolf Lammen, 20-Sep-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → (𝜓 → 𝜒))    &   ⊢ ((𝜑 → 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜃)
Theorem	wl-syls1 36911	Replacing a nested consequent. A sort of syllogism in antecedent position. (Contributed by Wolf Lammen, 20-Sep-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜓 → 𝜒)    &   ⊢ ((𝜑 → 𝜒) → 𝜃)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜃)
Theorem	wl-syls2 36912	Replacing a nested antecedent. A sort of syllogism in antecedent position. (Contributed by Wolf Lammen, 20-Sep-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝜓)    &   ⊢ ((𝜑 → 𝜒) → 𝜃)    ⇒   ⊢ ((𝜓 → 𝜒) → 𝜃)
Theorem	wl-embant 36913	A true wff can always be added as a nested antecedent to an antecedent. Note: this theorem is intuitionistically valid. (Contributed by Wolf Lammen, 4-Oct-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝜑    &   ⊢ (𝜓 → 𝜒)    ⇒   ⊢ ((𝜑 → 𝜓) → 𝜒)
Theorem	wl-orel12 36914	In a conjunctive normal form a pair of nodes like (𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ 𝜒) eliminates the need of a node (𝜓 ∨ 𝜒). This theorem allows simplifications in that respect. (Contributed by Wolf Lammen, 20-Jun-2020.)
⊢ (((𝜑 ∨ 𝜓) ∧ (¬ 𝜑 ∨ 𝜒)) → (𝜓 ∨ 𝜒))
Theorem	wl-cases2-dnf 36915	A particular instance of orddi 1008 and anddi 1009 converting between disjunctive and conjunctive normal forms, when both 𝜑 and ¬ 𝜑 appear. This theorem in fact rephrases cases2 1046, and is related to consensus 1051. I restate it here in DNF and CNF. The proof deliberately does not use df-ifp 1062 and dfifp4 1065, by which it can be shortened. (Contributed by Wolf Lammen, 21-Jun-2020.) (Proof modification is discouraged.)
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∧ (𝜑 ∨ 𝜒)))
Theorem	wl-cbvmotv 36916*	Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by Wolf Lammen, 5-Mar-2023.)
⊢ (∃*𝑥⊤ → ∃*𝑦⊤)
Theorem	wl-moteq 36917	Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by Wolf Lammen, 5-Mar-2023.)
⊢ (∃*𝑥⊤ → 𝑦 = 𝑧)
Theorem	wl-motae 36918	Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by Wolf Lammen, 5-Mar-2023.)
⊢ (∃*𝑢⊤ → ∀𝑥 𝑦 = 𝑧)
Theorem	wl-moae 36919*	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 1964 in the proof, that ensures "at least one thing exists". For other equivalences see wl-euae 36920 and exists1 2651. Gerard Lang pointed out, that ∃𝑦∀𝑥𝑥 = 𝑦 with disjoint 𝑥 and 𝑦 (df-mo 2529, trut 1540) 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 36920*	Two ways to express "exactly one thing exists" . (Contributed by Wolf Lammen, 5-Mar-2023.)
⊢ (∃!𝑥⊤ ↔ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-nax6im 36921*	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 1959 requires us to formally assign a boolean value to an equation, say always false, unless you want to give up on exmid 893, for example. Whatever it is, we start out with the contraposition of ax-6 1964, 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 of discourse could be. (Contributed by Wolf Lammen, 12-Mar-2023.)
⊢ (¬ ∃𝑥 𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ (¬ ∃𝑥⊤ → 𝜑)
Theorem	wl-hbae1 36922	This specialization of hbae 2425 does not depend on ax-11 2147. (Contributed by Wolf Lammen, 8-Aug-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦∀𝑥 𝑥 = 𝑦)
Theorem	wl-naevhba1v 36923*	An instance of hbn1w 2042 applied to equality. (Contributed by Wolf Lammen, 7-Apr-2021.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-spae 36924	Prove an instance of sp 2169 from ax-13 2366 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 2164. Note that this theorem is also provable from ax-12 2164 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 1978 and spaev 2048 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.)
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦)
Theorem	wl-speqv 36925*	Under the assumption ¬ 𝑥 = 𝑦 a specialized version of sp 2169 is provable from Tarski's FOL and ax13v 2367 only. Note that this reverts the implication in ax13lem1 2368, so in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (∀𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦))
Theorem	wl-19.8eqv 36926*	Under the assumption ¬ 𝑥 = 𝑦 a specialized version of 19.8a 2167 is provable from Tarski's FOL and ax13v 2367 only. Note that this reverts the implication in ax13lem2 2370, so in fact (¬ 𝑥 = 𝑦 → (∃𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∃𝑥 𝑧 = 𝑦))
Theorem	wl-19.2reqv 36927*	Under the assumption ¬ 𝑥 = 𝑦 the reverse direction of 19.2 1973 is provable from Tarski's FOL and ax13v 2367 only. Note that in conjunction with 19.2 1973 in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ ∃𝑥𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.)
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
Theorem	wl-nfalv 36928*	If 𝑥 is not present in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Wolf Lammen, 11-Jan-2020.)
⊢ Ⅎ𝑥∀𝑦𝜑
Theorem	wl-nfimf1 36929	An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim 1892 in dvelimdf 2443 to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018.)
⊢ (∀𝑥𝜑 → (Ⅎ𝑥(𝜑 → 𝜓) ↔ Ⅎ𝑥𝜓))
Theorem	wl-nfae1 36930	Unlike nfae 2427, this specialized theorem avoids ax-11 2147. (Contributed by Wolf Lammen, 26-Jun-2019.)
⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑥
Theorem	wl-nfnae1 36931	Unlike nfnae 2428, this specialized theorem avoids ax-11 2147. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑥
Theorem	wl-aetr 36932	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑧))
Theorem	wl-axc11r 36933	Same as axc11r 2360, but using ax12 2417 instead of ax-12 2164 directly. This better reflects axiom usage in theorems dependent on it. (Contributed by NM, 25-Jul-2015.) Avoid direct use of ax-12 2164. (Revised by Wolf Lammen, 30-Mar-2024.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Theorem	wl-dral1d 36934	A version of dral1 2433 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 36946 and nf5di 2274 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)))
Theorem	wl-cbvalnaed 36935	wl-cbvalnae 36936 with a context. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜓))    &   ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒))    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))
Theorem	wl-cbvalnae 36936	A more general version of cbval 2392 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 2442, nfsb2 2477 or dveeq1 2374. (Contributed by Wolf Lammen, 4-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑)    &   ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓)
Theorem	wl-exeq 36937	The semantics of ∃𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-aleq 36938	The semantics of ∀𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.)
⊢ (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)))
Theorem	wl-nfeqfb 36939	Extend nfeqf 2375 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.)
⊢ (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))
Theorem	wl-nfs1t 36940	If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Closed form of nfs1 2482. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑)
Theorem	wl-equsalvw 36941*	Version of equsalv 2251 with a disjoint variable condition, and of equsal 2411 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 36942	Deduction version of equsal 2411. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ Ⅎ𝑥𝜑    &   ⊢ (𝜑 → Ⅎ𝑥𝜒)    &   ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)))    ⇒   ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒))
Theorem	wl-equsal 36943	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 36942 first, and then deriving more specialized versions wl-equsal 36943 and wl-equsal1t 36944 then is more efficient than the other way round, which is possible, too. See also equsal 2411. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.)
⊢ Ⅎ𝑥𝜓    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓)
Theorem	wl-equsal1t 36944	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 2411, spimt 2380 or sbft 2254, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.)
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑))
Theorem	wl-equsalcom 36945	This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑))
Theorem	wl-equsal1i 36946	The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.)
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑)    &   ⊢ (𝑥 = 𝑦 → 𝜑)    ⇒   ⊢ 𝜑
Theorem	wl-sb6rft 36947	A specialization of wl-equsal1t 36944. Closed form of sb6rf 2462. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)))
Theorem	wl-cbvalsbi 36948*	Change bounded variables in a special case. The reverse direction seems to involve ax-11 2147. My hope is that I will in some future be able to prove mo3 2553 with reversed quantifiers not using ax-11 2147. See also the remark in mo4 2555, which lead me to this effort. (Contributed by Wolf Lammen, 5-Mar-2024.)
⊢ (∀𝑥𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	wl-sbrimt 36949	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2293. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)))
Theorem	wl-sblimt 36950	Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2293. (Contributed by Wolf Lammen, 26-Jul-2019.)
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)))
Theorem	wl-sb9v 36951*	Commutation of quantification and substitution variables based on fewer axioms than sb9 2513. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)
Theorem	wl-sb8ft 36952*	Substitution of variable in universal quantifier. Closed form of sb8f 2344. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8eft 36953*	Substitution of variable in existentialal quantifier. Closed form of sb8ef 2346. (Contributed by Wolf Lammen, 27-Apr-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8t 36954	Substitution of variable in universal quantifier. Closed form of sb8 2511. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8et 36955	Substitution of variable in universal quantifier. Closed form of sb8e 2512. (Contributed by Wolf Lammen, 27-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sbhbt 36956	Closed form of sbhb 2515. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-sbnf1 36957	Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2349. Note: This theorem shows that sbnf2 2349 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)))
Theorem	wl-equsb3 36958	equsb3 2094 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.)
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧))
Theorem	wl-equsb4 36959	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 36960	Version of 2sb6 2082 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    ⇒   ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓)))
Theorem	wl-sbcom2d-lem1 36961*	Lemma used to prove wl-sbcom2d 36963. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑)))
Theorem	wl-sbcom2d-lem2 36962*	Lemma used to prove wl-sbcom2d 36963. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.)
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑)))
Theorem	wl-sbcom2d 36963	Version of sbcom2 2154 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.)
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤)    &   ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧)    &   ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦)    ⇒   ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓))
Theorem	wl-sbalnae 36964	A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal1 36965*	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 36964 now. See also sbal1 2522. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-sbal2 36966*	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 36964 now. See also sbal2 2523. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑))
Theorem	wl-2spsbbi 36967	spsbbi 2069 applied twice. (Contributed by Wolf Lammen, 5-Aug-2023.)
⊢ (∀𝑎∀𝑏(𝜑 ↔ 𝜓) → ([𝑦 / 𝑏][𝑥 / 𝑎]𝜑 ↔ [𝑦 / 𝑏][𝑥 / 𝑎]𝜓))
Theorem	wl-lem-exsb 36968*	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
Theorem	wl-lem-nexmo 36969	This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.)
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧))
Theorem	wl-lem-moexsb 36970*	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 36971	This theorem extends alanimi 1811 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.)
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))    ⇒   ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒))
Theorem	wl-mo2df 36972	Version of mof 2552 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 36973	Closed form of mof 2552 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-eudf 36974	Version of eu6 2563 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 36975	Closed form of eu6 2563 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
Theorem	wl-euequf 36976	euequ 2586 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦)
Theorem	wl-mo2t 36977*	Closed form of mof 2552. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
Theorem	wl-mo3t 36978*	Closed form of mo3 2553. (Contributed by Wolf Lammen, 18-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
Theorem	wl-nfsbtv 36979*	Closed form of nfsbv 2318. (Contributed by Wolf Lammen, 2-May-2025.)
⊢ (∀𝑥Ⅎ𝑧𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)
Theorem	wl-sb8eut 36980	Substitution of variable in universal quantifier. Closed form of sb8eu 2589. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8eutv 36981*	Substitution of variable in universal quantifier. Closed form of sb8euv 2588. (Contributed by Wolf Lammen, 3-May-2025.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8mot 36982	Substitution of variable in universal quantifier. Closed form of sb8mo 2590. (Contributed by Wolf Lammen, 11-Aug-2019.)
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑))
Theorem	wl-sb8motv 36983*	Substitution of variable in universal quantifier. Closed form of sb8mo 2590 without ax-13 2366, but requiring 𝑥 and 𝑦 being disjoint. This theorem relates to wl-mo3t 36978, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2254 and sbco 2501. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 36978 in a simple fashion. From an educational standpoint, one would assume wl-mo3t 36978 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 36984	A closed form of issetf 3484. The proof here is a modification of a subproof in vtoclgft 3536, where it could be used to shorten the proof. (Contributed by Wolf Lammen, 25-Jan-2025.)
⊢ (Ⅎ𝑥𝐴 → (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴))
Theorem	wl-axc11rc11 36985	Proving axc11r 2360 from axc11 2424. The hypotheses are two instances of axc11 2424 used in the proof here. Some systems introduce axc11 2424 as an axiom, see for example System S2 in https://us.metamath.org/downloads/finiteaxiom.pdf 2424. By contrast, this database sees the variant axc11r 2360, directly derived from ax-12 2164, as foundational. Later axc11 2424 is proven somewhat trickily, requiring ax-10 2130 and ax-13 2366, see its proof. (Contributed by Wolf Lammen, 18-Jul-2023.)
⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑦 𝑦 = 𝑥 → ∀𝑥 𝑦 = 𝑥))    &   ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑))    ⇒   ⊢ (∀𝑦 𝑦 = 𝑥 → (∀𝑥𝜑 → ∀𝑦𝜑))
Axiom	ax-wl-11v 36986*	Version of ax-11 2147 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2147. It will later be converted into a theorem directly based on ax-11 2147. (Contributed by Wolf Lammen, 28-Jun-2019.)
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑)
Theorem	wl-ax11-lem1 36987	A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧))
Theorem	wl-ax11-lem2 36988*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦)
Theorem	wl-ax11-lem3 36989*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦)
Theorem	wl-ax11-lem4 36990*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦)
Theorem	wl-ax11-lem5 36991	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑))
Theorem	wl-ax11-lem6 36992*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem7 36993	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑))
Theorem	wl-ax11-lem8 36994*	Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑))
Theorem	wl-ax11-lem9 36995	The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.)
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑))
Theorem	wl-ax11-lem10 36996*	We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 191 can be used in conjunction with wl-ax11-lem9 36995 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 36997*	Variant of df-clab 2705, 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 2698, df-clel 2805 and df-cleq 2719. 𝑥 ∈ 𝐴 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 2101, ax-9 2109, or df-clel 2805. Theorem cleljust 2108 shows that a possible choice does not matter. The original df-clab 2705 can be rederived, see wl-dfclab 36998. 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 36998	Rederive df-clab 2705 from wl-clabv 36997. (Contributed by Wolf Lammen, 31-May-2023.) (Proof modification is discouraged.)
⊢ (𝑥 ∈ {𝑦 ∣ 𝜑} ↔ [𝑥 / 𝑦]𝜑)
Theorem	wl-clabtv 36999*	Using class abstraction in a context, requiring 𝑥 and 𝜑 disjoint, but based on fewer axioms than wl-clabt 37000. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})
Theorem	wl-clabt 37000	Using class abstraction in a context. For a version based on fewer axioms see wl-clabtv 36999. (Contributed by Wolf Lammen, 29-May-2023.)
⊢ Ⅎ𝑥𝜑    ⇒   ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)})