Home | Intuitionistic Logic Explorer Theorem List (p. 20 of 108) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2sb6 1901* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | sbcom2v 1902* | Lemma for proving sbcom2 1904. It is the same as sbcom2 1904 but with additional distinct variable constraints on 𝑥 and 𝑦, and on 𝑤 and 𝑧. (Contributed by Jim Kingdon, 19-Feb-2018.) |
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑) | ||
Theorem | sbcom2v2 1903* | Lemma for proving sbcom2 1904. It is the same as sbcom2v 1902 but removes the distinct variable constraint on 𝑥 and 𝑦. (Contributed by Jim Kingdon, 19-Feb-2018.) |
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑) | ||
Theorem | sbcom2 1904* | Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 27-May-1997.) (Proof modified to be intuitionistic by Jim Kingdon, 19-Feb-2018.) |
⊢ ([𝑤 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑤 / 𝑧]𝜑) | ||
Theorem | sb6a 1905* | Equivalence for substitution. (Contributed by NM, 5-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)) | ||
Theorem | 2sb5rf 1906* | Reversed double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → ∀𝑧𝜑) & ⊢ (𝜑 → ∀𝑤𝜑) ⇒ ⊢ (𝜑 ↔ ∃𝑧∃𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) ∧ [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | 2sb6rf 1907* | Reversed double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ (𝜑 → ∀𝑧𝜑) & ⊢ (𝜑 → ∀𝑤𝜑) ⇒ ⊢ (𝜑 ↔ ∀𝑧∀𝑤((𝑧 = 𝑥 ∧ 𝑤 = 𝑦) → [𝑧 / 𝑥][𝑤 / 𝑦]𝜑)) | ||
Theorem | dfsb7 1908* | An alternate definition of proper substitution df-sb 1686. By introducing a dummy variable 𝑧 in the definiens, we are able to eliminate any distinct variable restrictions among the variables 𝑥, 𝑦, and 𝜑 of the definiendum. No distinct variable conflicts arise because 𝑧 effectively insulates 𝑥 from 𝑦. To achieve this, we use a chain of two substitutions in the form of sb5 1808, first 𝑧 for 𝑥 then 𝑦 for 𝑧. Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1909 provides a version where 𝜑 and 𝑧 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb7f 1909* | This version of dfsb7 1908 does not require that 𝜑 and 𝑧 be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1459 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1686 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb7af 1910* | An alternate definition of proper substitution df-sb 1686. Similar to dfsb7a 1911 but does not require that 𝜑 and 𝑧 be distinct. Similar to sb7f 1909 in that it involves a dummy variable 𝑧, but expressed in terms of ∀ rather than ∃. (Contributed by Jim Kingdon, 5-Feb-2018.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) | ||
Theorem | dfsb7a 1911* | An alternate definition of proper substitution df-sb 1686. Similar to dfsb7 1908 in that it involves a dummy variable 𝑧, but expressed in terms of ∀ rather than ∃. For a version which only requires Ⅎ𝑧𝜑 rather than 𝑧 and 𝜑 being distinct, see sb7af 1910. (Contributed by Jim Kingdon, 5-Feb-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑧(𝑧 = 𝑦 → ∀𝑥(𝑥 = 𝑧 → 𝜑))) | ||
Theorem | sb10f 1912* | Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. (Contributed by NM, 9-May-2005.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑)) | ||
Theorem | sbid2v 1913* | An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbelx 1914* | Elimination of substitution. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbel2x 1915* | Elimination of double substitution. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ [𝑦 / 𝑤][𝑥 / 𝑧]𝜑)) | ||
Theorem | sbalyz 1916* | Move universal quantifier in and out of substitution. Identical to sbal 1917 except that it has an additional distinct variable constraint on 𝑦 and 𝑧. (Contributed by Jim Kingdon, 29-Dec-2017.) |
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | sbal 1917* | Move universal quantifier in and out of substitution. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.) |
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | sbal1yz 1918* | Lemma for proving sbal1 1919. Same as sbal1 1919 but with an additional distinct variable constraint on 𝑦 and 𝑧. (Contributed by Jim Kingdon, 23-Feb-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | sbal1 1919* | A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 5-Aug-1993.) (Proof rewitten by Jim Kingdon, 24-Feb-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | sbexyz 1920* | Move existential quantifier in and out of substitution. Identical to sbex 1921 except that it has an additional distinct variable constraint on 𝑦 and 𝑧. (Contributed by Jim Kingdon, 29-Dec-2017.) |
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | sbex 1921* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) (Proof rewritten by Jim Kingdon, 12-Feb-2018.) |
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | sbalv 1922* | Quantify with new variable inside substitution. (Contributed by NM, 18-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥]∀𝑧𝜑 ↔ ∀𝑧𝜓) | ||
Theorem | sbco4lem 1923* | Lemma for sbco4 1924. It replaces the temporary variable 𝑣 with another temporary variable 𝑤. (Contributed by Jim Kingdon, 26-Sep-2018.) |
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sbco4 1924* | Two ways of exchanging two variables. Both sides of the biconditional exchange 𝑥 and 𝑦, either via two temporary variables 𝑢 and 𝑣, or a single temporary 𝑤. (Contributed by Jim Kingdon, 25-Sep-2018.) |
⊢ ([𝑦 / 𝑢][𝑥 / 𝑣][𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | exsb 1925* | An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.) |
⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2exsb 1926* | An equivalent expression for double existence. (Contributed by NM, 2-Feb-2005.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | dvelimALT 1927* | Version of dvelim 1934 that doesn't use ax-10 1436. Because it has different distinct variable constraints than dvelim 1934 and is used in important proofs, it would be better if it had a name which does not end in ALT (ideally more close to set.mm naming). (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimfv 1928* | Like dvelimf 1932 but with a distinct variable constraint on 𝑥 and 𝑧. (Contributed by Jim Kingdon, 6-Mar-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | hbsb4 1929 | A variable not free remains so after substitution with a distinct variable. (Contributed by NM, 5-Aug-1993.) (Proof rewritten by Jim Kingdon, 23-Mar-2018.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑)) | ||
Theorem | hbsb4t 1930 | A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1929). (Contributed by NM, 7-Apr-2004.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
⊢ (∀𝑥∀𝑧(𝜑 → ∀𝑧𝜑) → (¬ ∀𝑧 𝑧 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑))) | ||
Theorem | nfsb4t 1931 | A variable not free remains so after substitution with a distinct variable (closed form of hbsb4 1929). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof rewritten by Jim Kingdon, 9-May-2018.) |
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) | ||
Theorem | dvelimf 1932 | Version of dvelim 1934 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑧𝜓) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimdf 1933 | Deduction form of dvelimf 1932. This version may be useful if we want to avoid ax-17 1459 and use ax-16 1735 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑧𝜒) & ⊢ (𝜑 → (𝑧 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜒)) | ||
Theorem | dvelim 1934* |
This theorem can be used to eliminate a distinct variable restriction on
𝑥 and 𝑧 and replace it with the
"distinctor" ¬ ∀𝑥𝑥 = 𝑦
as an antecedent. 𝜑 normally has 𝑧 free and can be read
𝜑(𝑧), and 𝜓 substitutes 𝑦 for
𝑧
and can be read
𝜑(𝑦). We don't require that 𝑥 and
𝑦
be distinct: if
they aren't, the distinctor will become false (in multiple-element
domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses with ∀𝑥∀𝑧, conjoin them, and apply dvelimdf 1933. Other variants of this theorem are dvelimf 1932 (with no distinct variable restrictions) and dvelimALT 1927 (that avoids ax-10 1436). (Contributed by NM, 23-Nov-1994.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓)) | ||
Theorem | dvelimor 1935* | Disjunctive distinct variable constraint elimination. A user of this theorem starts with a formula 𝜑 (containing 𝑧) and a distinct variable constraint between 𝑥 and 𝑧. The theorem makes it possible to replace the distinct variable constraint with the disjunct ∀𝑥𝑥 = 𝑦 (𝜓 is just a version of 𝜑 with 𝑦 substituted for 𝑧). (Contributed by Jim Kingdon, 11-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥𝜓) | ||
Theorem | dveeq1 1936* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Proof rewritten by Jim Kingdon, 19-Feb-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | dveel1 1937* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → ∀𝑥 𝑦 ∈ 𝑧)) | ||
Theorem | dveel2 1938* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)) | ||
Theorem | sbal2 1939* | Move quantifier in and out of substitution. (Contributed by NM, 2-Jan-2002.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | nfsb4or 1940 | A variable not free remains so after substitution with a distinct variable. (Contributed by Jim Kingdon, 11-May-2018.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (∀𝑧 𝑧 = 𝑦 ∨ Ⅎ𝑧[𝑦 / 𝑥]𝜑) | ||
Syntax | weu 1941 | Extend wff definition to include existential uniqueness ("there exists a unique 𝑥 such that 𝜑"). |
wff ∃!𝑥𝜑 | ||
Syntax | wmo 1942 | Extend wff definition to include uniqueness ("there exists at most one 𝑥 such that 𝜑"). |
wff ∃*𝑥𝜑 | ||
Theorem | eujust 1943* | A soundness justification theorem for df-eu 1944, showing that the definition is equivalent to itself with its dummy variable renamed. Note that 𝑦 and 𝑧 needn't be distinct variables. (Contributed by NM, 11-Mar-2010.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑧∀𝑥(𝜑 ↔ 𝑥 = 𝑧)) | ||
Definition | df-eu 1944* | Define existential uniqueness, i.e. "there exists exactly one 𝑥 such that 𝜑." Definition 10.1 of [BellMachover] p. 97; also Definition *14.02 of [WhiteheadRussell] p. 175. Other possible definitions are given by eu1 1966, eu2 1985, eu3 1987, and eu5 1988 (which in some cases we show with a hypothesis 𝜑 → ∀𝑦𝜑 in place of a distinct variable condition on 𝑦 and 𝜑). Double uniqueness is tricky: ∃!𝑥∃!𝑦𝜑 does not mean "exactly one 𝑥 and one 𝑦 " (see 2eu4 2034). (Contributed by NM, 5-Aug-1993.) |
⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Definition | df-mo 1945 | Define "there exists at most one 𝑥 such that 𝜑." Here we define it in terms of existential uniqueness. Notation of [BellMachover] p. 460, whose definition we show as mo3 1995. For another possible definition see mo4 2002. (Contributed by NM, 5-Aug-1993.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑)) | ||
Theorem | euf 1946* | A version of the existential uniqueness definition with a hypothesis instead of a distinct variable condition. (Contributed by NM, 12-Aug-1993.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) | ||
Theorem | eubidh 1947 | Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | ||
Theorem | eubid 1948 | Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | ||
Theorem | eubidv 1949* | Formula-building rule for uniqueness quantifier (deduction rule). (Contributed by NM, 9-Jul-1994.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃!𝑥𝜓 ↔ ∃!𝑥𝜒)) | ||
Theorem | eubii 1950 | Introduce uniqueness quantifier to both sides of an equivalence. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑥𝜓) | ||
Theorem | hbeu1 1951 | Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) |
⊢ (∃!𝑥𝜑 → ∀𝑥∃!𝑥𝜑) | ||
Theorem | nfeu1 1952 | Bound-variable hypothesis builder for uniqueness. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃!𝑥𝜑 | ||
Theorem | nfmo1 1953 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑥∃*𝑥𝜑 | ||
Theorem | sb8eu 1954 | Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8mo 1955 | Variable substitution for "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | nfeudv 1956* | Deduction version of nfeu 1960. Similar to nfeud 1957 but has the additional constraint that 𝑥 and 𝑦 must be distinct. (Contributed by Jim Kingdon, 25-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfeud 1957 | Deduction version of nfeu 1960. (Contributed by NM, 15-Feb-2013.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 25-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃!𝑦𝜓) | ||
Theorem | nfmod 1958 | Bound-variable hypothesis builder for "at most one." (Contributed by Mario Carneiro, 14-Nov-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥∃*𝑦𝜓) | ||
Theorem | nfeuv 1959* | Bound-variable hypothesis builder for existential uniqueness. This is similar to nfeu 1960 but has the additional constraint that 𝑥 and 𝑦 must be distinct. (Contributed by Jim Kingdon, 23-May-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦𝜑 | ||
Theorem | nfeu 1960 | Bound-variable hypothesis builder for existential uniqueness. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Revised by Mario Carneiro, 7-Oct-2016.) (Proof rewritten by Jim Kingdon, 23-May-2018.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃!𝑦𝜑 | ||
Theorem | nfmo 1961 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃*𝑦𝜑 | ||
Theorem | hbeu 1962 | Bound-variable hypothesis builder for uniqueness. Note that 𝑥 and 𝑦 needn't be distinct. (Contributed by NM, 8-Mar-1995.) (Proof rewritten by Jim Kingdon, 24-May-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃!𝑦𝜑 → ∀𝑥∃!𝑦𝜑) | ||
Theorem | hbeud 1963 | Deduction version of hbeu 1962. (Contributed by NM, 15-Feb-2013.) (Proof rewritten by Jim Kingdon, 25-May-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → (∃!𝑦𝜓 → ∀𝑥∃!𝑦𝜓)) | ||
Theorem | sb8euh 1964 | Variable substitution in uniqueness quantifier. (Contributed by NM, 7-Aug-1994.) (Revised by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | cbveu 1965 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 25-Nov-1994.) (Revised by Mario Carneiro, 7-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃!𝑦𝜓) | ||
Theorem | eu1 1966* | An alternate way to express uniqueness used by some authors. Exercise 2(b) of [Margaris] p. 110. (Contributed by NM, 20-Aug-1993.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃!𝑥𝜑 ↔ ∃𝑥(𝜑 ∧ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑥 = 𝑦))) | ||
Theorem | euor 1967 | Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | euorv 1968* | Introduce a disjunct into a uniqueness quantifier. (Contributed by NM, 23-Mar-1995.) |
⊢ ((¬ 𝜑 ∧ ∃!𝑥𝜓) → ∃!𝑥(𝜑 ∨ 𝜓)) | ||
Theorem | mo2n 1969* | There is at most one of something which does not exist. (Contributed by Jim Kingdon, 2-Jul-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | mon 1970 | There is at most one of something which does not exist. (Contributed by Jim Kingdon, 5-Jul-2018.) |
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | euex 1971 | Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (∃!𝑥𝜑 → ∃𝑥𝜑) | ||
Theorem | eumo0 1972* | Existential uniqueness implies "at most one." (Contributed by NM, 8-Jul-1994.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃!𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)) | ||
Theorem | eumo 1973 | Existential uniqueness implies "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.) |
⊢ (∃!𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | eumoi 1974 | "At most one" inferred from existential uniqueness. (Contributed by NM, 5-Apr-1995.) |
⊢ ∃!𝑥𝜑 ⇒ ⊢ ∃*𝑥𝜑 | ||
Theorem | mobidh 1975 | Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | mobid 1976 | Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by NM, 8-Mar-1995.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | mobidv 1977* | Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.) |
⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒)) | ||
Theorem | mobii 1978 | Formula-building rule for "at most one" quantifier (inference rule). (Contributed by NM, 9-Mar-1995.) (Revised by Mario Carneiro, 17-Oct-2016.) |
⊢ (𝜓 ↔ 𝜒) ⇒ ⊢ (∃*𝑥𝜓 ↔ ∃*𝑥𝜒) | ||
Theorem | hbmo1 1979 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 8-Mar-1995.) |
⊢ (∃*𝑥𝜑 → ∀𝑥∃*𝑥𝜑) | ||
Theorem | hbmo 1980 | Bound-variable hypothesis builder for "at most one." (Contributed by NM, 9-Mar-1995.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃*𝑦𝜑 → ∀𝑥∃*𝑦𝜑) | ||
Theorem | cbvmo 1981 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 9-Mar-1995.) (Revised by Andrew Salmon, 8-Jun-2011.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∃*𝑦𝜓) | ||
Theorem | mo23 1982* | An implication between two definitions of "there exists at most one." (Contributed by Jim Kingdon, 25-Jun-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | mor 1983* | Converse of mo23 1982 with an additional ∃𝑥𝜑 condition. (Contributed by Jim Kingdon, 25-Jun-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 → (∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | modc 1984* | Equivalent definitions of "there exists at most one," given decidable existence. (Contributed by Jim Kingdon, 1-Jul-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (DECID ∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | eu2 1985* | An alternate way of defining existential uniqueness. Definition 6.10 of [TakeutiZaring] p. 26. (Contributed by NM, 8-Jul-1994.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) | ||
Theorem | eu3h 1986* | An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | eu3 1987* | An alternate way to express existential uniqueness. (Contributed by NM, 8-Jul-1994.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | eu5 1988 | Uniqueness in terms of "at most one." (Contributed by NM, 23-Mar-1995.) (Proof rewritten by Jim Kingdon, 27-May-2018.) |
⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑)) | ||
Theorem | exmoeu2 1989 | Existence implies "at most one" is equivalent to uniqueness. (Contributed by NM, 5-Apr-2004.) |
⊢ (∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃!𝑥𝜑)) | ||
Theorem | moabs 1990 | Absorption of existence condition by "at most one." (Contributed by NM, 4-Nov-2002.) |
⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃*𝑥𝜑)) | ||
Theorem | exmodc 1991 | If existence is decidable, something exists or at most one exists. (Contributed by Jim Kingdon, 30-Jun-2018.) |
⊢ (DECID ∃𝑥𝜑 → (∃𝑥𝜑 ∨ ∃*𝑥𝜑)) | ||
Theorem | exmonim 1992 | There is at most one of something which does not exist. Unlike exmodc 1991 there is no decidability condition. (Contributed by Jim Kingdon, 22-Sep-2018.) |
⊢ (¬ ∃𝑥𝜑 → ∃*𝑥𝜑) | ||
Theorem | mo2r 1993* | A condition which implies "at most one." (Contributed by Jim Kingdon, 2-Jul-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃*𝑥𝜑) | ||
Theorem | mo3h 1994* | Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that 𝑦 not occur in 𝜑 in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | mo3 1995* | Alternate definition of "at most one." Definition of [BellMachover] p. 460, except that definition has the side condition that 𝑦 not occur in 𝜑 in place of our hypothesis. (Contributed by NM, 8-Mar-1995.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃*𝑥𝜑 ↔ ∀𝑥∀𝑦((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) | ||
Theorem | mo2dc 1996* | Alternate definition of "at most one" where existence is decidable. (Contributed by Jim Kingdon, 2-Jul-2018.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (DECID ∃𝑥𝜑 → (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))) | ||
Theorem | euan 1997 | Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 19-Feb-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃!𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥𝜓)) | ||
Theorem | euanv 1998* | Introduction of a conjunct into uniqueness quantifier. (Contributed by NM, 23-Mar-1995.) |
⊢ (∃!𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃!𝑥𝜓)) | ||
Theorem | euor2 1999 | Introduce or eliminate a disjunct in a uniqueness quantifier. (Contributed by NM, 21-Oct-2005.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |
⊢ (¬ ∃𝑥𝜑 → (∃!𝑥(𝜑 ∨ 𝜓) ↔ ∃!𝑥𝜓)) | ||
Theorem | sbmo 2000* | Substitution into "at most one". (Contributed by Jeff Madsen, 2-Sep-2009.) |
⊢ ([𝑦 / 𝑥]∃*𝑧𝜑 ↔ ∃*𝑧[𝑦 / 𝑥]𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |