![]() |
Metamath
Proof Explorer Theorem List (p. 23 of 437) | < 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: | ![]() (1-28351) |
![]() (28352-29876) |
![]() (29877-43667) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | alrimd 2201 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2192. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximd 2202 | Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1877. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | exlimi 2203 | Inference associated with 19.23 2197. See exlimiv 1973 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 2204 | 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 | exlimdd 2205 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimimdd 2206 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nexd 2207 | Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albid 2208 | Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbid 2209 | Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | nfbidf 2210 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1828 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒)) | ||
Theorem | 19.16 2211 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓)) | ||
Theorem | 19.17 2212 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓)) | ||
Theorem | 19.27 2213 | Theorem 19.27 of [Margaris] p. 90. See 19.27v 2038 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28 2214 | Theorem 19.28 of [Margaris] p. 90. See 19.28v 2039 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.19 2215 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | 19.36 2216 | Theorem 19.36 of [Margaris] p. 90. See 19.36v 2036 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓)) | ||
Theorem | 19.36i 2217 | Inference associated with 19.36 2216. See 19.36iv 1989 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 & ⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | 19.37 2218 | Theorem 19.37 of [Margaris] p. 90. See 19.37v 2040 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.32 2219 | Theorem 19.32 of [Margaris] p. 90. See 19.32v 1983 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)) | ||
Theorem | 19.31 2220 | Theorem 19.31 of [Margaris] p. 90. See 19.31v 1984 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.41 2221 | Theorem 19.41 of [Margaris] p. 90. See 19.41v 1992 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-1OLD 2222 | One direction of 19.42 2223. Obsolete as of 9-Oct-2022. (Contributed by Wolf Lammen, 10-Jul-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ((𝜑 ∧ ∃𝑥𝜓) → ∃𝑥(𝜑 ∧ 𝜓)) | ||
Theorem | 19.42 2223 | Theorem 19.42 of [Margaris] p. 90. See 19.42v 1996 for a version requiring fewer axioms. See exan 1906 for an immediate version. (Contributed by NM, 18-Aug-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.44 2224 | Theorem 19.44 of [Margaris] p. 90. See 19.44v 2041 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.45 2225 | Theorem 19.45 of [Margaris] p. 90. See 19.45v 2042 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | sbimd 2226 | Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbbid 2227 | Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2135 and ax-13 2334. (Revised by Wolf Lammen, 24-Nov-2022.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbequ1 2228 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbequ12 2229 | An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbequ12r 2230 | An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | sbequ12a 2231 | An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid 2232 | 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 | axc16g 2233* | Generalization of axc16 2234. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2055 }, theorem ax12v 2164. (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 2334, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2238. (Revised by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | axc16 2234* | Proof of older axiom ax-c16 35051. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gb 2235* | Biconditional strengthening of axc16g 2233. (Contributed by NM, 15-May-1993.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) | ||
Theorem | axc16nf 2236* | If dtru 5084 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 2150. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2135. (Revised by Wolf lammen, 12-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | axc11v 2237* | Version of axc11 2396 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2055 }, from ax12v 2164 (contrary to axc11 2396 which seems to require the full ax-12 2163 and ax-13 2334). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | axc11rv 2238* | Version of axc11r 2333 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2055 }, from ax12v 2164 (contrary to axc11 2396 which seems to require the full ax-12 2163 and ax-13 2334). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑)) | ||
Theorem | spimv1 2239* | Version of spim 2352 with a disjoint variable condition, which does not require ax-13 2334. See spimvw 2045 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2355 for another variant. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | cbv3v2 2240* | Version of cbv3 2362 with two disjoint variable conditions, which does not require ax-11 2150 nor ax-13 2334. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | equsalv 2241* | Version of equsal 2382 with a disjoint variable condition, which does not require ax-13 2334. See equsalvw 2051 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2242. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexv 2242* | Version of equsex 2383 with a disjoint variable condition, which does not require ax-13 2334. See equsexvw 2052 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2241. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | sb2v 2243* | Version of sb2 2427 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | stdpc4v 2244* | If a statement 𝜑 holds for all 𝑥, then it also holds for the specific case of 𝑦 (properly) substituted for 𝑥. Version of stdpc4 2428 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) |
⊢ (∀𝑥𝜑 → [𝑦 / 𝑥]𝜑) | ||
Theorem | sbftv 2245* | Substitution for a variable not free in a wff does not affect it, closed form. Version of sbft 2455 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbfv 2246* | Substitution for a variable not free in a wff does not affect it. Version of sbf 2456 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | equsb1vOLD 2247* | Obsolete version of equsb1v 2049 as of 30-May-2023. (Contributed by BJ, 11-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | sb56 2248* | Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 2012. The implication "to the left" is equs4 2381 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v 2050, requires fewer axioms). Theorem equs45f 2425 replaces the disjoint variable condition with a non-freeness hypothesis and equs5 2426 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2242 in place of equsex 2383 in order to remove dependency on ax-13 2334. (Revised by BJ, 20-Dec-2020.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb4v 2249* | Version of sb4 2432 with a disjoint variable condition instead of a distinctor antecedent, which does not require ax-13 2334. (Contributed by BJ, 23-Jun-2019.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb6 2250* | 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", sb2v 2243, also holds without a disjoint variable condition (sb2 2427). Theorem sb6f 2461 replaces the disjoint variable condition with a non-freeness hypothesis. Theorem sb4b 2434 replaces it with a distinctor antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5 2251* | Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1 2014 and does not require any disjoint variable condition. Theorem sb5f 2462 replaces the disjoint variable condition with a non-freeness hypothesis. (Contributed by NM, 18-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | 2sb5 2252* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑)) | ||
Theorem | 2sb6 2253* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∀𝑥∀𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝜑)) | ||
Theorem | nfs1v 2254* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by Mario Carneiro, 11-Aug-2016.) Shorten nfs1v and hbs1 2255 combined. (Revised by Wolf Lammen, 28-Jul-2022.) |
⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | hbs1 2255* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nf5 2256 | Alternate definition of df-nf 1828. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1828 changed. (Revised by Wolf Lammen, 11-Sep-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | ||
Theorem | nf6 2257 | An alternate definition of df-nf 1828. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑)) | ||
Theorem | nf5d 2258 | Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | nf5di 2259 | 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 2260 | 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 2261 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2192 and 19.21v 1982. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.23h 2262 | Theorem 19.23 of [Margaris] p. 90. See 19.23 2197. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | exlimih 2263 | Inference associated with 19.23 2197. See exlimiv 1973 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 2264 | Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | equsalhw 2265* | Version of equsalh 2385 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsalhwOLD 2266* | Obsolete version of equsalhw 2265 as of 8-Jul-2022. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexhv 2267* | Version of equsexh 2386 with a disjoint variable condition, which does not require ax-13 2334. (Contributed by BJ, 31-May-2019.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | hba1 2268 | 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 2269 | Closed theorem version of bound-variable hypothesis builder hbn 2270. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbn 2270 | 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 2271 | Deduction form of bound-variable hypothesis builder hbn 2270. (Contributed by NM, 3-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓)) | ||
Theorem | hbim1 2272 | A closed form of hbim 2274. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hbimd 2273 | Deduction form of bound-variable hypothesis builder hbim 2274. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | ||
Theorem | hbim 2274 | 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 2275 | 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 2276 | 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.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → ∀𝑥(𝜑 ∧ 𝜓 ∧ 𝜒)) | ||
Theorem | sbnv 2277* | Substitution is not affected by negation. Version of sbn 2467 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbi1v 2278* | Move implication out of substitution. Version of sbi1 2468 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbi2v 2279* | Move implication into substitution. Version of sbi2 2469 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbimv 2280* | Substitution distributes over implication. Version of sbim 2471 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbanv 2281* | Substitution distributes over conjunction. Version of sban 2475 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 ∧ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∧ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbiv 2282* | Substitution distributes over a biconditional. Version of sbbi 2477 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbimv 2283* | Specialization of implication. Version of spsbim 2470 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 19-Jan-2023.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | spsbimvOLD 2284* | Obsolete version of spsbimv 2283 as of 16-Mar-2023. (Contributed by Wolf Lammen, 19-Jan-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥(𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbisv 2285* | Introduce left biconditional inside of a substitution. Version of sblbis 2480 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbiev 2286* | Conversion of implicit substitution to explicit substitution. Version of sbie 2484 with a disjoint variable condition, not requiring ax-13 2334. (Contributed by Wolf Lammen, 18-Jan-2023.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbequivv 2287* | Version of sbequi 2451 with disjoint variable conditions, not requiring ax-13 2334. (Contributed by Wolf Lammen, 19-Jan-2023.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | sbequvv 2288* | Version of sbequ 2452 with disjoint variable conditions, not requiring ax-13 2334. (Contributed by Wolf Lammen, 19-Jan-2023.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) | ||
Theorem | sbcom3vv 2289* | Version of sbcom3 2487 with disjoint variable conditions, not requiring ax-13 2334. (Contributed by Wolf Lammen, 19-Jan-2023.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | sbco2vv 2290* | Version of sbco2 2492 with disjoint variable conditions, not requiring ax-13 2334. (Contributed by Wolf Lammen, 29-Apr-2023.) |
⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | equsb3v 2291* | Version of equsb3 2510 with an extra disjoint variable condition on 𝑥 and 𝑦, not requiring ax-13 2334. (Contributed by Raph Levien and FL, 4-Dec-2005.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Remove dependency on ax-13 2334. (Revised by Wolf Lammen, 19-Jan-2023.) |
⊢ ([𝑥 / 𝑦]𝑦 = 𝑧 ↔ 𝑥 = 𝑧) | ||
Theorem | axc7 2292 |
Show that the original axiom ax-c7 35044 can be derived from ax-10 2135
(hbn1 2136) , sp 2167 and propositional calculus. See ax10fromc7 35054 for the
rederivation of ax-10 2135 from ax-c7 35044.
Normally, axc7 2292 should be used rather than ax-c7 35044, except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008.) |
⊢ (¬ ∀𝑥 ¬ ∀𝑥𝜑 → 𝜑) | ||
Theorem | axc7e 2293 | Abbreviated version of axc7 2292 using the existential quantifier. Corresponds to the dual of Axiom (B) of modal logic. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
⊢ (∃𝑥∀𝑥𝜑 → 𝜑) | ||
Theorem | modal-b 2294 | The analogue in our predicate calculus of the Brouwer axiom (B) of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
⊢ (𝜑 → ∀𝑥 ¬ ∀𝑥 ¬ 𝜑) | ||
Theorem | 19.9ht 2295 | A closed version of 19.9h 2260. (Contributed by NM, 13-May-1993.) (Proof shortened by Wolf Lammen, 3-Mar-2018.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (∃𝑥𝜑 → 𝜑)) | ||
Theorem | axc4 2296 |
Show that the original axiom ax-c4 35043 can be derived from ax-4 1853
(alim 1854), ax-10 2135 (hbn1 2136), sp 2167 and propositional calculus. See
ax4fromc4 35053 for the rederivation of ax-4 1853
from ax-c4 35043.
Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114. (Contributed by NM, 21-May-2008.) (Proof modification is discouraged.) |
⊢ (∀𝑥(∀𝑥𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓)) | ||
Theorem | axc4i 2297 | Inference version of axc4 2296. (Contributed by NM, 3-Jan-1993.) |
⊢ (∀𝑥𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑥𝜓) | ||
Theorem | axc7eOLD 2298 | Obsolete version of axc7e 2293 as of 8-Jul-2022. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∃𝑥∀𝑥𝜑 → 𝜑) | ||
Theorem | nfal 2299 | If 𝑥 is not free in 𝜑, it is not free in ∀𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∀𝑦𝜑 | ||
Theorem | nfex 2300 | If 𝑥 is not free in 𝜑, it is not free in ∃𝑦𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Reduce symbol count in nfex 2300, hbex 2301. (Revised by Wolf Lammen, 16-Oct-2021.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥∃𝑦𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |