Home | Metamath
Proof Explorer Theorem List (p. 23 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.23 2201 | Theorem 19.23 of [Margaris] p. 90. See 19.23v 1934 for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | alimd 2202 | Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1802. See alimdh 1809, alimdv 1908 for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
Theorem | alrimi 2203 | Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2197. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | alrimdd 2204 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2197. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | alrimd 2205 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2197. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximd 2206 | Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1825. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | exlimi 2207 | Inference associated with 19.23 2201. See exlimiv 1922 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exlimd 2208 | Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 23-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 12-Jan-2018.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | exlimimdd 2209 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2210. (Revised by Wolf Lammen, 3-Sep-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimdd 2210 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimddOLD 2211 | Obsolete version of exlimdd 2210 as of 3-Sep-2023. (Contributed by Mario Carneiro, 9-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimimddOLD 2212 | Obsolete version of exlimimdd 2209 as of 3-Sep-2023. (Contributed by ML, 17-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nexd 2213 | Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albid 2214 | Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbid 2215 | Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | nfbidf 2216 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1776 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒)) | ||
Theorem | 19.16 2217 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓)) | ||
Theorem | 19.17 2218 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓)) | ||
Theorem | 19.27 2219 | Theorem 19.27 of [Margaris] p. 90. See 19.27v 1987 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28 2220 | Theorem 19.28 of [Margaris] p. 90. See 19.28v 1988 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.19 2221 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | 19.36 2222 | Theorem 19.36 of [Margaris] p. 90. See 19.36v 1985 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓)) | ||
Theorem | 19.36i 2223 | Inference associated with 19.36 2222. See 19.36iv 1938 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 & ⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | 19.37 2224 | Theorem 19.37 of [Margaris] p. 90. See 19.37v 1989 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.32 2225 | Theorem 19.32 of [Margaris] p. 90. See 19.32v 1932 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)) | ||
Theorem | 19.31 2226 | Theorem 19.31 of [Margaris] p. 90. See 19.31v 1933 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.41 2227 | Theorem 19.41 of [Margaris] p. 90. See 19.41v 1941 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.42 2228 | Theorem 19.42 of [Margaris] p. 90. See 19.42v 1945 for a version requiring fewer axioms. See exan 1853 for an immediate version. (Contributed by NM, 18-Aug-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.44 2229 | Theorem 19.44 of [Margaris] p. 90. See 19.44v 1990 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.45 2230 | Theorem 19.45 of [Margaris] p. 90. See 19.45v 1991 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | spimfv 2231* | Version of spim 2396 with a disjoint variable condition, which does not require ax-13 2381. See spimvw 1993 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2399 for another variant. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | chvarfv 2232* | Version of chvar 2404 with a disjoint variable condition, which does not require ax-13 2381. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3v2 2233* | Version of cbv3 2406 with two disjoint variable conditions, which does not require ax-11 2151 nor ax-13 2381. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | sb4av 2234* | Version of sb4a 2502 with a disjoint variable condition, which does not require ax-13 2381. (Contributed by BJ, 15-Dec-2023.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | sbimd 2235 | Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2061. (Revised by Steven Nguyen, 9-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbbid 2236 | Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2136 and ax-13 2381. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2061. (Revised by Steven Nguyen, 11-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | 2sbbid 2237 | Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒)) | ||
Theorem | sbbidOLD 2238 | Obsolete version of sbbid 2236 as of 10-Jul-2023. Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2136 and ax-13 2381. (Revised by Wolf Lammen, 24-Nov-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbequ1 2239 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) |
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)) | ||
Theorem | sbequ2 2240 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.) |
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑)) | ||
Theorem | sbequ2OLD 2241 | Obsolete version of sbequ2 2240 as of 3-Feb-2024. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑)) | ||
Theorem | stdpc7 2242 | One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2026.) 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 | sbequ12 2243 | An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbequ12r 2244 | An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | sbelx 2245* | Elimination of substitution. Also see sbel2x 2491. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2381. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2136. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbequ12a 2246 | An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid 2247 | An identity theorem for substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 30-Sep-2018.) |
⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | sbcov 2248* | Version of sbco 2542 with a disjoint variable condition using fewer axioms. (Contributed by Gino Giotto, 7-Aug-2023.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sb6a 2249* | Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid2vw 2250* | Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2544, at the expense of an extra distinct variable condition. (Contributed by Wolf Lammen, 5-Aug-2023.) |
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑) | ||
Theorem | axc16g 2251* | Generalization of axc16 2252. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2006 }, theorem ax12v 2168. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 18-Feb-2018.) Remove dependency on ax-13 2381, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2256. (Revised by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | axc16 2252* | Proof of older axiom ax-c16 35908. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gb 2253* | Biconditional strengthening of axc16g 2251. (Contributed by NM, 15-May-1993.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) | ||
Theorem | axc16nf 2254* | If dtru 5262 is false, then there is only one element in the universe, so everything satisfies Ⅎ. (Contributed by Mario Carneiro, 7-Oct-2016.) Remove dependency on ax-11 2151. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2136. (Revised by Wolf lammen, 12-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | axc11v 2255* | Version of axc11 2444 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2006 }, from ax12v 2168 (contrary to axc11 2444 which seems to require the full ax-12 2167 and ax-13 2381). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | axc11rv 2256* | Version of axc11r 2377 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2006 }, from ax12v 2168 (contrary to axc11 2444 which seems to require the full ax-12 2167 and ax-13 2381, and to axc11r 2377 which seems to require the full ax-12 2167). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑)) | ||
Theorem | drsb2 2257 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). (Contributed by NM, 27-Feb-2005.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | equsalv 2258* | Version of equsal 2430 with a disjoint variable condition, which does not require ax-13 2381. See equsalvw 2001 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2259. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexv 2259* | Version of equsex 2431 with a disjoint variable condition, which does not require ax-13 2381. See equsexvw 2002 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2258. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | sbft 2260 | Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbf 2261 | Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2089. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | sbf2 2262 | Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.) |
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | sbh 2263 | Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | nfs1v 2264* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2264 and hbs1 2265 combined. (Revised by Wolf Lammen, 28-Jul-2022.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | hbs1 2265* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1f 2266 | If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | sb5 2267* | Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v 2086 and even needs no disjoint variable condition, see sb1 2496. Theorem sb5f 2531 replaces the disjoint variable condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) Shorten sb56 2268. (Revised by Wolf Lammen, 4-Sep-2023.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb56 2268* | Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct, namely, alternate definitions sb5 2267 and sb6 2084. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 2061. The implication "to the left" is equs4 2429 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v 1997, requires fewer axioms). Theorem equs45f 2474 replaces the disjoint variable condition with a non-freeness hypothesis and equs5 2475 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2259 in place of equsex 2431 in order to remove dependency on ax-13 2381. (Revised by BJ, 20-Dec-2020.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb56OLD 2269* | Obsolete version of sb56 2268 as of 4-Sep-2023. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2259 in place of equsex 2431 in order to remove dependency on ax-13 2381. (Revised by BJ, 20-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5av 2270* | Version of equs5a 2472 with a disjoint variable condition, which does not require ax-13 2381. See also sb56 2268. (Contributed by Gino Giotto, 15-Dec-2023.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb6OLD 2271* | Obsolete version of sb6 2084 as of 7-Jul-2023. Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. The implication "to the left", sb2vOLD 2088, also holds without a disjoint variable condition (sb2 2497). Theorem sb6f 2530 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2492 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5OLD 2272* | Obsolete version of sb5 2267 as of 4-Sep-2023.) (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | 2sb5 2273* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑)) | ||
Theorem | sbco4lem 2274* | Lemma for sbco4 2275. It replaces the temporary variable 𝑣 with another temporary variable 𝑤. (Contributed by Jim Kingdon, 26-Sep-2018.) |
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sbco4 2275* | 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 | dfsb7 2276* | An alternate definition of proper substitution df-sb 2061. 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 2267, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2797. Theorem sb7h 2562 provides a version where 𝜑 and 𝑦 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2061. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | dfsb7OLD 2277* | Obsolete version of dfsb7 2276 as of 3-Sep-2023. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2061. (Revised by BJ, 25-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sbn 2278 | Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) Revise df-sb 2061. (Revised by BJ, 25-Dec-2020.) |
⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑) | ||
Theorem | sbex 2279* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) |
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | sbbibOLD 2280* | Obsolete version of sbbib 2371 as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | nf5 2281 | Alternate definition of df-nf 1776. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1776 changed. (Revised by Wolf Lammen, 11-Sep-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | ||
Theorem | nf6 2282 | An alternate definition of df-nf 1776. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑)) | ||
Theorem | nf5d 2283 | Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | nf5di 2284 | Since the converse holds by a1i 11, this inference shows that we can represent a not-free hypothesis with either Ⅎ𝑥𝜑 (inference form) or (𝜑 → Ⅎ𝑥𝜑) (deduction form). (Contributed by NM, 17-Aug-2018.) (Proof shortened by Wolf Lammen, 10-Jul-2019.) |
⊢ (𝜑 → Ⅎ𝑥𝜑) ⇒ ⊢ Ⅎ𝑥𝜑 | ||
Theorem | 19.9h 2285 | A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) (Proof shortened by Wolf Lammen, 5-Jan-2018.) (Proof shortened by Wolf Lammen, 14-Jul-2020.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∃𝑥𝜑 ↔ 𝜑) | ||
Theorem | 19.21h 2286 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2197 and 19.21v 1931. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.23h 2287 | Theorem 19.23 of [Margaris] p. 90. See 19.23 2201. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | exlimih 2288 | Inference associated with 19.23 2201. See exlimiv 1922 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (∃𝑥𝜑 → 𝜓) | ||
Theorem | exlimdh 2289 | Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | equsalhw 2290* | Version of equsalh 2433 with a disjoint variable condition, which does not require ax-13 2381. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexhv 2291* | Version of equsexh 2434 with a disjoint variable condition, which does not require ax-13 2381. (Contributed by BJ, 31-May-2019.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | hba1 2292 | The setvar 𝑥 is not free in ∀𝑥𝜑. This corresponds to the axiom (4) of modal logic. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 24-Jan-1993.) (Proof shortened by Wolf Lammen, 12-Oct-2021.) |
⊢ (∀𝑥𝜑 → ∀𝑥∀𝑥𝜑) | ||
Theorem | hbnt 2293 | Closed theorem version of bound-variable hypothesis builder hbn 2294. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbn 2294 | If 𝑥 is not free in 𝜑, it is not free in ¬ 𝜑. (Contributed by NM, 10-Jan-1993.) (Proof shortened by Wolf Lammen, 17-Dec-2017.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (¬ 𝜑 → ∀𝑥 ¬ 𝜑) | ||
Theorem | hbnd 2295 | Deduction form of bound-variable hypothesis builder hbn 2294. (Contributed by NM, 3-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓)) | ||
Theorem | hbim1 2296 | A closed form of hbim 2298. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hbimd 2297 | Deduction form of bound-variable hypothesis builder hbim 2298. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | ||
Theorem | hbim 2298 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 → 𝜓). (Contributed by NM, 24-Jan-1993.) (Proof shortened by Mel L. O'Cat, 3-Mar-2008.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hban 2299 | If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ∧ 𝜓). (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | hb3an 2300 | If 𝑥 is not free in 𝜑, 𝜓, and 𝜒, it is not free in (𝜑 ∧ 𝜓 ∧ 𝜒). (Contributed by NM, 14-Sep-2003.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |