![]() |
Metamath
Proof Explorer Theorem List (p. 337 of 431) | < 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-28076) |
![]() (28077-29601) |
![]() (29602-43056) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wl-dfnan2 33601 | An alternative definition of "nand" based on imnan 437. See df-nan 1589 for the original definition. This theorem allows various shortenings. (Contributed by Wolf Lammen, 26-Jun-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜑 → ¬ 𝜓)) | ||
Theorem | wl-nancom 33602 | The 'nand' operator commutes. (Contributed by Mario Carneiro, 9-May-2015.) (Revised by Wolf Lammen, 26-Jun-2020.) |
⊢ ((𝜑 ⊼ 𝜓) ↔ (𝜓 ⊼ 𝜑)) | ||
Theorem | wl-nannan 33603 | Lemma for handling nested 'nand's. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Revised by Wolf Lammen, 26-Jun-2020.) |
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) | ||
Theorem | wl-nannot 33604 | Show equivalence between negation and the Nicod version. To derive nic-dfneg 1736, apply nanbi 1595. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Revised by Wolf Lammen, 26-Jun-2020.) |
⊢ (¬ 𝜑 ↔ (𝜑 ⊼ 𝜑)) | ||
Theorem | wl-nanbi1 33605 | Introduce a right anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) (Revised by Wolf Lammen, 27-Jun-2020.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒))) | ||
Theorem | wl-nanbi2 33606 | Introduce a left anti-conjunct to both sides of a logical equivalence. (Contributed by SF, 2-Jan-2018.) (Revised by Wolf Lammen, 27-Jun-2020.) |
⊢ ((𝜑 ↔ 𝜓) → ((𝜑 ⊼ 𝜒) ↔ (𝜓 ⊼ 𝜒))) | ||
Theorem | wl-naev 33607* | 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 33608 | This specialization of hbae 2449 does not depend on ax-11 2175. (Contributed by Wolf Lammen, 8-Aug-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑦∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-naevhba1v 33609* | An instance of hbn1w 2116 applied to equality. (Contributed by Wolf Lammen, 7-Apr-2021.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑥 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-hbnaev 33610* | Any variable is free in ¬ ∀𝑥𝑥 = 𝑦, if 𝑥 and 𝑦 are distinct. The latter condition can actually be lifted, but this version is easier to prove. The proof does not use ax-10 2160. (Contributed by Wolf Lammen, 9-Apr-2021.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-spae 33611 |
Prove an instance of sp 2192 from ax-13 2383 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 2188. Note that this theorem is also provable from ax-12 2188 alone, so you can pick the axiom it is based on. Compare this result to 19.3v 2055 and spaev 2121 having distinct variable conditions, but a smaller footprint on axiom usage. (Contributed by Wolf Lammen, 5-Apr-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) | ||
Theorem | wl-cbv3vv 33612* | Avoiding ax-11 2175. (Contributed by Wolf Lammen, 30-Aug-2021.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | wl-speqv 33613* | Under the assumption ¬ 𝑥 = 𝑦 a specialized version of sp 2192 is provable from Tarski's FOL and ax13v 2384 only. Note that this reverts the implication in ax13lem1 2385, so in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.) |
⊢ (¬ 𝑥 = 𝑦 → (∀𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦)) | ||
Theorem | wl-19.8eqv 33614* | Under the assumption ¬ 𝑥 = 𝑦 a specialized version of 19.8a 2191 is provable from Tarski's FOL and ax13v 2384 only. Note that this reverts the implication in ax13lem2 2433, so in fact (¬ 𝑥 = 𝑦 → (∃𝑥𝑧 = 𝑦 ↔ 𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∃𝑥 𝑧 = 𝑦)) | ||
Theorem | wl-19.2reqv 33615* | Under the assumption ¬ 𝑥 = 𝑦 the reverse direction of 19.2 2050 is provable from Tarski's FOL and ax13v 2384 only. Note that in conjunction with 19.2 2050 in fact (¬ 𝑥 = 𝑦 → (∀𝑥𝑧 = 𝑦 ↔ ∃𝑥𝑧 = 𝑦)) holds. (Contributed by Wolf Lammen, 17-Apr-2021.) |
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | wl-dveeq12 33616* | The current form of ax-13 2383 has a particular disadvantage: The condition ¬ 𝑥 = 𝑦 is less versatile than the general form ¬ ∀𝑥𝑥 = 𝑦. You need ax-10 2160 to arrive at the more general form presented here. You need 19.8a 2191 (or ax-12 2188) to restore 𝑦 = 𝑧 from ∃𝑥𝑦 = 𝑧 again. (Contributed by Wolf Lammen, 9-Jun-2021.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | wl-nfalv 33617* | If 𝑥 is not present in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Wolf Lammen, 11-Jan-2020.) |
⊢ Ⅎ𝑥∀𝑦𝜑 | ||
Theorem | wl-nfimf1 33618 | An antecedent is irrelevant to a not-free property, if it always holds. I used this variant of nfim 1966 in dvelimdf 2467 to simplify the proof. (Contributed by Wolf Lammen, 14-Oct-2018.) |
⊢ (∀𝑥𝜑 → (Ⅎ𝑥(𝜑 → 𝜓) ↔ Ⅎ𝑥𝜓)) | ||
Theorem | wl-nfnbi 33619 | Being free does not depend on an outside negation in an expression. This theorem is slightly more general than nfn 1925 or nfnd 1926. (Contributed by Wolf Lammen, 5-May-2018.) |
⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | wl-nfae1 33620 | Unlike nfae 2450, this specialized theorem avoids ax-11 2175. (Contributed by Wolf Lammen, 26-Jun-2019.) |
⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑥 | ||
Theorem | wl-nfnae1 33621 | Unlike nfnae 2452, this specialized theorem avoids ax-11 2175. (Contributed by Wolf Lammen, 27-Jun-2019.) |
⊢ Ⅎ𝑥 ¬ ∀𝑦 𝑦 = 𝑥 | ||
Theorem | wl-aetr 33622 | A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 → ∀𝑦 𝑦 = 𝑧)) | ||
Theorem | wl-dral1d 33623 | A version of dral1 2457 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 33634 and nf5di 2258 show that this is in fact pointless. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜓 ↔ ∀𝑦𝜒))) | ||
Theorem | wl-cbvalnaed 33624 | wl-cbvalnae 33625 with a context. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜓)) & ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | wl-cbvalnae 33625 | A more general version of cbval 2408 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 2466, nfsb2 2489 or dveeq1 2437. (Contributed by Wolf Lammen, 4-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝜑) & ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | wl-exeq 33626 | The semantics of ∃𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.) |
⊢ (∃𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∨ ∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥 𝑥 = 𝑧)) | ||
Theorem | wl-aleq 33627 | The semantics of ∀𝑥𝑦 = 𝑧. (Contributed by Wolf Lammen, 27-Apr-2018.) |
⊢ (∀𝑥 𝑦 = 𝑧 ↔ (𝑦 = 𝑧 ∧ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧))) | ||
Theorem | wl-nfeqfb 33628 | Extend nfeqf 2438 to an equivalence. (Contributed by Wolf Lammen, 31-Jul-2019.) |
⊢ (Ⅎ𝑥 𝑦 = 𝑧 ↔ (∀𝑥 𝑥 = 𝑦 ↔ ∀𝑥 𝑥 = 𝑧)) | ||
Theorem | wl-nfs1t 33629 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Closed form of nfs1 2494. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (Ⅎ𝑦𝜑 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | wl-equsald 33630 | Deduction version of equsal 2428. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜓) ↔ 𝜒)) | ||
Theorem | wl-equsal 33631 | 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 33630 first, and then deriving more specialized versions wl-equsal 33631 and wl-equsal1t 33632 then is more efficient than the other way round, which is possible, too. See also equsal 2428. (Revised by Wolf Lammen, 27-Jul-2019.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | wl-equsal1t 33632 |
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 2428, spimt 2390 or sbft 2508, to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜑)) | ||
Theorem | wl-equsalcom 33633 | This simple equivalence eases substitution of one expression for the other. (Contributed by Wolf Lammen, 1-Sep-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ ∀𝑥(𝑦 = 𝑥 → 𝜑)) | ||
Theorem | wl-equsal1i 33634 | The antecedent 𝑥 = 𝑦 is irrelevant, if one or both setvar variables are not free in 𝜑. (Contributed by Wolf Lammen, 1-Sep-2018.) |
⊢ (Ⅎ𝑥𝜑 ∨ Ⅎ𝑦𝜑) & ⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | wl-sb6rft 33635 | A specialization of wl-equsal1t 33632. Closed form of sb6rf 2552. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (Ⅎ𝑥𝜑 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑))) | ||
Theorem | wl-sbrimt 33636 | Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2525. (Contributed by Wolf Lammen, 26-Jul-2019.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))) | ||
Theorem | wl-sblimt 33637 | Substitution with a variable not free in antecedent affects only the consequent. Closed form of sbrim 2525. (Contributed by Wolf Lammen, 26-Jul-2019.) |
⊢ (Ⅎ𝑥𝜓 → ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓))) | ||
Theorem | wl-sb8t 33638 | Substitution of variable in universal quantifier. Closed form of sb8 2553. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8et 33639 | Substitution of variable in universal quantifier. Closed form of sb8e 2554. (Contributed by Wolf Lammen, 27-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sbhbt 33640 | Closed form of sbhb 2567. Characterizing the expression 𝜑 → ∀𝑥𝜑 using a substitution expression. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | wl-sbnf1 33641 | Two ways expressing that 𝑥 is effectively not free in 𝜑. Simplified version of sbnf2 2568. Note: This theorem shows that sbnf2 2568 has unnecessary distinct variable constraints. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (Ⅎ𝑥𝜑 ↔ ∀𝑥∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑))) | ||
Theorem | wl-equsb3 33642 | equsb3 2561 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧)) | ||
Theorem | wl-equsb4 33643 | 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 33644 | Version of sb6 2558 suitable for elimination of unnecessary dv restrictions. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | wl-sb5nae 33645 | Version of sb5 2559 suitable for elimination of unnecessary dv restrictions. (Contributed by Wolf Lammen, 28-Jul-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | wl-2sb6d 33646 | Version of 2sb6 2573 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.) |
⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑥) & ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑤) & ⊢ (𝜑 → ¬ ∀𝑦 𝑦 = 𝑧) & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧) ⇒ ⊢ (𝜑 → ([𝑧 / 𝑥][𝑤 / 𝑦]𝜓 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜓))) | ||
Theorem | wl-sbcom2d-lem1 33647* | Lemma used to prove wl-sbcom2d 33649. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.) |
⊢ ((𝑢 = 𝑦 ∧ 𝑣 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑤 → ([𝑢 / 𝑥][𝑣 / 𝑧]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑))) | ||
Theorem | wl-sbcom2d-lem2 33648* | Lemma used to prove wl-sbcom2d 33649. (Contributed by Wolf Lammen, 10-Aug-2019.) (New usage is discouraged.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → 𝜑))) | ||
Theorem | wl-sbcom2d 33649 | Version of sbcom2 2574 with a context, and distinct variable conditions replaced with distinctors. (Contributed by Wolf Lammen, 4-Aug-2019.) |
⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑤) & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑧) & ⊢ (𝜑 → ¬ ∀𝑧 𝑧 = 𝑦) ⇒ ⊢ (𝜑 → ([𝑤 / 𝑧][𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜓)) | ||
Theorem | wl-sbalnae 33650 | A theorem used in elimination of disjoint variable restrictions by replacing them with distinctors. (Contributed by Wolf Lammen, 25-Jul-2019.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal1 33651* | 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 33650 now. See also sbal1 2589. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-sbal2 33652* | 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 33650 now. See also sbal2 2590. (Revised by Wolf Lammen, 25-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | wl-lem-exsb 33653* | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | wl-lem-nexmo 33654 | This theorem provides a basic working step in proving theorems about ∃* or ∃!. (Contributed by Wolf Lammen, 3-Oct-2019.) |
⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑧)) | ||
Theorem | wl-lem-moexsb 33655* |
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 33656 | This theorem extends alanimi 1885 to a biconditional. Recurrent usage stacks up more quantifiers. (Contributed by Wolf Lammen, 4-Oct-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ (∀𝑥𝜑 ↔ (∀𝑥𝜓 ∧ ∀𝑥𝜒)) | ||
Theorem | wl-mo2df 33657 | Version of mo2 2608 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate dv conditions. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) & ⊢ (𝜑 → Ⅎ𝑦𝜓) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo2tf 33658 | Closed form of mo2 2608 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 20-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-eudf 33659 | Version of df-eu 2603 with a context and a distinctor replacing a distinct variable condition. This version should be used only to eliminate dv conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → ¬ ∀𝑥 𝑥 = 𝑦) & ⊢ (𝜑 → Ⅎ𝑦𝜓) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-eutf 33660 | Closed form of df-eu 2603 with a distinctor avoiding distinct variable conditions. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥Ⅎ𝑦𝜑) → (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) | ||
Theorem | wl-euequ1f 33661 | euequ1 2605 proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃!𝑥 𝑥 = 𝑦) | ||
Theorem | wl-mo2t 33662* | Closed form of mo2 2608. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | wl-mo3t 33663* | Closed form of mo3 2637. (Contributed by Wolf Lammen, 18-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | wl-sb8eut 33664 | Substitution of variable in universal quantifier. Closed form of sb8eu 2633. (Contributed by Wolf Lammen, 11-Aug-2019.) |
⊢ (∀𝑥Ⅎ𝑦𝜑 → (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑)) | ||
Theorem | wl-sb8mot 33665 |
Substitution of variable in universal quantifier. Closed form of
sb8mo 2634.
This theorem relates to wl-mo3t 33663, since replacing 𝜑 with [𝑦 / 𝑥]𝜑 in the latter yields subexpressions like [𝑥 / 𝑦][𝑦 / 𝑥]𝜑, which can be reduced to 𝜑 via sbft 2508 and sbco 2541. So ∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑 is provable from wl-mo3t 33663 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 33663 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 33666* | Version of ax-11 2175 with distinct variable conditions. Currently implemented as an axiom to detect unintended references to the foundational axiom ax-11 2175. It will later be converted into a theorem directly based on ax-11 2175. (Contributed by Wolf Lammen, 28-Jun-2019.) |
⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | wl-ax11-lem1 33667 | A transitive law for variable identifying expressions. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑦 𝑦 = 𝑧)) | ||
Theorem | wl-ax11-lem2 33668* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → ∀𝑥 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem3 33669* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑢 𝑢 = 𝑦) | ||
Theorem | wl-ax11-lem4 33670* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ Ⅎ𝑥(∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) | ||
Theorem | wl-ax11-lem5 33671 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑢 𝑢 = 𝑦 → (∀𝑢[𝑢 / 𝑦]𝜑 ↔ ∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem6 33672* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem7 33673 | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝜑) ↔ (¬ ∀𝑥 𝑥 = 𝑦 ∧ ∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem8 33674* | Lemma. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ ((∀𝑢 𝑢 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (∀𝑢∀𝑥[𝑢 / 𝑦]𝜑 ↔ ∀𝑦∀𝑥𝜑)) | ||
Theorem | wl-ax11-lem9 33675 | The easy part when 𝑥 coincides with 𝑦. (Contributed by Wolf Lammen, 30-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦∀𝑥𝜑 ↔ ∀𝑥∀𝑦𝜑)) | ||
Theorem | wl-ax11-lem10 33676* | We now have prepared everything. The unwanted variable 𝑢 is just in one place left. pm2.61 183 can be used in conjunction with wl-ax11-lem9 33675 to eliminate the second antecedent. Missing is something along the lines of ax-6 2046, 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-sbcom3 33677 |
Substituting 𝑦 for 𝑥 and then 𝑧 for
𝑦
is equivalent to
substituting 𝑧 for both 𝑥 and 𝑦. Copy
of ~? sbcom3OLD with
a shortened proof.
Keep this theorem for a while here because an external reference to it exists. (Contributed by Giovanni Mascellani, 8-Apr-2018.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑧 / 𝑦]𝜑) | ||
Syntax | wcel-wl 33678 | Redefine ∈ in a class context to avoid overloading and syntax check errors in mmj2. This operator requires 𝑥 and 𝐵 distinct. |
wff 𝑥 ∈ 𝐵 | ||
Theorem | wel-wl 33679 | Redefine ∈ in a set context to avoid syntax check errors in mmj2. 𝑥 and 𝑦 must be distinct. (Contributed by Wolf Lammen, 27-Nov-2021.) |
wff 𝑥 ∈ 𝑦 | ||
Syntax | wcel2-wl 33680 | Redefine ∈ in a class context to avoid overloading and syntax check errors in mmj2. 𝑥 and 𝐵 may not be distinct. |
wff 𝑥 ∈ 𝐵 | ||
Theorem | wel2-wl 33681 | Redefine ∈ in a set context to avoid syntax check errors in mmj2. It is no syntactic error to assign the same variable to 𝑥 and 𝑦. (Contributed by Wolf Lammen, 27-Nov-2021.) |
wff 𝑥 ∈ 𝑦 | ||
Axiom | ax-wl-8cl 33682* |
In ZFC, as presented in this document, classes are meant to be just a
notational convenience, that can be reduced to pure set theory by means
of df-clab 2739 (there stated in the eliminable property).
That is, in an
expression 𝑥 ∈ 𝐴, the class variable 𝐴 is
implicitely assumed
to represent an expression {𝑧 ∣ 𝜑} with some appropriate 𝜑.
Unfortunately, 𝜑 syntactically covers any well-formed
formula
(wff), including 𝑧 ∈ 𝐴. This choice inevitably breaks the
stated
property. And it potentially carries over to any expression containing
class variables. To fix this, a simple rule could exclude class
variables at all in a class defining wff. A more elaborate rule could
detect, and limit exclusion to proper classes (potentially problematic).
In any case, the verification process should enforce any such rule
during replacement, which it currently does not. The result is that we
rely on the awareness of theorem designers to this problem. It seems,
in ZFC proper classes are reduced to a few instances only, so a careful
study may reveal that this limited use does not impose logical loop
holes. It must be said, still, this necessary extra knowledge
contradicts the general philosophy of Metamath, trying to establish
certainty by a machine executable confirmation.
An extension to ZFC allows classes to exist on their own. Classes are then extensions to sets, also seamlessly extending the idea of elementhood. In order to move from the general to the specific, sets presuppose classes, so classes should be introduced first. This is somewhat in opposition to the classic order of introduction of syntactic elements, but has been carried out in the past, for example by the von-Neumann theory of classes. In the context of Metamath, which is a purely text-based syntactical concept, no semantics are imposed at the very beginning on classes. Instead axioms will narrow down bit by bit how elementhood behaves in proofs, of course always with the intuitive understanding of a human in mind. One basic property of elementhood we expect is that the 'element' is replaceable with something equal to it. Or that equality is finer grained than the elementhood relation. This idea is formally expressed in terms coined 'implicit substitution' in this document: ((𝑥 = 𝑦) → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)). This axiom prepares this notation. Note that particular constructions of classes like that in df-clab 2739 in fact allow to prove this axiom. Can we expect to eliminate this axiom then? No, the generalizing term still refers to an unexplained subterm 𝑥 ∈ 𝐴, so this axiom recurs in the general case. On the other hand, our axiom here stays true, even when just the existence of a class is known, as is often the case after applying the axiom of choice, without a chance to actually construct it. We provide a version of this axiom, that requires all variables to be distinct. Step by step these restrictions are lifted, in the end covering the most general term 𝐴 ∈ 𝐵. This axiom is meant as a replacement for ax-8 2133. (Contributed by Wolf Lammen, 27-Nov-2021.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) | ||
Theorem | wl-ax8clv1 33683* | Lifting the distinct variable constraint on 𝑥 and 𝑦 in ax-wl-8cl 33682. (Contributed by Wolf Lammen, 27-Nov-2021.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) | ||
Theorem | wl-clelv2-just 33684* | Show that the definition df-wl-clelv2 33685 is conservative. (Contributed by Wolf Lammen, 27-Nov-2021.) |
⊢ (𝑥 ∈ 𝐴 ↔ ∀𝑢(𝑢 = 𝑥 → 𝑢 ∈ 𝐴)) | ||
Definition | df-wl-clelv2 33685* | Define the term 𝑥 ∈ 𝐴, 𝑥 in 𝐴 permitted. (Contributed by Wolf Lammen, 27-Nov-2021.) |
⊢ (𝑥 ∈ 𝐴 ↔ ∀𝑢(𝑢 = 𝑥 → 𝑢 ∈ 𝐴)) | ||
Theorem | wl-ax8clv2 33686 | Axiom ax-wl-8cl 33682 carries over to our new definition df-wl-clelv2 33685. (Contributed by Wolf Lammen, 27-Nov-2021.) |
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) | ||
Theorem | rabiun 33687* | Abstraction restricted to an indexed union. (Contributed by Brendan Leahy, 26-Oct-2017.) |
⊢ {𝑥 ∈ ∪ 𝑦 ∈ 𝐴 𝐵 ∣ 𝜑} = ∪ 𝑦 ∈ 𝐴 {𝑥 ∈ 𝐵 ∣ 𝜑} | ||
Theorem | iundif1 33688* | Indexed union of class difference with the subtrahend held constant. (Contributed by Brendan Leahy, 6-Aug-2018.) |
⊢ ∪ 𝑥 ∈ 𝐴 (𝐵 ∖ 𝐶) = (∪ 𝑥 ∈ 𝐴 𝐵 ∖ 𝐶) | ||
Theorem | imadifss 33689 | The difference of images is a subset of the image of the difference. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐹 “ 𝐴) ∖ (𝐹 “ 𝐵)) ⊆ (𝐹 “ (𝐴 ∖ 𝐵)) | ||
Theorem | cureq 33690 | Equality theorem for currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → curry 𝐴 = curry 𝐵) | ||
Theorem | unceq 33691 | Equality theorem for uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐴 = 𝐵 → uncurry 𝐴 = uncurry 𝐵) | ||
Theorem | curf 33692 | Functional property of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → curry 𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵)) | ||
Theorem | uncf 33693 | Functional property of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) → uncurry 𝐹:(𝐴 × 𝐵)⟶𝐶) | ||
Theorem | curfv 33694 | Value of currying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ (((𝐹 Fn (𝑉 × 𝑊) ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝑊 ∈ 𝑋) → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) | ||
Theorem | uncov 33695 | Value of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴uncurry 𝐹𝐵) = ((𝐹‘𝐴)‘𝐵)) | ||
Theorem | curunc 33696 | Currying of uncurrying. (Contributed by Brendan Leahy, 2-Jun-2021.) |
⊢ ((𝐹:𝐴⟶(𝐶 ↑𝑚 𝐵) ∧ 𝐵 ≠ ∅) → curry uncurry 𝐹 = 𝐹) | ||
Theorem | unccur 33697 | Uncurrying of currying. (Contributed by Brendan Leahy, 5-Jun-2021.) |
⊢ ((𝐹:(𝐴 × 𝐵)⟶𝐶 ∧ 𝐵 ∈ (𝑉 ∖ {∅}) ∧ 𝐶 ∈ 𝑊) → uncurry curry 𝐹 = 𝐹) | ||
Theorem | phpreu 33698* | Theorem related to pigeonhole principle. (Contributed by Brendan Leahy, 21-Aug-2020.) |
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵) → (∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 = 𝐶 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 ∈ 𝐵 𝑥 = 𝐶)) | ||
Theorem | finixpnum 33699* | A finite Cartesian product of numerable sets is numerable. (Contributed by Brendan Leahy, 24-Feb-2019.) |
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ dom card) → X𝑥 ∈ 𝐴 𝐵 ∈ dom card) | ||
Theorem | fin2solem 33700* | Lemma for fin2so 33701. (Contributed by Brendan Leahy, 29-Jun-2019.) |
⊢ ((𝑅 Or 𝑥 ∧ (𝑦 ∈ 𝑥 ∧ 𝑧 ∈ 𝑥)) → (𝑦𝑅𝑧 → {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑦} [⊊] {𝑤 ∈ 𝑥 ∣ 𝑤𝑅𝑧})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |