Home | Metamath
Proof Explorer Theorem List (p. 26 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sb3b 2501 | Simplified definition of substitution when variables are distinct. This is the biconditional strengthening of sb3 2502. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by BJ, 6-Oct-2018.) Shorten sb3 2502. (Revised by Wolf Lammen, 21-Feb-2021.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb3 2502 | One direction of a simplified definition of substitution when variables are distinct. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb1 2503 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb5 2276) or a non-freeness hypothesis (sb5f 2538). Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker sb1v 2095 when possible. (Contributed by NM, 13-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 21-Feb-2024.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2 2504 | One direction of a simplified definition of substitution. The converse requires either a disjoint variable condition (sb6 2093) or a non-freeness hypothesis (sb6f 2537). Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 13-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 26-Jul-2023.) (New usage is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | sb3OLD 2505 | Obsolete version of sb3 2502 as of 21-Feb-2024. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb4OLD 2506 | Obsolete as of 30-Jul-2023. Use sb4b 2499 instead. One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 25-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb1OLD 2507 | Obsolete version of sb1 2503 as of 21-Feb-2024. (Contributed by NM, 13-May-1993.) Revise df-sb 2070. (Revised by Wolf Lammen, 29-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb3bOLD 2508 | Obsolete version of sb3b 2501 as of 21-Feb-2024. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb4a 2509 | A version of one implication of sb4b 2499 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker sb4av 2244 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2070. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | dfsb1 2510 | Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2070. Note that it does not require dummy variables in its definiens; this is done by having 𝑥 free in the first conjunct and bound in the second. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2070. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | spsbeOLDOLD 2511 | Obsolete version of spsbe 2088 as of 7-Jul-2023. A specialization theorem. (Contributed by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥𝜑) | ||
Theorem | sb2vOLDOLD 2512* | Obsolete version of sb2 2504 as of 8-Jul-2023. Version of sb2 2504 with a disjoint variable condition, which does not require ax-13 2390. (Contributed by BJ, 31-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | sb4vOLDOLD 2513* | Obsolete version of sb4vOLD 2096 as of 8-Jul-2023. Version of sb4OLD 2506 with a disjoint variable condition instead of a distinctor antecedent, which does not require ax-13 2390. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbequ2OLDOLD 2514 | Obsolete version of sbequ2 2250 as of 8-Jul-2023. An equality theorem for substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | ||
Theorem | sbimiOLD 2515 | Obsolete version of sbimi 2079 as of 6-Jul-2023. Infer substitution into antecedent and consequent of an implication. (Contributed by NM, 25-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓) | ||
Theorem | sbimdvOLD 2516* | Obsolete version of sbimdv 2083 as of 6-Jul-2023. Deduction substituting both sides of an implication, with 𝜑 and 𝑥 disjoint. See also sbimd 2245. (Contributed by Wolf Lammen, 6-May-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | equsb1vOLDOLD 2517* | Obsolete version of equsb1v 2112 as of 19-Jun-2023. (Contributed by BJ, 11-Sep-2019.) Remove dependencies on axioms. (Revised by Wolf Lammen, 30-May-2023.) (Proof shortened by Steven Nguyen, 31-May-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | sbimdOLD 2518 | Obsolete version of sbimd as of 9-Jul-2023. (Contributed by Wolf Lammen, 24-Nov-2022.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | sbtvOLD 2519* | Obsolete version of sbt 2071 as of 6-Jul-2023. A substitution into a theorem yields a theorem. See sbt 2071 when 𝑥, 𝑦 need not be disjoint. (Contributed by BJ, 31-May-2019.) Reduce axioms. (Revised by Steven Nguyen, 25-Apr-2023.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝜑 ⇒ ⊢ [𝑥 / 𝑦]𝜑 | ||
Theorem | sbequ1OLD 2520 | Obsolete version of sbequ1 2249 as of 8-Jul-2023. An equality theorem for substitution. (Contributed by NM, 16-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | hbsb2 2521 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb2 2522 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | hbsb2a 2523 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | sb4e 2524 | One direction of a simplified definition of substitution that unlike sb4b 2499 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | hbsb2e 2525 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑) | ||
Theorem | hbsb3 2526 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out bj-hbsb3v 34139 for a weaker version requiring less axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1 2527 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out nfs1v 2160 for a version requiring less axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | axc16ALT 2528* | Alternate proof of axc16 2262, shorter but requiring ax-10 2145, ax-11 2161, ax-13 2390 and using df-nf 1785 and df-sb 2070. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gALT 2529* | Alternate proof of axc16g 2261 that uses df-sb 2070 and requires ax-10 2145, ax-11 2161, ax-13 2390. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | equsb1 2530 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker equsb1v 2112 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | equsb2 2531 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out equsb1v 2112 for a version requiring less axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑦 = 𝑥 | ||
Theorem | dfsb2 2532 | An alternate definition of proper substitution that, like dfsb1 2510, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dfsb3 2533 | An alternate definition of proper substitution df-sb 2070 that uses only primitive connectives (no defined terms) on the right-hand side. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sbequiOLD 2534 | Obsolete proof of sbequi 2091 as of 7-Jul-2023. An equality theorem for substitution. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | ||
Theorem | drsb1 2535 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑)) | ||
Theorem | sb2ae 2536* | In the case of two successive substitutions for two always equal variables, the second substitution has no effect. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑)) | ||
Theorem | sb6f 2537 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2504 and does not require the non-freeness hypothesis. Theorem sb6 2093 replaces the non-freeness hypothesis with a disjoint variable condition and uses less axioms. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5f 2538 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2503 and does not require the non-freeness hypothesis. Theorem sb5 2276 replaces the non-freeness hypothesis with a disjoint variable condition and uses less axioms. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | nfsb4t 2539 | A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2540). Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (New usage is discouraged.) |
⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb4 2540 | A variable not free in a proposition remains so after substitution in that proposition with a distinct variable. Usage of this theorem is discouraged because it depends on ax-13 2390. Theorem nfsb 2565 replaces the distinctor with a disjoint variable condition. Visit also nfsbv 2349 for a weaker version of nfsb 2565 not requiring ax-13 2390. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sbnOLD 2541 | Obsolete version of sbn 2287 as of 8-Jul-2023. Negation inside and outside of substitution are equivalent. For a version requiring disjoint variables, but fewer axioms, see sbnvOLD 2322. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbi1OLD 2542 | Obsolete version of sbi1 2076 as of 24-Jul-2023. Removal of implication from substitution. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) → ([𝑦 / 𝑥]𝜑 → [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbequ8 2543 | Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2070. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbie 2544 | Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2330 and sbievw 2103. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) | ||
Theorem | sbied 2545 | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2544) Usage of this theorem is discouraged because it depends on ax-13 2390. See sbiedw 2332, sbiedvw 2104 for variants using disjoint variables, but requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑥𝜒) & ⊢ (𝜑 → (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | sbiedv 2546* | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2544). Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker sbiedvw 2104 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | 2sbiev 2547* | Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See 2sbievw 2105 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbcom3 2548 | Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2390. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2106. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2161. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | sbco 2549 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. See sbcov 2258 for a version with a disjoint variable condition requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbid2 2550 | An identity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out sbid2vw 2260 for a weaker version requiring fewer axioms. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbid2v 2551* | An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). Usage of this theorem is discouraged because it depends on ax-13 2390. See sbid2vw 2260 for a version with an extra disjoint variable condition requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbidm 2552 | An idempotent law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 30-Jun-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 13-Jul-2019.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2 2553 | A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2352 and sbco2vv 2108. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 17-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbco2d 2554 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbco3 2555 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) | ||
Theorem | sbcom 2556 | A commutativity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out sbcom3vv 2106 for a version requiring less axioms. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 20-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑧][𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥][𝑦 / 𝑧]𝜑) | ||
Theorem | sbtrt 2557 | Partially closed form of sbtr 2558. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by BJ, 4-Jun-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑦[𝑦 / 𝑥]𝜑 → 𝜑) | ||
Theorem | sbtr 2558 | A partial converse to sbt 2071. If the substitution of a variable for a non-free one in a wff gives a theorem, then the original wff is a theorem. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by BJ, 15-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ [𝑦 / 𝑥]𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | sb8 2559 | Substitution of variable in universal quantifier. Usage of this theorem is discouraged because it depends on ax-13 2390. For a version requiring disjoint variables, but fewer axioms, see sb8v 2373. (Contributed by NM, 16-May-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑥𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb8e 2560 | Substitution of variable in existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2390. For a version requiring disjoint variables, but fewer axioms, see sb8ev 2374. (Contributed by NM, 12-Aug-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Jim Kingdon, 15-Jan-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∃𝑥𝜑 ↔ ∃𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb9 2561 | Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2562. (Revised by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb9i 2562 | Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sbhb 2563* | Two ways of expressing "𝑥 is (effectively) not free in 𝜑". Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 29-May-2009.) (New usage is discouraged.) |
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsbd 2564* | Deduction version of nfsb 2565. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 15-Feb-2013.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓) | ||
Theorem | nfsb 2565* | If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Usage of this theorem is discouraged because it depends on ax-13 2390. For a version requiring more disjoint variables, but fewer axioms, see nfsbv 2349. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | nfsbOLD 2566* | Obsolete version of nfsb 2565 as of 25-Feb-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | hbsb 2567* | If 𝑧 is not free in 𝜑, it is not free in [𝑦 / 𝑥]𝜑 when 𝑦 and 𝑧 are distinct. Usage of this theorem is discouraged because it depends on ax-13 2390. Use the weaker hbsbw 2351 when possible. (Contributed by NM, 12-Aug-1993.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sb7f 2568* | This version of dfsb7 2285 does not require that 𝜑 and 𝑧 be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1911 i.e. that doesn't have the concept of a variable not occurring in a wff. (dfsb1 2510 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb7h 2569* | This version of dfsb7 2285 does not require that 𝜑 and 𝑧 be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-5 1911 i.e. that doesn't have the concept of a variable not occurring in a wff. (dfsb1 2510 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | dfsb7OLDOLD 2570* |
Obsolete version of dfsb7 2285 as of 8-Jul-2023.
An alternate definition of proper substitution df-sb 2070. 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 2802. Theorem sb7h 2569 provides a version where 𝜑 and 𝑧 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb10f 2571* | Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. Usage of this theorem is discouraged because it depends on ax-13 2390. (Contributed by NM, 9-May-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑)) | ||
Theorem | sbal1 2572* | Obsolete version of sbal 2166 as of 13-Jul-2023. A theorem used in elimination of disjoint variable restriction on 𝑥 and 𝑦 by replacing it with a distinctor ¬ ∀𝑥𝑥 = 𝑧. (Contributed by NM, 15-May-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑧 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | sbal2 2573* | Move quantifier in and out of substitution. Usage of this theorem is discouraged because it depends on ax-13 2390. Check out sbal 2166 for a version replacing the distinctor with a disjoint variable condition, requiring fewer axioms. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022.) (Proof shortened by Wolf Lammen, 23-Sep-2023.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | sbal2OLD 2574* | Obsolete version of sbal2 2573 as of 23-Sep-2023. (Contributed by NM, 2-Jan-2002.) Remove a distinct variable constraint. (Revised by Wolf Lammen, 24-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑)) | ||
Theorem | sbalOLD 2575* | Obsolete version of sbal 2166 as of 13-Aug-2023. Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 29-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ([𝑧 / 𝑦]∀𝑥𝜑 ↔ ∀𝑥[𝑧 / 𝑦]𝜑) | ||
Theorem | 2sb8e 2576* | An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 2390. For a version requiring more disjoint variables, but fewer axioms, see 2sb8ev 2375. (Contributed by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
The definition of substitution (df-sb 2070) used to be dfsb1 2510. These two definitions are proved equivalent by proving dfsb7 2285 from both, which takes several intermediate theorems and uses many axioms. | ||
Theorem | sbimiALT 2577 | Alternate version of sbimi 2079. (Contributed by NM, 25-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜃 → 𝜏) | ||
Theorem | sbbiiALT 2578 | Alternate version of sbbii 2081. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜃 ↔ 𝜏) | ||
Theorem | sbequ1ALT 2579 | Alternate version of sbequ1 2249. (Contributed by NM, 16-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜃)) | ||
Theorem | sbequ2ALT 2580 | Alternate version of sbequ2 2250. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜃 → 𝜑)) | ||
Theorem | sbequ12ALT 2581 | Alternate version of sbequ12 2253. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) | ||
Theorem | sb1ALT 2582 | Alternate version of sb1 2503. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2vOLDALT 2583* | Alternate version of sb2vOLD 2097. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜃) | ||
Theorem | sb4vOLDALT 2584* | Alternate version of sb4vOLD 2096. (Contributed by BJ, 23-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb6ALT 2585* | Alternate version of sb6 2093. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5ALT2 2586* | Alternate version of sb5 2276. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2ALT 2587 | Alternate version of sb2 2504. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜃) | ||
Theorem | sb4ALT 2588 | Alternate version of one implication of sb4b 2499. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | spsbeALT 2589 | Alternate version of spsbe 2088. (Contributed by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 → ∃𝑥𝜑) | ||
Theorem | stdpc4ALT 2590 | Alternate version of stdpc4 2073. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥𝜑 → 𝜃) | ||
Theorem | dfsb2ALT 2591 | Alternate version of dfsb2 2532. (Contributed by NM, 17-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dfsb3ALT 2592 | Alternate version of dfsb3 2533. (Contributed by NM, 6-Mar-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sbftALT 2593 | Alternate version of sbft 2270. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (Ⅎ𝑥𝜑 → (𝜃 ↔ 𝜑)) | ||
Theorem | sbfALT 2594 | Alternate version of sbf 2271. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | sbnALT 2595 | Alternate version of sbn 2287. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜑))) ⇒ ⊢ (𝜏 ↔ ¬ 𝜃) | ||
Theorem | sbequiALT 2596 | Alternate version of sbequi 2091. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑧 = 𝑥 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑥 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑧 = 𝑦 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜃 → 𝜏)) | ||
Theorem | sbequALT 2597 | Alternate version of sbequ 2090. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑧 = 𝑥 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑥 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑧 = 𝑦 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜏)) | ||
Theorem | sb4aALT 2598 | Alternate version of sb4a 2509. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → ∀𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑))) ⇒ ⊢ (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | hbsb2ALT 2599 | Alternate version of hbsb2 2521. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜃 → ∀𝑥𝜃)) | ||
Theorem | nfsb2ALT 2600 | Alternate version of nfsb2 2522. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |