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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.23t 2201 | Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23 2202. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) df-nf 1776 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.) |
⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
Theorem | 19.23 2202 | 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 2203 | 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 2204 | Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2198. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | alrimdd 2205 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2198. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | alrimd 2206 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2198. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximd 2207 | 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 2208 | Inference associated with 19.23 2202. 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 2209 | 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 2210 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2211. (Revised by Wolf Lammen, 3-Sep-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimdd 2211 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimddOLD 2212 | Obsolete version of exlimdd 2211 as of 3-Sep-2023. (Contributed by Mario Carneiro, 9-Feb-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimimddOLD 2213 | Obsolete version of exlimimdd 2210 as of 3-Sep-2023. (Contributed by ML, 17-Jul-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nexd 2214 | Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albid 2215 | Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbid 2216 | Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | nfbidf 2217 | 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 2218 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓)) | ||
Theorem | 19.17 2219 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓)) | ||
Theorem | 19.27 2220 | 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 2221 | 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 2222 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | 19.36 2223 | 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 2224 | Inference associated with 19.36 2223. See 19.36iv 1938 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 & ⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | 19.37 2225 | 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 2226 | 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 2227 | 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 2228 | 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 2229 | 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 2230 | 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 2231 | 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 2232* | Version of spim 2399 with a disjoint variable condition, which does not require ax-13 2383. See spimvw 1993 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2402 for another variant. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | chvarfv 2233* | Version of chvar 2407 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3v2 2234* | Version of cbv3 2409 with two disjoint variable conditions, which does not require ax-11 2151 nor ax-13 2383. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | sb4av 2235* | Version of sb4a 2505 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 15-Dec-2023.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | sbimd 2236 | 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 2237 | Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2136 and ax-13 2383. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2061. (Revised by Steven Nguyen, 11-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | 2sbbid 2238 | Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒)) | ||
Theorem | sbbidOLD 2239 | Obsolete version of sbbid 2237 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 2383. (Revised by Wolf Lammen, 24-Nov-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbequ1 2240 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2061. (Revised by BJ, 22-Dec-2020.) |
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)) | ||
Theorem | sbequ2 2241 | 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 2242 | Obsolete version of sbequ2 2241 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 2243 | 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 2244 | An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbequ12r 2245 | An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | sbelx 2246* | Elimination of substitution. Also see sbel2x 2494. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2383. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2136. (Revised by Gino Giotto, 20-Aug-2023.) |
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbequ12a 2247 | An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid 2248 | 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 2249* | Version of sbco 2545 with a disjoint variable condition using fewer axioms. (Contributed by Gino Giotto, 7-Aug-2023.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sb6a 2250* | Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid2vw 2251* | Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2547, at the expense of an extra distinct variable condition. (Contributed by Wolf Lammen, 5-Aug-2023.) |
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑) | ||
Theorem | axc16g 2252* | Generalization of axc16 2253. 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 2383, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2257. (Revised by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | axc16 2253* | Proof of older axiom ax-c16 35910. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gb 2254* | Biconditional strengthening of axc16g 2252. (Contributed by NM, 15-May-1993.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) | ||
Theorem | axc16nf 2255* | If dtru 5263 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 2256* | Version of axc11 2447 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 2447 which seems to require the full ax-12 2167 and ax-13 2383). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | axc11rv 2257* | Version of axc11r 2379 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 2447 which seems to require the full ax-12 2167 and ax-13 2383, and to axc11r 2379 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 2258 | 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 2259* | Version of equsal 2433 with a disjoint variable condition, which does not require ax-13 2383. See equsalvw 2001 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2260. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexv 2260* | Version of equsex 2434 with a disjoint variable condition, which does not require ax-13 2383. See equsexvw 2002 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2259. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | sbft 2261 | 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 2262 | 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 2263 | Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.) |
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | sbh 2264 | Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | nfs1v 2265* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v 2265 and hbs1 2266 combined. (Revised by Wolf Lammen, 28-Jul-2022.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | hbs1 2266* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1f 2267 | If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | sb5 2268* | 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 2499. Theorem sb5f 2534 replaces the disjoint variable condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) Shorten sb56 2269. (Revised by Wolf Lammen, 4-Sep-2023.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb56 2269* | Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct, namely, alternate definitions sb5 2268 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 2432 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v 1997, requires fewer axioms). Theorem equs45f 2477 replaces the disjoint variable condition with a non-freeness hypothesis and equs5 2478 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2260 in place of equsex 2434 in order to remove dependency on ax-13 2383. (Revised by BJ, 20-Dec-2020.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb56OLD 2270* | Obsolete version of sb56 2269 as of 4-Sep-2023. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2260 in place of equsex 2434 in order to remove dependency on ax-13 2383. (Revised by BJ, 20-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5av 2271* | Version of equs5a 2475 with a disjoint variable condition, which does not require ax-13 2383. See also sb56 2269. (Contributed by Gino Giotto, 15-Dec-2023.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb6OLD 2272* | 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 2500). Theorem sb6f 2533 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2495 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 2273* | Obsolete version of sb5 2268 as of 4-Sep-2023.) (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | 2sb5 2274* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑)) | ||
Theorem | sbco4lem 2275* | Lemma for sbco4 2276. It replaces the temporary variable 𝑣 with another temporary variable 𝑤. (Contributed by Jim Kingdon, 26-Sep-2018.) |
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | sbco4 2276* | 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 2277* | 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 2268, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2800. Theorem sb7h 2565 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 2278* | Obsolete version of dfsb7 2277 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 2279 | 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 2280* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) |
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | sbbibOLD 2281* | Obsolete version of sbbib 2373 as of 4-Sep-2023. (Contributed by AV, 6-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑦([𝑦 / 𝑥]𝜑 ↔ 𝜓) ↔ ∀𝑥(𝜑 ↔ [𝑥 / 𝑦]𝜓)) | ||
Theorem | nf5 2282 | 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 2283 | An alternate definition of df-nf 1776. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑)) | ||
Theorem | nf5d 2284 | Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | nf5di 2285 | 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 2286 | 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 2287 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2198 and 19.21v 1931. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.23h 2288 | Theorem 19.23 of [Margaris] p. 90. See 19.23 2202. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | exlimih 2289 | Inference associated with 19.23 2202. 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 2290 | Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | equsalhw 2291* | Version of equsalh 2436 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexhv 2292* | Version of equsexh 2437 with a disjoint variable condition, which does not require ax-13 2383. (Contributed by BJ, 31-May-2019.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | hba1 2293 | 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 2294 | Closed theorem version of bound-variable hypothesis builder hbn 2295. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbn 2295 | 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 2296 | Deduction form of bound-variable hypothesis builder hbn 2295. (Contributed by NM, 3-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓)) | ||
Theorem | hbim1 2297 | A closed form of hbim 2299. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hbimd 2298 | Deduction form of bound-variable hypothesis builder hbim 2299. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | ||
Theorem | hbim 2299 | 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 2300 | 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.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ∀𝑥(𝜑 ∧ 𝜓)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |