| Metamath
Proof Explorer Theorem List (p. 23 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 19.3t 2201 | Closed form of 19.3 2202 and version of 19.9t 2204 with a universal quantifier. (Contributed by NM, 9-Nov-2020.) (Proof shortened by BJ, 9-Oct-2022.) |
| ⊢ (Ⅎ𝑥𝜑 → (∀𝑥𝜑 ↔ 𝜑)) | ||
| Theorem | 19.3 2202 | A wff may be quantified with a variable not free in it. Version of 19.9 2205 with a universal quantifier. Theorem 19.3 of [Margaris] p. 89. See 19.3v 1981 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ 𝜑) | ||
| Theorem | 19.9d 2203 | A deduction version of one direction of 19.9 2205. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) df-nf 1784 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
| ⊢ (𝜓 → Ⅎ𝑥𝜑) ⇒ ⊢ (𝜓 → (∃𝑥𝜑 → 𝜑)) | ||
| Theorem | 19.9t 2204 | Closed form of 19.9 2205 and version of 19.3t 2201 with an existential quantifier. (Contributed by NM, 13-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 14-Jul-2020.) |
| ⊢ (Ⅎ𝑥𝜑 → (∃𝑥𝜑 ↔ 𝜑)) | ||
| Theorem | 19.9 2205 | A wff may be existentially quantified with a variable not free in it. Version of 19.3 2202 with an existential quantifier. Theorem 19.9 of [Margaris] p. 89. See 19.9v 1983 for a version requiring fewer axioms. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) Revised to shorten other proofs. (Revised by Wolf Lammen, 14-Jul-2020.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ 𝜑) | ||
| Theorem | 19.21t 2206 | Closed form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2207. (Contributed by NM, 27-May-1997.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 3-Jan-2018.) df-nf 1784 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 3-Nov-2021.) |
| ⊢ (Ⅎ𝑥𝜑 → (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))) | ||
| Theorem | 19.21 2207 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as "𝑥 is not free in 𝜑". See 19.21v 1939 for a version requiring fewer axioms. See also 19.21h 2287. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) df-nf 1784 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) | ||
| Theorem | stdpc5 2208 | An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎ𝑥𝜑 can be thought of as emulating "𝑥 is not free in 𝜑". With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example 𝑥 would not (for us) be free in 𝑥 = 𝑥 by nfequid 2012. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. See stdpc5v 1938 for a version requiring fewer axioms. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) Remove dependency on ax-10 2141. (Revised by Wolf Lammen, 4-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) | ||
| Theorem | 19.21-2 2209 | Version of 19.21 2207 with two quantifiers. (Contributed by NM, 4-Feb-2005.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥∀𝑦𝜓)) | ||
| Theorem | 19.23t 2210 | Closed form of Theorem 19.23 of [Margaris] p. 90. See 19.23 2211. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 13-Aug-2020.) df-nf 1784 changed. (Revised by Wolf Lammen, 11-Sep-2021.) (Proof shortened by BJ, 8-Oct-2022.) |
| ⊢ (Ⅎ𝑥𝜓 → (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓))) | ||
| Theorem | 19.23 2211 | Theorem 19.23 of [Margaris] p. 90. See 19.23v 1942 for a version requiring fewer axioms. (Contributed by NM, 24-Jan-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (∃𝑥𝜑 → 𝜓)) | ||
| Theorem | alimd 2212 | Deduction form of Theorem 19.20 of [Margaris] p. 90, see alim 1810. See alimdh 1817, alimdv 1916 for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 → ∀𝑥𝜒)) | ||
| Theorem | alrimi 2213 | Inference form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2207. (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜑 → ∀𝑥𝜓) | ||
| Theorem | alrimdd 2214 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2207. (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
| Theorem | alrimd 2215 | Deduction form of Theorem 19.21 of [Margaris] p. 90, see 19.21 2207. (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜓 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (𝜓 → ∀𝑥𝜒)) | ||
| Theorem | eximd 2216 | Deduction form of Theorem 19.22 of [Margaris] p. 90, see exim 1834. (Contributed by NM, 29-Jun-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒)) | ||
| Theorem | exlimi 2217 | Inference associated with 19.23 2211. See exlimiv 1930 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 2218 | 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 2219 | Existential elimination rule of natural deduction. (Contributed by ML, 17-Jul-2020.) Shorten exlimdd 2220. (Revised by Wolf Lammen, 3-Sep-2023.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
| Theorem | exlimdd 2220 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑥𝜒 & ⊢ (𝜑 → ∃𝑥𝜓) & ⊢ ((𝜑 ∧ 𝜓) → 𝜒) ⇒ ⊢ (𝜑 → 𝜒) | ||
| Theorem | nexd 2221 | Deduction for generalization rule for negated wff. (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → ¬ ∃𝑥𝜓) | ||
| Theorem | albid 2222 | Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) | ||
| Theorem | exbid 2223 | Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (∃𝑥𝜓 ↔ ∃𝑥𝜒)) | ||
| Theorem | nfbidf 2224 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) df-nf 1784 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → (Ⅎ𝑥𝜓 ↔ Ⅎ𝑥𝜒)) | ||
| Theorem | 19.16 2225 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∀𝑥𝜓)) | ||
| Theorem | 19.17 2226 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
| ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (∀𝑥𝜑 ↔ 𝜓)) | ||
| Theorem | 19.27 2227 | Theorem 19.27 of [Margaris] p. 90. See 19.27v 1989 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
| ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (∀𝑥𝜑 ∧ 𝜓)) | ||
| Theorem | 19.28 2228 | Theorem 19.28 of [Margaris] p. 90. See 19.28v 1990 for a version requiring fewer axioms. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 7-May-2025.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∀𝑥𝜓)) | ||
| Theorem | 19.19 2229 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝜑 ↔ ∃𝑥𝜓)) | ||
| Theorem | 19.36 2230 | Theorem 19.36 of [Margaris] p. 90. See 19.36v 1987 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
| ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (∀𝑥𝜑 → 𝜓)) | ||
| Theorem | 19.36i 2231 | Inference associated with 19.36 2230. See 19.36iv 1946 for a version requiring fewer axioms. (Contributed by NM, 24-Jun-1993.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ ∃𝑥(𝜑 → 𝜓) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
| Theorem | 19.37 2232 | Theorem 19.37 of [Margaris] p. 90. See 19.37v 1991 for a version requiring fewer axioms. (Contributed by NM, 21-Jun-1993.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∃𝑥𝜓)) | ||
| Theorem | 19.32 2233 | Theorem 19.32 of [Margaris] p. 90. See 19.32v 1940 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∀𝑥𝜓)) | ||
| Theorem | 19.31 2234 | Theorem 19.31 of [Margaris] p. 90. See 19.31v 1941 for a version requiring fewer axioms. (Contributed by NM, 14-May-1993.) |
| ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∀𝑥(𝜑 ∨ 𝜓) ↔ (∀𝑥𝜑 ∨ 𝜓)) | ||
| Theorem | 19.41 2235 | Theorem 19.41 of [Margaris] p. 90. See 19.41v 1949 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 2236 | Theorem 19.42 of [Margaris] p. 90. See 19.42v 1953 for a version requiring fewer axioms. See exan 1862 for an immediate version. (Contributed by NM, 18-Aug-1993.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∧ 𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓)) | ||
| Theorem | 19.44 2237 | Theorem 19.44 of [Margaris] p. 90. See 19.44v 1992 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
| ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (∃𝑥𝜑 ∨ 𝜓)) | ||
| Theorem | 19.45 2238 | Theorem 19.45 of [Margaris] p. 90. See 19.45v 1993 for a version requiring fewer axioms. (Contributed by NM, 12-Mar-1993.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (∃𝑥(𝜑 ∨ 𝜓) ↔ (𝜑 ∨ ∃𝑥𝜓)) | ||
| Theorem | spimfv 2239* | Specialization, using implicit substitution. Version of spim 2392 with a disjoint variable condition, which does not require ax-13 2377. See spimvw 1995 for a version with two disjoint variable conditions, requiring fewer axioms, and spimv 2395 for another variant. (Contributed by NM, 10-Jan-1993.) (Revised by BJ, 31-May-2019.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → 𝜓) | ||
| Theorem | chvarfv 2240* | Implicit substitution of 𝑦 for 𝑥 into a theorem. Version of chvar 2400 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by Raph Levien, 9-Jul-2003.) (Revised by BJ, 31-May-2019.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ 𝜑 ⇒ ⊢ 𝜓 | ||
| Theorem | cbv3v2 2241* | Version of cbv3 2402 with two disjoint variable conditions, which does not require ax-11 2157 nor ax-13 2377. (Contributed by BJ, 24-Jun-2019.) (Proof shortened by Wolf Lammen, 30-Aug-2021.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) ⇒ ⊢ (∀𝑥𝜑 → ∀𝑦𝜓) | ||
| Theorem | sbalex 2242* |
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 2065.
That both sides of the biconditional express proper substitution is proved by sb5 2276 and sb6 2085. The implication "to the left" is equs4v 1999 and does not require ax-10 2141 nor ax-12 2177. It also holds without disjoint variable condition if we allow more axioms (see equs4 2421). Theorem 6.2 of [Quine] p. 40. Theorem equs5 2465 replaces the disjoint variable condition with a distinctor antecedent. Theorem equs45f 2464 replaces the disjoint variable condition on 𝑥, 𝑡 with the nonfreeness hypothesis of 𝑡 in 𝜑. (Contributed by NM, 14-Apr-2008.) Revised to use equsexv 2268 in place of equsex 2423 in order to remove dependency on ax-13 2377. (Revised by BJ, 20-Dec-2020.) Revise to remove dependency on df-sb 2065. (Revised by BJ, 21-Sep-2024.) (Proof shortened by SN, 14-Aug-2025.) |
| ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
| Theorem | sbalexOLD 2243* | Obsolete version of sbalex 2242 as of 14-Aug-2025. (Contributed by NM, 14-Apr-2008.) (Revised by BJ, 20-Dec-2020.) (Revised by BJ, 21-Sep-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (∃𝑥(𝑥 = 𝑡 ∧ 𝜑) ↔ ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
| Theorem | sb4av 2244* | Version of sb4a 2485 with a disjoint variable condition, which does not require ax-13 2377. The distinctor antecedent from sb4b 2480 is replaced by a disjoint variable condition in this theorem. (Contributed by NM, 2-Feb-2007.) (Revised by BJ, 15-Dec-2023.) |
| ⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
| Theorem | sbimd 2245 | Deduction substituting both sides of an implication. (Contributed by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2065. (Revised by Steven Nguyen, 9-Jul-2023.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
| Theorem | sbbid 2246 | Deduction substituting both sides of a biconditional. (Contributed by NM, 30-Jun-1993.) Remove dependency on ax-10 2141 and ax-13 2377. (Revised by Wolf Lammen, 24-Nov-2022.) Revise df-sb 2065. (Revised by Steven Nguyen, 11-Jul-2023.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) | ||
| Theorem | 2sbbid 2247 | Deduction doubly substituting both sides of a biconditional. (Contributed by AV, 30-Jul-2023.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 ↔ 𝜒)) & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜑 → ([𝑡 / 𝑥][𝑢 / 𝑦]𝜓 ↔ [𝑡 / 𝑥][𝑢 / 𝑦]𝜒)) | ||
| Theorem | sbequ1 2248 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2065. (Revised by BJ, 22-Dec-2020.) |
| ⊢ (𝑥 = 𝑡 → (𝜑 → [𝑡 / 𝑥]𝜑)) | ||
| Theorem | sbequ2 2249 | An equality theorem for substitution. (Contributed by NM, 16-May-1993.) Revise df-sb 2065. (Revised by BJ, 22-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Feb-2024.) |
| ⊢ (𝑥 = 𝑡 → ([𝑡 / 𝑥]𝜑 → 𝜑)) | ||
| Theorem | stdpc7 2250 | One of the two equality axioms of standard predicate calculus, called substitutivity of equality. (The other one is stdpc6 2027.) 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 2251 | An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
| ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) | ||
| Theorem | sbequ12r 2252 | An equality theorem for substitution. (Contributed by NM, 6-Oct-2004.) (Proof shortened by Andrew Salmon, 21-Jun-2011.) |
| ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑦]𝜑 ↔ 𝜑)) | ||
| Theorem | sbelx 2253* | Elimination of substitution. Also see sbel2x 2479. (Contributed by NM, 5-Aug-1993.) Avoid ax-13 2377. (Revised by Wolf Lammen, 6-Aug-2023.) Avoid ax-10 2141. (Revised by GG, 20-Aug-2023.) |
| ⊢ (𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑦]𝜑)) | ||
| Theorem | sbequ12a 2254 | An equality theorem for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Jun-2019.) |
| ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ [𝑥 / 𝑦]𝜑)) | ||
| Theorem | sbid 2255 | 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 2256* | A composition law for substitution. Version of sbco 2512 with a disjoint variable condition using fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by GG, 7-Aug-2023.) (Proof shortened by SN, 26-Aug-2025.) |
| ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
| Theorem | sbcovOLD 2257* | Obsolete version of sbcov 2256 as of 26-Aug-2025. (Contributed by NM, 14-May-1993.) (Revised by GG, 7-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
| Theorem | sb6a 2258* | Equivalence for substitution. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 23-Sep-2018.) |
| ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → [𝑥 / 𝑦]𝜑)) | ||
| Theorem | sbid2vw 2259* | Reverting substitution yields the original expression. Based on fewer axioms than sbid2v 2514, at the expense of an extra distinct variable condition. (Contributed by NM, 14-May-1993.) (Revised by Wolf Lammen, 5-Aug-2023.) |
| ⊢ ([𝑡 / 𝑥][𝑥 / 𝑡]𝜑 ↔ 𝜑) | ||
| Theorem | axc16g 2260* | Generalization of axc16 2261. Use the latter when sufficient. This proof only requires, on top of { ax-1 6-- ax-7 2007 }, Theorem ax12v 2178. (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 2377, along an idea of BJ. (Revised by Wolf Lammen, 30-Nov-2019.) (Revised by BJ, 7-Jul-2021.) Shorten axc11rv 2265. (Revised by Wolf Lammen, 11-Oct-2021.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
| Theorem | axc16 2261* | Proof of older axiom ax-c16 38893. (Contributed by NM, 8-Nov-2006.) (Revised by NM, 22-Sep-2017.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
| Theorem | axc16gb 2262* | Biconditional strengthening of axc16g 2260. (Contributed by NM, 15-May-1993.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 ↔ ∀𝑧𝜑)) | ||
| Theorem | axc16nf 2263* | If dtru 5441 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 2157. (Revised by Wolf Lammen, 9-Sep-2018.) (Proof shortened by BJ, 14-Jun-2019.) Remove dependency on ax-10 2141. (Revised by Wolf Lammen, 12-Oct-2021.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → Ⅎ𝑧𝜑) | ||
| Theorem | axc11v 2264* | Version of axc11 2435 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2007 }, from ax12v 2178 (contrary to axc11 2435 which seems to require the full ax-12 2177 and ax-13 2377). (Contributed by NM, 16-May-2008.) (Revised by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑥𝜑 → ∀𝑦𝜑)) | ||
| Theorem | axc11rv 2265* | Version of axc11r 2371 with a disjoint variable condition on 𝑥 and 𝑦, which is provable, on top of { ax-1 6-- ax-7 2007 }, from ax12v 2178 (contrary to axc11 2435 which seems to require the full ax-12 2177 and ax-13 2377, and to axc11r 2371 which seems to require the full ax-12 2177). (Contributed by BJ, 6-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.) |
| ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦𝜑 → ∀𝑥𝜑)) | ||
| Theorem | drsb2 2266 | 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 2267* | An equivalence related to implicit substitution. Version of equsal 2422 with a disjoint variable condition, which does not require ax-13 2377. See equsalvw 2003 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsexv 2268. (Contributed by NM, 2-Jun-1993.) (Revised by BJ, 31-May-2019.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
| Theorem | equsexv 2268* | An equivalence related to implicit substitution. Version of equsex 2423 with a disjoint variable condition, which does not require ax-13 2377. See equsexvw 2004 for a version with two disjoint variable conditions requiring fewer axioms. See also the dual form equsalv 2267. (Contributed by NM, 5-Aug-1993.) (Revised by BJ, 31-May-2019.) Avoid ax-10 2141. (Revised by GG, 18-Nov-2024.) |
| ⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) ↔ 𝜓) | ||
| Theorem | equsexvOLD 2269* | Obsolete version of equsexv 2268 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 2270 | 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 2271 | Substitution for a variable not free in a wff does not affect it. For a version requiring disjoint variables but fewer axioms, see sbv 2088. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
| Theorem | sbf2 2272 | Substitution has no effect on a bound variable. (Contributed by NM, 1-Jul-2005.) |
| ⊢ ([𝑦 / 𝑥]∀𝑥𝜑 ↔ ∀𝑥𝜑) | ||
| Theorem | sbh 2273 | Substitution for a variable not free in a wff does not affect it. (Contributed by NM, 14-May-1993.) |
| ⊢ (𝜑 → ∀𝑥𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑) | ||
| Theorem | hbs1 2274* | The setvar 𝑥 is not free in [𝑦 / 𝑥]𝜑 when 𝑥 and 𝑦 are distinct. (Contributed by NM, 26-May-1993.) |
| ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
| Theorem | nfs1f 2275 | If 𝑥 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
| ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
| Theorem | sb5 2276* | Alternate definition of substitution when variables are disjoint. Similar to Theorem 6.1 of [Quine] p. 40. The implication "to the right" is sb1v 2087 and even needs no disjoint variable condition, see sb1 2483. Theorem sb5f 2503 replaces the disjoint variable condition with a nonfreeness hypothesis. (Contributed by NM, 18-Aug-1993.) (Revised by Wolf Lammen, 4-Sep-2023.) |
| ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
| Theorem | equs5av 2277* | A property related to substitution that replaces the distinctor from equs5 2465 to a disjoint variable condition. Version of equs5a 2462 with a disjoint variable condition, which does not require ax-13 2377. See also sbalex 2242. (Contributed by NM, 2-Feb-2007.) (Revised by GG, 15-Dec-2023.) |
| ⊢ (∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
| Theorem | 2sb5 2278* | Equivalence for double substitution. (Contributed by NM, 3-Feb-2005.) |
| ⊢ ([𝑧 / 𝑥][𝑤 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) ∧ 𝜑)) | ||
| Theorem | dfsb7 2279* | An alternate definition of proper substitution df-sb 2065. 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 2276, first 𝑦 for 𝑥 then 𝑡 for 𝑦. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2715. Theorem sb7h 2531 provides a version where 𝜑 and 𝑦 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) Revise df-sb 2065. (Revised by BJ, 25-Dec-2020.) (Proof shortened by Wolf Lammen, 3-Sep-2023.) |
| ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
| Theorem | sbn 2280 | 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 2065. (Revised by BJ, 25-Dec-2020.) |
| ⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑) | ||
| Theorem | sbex 2281* | Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003.) |
| ⊢ ([𝑧 / 𝑦]∃𝑥𝜑 ↔ ∃𝑥[𝑧 / 𝑦]𝜑) | ||
| Theorem | nf5 2282 | Alternate definition of df-nf 1784. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1784 changed. (Revised by Wolf Lammen, 11-Sep-2021.) |
| ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | ||
| Theorem | nf6 2283 | An alternate definition of df-nf 1784. (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 2207 and 19.21v 1939. (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 2211. (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 2211. See exlimiv 1930 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 2425 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 29-Nov-2015.) (Proof shortened by Wolf Lammen, 8-Jul-2022.) |
| ⊢ (𝜓 → ∀𝑥𝜓) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) ↔ 𝜓) | ||
| Theorem | equsexhv 2292* | An equivalence related to implicit substitution. Version of equsexh 2426 with a disjoint variable condition, which does not require ax-13 2377. (Contributed by NM, 5-Aug-1993.) (Revised 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 > |