| Metamath Proof Explorer | < Previous Next > | |
| Browser slow? Try the
Unicode version. |
| Color key: | (1-11257) |
(11258-12844) |
(12845-19026) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sbal1 2001 |
A theorem used in elimination of disjoint variable restriction on |
| Theorem | sbal 2002 | Move universal quantifier in and out of substitution. |
| Theorem | sbex 2003 | Move existential quantifier in and out of substitution. |
| Theorem | sbalv 2004 | Quantify with new variable inside substitution. |
| Theorem | exsb 2005 | An equivalent expression for existence. |
| Theorem | 2exsb 2006 | An equivalent expression for double existence. |
| Theorem | dvelim 2007 |
This theorem can be used to eliminate a distinct variable restriction on
To obtain a closed-theorem form of this inference, prefix the hypotheses
with Other variants of this theorem are dvelimf 1897 (with no distinct variable restrictions), dvelimfALT 1794 (that avoids ax-11 1597), and dvelimALT 2008 (that avoids ax-10 1596). |
| Theorem | dvelimALT 2008 | Version of dvelim 2007 that doesn't use ax-10 1596. (See dvelimfALT 1794 for a version that doesn't use ax-11 1597.) |
| Theorem | dveeq1 2009 | Quantifier introduction when one pair of variables is distinct. |
| Theorem | dveeq1ALT 2010 | Version of dveeq1 2009 using ax-16 1854 instead of ax-17 1605. |
| Theorem | dveel1 2011 | Quantifier introduction when one pair of variables is distinct. |
| Theorem | dveel2 2012 | Quantifier introduction when one pair of variables is distinct. |
| Theorem | sbal2 2013 | Move quantifier in and out of substitution. |
| Theorem | ax15 2014 |
Axiom ax-15 2015 is redundant if we assume ax-17 1605. Remark 9.6 in
[Megill] p. 448 (p. 16 of the preprint),
regarding axiom scheme C14'.
Note that This theorem should not be referenced in any proof. Instead, use ax-15 2015 below so that theorems needing ax-15 2015 can be more easily identified. |
| Axiom | ax-15 2015 | Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 1605; see theorem ax15 2014. Alternately, ax-17 1605 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1605. We retain ax-15 2015 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1605, which might be easier to study for some theoretical purposes. |
| Theorem | ax17el 2016 | Theorem to add distinct quantifier to atomic formula. This theorem demonstrates the induction basis for ax-17 1605 considered as a metatheorem.) |
| Theorem | dveel2ALT 2017 | Version of dveel2 2012 using ax-16 1854 instead of ax-17 1605. |
| Theorem | ax11eq 2018 | Basis step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Atomic formula for equality predicate. |
| Theorem | ax11el 2019 | Basis step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Atomic formula for membership predicate. |
| Theorem | ax11f 2020 |
Basis step for constructing a substitution instance of ax-11o 1864 without
using ax-11o 1864. We can start with any formula |
| Theorem | ax11indn 2021 | Induction step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Negation case. |
| Theorem | ax11indi 2022 | Induction step for constructing a substitution instance of ax-11o 1864 without using ax-11o 1864. Implication case. |
| Theorem | ax11indalem 2023 | Lemma for ax11inda2 2025 and ax11inda 2026. [Auxiliary lemma - not displayed.] |
| Theorem | ax11inda2ALT 2024 | A proof of ax11inda2 2025 that is slightly more direct. |
| Theorem | ax11inda2 2025 |
Induction step for constructing a substitution instance of ax-11o 1864
without using ax-11o 1864. Quantification case. When |
| Theorem | ax11inda 2026 |
Induction step for constructing a substitution instance of ax-11o 1864
without using ax-11o 1864. Quantification case. (When |
| Theorem | a12stdy1 2027 |
Part of a study related to ax-12 1598. The consequent introduces a new
variable |
| Theorem | a12stdy2 2028 | Part of a study related to ax-12 1598. The consequent is quantified with a different variable. There are no distinct variable restrictions. |
| Theorem | a12stdy3 2029 | Part of a study related to ax-12 1598. The consequent introduces two new variables. There are no distinct variable restrictions. |
| Theorem | a12stdy4 2030 | Part of a study related to ax-12 1598. The second antecedent of ax-12 1598 is replaced. There are no distinct variable restrictions. |
| Theorem | a12lem1 2031 | Proof of first hypothesis of a12study 2033. |
| Theorem | a12lem2 2032 | Proof of second hypothesis of a12study 2033. |
| Theorem | a12study 2033 | Rederivation of axiom ax-12 1598 from two shorter formulas, without using ax-12 1598. See a12lem1 2031 and a12lem2 2032 for the proofs of the hypotheses (using ax-12 1598). This is the only known breakdown of ax-12 1598 into shorter formulas. See a12studyALT 2034 for an alternate proof. Note that the proof depends on ax-11o 1864, whose proof ax11o 1863 depends on ax-12 1598, meaning that we would have to replace ax-11 1597 with ax-11o 1864 in an axiomatization that uses the hypotheses in place of ax-12 1598. Whether this can be avoided is an open problem. |
| Theorem | a12studyALT 2034 | Alternate proof of a12study 2033, also without using ax-12 1598. |
| Theorem | a12study2 2035 | Reprove ax-12 1598 using dvelimfALT2 1858, showing that ax-12 1598 can be replaced by dveeq2 1856 if we allow distinct variables in axioms other than ax-17 1605. (Contributed by Andrew Salmon, 21-Jul-2011.) |
| Theorem | a12study3 2036 |
Rederivation of axiom ax-12 1598 from two other formulas, without using
ax-12 1598. See equvini 1811 and equveli 1812 for the proofs of the hypotheses
(using ax-12 1598). Although the second hypothesis (when
expanded to
primitives) is longer than ax-12 1598, an open problem is whether it can
be derived without ax-12 1598 or from a simpler axiom.
Note also that the proof depends on ax-11o 1864, whose proof ax11o 1863 depends on ax-12 1598, meaning that we would have to replace ax-11 1597 with ax-11o 1864 in an axiomatization that uses the hypotheses in place of ax-12 1598. Whether this can be avoided is an open problem. |
| Existential uniqueness | ||
| Syntax | weu 2037 |
Extend wff definition to include existential uniqueness ("there exists a
unique |
| Syntax | wmo 2038 |
Extend wff definition to include uniqueness ("there exists at most one
|
| Theorem | eujust 2039 |
A soundness justification theorem for df-eu 2041, showing that the
definition is equivalent to itself with its dummy variable renamed.
Note that |
| Theorem | eujustALT 2040 |
A soundness justification theorem for df-eu 2041, showing that the
definition is equivalent to itself with its dummy variable renamed.
Note that |
| Definition | df-eu 2041 |
Define existential uniqueness, i.e. "there exists exactly one |
| Definition | df-mo 2042 |
Define "there exists at most one |
| Theorem | euf 2043 | A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. |
| Theorem | eubid 2044 | Formula-building rule for uniqueness quantifier (deduction rule). |
| Theorem | eubidv 2045 | Formula-building rule for uniqueness quantifier (deduction rule). |
| Theorem | eubii 2046 | Introduce uniqueness quantifier to both sides of an equivalence. |
| Theorem | hbeu1 2047 | Bound-variable hypothesis builder for uniqueness. |
| Theorem | hbeu 2048 |
Bound-variable hypothesis builder for "at most one." Note that |
| Theorem | hbeud 2049 | Deduction version of hbeu 2048. |
| Theorem | sb8eu 2050 | Variable substitution in uniqueness quantifier. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 9-Jul-2011.) |
| Theorem | cbveu 2051 | Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.) |
| Theorem | eu1 2052 | An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. |
| Theorem | mo 2053 | Equivalent definitions of "there exists at most one." |
| Theorem | euex 2054 | Existential uniqueness implies existence. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| Theorem | eumo0 2055 | Existential uniqueness implies "at most one." |
| Theorem | eu2 2056 | An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. |
| Theorem | eu3 2057 | An alternate way to express existential uniqueness. |
| Theorem | euor 2058 | Introduce a disjunct into a uniqueness quantifier. |
| Theorem | euorv 2059 | Introduce a disjunct into a uniqueness quantifier. |
| Theorem | mo2 2060 | Alternate definition of "at most one." |
| Theorem | sbmo 2061 | Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.) |
| Theorem | mo3 2062 |
Alternate definition of "at most one." Definition of [BellMachover]
p. 460, except that definition has the side condition that |
| Theorem | mo4f 2063 | "At most one" expressed using implicit substitution. |
| Theorem | mo4 2064 | "At most one" expressed using implicit substitution. |
| Theorem | mobid 2065 | Formula-building rule for "at most one" quantifier (deduction rule). |
| Theorem | mobii 2066 | Formula-building rule for "at most one" quantifier (inference rule). |
| Theorem | hbmo1 2067 | Bound-variable hypothesis builder for "at most one." |
| Theorem | hbmo 2068 | Bound-variable hypothesis builder for "at most one." |
| Theorem | cbvmo 2069 | Rule used to change bound variables, using implicit substitition. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 8-Jun-2011.) |
| Theorem | eu5 2070 | Uniqueness in terms of "at most one." |
| Theorem | eu4 2071 | Uniqueness using implicit substitution. |
| Theorem | eumo 2072 | Existential uniqueness implies "at most one." |
| Theorem | eumoi 2073 | "At most one" inferred from existential uniqueness. |
| Theorem | exmoeu 2074 | Existence in terms of "at most one" and uniqueness. |
| Theorem | exmoeu2 2075 | Existence implies "at most one" is equivalent to uniqueness. |
| Theorem | moabs 2076 | Absorption of existence condition by "at most one." |
| Theorem | exmo 2077 | Something exists or at most one exists. |
| Theorem | immo 2078 | "At most one" is preserved through implication (notice wff reversal). |
| Theorem | immoi 2079 | "At most one" is preserved through implication (notice wff reversal). |
| Theorem | moimv 2080 | Move antecedent outside of "at most one." |
| Theorem | euimmo 2081 | Uniqueness implies "at most one" through implication. |
| Theorem | euim 2082 | Add existential uniqueness quantifiers to an implication. Note the reversed implication in the antecedent. (The proof was shortened by Andrew Salmon, 14-Jun-2011.) |
| Theorem | moan 2083 | "At most one" is still the case when a conjunct is added. |
| Theorem | moani 2084 | "At most one" is still true when a conjunct is added. |
| Theorem | moor 2085 | "At most one" is still the case when a disjunct is removed. |
| Theorem | mooran1 2086 | "At most one" imports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| Theorem | mooran2 2087 | "At most one" exports disjunction to conjunction. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| Theorem | moanim 2088 | Introduction of a conjunct into "at most one" quantifier. |
| Theorem | euan 2089 | Introduction of a conjunct into uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| Theorem | moanimv 2090 | Introduction of a conjunct into "at most one" quantifier. |
| Theorem | moaneu 2091 | Nested "at most one" and uniqueness quantifiers. |
| Theorem | moanmo 2092 | Nested "at most one" quantifiers. |
| Theorem | euanv 2093 | Introduction of a conjunct into uniqueness quantifier. |
| Theorem | mopick 2094 | "At most one" picks a variable value, eliminating an existential quantifier. |
| Theorem | eupick 2095 |
Existential uniqueness "picks" a variable value for which another wff
is
true. If there is only one thing |
| Theorem | eupicka 2096 | Version of eupick 2095 with closed formulas. |
| Theorem | eupickb 2097 | Existential uniqueness "pick" showing wff equivalence. |
| Theorem | eupickbi 2098 | Theorem *14.26 in [WhiteheadRussell] p. 192. (Contributed by Andrew Salmon, 11-Jul-2011.) |
| Theorem | mopick2 2099 | "At most one" can show the existence of a common value. In this case we can infer existence of conjunction from a conjunction of existence, and it is one way to achieve the converse of 19.40 1731. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| Theorem | euor2 2100 | Introduce or eliminate a disjunct in a uniqueness quantifier. (The proof was shortened by Andrew Salmon, 9-Jul-2011.) |
| MPE Home Contents | Copyright terms: Public domain | < Previous Next > |