![]() |
Metamath
Proof Explorer Theorem List (p. 340 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28364) |
![]() (28365-29889) |
![]() (29890-43671) |
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.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ (𝜑 → 𝜓)}) | ||
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 𝐴𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |