![]() |
Metamath
Proof Explorer Theorem List (p. 23 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48424) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | alrimi 2201 | Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2195. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
Theorem | alrimdd 2202 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2195. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | alrimd 2203 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2195. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
Theorem | eximd 2204 | Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1828. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
Theorem | exlimi 2205 | Inference associated with 19.23 2199. See exlimiv 1925 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 2206 | 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 2207 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2208. (Revised by Wolf Lammen, 3-Sep-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | exlimdd 2208 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | nexd 2209 | Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
Theorem | albid 2210 | Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
Theorem | exbid 2211 | Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
Theorem | nfbidf 2212 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1778 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒)) | ||
Theorem | 19.16 2213 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓)) | ||
Theorem | 19.17 2214 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓)) | ||
Theorem | 19.27 2215 | Theorem 19.27 of [Margaris] p. 90. See 19.27v 1985 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
Theorem | 19.28 2216 | Theorem 19.28 of [Margaris] p. 90. See 19.28v 1986 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 7-May-2025.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
Theorem | 19.19 2217 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓)) | ||
Theorem | 19.36 2218 | Theorem 19.36 of [Margaris] p. 90. See 19.36v 1983 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓)) | ||
Theorem | 19.36i 2219 | Inference associated with 19.36 2218. See 19.36iv 1942 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
⊢ Ⅎ𝑥𝜓 & ⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | 19.37 2220 | Theorem 19.37 of [Margaris] p. 90. See 19.37v 1987 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) | ||
Theorem | 19.32 2221 | Theorem 19.32 of [Margaris] p. 90. See 19.32v 1935 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)) | ||
Theorem | 19.31 2222 | Theorem 19.31 of [Margaris] p. 90. See 19.31v 1936 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.41 2223 | Theorem 19.41 of [Margaris] p. 90. See 19.41v 1945 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 2224 | Theorem 19.42 of [Margaris] p. 90. See 19.42v 1949 for a version requiring fewer axioms. See exan 1857 for an immediate version. (Contributed by NM, 18-Aug-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | ||
Theorem | 19.44 2225 | Theorem 19.44 of [Margaris] p. 90. See 19.44v 1988 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓)) | ||
Theorem | 19.45 2226 | Theorem 19.45 of [Margaris] p. 90. See 19.45v 1989 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓)) | ||
Theorem | spimfv 2227* | Specialization, using implicit substitution. Version of spim 2380 with a disjoint variable condition, which does not require ax-13 2365. See spimvw 1991 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2383 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
Theorem | chvarfv 2228* | Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2388 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
Theorem | cbv3v2 2229* | Version of cbv3 2390 with two disjoint variable conditions, which does not require ax-11 2146 nor ax-13 2365. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
Theorem | sbalex 2230* |
Equivalence of two ways to express proper substitution of a setvar for
another setvar disjoint from it in a formula. This proof of their
equivalence does not use df-sb 2060.
That both sides of the biconditional express proper substitution is proved by sb5 2262 and sb6 2080. The implication "to the left" is equs4v 1995 and does not require ax-10 2129 nor ax-12 2166. It also holds without disjoint variable condition if we allow more axioms (see equs4 2409). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2453 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2452 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2254 in place of equsex 2411 in order to remove dependency on ax-13 2365. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2060. (Revised by BJ, 21-Sep-2024.) |
⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | sb4av 2231* | Version of sb4a 2473 with a disjoint variable condition, which does not require ax-13 2365. The distinctor antecedent from sb4b 2468 is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | sbimd 2232 | Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2060. (Revised by Steven Nguyen, 9-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbbid 2233 | Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2129 and ax-13 2365. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2060. (Revised by Steven Nguyen, 11-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | 2sbbid 2234 | Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒)) | ||
Theorem | sbequ1 2235 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2060. (Revised by BJ, 22-Dec-2020.) |
⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)) | ||
Theorem | sbequ2 2236 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2060. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.) |
⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑)) | ||
Theorem | stdpc7 2237 | One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2023.) 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 2238 | An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | ||
Theorem | sbequ12r 2239 | An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) | ||
Theorem | sbelx 2240* | Elimination of substitution. Also see sbel2x 2467. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2365. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2129. (Revised by GG, 20-Aug-2023.) |
⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbequ12a 2241 | An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid 2242 | 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 2243* | A composition law for substitution. Version of sbco 2500 with a disjoint variable condition using fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by GG, 7-Aug-2023.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sb6a 2244* | Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)) | ||
Theorem | sbid2vw 2245* | Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2502, at the expense of an extra distinct variable condition. (Contributed by NM, 14-May-1993.) (Revised by Wolf Lammen, 5-Aug-2023.) |
⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑) | ||
Theorem | axc16g 2246* | Generalization of axc16 2247. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2003 }, Theorem ax12v 2167. (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 2365, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2251. (Revised by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | axc16 2247* | Proof of older axiom ax-c16 38494. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gb 2248* | Biconditional strengthening of axc16g 2246. (Contributed by NM, 15-May-1993.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) | ||
Theorem | axc16nf 2249* | If dtru 5438 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 2146. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2129. (Revised by Wolf Lammen, 12-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
Theorem | axc11v 2250* | Version of axc11 2423 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2003 }, from ax12v 2167 (contrary to axc11 2423 which seems to require the full ax-12 2166 and ax-13 2365). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
Theorem | axc11rv 2251* | Version of axc11r 2359 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2003 }, from ax12v 2167 (contrary to axc11 2423 which seems to require the full ax-12 2166 and ax-13 2365, and to axc11r 2359 which seems to require the full ax-12 2166). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑)) | ||
Theorem | drsb2 2252 | 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 2253* | An equivalence related to implicit substitution. Version of equsal 2410 with a disjoint variable condition, which does not require ax-13 2365. See equsalvw 1999 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2254. (Contributed by NM, 2-Jun-1993.) (Revised by BJ, 31-May-2019.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexv 2254* | An equivalence related to implicit substitution. Version of equsex 2411 with a disjoint variable condition, which does not require ax-13 2365. See equsexvw 2000 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2253. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid ax-10 2129. (Revised by GG, 18-Nov-2024.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | equsexvOLD 2255* | Obsolete version of equsexv 2254 as of 18-Nov-2024. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | sbft 2256 | Substitution has no effect on a nonfree variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.) |
⊢ (Ⅎ𝑥𝜑 → ([𝑦 / 𝑥]𝜑 ↔ 𝜑)) | ||
Theorem | sbf 2257 | Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2083. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | sbf2 2258 | Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.) |
⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
Theorem | sbh 2259 | Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
Theorem | hbs1 2260* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1f 2261 | If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | sb5 2262* | Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v 2082 and even needs no disjoint variable condition, see sb1 2471. Theorem sb5f 2491 replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Revised by Wolf Lammen, 4-Sep-2023.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb5OLD 2263* | Obsolete version of sb5 2262 as of 21-Sep-2024. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb56OLD 2264* | Obsolete version of sbalex 2230 as of 21-Sep-2024. Two equivalent ways of expressing the proper substitution of 𝑦 for 𝑥 in 𝜑, when 𝑥 and 𝑦 are distinct, namely, alternate definitions sb5 2262 and sb6 2080. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 2060. The implication "to the left" is equs4 2409 and does not require any disjoint variable condition (but the version with a disjoint variable condition, equs4v 1995, requires fewer axioms). Theorem equs45f 2452 replaces the disjoint variable condition with a nonfreeness hypothesis and equs5 2453 replaces it with a distinctor as antecedent. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2254 in place of equsex 2411 in order to remove dependency on ax-13 2365. (Revised by BJ, 20-Dec-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | equs5av 2265* | A property related to substitution that replaces the distinctor from equs5 2453 to a disjoint variable condition. Version of equs5a 2450 with a disjoint variable condition, which does not require ax-13 2365. See also sbalex 2230. (Contributed by NM, 2-Feb-2007.) (Revised by GG, 15-Dec-2023.) |
⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | 2sb5 2266* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑)) | ||
Theorem | sbco4lemOLD 2267* | Obsolete version of sbco4lem 2163 as of 12-Oct-2024. (Contributed by Jim Kingdon, 26-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑥 / 𝑣][𝑦 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑥 / 𝑤][𝑦 / 𝑥][𝑤 / 𝑦]𝜑) | ||
Theorem | dfsb7 2268* | An alternate definition of proper substitution df-sb 2060. 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 2262, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2703. Theorem sb7h 2519 provides a version where 𝜑 and 𝑦 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2060. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sbn 2269 | 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 2060. (Revised by BJ, 25-Dec-2020.) |
⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑) | ||
Theorem | sbex 2270* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) |
⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | nf5 2271 | Alternate definition of df-nf 1778. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1778 changed. (Revised by Wolf Lammen, 11-Sep-2021.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | ||
Theorem | nf6 2272 | An alternate definition of df-nf 1778. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(∃𝑥𝜑 → 𝜑)) | ||
Theorem | nf5d 2273 | Deduce that 𝑥 is not free in 𝜓 in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → Ⅎ𝑥𝜓) | ||
Theorem | nf5di 2274 | 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 2275 | 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 2276 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See also 19.21 2195 and 19.21v 1934. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
Theorem | 19.23h 2277 | Theorem 19.23 of [Margaris] p. 90. See 19.23 2199. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
⊢ (𝜓 → ∀𝑥𝜓) ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
Theorem | exlimih 2278 | Inference associated with 19.23 2199. See exlimiv 1925 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 2279 | Deduction form of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-Jan-1997.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜒 → ∀𝑥𝜒) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒)) | ||
Theorem | equsalhw 2280* | Version of equsalh 2413 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
Theorem | equsexhv 2281* | An equivalence related to implicit substitution. Version of equsexh 2414 with a disjoint variable condition, which does not require ax-13 2365. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) |
⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
Theorem | hba1 2282 | 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 2283 | Closed theorem version of bound-variable hypothesis builder hbn 2284. (Contributed by NM, 10-May-1993.) (Proof shortened by Wolf Lammen, 14-Oct-2021.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜑) → (¬ 𝜑 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbn 2284 | 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 2285 | Deduction form of bound-variable hypothesis builder hbn 2284. (Contributed by NM, 3-Jan-2002.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ (𝜑 → (¬ 𝜓 → ∀𝑥 ¬ 𝜓)) | ||
Theorem | hbim1 2286 | A closed form of hbim 2288. (Contributed by NM, 2-Jun-1993.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) ⇒ ⊢ ((𝜑 → 𝜓) → ∀𝑥(𝜑 → 𝜓)) | ||
Theorem | hbimd 2287 | Deduction form of bound-variable hypothesis builder hbim 2288. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) |
⊢ (𝜑 → ∀𝑥𝜑) & ⊢ (𝜑 → (𝜓 → ∀𝑥𝜓)) & ⊢ (𝜑 → (𝜒 → ∀𝑥𝜒)) ⇒ ⊢ (𝜑 → ((𝜓 → 𝜒) → ∀𝑥(𝜓 → 𝜒))) | ||
Theorem | hbim 2288 | 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 2289 | 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 2290 | 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 | sbi2 2291 | Introduction of implication into substitution. (Contributed by NM, 14-May-1993.) |
⊢ (([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) → [𝑦 / 𝑥](𝜑 → 𝜓)) | ||
Theorem | sbim 2292 | Implication inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbrim 2293 | Substitution in an implication with a variable not free in the antecedent affects only the consequent. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) Avoid ax-10 2129. (Revised by GG, 20-Nov-2024.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbrimOLD 2294 | Obsolete version of sbrim 2293 as of 20-Nov-2024. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblim 2295 | Substitution in an implication with a variable not free in the consequent affects only the antecedent. (Contributed by NM, 14-Nov-2013.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜓 ⇒ ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ([𝑦 / 𝑥]𝜑 → 𝜓)) | ||
Theorem | sbor 2296 | Disjunction inside and outside of a substitution are equivalent. (Contributed by NM, 29-Sep-2002.) |
⊢ ([𝑦 / 𝑥](𝜑 ∨ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ∨ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbbi 2297 | Equivalence inside and outside of a substitution are equivalent. (Contributed by NM, 14-May-1993.) |
⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜓) ↔ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sblbis 2298 | Introduce left biconditional inside of a substitution. (Contributed by NM, 19-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜒 ↔ 𝜑) ↔ ([𝑦 / 𝑥]𝜒 ↔ 𝜓)) | ||
Theorem | sbrbis 2299 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbrbif 2300 | Introduce right biconditional inside of a substitution. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
⊢ Ⅎ𝑥𝜒 & ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝑦 / 𝑥](𝜑 ↔ 𝜒) ↔ (𝜓 ↔ 𝜒)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |