![]() |
Metamath
Proof Explorer Theorem List (p. 21 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-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.42vvv 2001* | Version of 19.42 2223 with three quantifiers and a disjoint variable condition requiring fewer axioms. (Contributed by NM, 21-Sep-2011.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥∃𝑦∃𝑧𝜓)) | ||
Theorem | exdistr2 2002* | Distribution of existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦∃𝑧𝜓)) | ||
Theorem | 3exdistr 2003* | Distribution of existential quantifiers in a triple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧𝜒))) | ||
Theorem | 4exdistr 2004* | Distribution of existential quantifiers in a quadruple conjunction. (Contributed by NM, 9-Mar-1995.) (Proof shortened by Wolf Lammen, 20-Jan-2018.) |
⊢ (∃𝑥∃𝑦∃𝑧∃𝑤((𝜑 ∧ 𝜓) ∧ (𝜒 ∧ 𝜃)) ↔ ∃𝑥(𝜑 ∧ ∃𝑦(𝜓 ∧ ∃𝑧(𝜒 ∧ ∃𝑤𝜃)))) | ||
The equality predicate was introduced above in wceq 1601 for use by df-tru 1605. See the comments in that section. In this section, we continue with its first "real" use. | ||
Theorem | weq 2005 |
Extend wff definition to include atomic formulas using the equality
predicate.
(Instead of introducing weq 2005 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 1601. This lets us avoid overloading the = connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 2005 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1601. Note: To see the proof steps of this syntax proof, type "MM> SHOW PROOF weq / ALL" in the Metamath program.) (Contributed by NM, 24-Jan-2006.) |
wff 𝑥 = 𝑦 | ||
Theorem | equs3 2006 | Lemma used in proofs of substitution properties. (Contributed by NM, 10-May-1993.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ¬ ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) | ||
Theorem | speimfw 2007 | Specialization, with additional weakening (compared to 19.2 2026) to allow bundling of 𝑥 and 𝑦. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Dec-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (¬ ∀𝑥 ¬ 𝑥 = 𝑦 → (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | speimfwALT 2008 | Alternate proof of speimfw 2007 (longer compressed proof, but fewer essential steps). (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Aug-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (¬ ∀𝑥 ¬ 𝑥 = 𝑦 → (∀𝑥𝜑 → ∃𝑥𝜓)) | ||
Theorem | spimfw 2009 | Specialization, with additional weakening (compared to sp 2167) to allow bundling of 𝑥 and 𝑦. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (¬ ∀𝑥 ¬ 𝑥 = 𝑦 → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | ax12i 2010 | Inference that has ax-12 2163 (without ∀𝑦) as its conclusion. Uses only Tarski's FOL axiom schemes. The hypotheses may be eliminable without using ax-12 2163 in special cases. Proof similar to Lemma 16 of [Tarski] p. 70. (Contributed by NM, 20-May-2008.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Syntax | wsb 2011 | Extend wff definition to include proper substitution (read "the wff that results when 𝑦 is properly substituted for 𝑥 in wff 𝜑"). (Contributed by NM, 24-Jan-2006.) |
wff [𝑦 / 𝑥]𝜑 | ||
Definition | df-sb 2012 |
Define proper substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the
preprint). For our notation, we use [𝑦 / 𝑥]𝜑 to mean "the wff
that results from the proper substitution of 𝑦 for 𝑥 in the
wff
𝜑". That is, 𝑦
properly replaces 𝑥. For example,
[𝑥 /
𝑦]𝑧 ∈ 𝑦 is the same as 𝑧 ∈ 𝑥, as shown in elsb4 2516. We
can also use [𝑦 / 𝑥]𝜑 in place of the "free for"
side condition
used in traditional predicate calculus; see, for example, stdpc4 2428.
Our notation was introduced in Haskell B. Curry's Foundations of Mathematical Logic (1977), p. 316 and is frequently used in textbooks of lambda calculus and combinatory logic. This notation improves the common but ambiguous notation, "𝜑(𝑦) is the wff that results when 𝑦 is properly substituted for 𝑥 in 𝜑(𝑥)". For example, if the original 𝜑(𝑥) is 𝑥 = 𝑦, then 𝜑(𝑦) is 𝑦 = 𝑦, from which we obtain that 𝜑(𝑥) is 𝑥 = 𝑥. So what exactly does 𝜑(𝑥) mean? Curry's notation solves this problem. In most books, proper substitution has a somewhat complicated recursive definition with multiple cases based on the occurrences of free and bound variables in the wff. Instead, we use a single formula that is exactly equivalent and gives us a direct definition. We later prove that our definition has the properties we expect of proper substitution (see theorems sbequ 2452, sbcom2 2523 and sbid2v 2490). Note that our definition is valid even when 𝑥 and 𝑦 are replaced with the same variable, as sbid 2232 shows. We achieve this by having 𝑥 free in the first conjunct and bound in the second. We can also achieve this by using a dummy variable, as the alternate definition dfsb7 2535 shows (which some logicians may prefer because it does not mix free and bound variables). Another version that mixes free and bound variables is dfsb3 2450. When 𝑥 and 𝑦 are distinct, we can express proper substitution with the simpler expressions of sb5 2251 and sb6 2250. There are no restrictions on any of the variables, including what variables may occur in wff 𝜑. (Contributed by NM, 10-May-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sbequ2 2013 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | ||
Theorem | sb1 2014 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2251) or a non-freeness hypothesis (sb5f 2462). (Contributed by NM, 13-May-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | spsbe 2015 | A specialization theorem. (Contributed by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥𝜑) | ||
Theorem | sbequ8 2016 | Elimination of equality from antecedent after substitution. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbimi 2017 | Infer substitution into antecedent and consequent of an implication. (Contributed by NM, 25-Jun-1998.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) | ||
Theorem | sbimdv 2018* | Deduction substituting both sides of an implication, with 𝜑 and 𝑥 disjoint. See also sbimd 2226. (Contributed by Wolf Lammen, 6-May-2023.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbbii 2019 | Infer substitution into both sides of a logical equivalence. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓) | ||
Theorem | sbbidv 2020* | Deduction substituting both sides of a biconditional, with 𝜑 and 𝑥 disjoint. See also sbbid 2227. (Contributed by Wolf Lammen, 6-May-2023.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Axiom | ax-6 2021 |
Axiom of Existence. One of the equality and substitution axioms of
predicate calculus with equality. This axiom tells us is that at least
one thing exists. In this form (not requiring that 𝑥 and 𝑦 be
distinct) it was used in an axiom system of Tarski (see Axiom B7' in
footnote 1 of [KalishMontague] p.
81.) It is equivalent to axiom scheme
C10' in [Megill] p. 448 (p. 16 of the
preprint); the equivalence is
established by axc10 2349 and ax6fromc10 35055. A more convenient form of this
axiom is ax6e 2347, which has additional remarks.
Raph Levien proved the independence of this axiom from the other logical axioms on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html. ax-6 2021 can be proved from the weaker version ax6v 2022 requiring that the variables be distinct; see theorem ax6 2348. ax-6 2021 can also be proved from the Axiom of Separation (in the form that we use that axiom, where free variables are not universally quantified). See theorem ax6vsep 5023. Except by ax6v 2022, this axiom should not be referenced directly. Instead, use theorem ax6 2348. (Contributed by NM, 10-Jan-1993.) (New usage is discouraged.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | ax6v 2022* |
Axiom B7 of [Tarski] p. 75, which requires that
𝑥
and 𝑦 be
distinct. This trivial proof is intended merely to weaken axiom ax-6 2021
by adding a distinct variable restriction ($d). From here on, ax-6 2021
should not be referenced directly by any other proof, so that theorem
ax6 2348 will show that we can recover ax-6 2021
from this weaker version if
it were an axiom (as it is in the case of Tarski).
Note: Introducing 𝑥, 𝑦 as a distinct variable group "out of the blue" with no apparent justification has puzzled some people, but it is perfectly sound. All we are doing is adding an additional prerequisite, similar to adding an unnecessary logical hypothesis, that results in a weakening of the theorem. This means that any future theorem that references ax6v 2022 must have a $d specified for the two variables that get substituted for 𝑥 and 𝑦. The $d does not propagate "backwards", i.e., it does not impose a requirement on ax-6 2021. When possible, use of this theorem rather than ax6 2348 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 7-Aug-2015.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | ax6ev 2023* | At least one individual exists. Weaker version of ax6e 2347. When possible, use of this theorem rather than ax6e 2347 is preferred since its derivation is much shorter and requires fewer axioms. (Contributed by NM, 3-Aug-2017.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | exgen 2024 | Rule of existential generalization, similar to universal generalization ax-gen 1839, but valid only if an individual exists. Its proof requires ax-6 2021 in our axiomatization but the equality predicate does not occur in its statement. Some fundamental theorems of predicate calculus can be proven from ax-gen 1839, ax-4 1853 and this theorem alone, not requiring ax-7 2055 or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.) (Proof shortened by Wolf Lammen, 9-Dec-2017.) |
⊢ 𝜑 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | extru 2025 | There exists a variable such that ⊤ holds; that is, there exists a variable. This corresponds under the standard translation to one of the formulations of the modal axiom (D), the other being 19.2 2026. (Contributed by Anthony Hart, 13-Sep-2011.) (Proof shortened by BJ, 12-May-2019.) |
⊢ ∃𝑥⊤ | ||
Theorem | 19.2 2026 | Theorem 19.2 of [Margaris] p. 89. This corresponds to the axiom (D) of modal logic (the other standard formulation being extru 2025). Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 2172 for a more conventional proof of a more general result, which uses additional axioms. The reverse implication is the defining property of effective nonfreeness (see df-nf 1828). (Contributed by NM, 2-Aug-2017.) Remove dependency on ax-7 2055. (Revised by Wolf Lammen, 4-Dec-2017.) |
⊢ (∀𝑥𝜑 → ∃𝑥𝜑) | ||
Theorem | 19.2d 2027 | Deduction associated with 19.2 2026. (Contributed by BJ, 12-May-2019.) |
⊢ (𝜑 → ∀𝑥𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | 19.8w 2028 | Weak version of 19.8a 2166 and instance of 19.2d 2027. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) (Revised by BJ, 31-Mar-2021.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (𝜑 → ∃𝑥𝜑) | ||
Theorem | 19.8v 2029* | Version of 19.8a 2166 with a disjoint variable condition, requiring fewer axioms. Converse of ax5e 1955. (Contributed by BJ, 12-Mar-2020.) |
⊢ (𝜑 → ∃𝑥𝜑) | ||
Theorem | 19.9v 2030* | Version of 19.9 2190 with a disjoint variable condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 2031. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 2055. (Revised by Wolf Lammen, 4-Dec-2017.) |
⊢ (∃𝑥𝜑 ↔ 𝜑) | ||
Theorem | 19.3v 2031* | Version of 19.3 2186 with a disjoint variable condition, requiring fewer axioms. Any formula can be universally quantified using a variable which it does not contain. See also 19.9v 2030. (Contributed by Anthony Hart, 13-Sep-2011.) Remove dependency on ax-7 2055. (Revised by Wolf Lammen, 4-Dec-2017.) |
⊢ (∀𝑥𝜑 ↔ 𝜑) | ||
Theorem | spvw 2032* | Version of sp 2167 when 𝑥 does not occur in 𝜑. Converse of ax-5 1953. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) |
⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | 19.39 2033 | Theorem 19.39 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∃𝑥𝜑 → ∃𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) | ||
Theorem | 19.24 2034 | Theorem 19.24 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∀𝑥𝜑 → ∀𝑥𝜓) → ∃𝑥(𝜑 → 𝜓)) | ||
Theorem | 19.34 2035 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ ((∀𝑥𝜑 ∨ ∃𝑥𝜓) → ∃𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | 19.36v 2036* | Version of 19.36 2216 with a disjoint variable condition instead of a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020.) |
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓)) | ||
Theorem | 19.12vvv 2037* | Version of 19.12vv 2316 with a disjoint variable condition, requiring fewer axioms. See also 19.12 2303. (Contributed by BJ, 18-Mar-2020.) |
⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓)) | ||
Theorem | 19.27v 2038* | Version of 19.27 2213 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 3-Jun-2004.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28v 2039* | Version of 19.28 2214 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 25-Mar-2004.) |
⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.37v 2040* | Version of 19.37 2218 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.44v 2041* | Version of 19.44 2224 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.45v 2042* | Version of 19.45 2225 with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | spimeh 2043* | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spimw 2044* | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimvw 2045* | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spnfw 2046 | Weak version of sp 2167. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.) |
⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | spfalw 2047 | Version of sp 2167 when 𝜑 is false. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 25-Dec-2017.) |
⊢ ¬ 𝜑 ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | exsbim 2048* | One direction of the equivalence in exsb 2327 is based on fewer axioms. (Contributed by Wolf Lammen, 2-Mar-2023.) |
⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑) | ||
Theorem | equsb1v 2049* | Version of equsb1 2444 with a disjoint variable condition, which neither requires ax-12 2163 nor ax-13 2334. (Contributed by BJ, 11-Sep-2019.) Remove dependencies on axioms. (Revised by Wolf Lammen, 30-May-2023.) (Proof shortened by Steven Nguyen, 31-May-2023.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | equs4v 2050* | Version of equs4 2381 with a disjoint variable condition, which requires fewer axioms. (Contributed by BJ, 31-May-2019.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | equsalvw 2051* | Version of equsalv 2241 with a disjoint variable condition, and of equsal 2382 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsexvw 2052. (Contributed by BJ, 31-May-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexvw 2052* | Version of equsexv 2242 with a disjoint variable condition, and of equsex 2383 with two disjoint variable conditions, which requires fewer axioms. See also the dual form equsalvw 2051. (Contributed by BJ, 31-May-2019.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | cbvaliw 2053* | Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbvalivw 2054* | Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Axiom | ax-7 2055 |
Axiom of Equality. One of the equality and substitution axioms of
predicate calculus with equality. It states that equality is a
right-Euclidean binary relation (this is similar, but not identical, to
being transitive, which is proved as equtr 2068). This axiom scheme is a
sub-scheme of Axiom Scheme B8 of system S2 of [Tarski], p. 75, whose
general form cannot be represented with our notation. Also appears as
Axiom C7 of [Monk2] p. 105 and Axiom Scheme
C8' in [Megill] p. 448 (p. 16
of the preprint).
The equality symbol was invented in 1557 by Robert Recorde. He chose a pair of parallel lines of the same length because "noe .2. thynges, can be moare equalle". We prove in ax7 2063 that this axiom can be recovered from its weakened version ax7v 2056 where 𝑥 and 𝑦 are assumed to be disjoint variables. In particular, the only theorem referencing ax-7 2055 should be ax7v 2056. See the comment of ax7v 2056 for more details on these matters. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 7-Dec-2020.) Use ax7 2063 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v 2056* |
Weakened version of ax-7 2055, with a disjoint variable condition on
𝑥,
𝑦. This should be
the only proof referencing ax-7 2055, and it
should be referenced only by its two weakened versions ax7v1 2057 and
ax7v2 2058, from which ax-7 2055
is then rederived as ax7 2063, which shows
that either ax7v 2056 or the conjunction of ax7v1 2057 and ax7v2 2058 is
sufficient.
In ax7v 2056, it is still allowed to substitute the same variable for 𝑥 and 𝑧, or the same variable for 𝑦 and 𝑧. Therefore, ax7v 2056 "bundles" (a term coined by Raph Levien) its "principal instance" (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) with 𝑥, 𝑦, 𝑧 distinct, and its "degenerate instances" (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥)) and (𝑥 = 𝑦 → (𝑥 = 𝑦 → 𝑦 = 𝑦)) with 𝑥, 𝑦 distinct. These degenerate instances are for instance used in the proofs of equcomiv 2061 and equid 2059 respectively. (Contributed by BJ, 7-Dec-2020.) Use ax7 2063 instead. (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v1 2057* | First of two weakened versions of ax7v 2056, with an extra disjoint variable condition on 𝑥, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | ax7v2 2058* | Second of two weakened versions of ax7v 2056, with an extra disjoint variable condition on 𝑦, 𝑧, see comments there. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | equid 2059 | Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
⊢ 𝑥 = 𝑥 | ||
Theorem | nfequid 2060 | Bound-variable hypothesis builder for 𝑥 = 𝑥. This theorem tells us that any variable, including 𝑥, is effectively not free in 𝑥 = 𝑥, even though 𝑥 is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.) |
⊢ Ⅎ𝑦 𝑥 = 𝑥 | ||
Theorem | equcomiv 2061* | Weaker form of equcomi 2064 with a disjoint variable condition on 𝑥, 𝑦. This is an intermediate step and equcomi 2064 is fully recovered later. (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | ax6evr 2062* | A commuted form of ax6ev 2023. (Contributed by BJ, 7-Dec-2020.) |
⊢ ∃𝑥 𝑦 = 𝑥 | ||
Theorem | ax7 2063 |
Proof of ax-7 2055 from ax7v1 2057 and ax7v2 2058 (and earlier axioms), proving
sufficiency of the conjunction of the latter two weakened versions of
ax7v 2056, which is itself a weakened version of ax-7 2055.
Note that the weakened version of ax-7 2055 obtained by adding a disjoint variable condition on 𝑥, 𝑧 (resp. on 𝑦, 𝑧) does not permit, together with the other axioms, to prove reflexivity (resp. symmetry). (Contributed by BJ, 7-Dec-2020.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 → 𝑦 = 𝑧)) | ||
Theorem | equcomi 2064 | Commutative law for equality. Equality is a symmetric relation. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 10-Jan-1993.) (Revised by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) | ||
Theorem | equcom 2065 | Commutative law for equality. Equality is a symmetric relation. (Contributed by NM, 20-Aug-1993.) |
⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥) | ||
Theorem | equcomd 2066 | Deduction form of equcom 2065, symmetry of equality. For the versions for classes, see eqcom 2785 and eqcomd 2784. (Contributed by BJ, 6-Oct-2019.) |
⊢ (𝜑 → 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → 𝑦 = 𝑥) | ||
Theorem | equcoms 2067 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝑥 = 𝑦 → 𝜑) ⇒ ⊢ (𝑦 = 𝑥 → 𝜑) | ||
Theorem | equtr 2068 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝑥 = 𝑧)) | ||
Theorem | equtrr 2069 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | ||
Theorem | equeuclr 2070 | Commuted version of equeucl 2071 (equality is left-Euclidean). (Contributed by BJ, 12-Apr-2021.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑦 = 𝑥)) | ||
Theorem | equeucl 2071 | Equality is a left-Euclidean binary relation. (Right-Euclideanness is stated in ax-7 2055.) Curried (exported) form of equtr2 2074. (Contributed by BJ, 11-Apr-2021.) |
⊢ (𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝑥 = 𝑦)) | ||
Theorem | equequ1 2072 | An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.) |
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) | ||
Theorem | equequ2 2073 | An equivalence law for equality. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) (Proof shortened by BJ, 12-Apr-2021.) |
⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) | ||
Theorem | equtr2 2074 | Equality is a left-Euclidean binary relation. Uncurried (imported) form of equeucl 2071. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by BJ, 11-Apr-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑧) → 𝑥 = 𝑦) | ||
Theorem | stdpc6 2075 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 2076.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain). (Contributed by NM, 16-Feb-2005.) |
⊢ ∀𝑥 𝑥 = 𝑥 | ||
Theorem | stdpc7 2076 | One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2075.) Translated to traditional notation, it can be read: "𝑥 = 𝑦 → (𝜑(𝑥, 𝑥) → 𝜑(𝑥, 𝑦)), provided that 𝑦 is free for 𝑥 in 𝜑(𝑥, 𝑥)". Axiom 7 of [Mendelson] p. 95. (Contributed by NM, 15-Feb-2005.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 → 𝜑)) | ||
Theorem | equvinv 2077* | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2135, ax-13 2334. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable (𝑧) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.) |
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvinvOLD 2078* | Obsolete version of equvinv 2077 as of 12-Jul-2022. (Contributed by NM, 9-Jan-1993.) Remove dependencies on ax-10 2135, ax-13 2334. (Revised by Wolf Lammen, 10-Jun-2019.) Move the quantified variable (𝑧) to the left of the equality signs. (Revised by Wolf Lammen, 11-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 = 𝑦)) | ||
Theorem | equvinva 2079* | A modified version of the forward implication of equvinv 2077 adapted to common usage. (Contributed by Wolf Lammen, 8-Sep-2018.) |
⊢ (𝑥 = 𝑦 → ∃𝑧(𝑥 = 𝑧 ∧ 𝑦 = 𝑧)) | ||
Theorem | equvelv 2080* | A biconditional form of equvel 2422 with disjoint variable conditions and proved from Tarski's FOL axiom schemes. (Contributed by Andrew Salmon, 2-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 10-Apr-2021.) (Proof shortened by Wolf Lammen, 12-Jul-2022.) |
⊢ (∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦) ↔ 𝑥 = 𝑦) | ||
Theorem | equvelvOLD 2081* | Obsolete version of equvelv 2080 as of 12-Jul-2022. (Contributed by Wolf Lammen, 10-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 = 𝑥 → 𝑧 = 𝑦)) | ||
Theorem | ax13b 2082 | An equivalence between two ways of expressing ax-13 2334. See the comment for ax-13 2334. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.) |
⊢ ((¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → 𝜑)) ↔ (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → 𝜑)))) | ||
Theorem | spfw 2083* | Weak version of sp 2167. Uses only Tarski's FOL axiom schemes. Lemma 9 of [KalishMontague] p. 87. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | spw 2084* | Weak version of the specialization scheme sp 2167. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2167 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2167 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2129 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2167 are spfw 2083 (minimal distinct variable requirements), spnfw 2046 (when 𝑥 is not free in ¬ 𝜑), spvw 2032 (when 𝑥 does not appear in 𝜑), sptruw 1850 (when 𝜑 is true), and spfalw 2047 (when 𝜑 is false). (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 27-Feb-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜑) | ||
Theorem | cbvalw 2085* | Change bound variable. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvalvw 2086* | Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvalv 2370 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexvw 2087* | Change bound variable. Uses only Tarski's FOL axiom schemes. See cbvexv 2371 for a version with fewer disjoint variable conditions but requiring more axioms. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | alcomiw 2088* | Weak version of alcom 2152. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 12-Jul-2022.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | alcomiwOLD 2089* | Obsolete version of alcomiw 2088 as of 12-Jul-2022. (Contributed by NM, 10-Apr-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → ∀𝑦∀𝑥𝜑) | ||
Theorem | hbn1fw 2090* | Weak version of ax-10 2135 from which we can prove any ax-10 2135 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 28-Feb-2018.) |
⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑) & ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓) & ⊢ (∀𝑦𝜓 → ∀𝑥∀𝑦𝜓) & ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑) & ⊢ (¬ ∀𝑦𝜓 → ∀𝑥 ¬ ∀𝑦𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | hbn1w 2091* | Weak version of hbn1 2136. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥𝜑 → ∀𝑥 ¬ ∀𝑥𝜑) | ||
Theorem | hba1w 2092* | Weak version of hba1 2268. See comments for ax10w 2123. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 10-Oct-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | hbe1w 2093* | Weak version of hbe1 2137. See comments for ax10w 2123. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | ||
Theorem | hbalw 2094* | Weak version of hbal 2160. Uses only Tarski's FOL axiom schemes. Unlike hbal 2160, this theorem requires that 𝑥 and 𝑦 be distinct, i.e. not be bundled. (Contributed by NM, 19-Apr-2017.) |
⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑦𝜑 → ∀𝑥∀𝑦𝜑) | ||
Theorem | spaev 2095* |
A special instance of sp 2167 applied to an equality with a disjoint
variable condition. Unlike the more general sp 2167, we
can prove this
without ax-12 2163. Instance of aeveq 2099.
The antecedent ∀𝑥𝑥 = 𝑦 with distinct 𝑥 and 𝑦 is a characteristic of a degenerate universe, in which just one object exists. Actually more than one object may still exist, but if so, we give up on equality as a discriminating term. Separating this degenerate case from a richer universe, where inequality is possible, is a common proof idea. The name of this theorem follows a convention, where the condition ∀𝑥𝑥 = 𝑦 is denoted by 'aev', a shorthand for 'all equal, with a distinct variable condition'. (Contributed by Wolf Lammen, 14-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦) | ||
Theorem | cbvaev 2096* | Change bound variable in an equality with a disjoint variable condition. Instance of aev 2100. (Contributed by NM, 22-Jul-2015.) (Revised by BJ, 18-Jun-2019.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑦) | ||
Theorem | aevlem0 2097* | Lemma for aevlem 2098. Instance of aev 2100. (Contributed by NM, 8-Jul-2016.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-12 2163. (Revised by Wolf Lammen, 14-Mar-2021.) (Revised by BJ, 29-Mar-2021.) (Proof shortened by Wolf Lammen, 30-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑥) | ||
Theorem | aevlem 2098* | Lemma for aev 2100 and axc16g 2233. Change free and bound variables. Instance of aev 2100. (Contributed by NM, 22-Jul-2015.) (Proof shortened by Wolf Lammen, 17-Feb-2018.) Remove dependency on ax-13 2334, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 29-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑧 = 𝑡) | ||
Theorem | aeveq 2099* | The antecedent ∀𝑥𝑥 = 𝑦 with a disjoint variable condition (typical of a one-object universe) forces equality of everything. (Contributed by Wolf Lammen, 19-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → 𝑧 = 𝑡) | ||
Theorem | aev 2100* | A "distinctor elimination" lemma with no restrictions on variables in the consequent. (Contributed by NM, 8-Nov-2006.) Remove dependency on ax-11 2150. (Revised by Wolf Lammen, 7-Sep-2018.) Remove dependency on ax-13 2334, inspired by an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) Remove dependency on ax-12 2163. (Revised by Wolf Lammen, 19-Mar-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧 𝑡 = 𝑢) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |