Home | Metamath
Proof Explorer Theorem List (p. 23 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nfbidfOLD 2201 | Obsolete proof of nfbidf 2092 as of 6-Oct-2021. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒)) | ||
Theorem | 19.3OLD 2202 | Obsolete proof of 19.3 2069 as of 6-Oct-2021. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ 𝜑) | ||
Theorem | 19.9dOLD 2203 | Obsolete proof of 19.9d 2070 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → Ⅎ𝑥𝜑) ⇒ ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | 19.9tOLD 2204 | Obsolete proof of 19.9t 2071 as of 6-Oct-2021. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) (Proof shortened by Wolf Lammen, 14-Jul-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 ↔ 𝜑)) | ||
Theorem | 19.9OLD 2205 | Obsolete proof of 19.9 2072 as of 6-Oct-2021. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ 𝜑) | ||
Theorem | 19.9hOLD 2206 | Obsolete proof of 19.9h 2120 as of 6-Oct-2021. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 5-Jan-2018.) (Proof shortened by Wolf Lammen, 14-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃𝑥𝜑 ↔ 𝜑) | ||
Theorem | nfa1OLDOLD 2207 | Obsolete proof of nfa1 2028 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥∀𝑥𝜑 | ||
Theorem | nfnf1OLDOLD 2208 | Obsolete proof of nfnf1 2031 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥Ⅎ𝑥𝜑 | ||
Theorem | nfntOLD 2209 | Obsolete proof of nfnt 1782 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | ||
Theorem | nfnOLD 2210 | Obsolete proof of nfn 1784 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥 ¬ 𝜑 | ||
Theorem | nfndOLD 2211 | Obsolete proof of nfnd 1785 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓) | ||
Theorem | 19.21t-1OLD 2212 | One direction of the bi-conditional in 19.21t 2073. Unlike the reverse implication, it does not depend on ax-10 2019. Obsolete as of 6-Oct-2021 (Contributed by Wolf Lammen, 4-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))) | ||
Theorem | 19.21tOLD 2213 | Obsolete proof of 19.21t 2073 as of 6-Oct-2021. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
Theorem | 19.21OLD 2214 | Obsolete proof of 19.21 2075 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.21-2OLD 2215 | Obsolete proof of 19.21-2 2078 as of 6-Oct-2021. (Contributed by NM, 4-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓)) | ||
Theorem | 19.21hOLD 2216 | Obsolete proof of 19.21h 2121 as of 6-Oct-2021. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | stdpc5OLDOLD 2217 | Obsolete proof of stdpc5 2076 as of 6-Oct-2021. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 4-Jul-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.23tOLD 2218 | Obsolete proof of 19.23t 2079 as of 6-Oct-2021. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
Theorem | 19.23OLD 2219 | Obsolete proof of 19.23 2080 as of 6-Oct-2021. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | 19.23hOLD 2220 | Obsolete proof of 19.23h 2122 as of 6-Oct-2021. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | exlimiOLD 2221 | Obsolete proof of exlimi 2086 as of 6-Oct-2021. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exlimihOLD 2222 | Obsolete proof of exlimih 2148 as of 6-Oct-2021. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exlimdOLD 2223 | Obsolete proof of exlimd 2087 as of 6-Oct-2021. (Contributed by NM, 23-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | exlimdhOLD 2224 | Obsolete proof of exlimdh 2149 as of 6-Oct-2021. (Contributed by NM, 28-Jan-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | nfdiOLD 2225 | Obsolete proof of nf5di 2119 as of 6-Oct-2021. (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜑) ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | nfimdOLD 2226 | Obsolete proof of nfimd 1823 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 → 𝜒)) | ||
Theorem | hbim1OLD 2227 | Obsolete proof of hbim 2127 as of 6-Oct-2021. (Contributed by NM, 2-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | nfim1OLD 2228 | Obsolete proof of nfim1 2067 as of 6-Oct-2021. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ Ⅎ𝑥(𝜑 → 𝜓) | ||
Theorem | nfimOLD 2229 | Obsolete proof of nfim 1825 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 → 𝜓) | ||
Theorem | hbimdOLD 2230 | Obsolete proof of hbimd 2126 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | ||
Theorem | hbimOLD 2231 | Obsolete proof of hbim 2127 as of 6-Oct-2021. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | nfandOLD 2232 | Obsolete proof of nfand 1826 as of 6-Oct-2021. (Contributed by Mario Carneiro, 7-Oct-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) | ||
Theorem | nf3andOLD 2233 | Obsolete proof of nf3and 1827 as of 6-Oct-2021. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → Ⅎ𝑥𝜃) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒 ∧ 𝜃)) | ||
Theorem | 19.27OLD 2234 | Obsolete proof of 19.27 2095 as of 6-Oct-2021. (Contributed by NM, 21-Jun-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28OLD 2235 | Obsolete proof of 19.28 2096 as of 6-Oct-2021. (Contributed by NM, 1-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | nfan1OLD 2236 | Obsolete proof of nfan1 2068 as of 6-Oct-2021. (Contributed by Mario Carneiro, 3-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | ||
Theorem | nfanOLDOLD 2237 | Obsolete proof of nfan 1828 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓) | ||
Theorem | nfnanOLD 2238 | Obsolete proof of nfnan 1830 as of 6-Oct-2021. (Contributed by Scott Fenton, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ⊼ 𝜓) | ||
Theorem | nf3anOLD 2239 | Obsolete proof of nf3an 1831 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ Ⅎ𝑥(𝜑 ∧ 𝜓 ∧ 𝜒) | ||
Theorem | hbanOLD 2240 | Obsolete proof of hban 2128 as of 6-Oct-2021. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | hb3anOLD 2241 | Obsolete proof of hb3an 2129 as of 6-Oct-2021. (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | nfbidOLD 2242 | Obsolete proof of nfbid 1832 as of 6-Oct-2021. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) ⇒ ⊢ (𝜑 → Ⅎ𝑥(𝜓 ↔ 𝜒)) | ||
Theorem | nfbiOLD 2243 | Obsolete proof of nfbi 1833 as of 6-Oct-2021. (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) | ||
Theorem | nforOLD 2244 | Obsolete proof of nfor 1834 as of 6-Oct-2021. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) | ||
Theorem | nf3orOLD 2245 | Obsolete proof of nf3or 1835 as of 6-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓 ∨ 𝜒) | ||
Axiom | ax-13 2246 |
Axiom of Quantified Equality. One of the equality and substitution axioms
of predicate calculus with equality.
An equivalent way to express this axiom that may be easier to understand is (¬ 𝑥 = 𝑦 → (¬ 𝑥 = 𝑧 → (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧))) (see ax13b 1964). Recall that in the intended interpretation, our variables are metavariables ranging over the variables of predicate calculus (the object language). In order for the first antecedent ¬ 𝑥 = 𝑦 to hold, 𝑥 and 𝑦 must have different values and thus cannot be the same object-language variable (so they are effectively "distinct variables" even though no $d is present). Similarly, 𝑥 and 𝑧 cannot be the same object-language variable. Therefore, 𝑥 will not occur in the wff 𝑦 = 𝑧 when the first two antecedents hold, so analogous to ax-5 1839, the conclusion (𝑦 = 𝑧 → ∀𝑥𝑦 = 𝑧) follows. Note that ax-5 1839 cannot prove this because its distinct variable ($d) requirement is not satisfied directly but only indirectly (outside of Metamath) by the argument above. The original version of this axiom was ax-c9 34175 and was replaced with this shorter ax-13 2246 in December 2015. The old axiom is proved from this one as theorem axc9 2302. The primary purpose of this axiom is to provide a way to introduce the quantifier ∀𝑥 on 𝑦 = 𝑧 even when 𝑥 and 𝑦 are substituted with the same variable. In this case, the first antecedent becomes ¬ 𝑥 = 𝑥 and the axiom still holds. Although this version is shorter, the original version axc9 2302 may be more practical to work with because of the "distinctor" form of its antecedents. A typical application of axc9 2302 is in dvelimh 2336 which converts a distinct variable pair to the distinctor antecedent ¬ ∀𝑥𝑥 = 𝑦. In particular, it is conjectured that it is not possible to prove ax6 2251 from ax6v 1889 without this axiom. This axiom can be weakened if desired by adding distinct variable restrictions on pairs 𝑥, 𝑧 and 𝑦, 𝑧. To show that, we add these restrictions to theorem ax13v 2247 and use only ax13v 2247 for further derivations. Thus, ax13v 2247 should be the only theorem referencing this axiom. Other theorems can reference either ax13v 2247 (preferred) or ax13 2249 (if the stronger form is needed). This axiom scheme is logically redundant (see ax13w 2013) but is used as an auxiliary axiom scheme to achieve scheme completeness (i.e. so that all possible cases of bundling can be proved; see text linked at mmtheorems.html#ax6dgen). It is not known whether this axiom can be derived from the others. (Contributed by NM, 21-Dec-2015.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13v 2247* |
A weaker version of ax-13 2246 with distinct variable restrictions on pairs
𝑥,
𝑧 and 𝑦, 𝑧. In order to show (with
ax13 2249) that this
weakening is still adequate, this should be the only theorem referencing
ax-13 2246 directly.
Had we additionally required 𝑥 and 𝑦 be distinct, too, this theorem would have been a direct consequence of ax-5 1839. So essentially this theorem states, that a distinct variable condition can be replaced with an inequality between set variables. (Contributed by NM, 30-Jun-2016.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax13lem1 2248* | A version of ax13v 2247 with one distinct variable restriction dropped. For convenience, 𝑦 is kept on the right side of equations. The proof of ax13 2249 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | ax13 2249 | Derive ax-13 2246 from ax13v 2247 and Tarski's FOL. This shows that the weakening in ax13v 2247 is still sufficient for a complete system. (Contributed by NM, 21-Dec-2015.) (Proof shortened by Wolf Lammen, 31-Jan-2018.) Reduce axiom usage (Revised by Wolf Lammen, 2-Jun-2021.) |
⊢ (¬ 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) | ||
Theorem | ax6e 2250 |
At least one individual exists. This is not a theorem of free logic,
which is sound in empty domains. For such a logic, we would add this
theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the
system consisting of ax-4 1737 through ax-9 1999,
all axioms other than
ax-6 1888 are believed to be theorems of free logic,
although the system
without ax-6 1888 is not complete in free logic.
It is preferred to use ax6ev 1890 when it is sufficient. (Contributed by NM, 14-May-1993.) Shortened after ax13lem1 2248 became available. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ ∃𝑥 𝑥 = 𝑦 | ||
Theorem | ax6 2251 |
Theorem showing that ax-6 1888 follows from the weaker version ax6v 1889.
(Even though this theorem depends on ax-6 1888,
all references of ax-6 1888 are
made via ax6v 1889. An earlier version stated ax6v 1889
as a separate axiom,
but having two axioms caused some confusion.)
This theorem should be referenced in place of ax-6 1888 so that all proofs can be traced back to ax6v 1889. When possible, use the weaker ax6v 1889 rather than ax6 2251 since the ax6v 1889 derivation is much shorter and requires fewer axioms. (Contributed by NM, 12-Nov-2013.) (Revised by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 4-Feb-2018.) |
⊢ ¬ ∀𝑥 ¬ 𝑥 = 𝑦 | ||
Theorem | axc10 2252 |
Show that the original axiom ax-c10 34171 can be derived from ax6 2251
and axc7 2132
(on top of propositional calculus, ax-gen 1722, and ax-4 1737). See
ax6fromc10 34181 for the rederivation of ax6 2251
from ax-c10 34171.
Normally, axc10 2252 should be used rather than ax-c10 34171, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → ∀𝑥𝜑) → 𝜑) | ||
Theorem | spimt 2253 | Closed theorem form of spim 2254. (Contributed by NM, 15-Jan-2008.) (Revised by Mario Carneiro, 17-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Feb-2018.) |
⊢ ((Ⅎ𝑥𝜓 ∧ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) → (∀𝑥𝜑 → 𝜓)) | ||
Theorem | spim 2254 | Specialization, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. The spim 2254 series of theorems requires that only one direction of the substitution hypothesis hold. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimed 2255 | Deduction version of spime 2256. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 19-Feb-2018.) |
⊢ (𝜒 → Ⅎ𝑥𝜑) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜒 → (𝜑 → ∃𝑥𝜓)) | ||
Theorem | spime 2256 | Existential introduction, using implicit substitution. Compare Lemma 14 of [Tarski] p. 70. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Mar-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spimv 2257* | A version of spim 2254 with a distinct variable requirement instead of a bound variable hypothesis. See also spimv1 2115 and spimvw 1927. See also spimvALT 2258. (Contributed by NM, 31-Jul-1993.) Removed dependency on ax-10 2019. (Revised by BJ, 29-Nov-2020.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimvALT 2258* | Alternate proof of spimv 2257. Shorter but requires more axioms. (Contributed by NM, 31-Jul-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spimev 2259* | Distinct-variable version of spime 2256. (Contributed by NM, 10-Jan-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (𝜑 → ∃𝑥𝜓) | ||
Theorem | spv 2260* | Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | spei 2261 | Inference from existential specialization, using implicit substitution. Remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜓 ⇒ ⊢ ∃𝑥𝜑 | ||
Theorem | chvar 2262 | Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by Mario Carneiro, 3-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | chvarv 2263* | Implicit substitution of 𝑦 for 𝑥 into a theorem. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 14-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | chvarvOLD 2264* | Obsolete proof of chvarv 2263 as of 14-Jul-2021. (Contributed by NM, 20-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3 2265 | Rule used to change bound variables, using implicit substitution, that does not use ax-c9 34175. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv3h 2266 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 8-Jun-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
⊢ (𝜑 → ∀𝑦𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | cbv1 2267 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv1h 2268 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 → 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 → ∀𝑦𝜒)) | ||
Theorem | cbv2h 2269 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 11-May-1993.) |
⊢ (𝜑 → (𝜓 → ∀𝑦𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (∀𝑥∀𝑦𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbv2 2270 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) Format hypotheses to common style. (Revised by Wolf Lammen, 13-May-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbval 2271 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvex 2272 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvalv 2273* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 17-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvalvOLD 2274* | Obsolete proof of cbvalv 2273 as of 17-Jul-2021. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | cbvexv 2275* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 17-Jul-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvexvOLD 2276* | Obsolete proof of cbvexv 2275 as of 17-Jul-2021. (Contributed by NM, 21-Jun-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | cbvald 2277* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2337. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexd 2278* | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2337. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → Ⅎ𝑦𝜓) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2 2279* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 22-Dec-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 22-Apr-2018.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2 2280* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 14-Sep-2003.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 16-Jun-2019.) |
⊢ Ⅎ𝑧𝜑 & ⊢ Ⅎ𝑤𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ Ⅎ𝑦𝜓 & ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvaldva 2281* | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvaldvaOLD 2282* | Obsolete proof of cbvaldva 2281 as of 18-Jul-2021. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑦𝜒)) | ||
Theorem | cbvexdva 2283* | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. (Contributed by David Moews, 1-May-2017.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbvexdvaOLD 2284* | Obsolete proof of cbvexdva 2283 as of 18-Jul-2021. (Contributed by David Moews, 1-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑦𝜒)) | ||
Theorem | cbval2v 2285* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbval2vOLD 2286* | Obsolete proof of cbval2v 2285 as of 18-Jul-2021. (Contributed by NM, 4-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑧∀𝑤𝜓) | ||
Theorem | cbvex2v 2287* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 18-Jul-2021.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex2vOLD 2288* | Obsolete proof of cbvex2v 2287 as of 18-Jul-2021. (Contributed by NM, 26-Jul-1995.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤𝜓) | ||
Theorem | cbvex4v 2289* | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) |
⊢ ((𝑥 = 𝑣 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) & ⊢ ((𝑧 = 𝑓 ∧ 𝑤 = 𝑔) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃𝑥∃𝑦∃𝑧∃𝑤𝜑 ↔ ∃𝑣∃𝑢∃𝑓∃𝑔𝜒) | ||
Theorem | equs4 2290 | Lemma used in proofs of implicit substitution properties. The converse requires either a dv condition (sb56 2150) or a non-freeness hypothesis (equs45f 2350). See equs4v 1930 for a version requiring fewer axioms. (Contributed by NM, 10-May-1993.) (Proof shortened by Mario Carneiro, 20-May-2014.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | equsal 2291 | An equivalence related to implicit substitution. See equsalvw 1931 and equsalv 2108 for versions with dv conditions proved from fewer axioms. See also the dual form equsex 2292. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 5-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsex 2292 | An equivalence related to implicit substitution. See equsexvw 1932 and equsexv 2109 for versions with dv conditions proved from fewer axioms. See also the dual form equsal 2291. See equsexALT 2293 for an alternate proof. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Proof shortened by Wolf Lammen, 6-Feb-2018.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsexALT 2293 | Alternate proof of equsex 2292. This proves the result directly, instead of as a corollary of equsal 2291 via equs4 2290. Note in particular that only existential quantifiers appear in the proof and that the only step requiring ax-13 2246 is ax6e 2250. This proof mimics that of equsal 2291 (in particular, note that pm5.32i 669, exbii 1774, 19.41 2103, mpbiran 953 correspond respectively to pm5.74i 260, albii 1747, 19.23 2080, a1bi 352). (Contributed by BJ, 20-Aug-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsalh 2294 | An equivalence related to implicit substitution. See equsalhw 2123 for a version with a dv condition requiring fewer axioms. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexh 2295 | An equivalence related to implicit substitution. See equsexhv 2124 for a version with a dv condition which does not require ax-13 2246. (Contributed by NM, 5-Aug-1993.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | ax13lem2 2296* | Lemma for nfeqf2 2297. This lemma is equivalent to ax13v 2247 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018.) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020.) (New usage is discouraged.) |
⊢ (¬ 𝑥 = 𝑦 → (∃𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦)) | ||
Theorem | nfeqf2 2297* | An equation between setvar is free of any other setvar. (Contributed by Wolf Lammen, 9-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦) | ||
Theorem | dveeq2 2298* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) (Revised by NM, 20-Jul-2015.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) | ||
Theorem | nfeqf1 2299* | An equation between setvar is free of any other setvar. (Contributed by Wolf Lammen, 10-Jun-2019.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑦 = 𝑧) | ||
Theorem | dveeq1 2300* | Quantifier introduction when one pair of variables is distinct. (Contributed by NM, 2-Jan-2002.) Remove dependency on ax-11 2034. (Revised by Wolf Lammen, 8-Sep-2018.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 = 𝑧 → ∀𝑥 𝑦 = 𝑧)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |