Home | Metamath
Proof Explorer Theorem List (p. 26 of 449) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44899) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sb3OLD 2501 | Obsolete version of sb3 2498 as of 21-Feb-2024. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑)) | ||
Theorem | sb4OLD 2502 | Obsolete as of 30-Jul-2023. Use sb4b 2495 instead. One direction of a simplified definition of substitution when variables are distinct. (Contributed by NM, 14-May-1993.) Revise df-sb 2066. (Revised by Wolf Lammen, 25-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sb1OLD 2503 | Obsolete version of sb1 2499 as of 21-Feb-2024. (Contributed by NM, 13-May-1993.) Revise df-sb 2066. (Revised by Wolf Lammen, 29-Jul-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb3bOLD 2504 | Obsolete version of sb3b 2497 as of 21-Feb-2024. (Contributed by BJ, 6-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | sb4a 2505 | A version of one implication of sb4b 2495 that does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker sb4av 2239 when possible. (Contributed by NM, 2-Feb-2007.) Revise df-sb 2066. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑡 / 𝑥]∀𝑡𝜑 → ∀𝑥(𝑥 = 𝑡 → 𝜑)) | ||
Theorem | dfsb1 2506 | Alternate definition of substitution. Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). This was the original definition before df-sb 2066. 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 2386. (Contributed by BJ, 9-Jul-2023.) Revise df-sb 2066. (Revised by Wolf Lammen, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) | ||
Theorem | spsbeOLDOLD 2507 | Obsolete version of spsbe 2084 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 2508* | Obsolete version of sb2 2500 as of 8-Jul-2023. Version of sb2 2500 with a disjoint variable condition, which does not require ax-13 2386. (Contributed by BJ, 31-May-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → [𝑦 / 𝑥]𝜑) | ||
Theorem | sb4vOLDOLD 2509* | Obsolete version of sb4vOLD 2092 as of 8-Jul-2023. Version of sb4OLD 2502 with a disjoint variable condition instead of a distinctor antecedent, which does not require ax-13 2386. (Contributed by BJ, 23-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbequ2OLDOLD 2510 | Obsolete version of sbequ2 2245 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 2511 | Obsolete version of sbimi 2075 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 2512* | Obsolete version of sbimdv 2079 as of 6-Jul-2023. Deduction substituting both sides of an implication, with 𝜑 and 𝑥 disjoint. See also sbimd 2240. (Contributed by Wolf Lammen, 6-May-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 → [𝑦 / 𝑥]𝜒)) | ||
Theorem | equsb1vOLDOLD 2513* | Obsolete version of equsb1v 2108 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 2514 | 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 2515* | Obsolete version of sbt 2067 as of 6-Jul-2023. A substitution into a theorem yields a theorem. See sbt 2067 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 2516 | Obsolete version of sbequ1 2244 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 2517 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsb2 2518 | Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | hbsb2a 2519 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]∀𝑦𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | sb4e 2520 | One direction of a simplified definition of substitution that unlike sb4b 2495 does not require a distinctor antecedent. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥(𝑥 = 𝑦 → ∃𝑦𝜑)) | ||
Theorem | hbsb2e 2521 | Special case of a bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 2-Feb-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]∃𝑦𝜑) | ||
Theorem | hbsb3 2522 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2386. Check out bj-hbsb3v 34132 for a weaker version requiring less axioms. (Contributed by NM, 14-May-1993.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑦𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑) | ||
Theorem | nfs1 2523 | If 𝑦 is not free in 𝜑, 𝑥 is not free in [𝑦 / 𝑥]𝜑. Usage of this theorem is discouraged because it depends on ax-13 2386. Check out nfs1v 2269 for a version requiring less axioms. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑 | ||
Theorem | axc16ALT 2524* | Alternate proof of axc16 2257, shorter but requiring ax-10 2141, ax-11 2156, ax-13 2386 and using df-nf 1781 and df-sb 2066. (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑥𝜑)) | ||
Theorem | axc16gALT 2525* | Alternate proof of axc16g 2256 that uses df-sb 2066 and requires ax-10 2141, ax-11 2156, ax-13 2386. (Contributed by NM, 15-May-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → (𝜑 → ∀𝑧𝜑)) | ||
Theorem | equsb1 2526 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker equsb1v 2108 if possible. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑥 = 𝑦 | ||
Theorem | equsb2 2527 | Substitution applied to an atomic wff. Usage of this theorem is discouraged because it depends on ax-13 2386. Check out equsb1v 2108 for a version requiring less axioms. (Contributed by NM, 10-May-1993.) (New usage is discouraged.) |
⊢ [𝑦 / 𝑥]𝑦 = 𝑥 | ||
Theorem | dfsb2 2528 | An alternate definition of proper substitution that, like dfsb1 2506, mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 17-Feb-2005.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dfsb3 2529 | An alternate definition of proper substitution df-sb 2066 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 2386. (Contributed by NM, 6-Mar-2007.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sbequiOLD 2530 | Obsolete proof of sbequi 2087 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 2531 | 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 2386. (Contributed by NM, 2-Jun-1993.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜑)) | ||
Theorem | sb2ae 2532* | 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 2386. (Contributed by BJ and WL, 9-Aug-2023.) (New usage is discouraged.) |
⊢ (∀𝑥 𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ [𝑣 / 𝑦]𝜑)) | ||
Theorem | sb6f 2533 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the left" is sb2 2500 and does not require the non-freeness hypothesis. Theorem sb6 2089 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 2386. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5f 2534 | Equivalence for substitution when 𝑦 is not free in 𝜑. The implication "to the right" is sb1 2499 and does not require the non-freeness hypothesis. Theorem sb5 2272 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 2386. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | nfsb4t 2535 | A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 2536). Usage of this theorem is discouraged because it depends on ax-13 2386. (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 2536 | 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 2386. Theorem nfsb 2561 replaces the distinctor with a disjoint variable condition. Visit also nfsbv 2345 for a weaker version of nfsb 2561 not requiring ax-13 2386. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sbnOLD 2537 | Obsolete version of sbn 2283 as of 8-Jul-2023. Negation inside and outside of substitution are equivalent. For a version requiring disjoint variables, but fewer axioms, see sbnvOLD 2318. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑) | ||
Theorem | sbi1OLD 2538 | Obsolete version of sbi1 2072 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 2539 | Elimination of equality from antecedent after substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 28-Jul-2018.) Revise df-sb 2066. (Revised by Wolf Lammen, 28-Jul-2023.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥](𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sbie 2540 | Conversion of implicit substitution to explicit substitution. For versions requiring disjoint variables, but fewer axioms, see sbiev 2326 and sbievw 2099. Usage of this theorem is discouraged because it depends on ax-13 2386. (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 2541 | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2540) Usage of this theorem is discouraged because it depends on ax-13 2386. See sbiedw 2328, sbiedvw 2100 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 2542* | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2540). Usage of this theorem is discouraged because it depends on ax-13 2386. Use the weaker sbiedvw 2100 when possible. (Contributed by NM, 7-Jan-2017.) (New usage is discouraged.) |
⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) | ||
Theorem | 2sbiev 2543* | Conversion of double implicit substitution to explicit substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. See 2sbievw 2101 for a version with extra disjoint variables, but based on fewer axioms. (Contributed by AV, 29-Jul-2023.) (New usage is discouraged.) |
⊢ ((𝑥 = 𝑡 ∧ 𝑦 = 𝑢) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ([𝑡 / 𝑥][𝑢 / 𝑦]𝜑 ↔ 𝜓) | ||
Theorem | sbcom3 2544 | Substituting 𝑦 for 𝑥 and then 𝑧 for 𝑦 is equivalent to substituting 𝑧 for both 𝑥 and 𝑦. Usage of this theorem is discouraged because it depends on ax-13 2386. For a version requiring a disjoint variable, but fewer axioms, see sbcom3vv 2102. (Contributed by Giovanni Mascellani, 8-Apr-2018.) Remove dependency on ax-11 2156. (Revised by Wolf Lammen, 16-Sep-2018.) (Proof shortened by Wolf Lammen, 16-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝑧 / 𝑥]𝜑) | ||
Theorem | sbco 2545 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. See sbcov 2253 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 2546 | An identity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Check out sbid2vw 2255 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 2547* | 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 2386. See sbid2vw 2255 for a version with an extra disjoint variable condition requiring fewer axioms. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥][𝑥 / 𝑦]𝜑 ↔ 𝜑) | ||
Theorem | sbidm 2548 | An idempotent law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (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 2549 | A composition law for substitution. For versions requiring fewer axioms, but more disjoint variable conditions, see sbco2v 2348 and sbco2vv 2104. Usage of this theorem is discouraged because it depends on ax-13 2386. (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 2550 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ Ⅎ𝑧𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → ([𝑦 / 𝑧][𝑧 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜓)) | ||
Theorem | sbco3 2551 | A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 2-Jun-1993.) (Proof shortened by Wolf Lammen, 18-Sep-2018.) (New usage is discouraged.) |
⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥][𝑥 / 𝑦]𝜑) | ||
Theorem | sbcom 2552 | A commutativity law for substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Check out sbcom3vv 2102 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 2553 | Partially closed form of sbtr 2554. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by BJ, 4-Jun-2019.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (∀𝑦[𝑦 / 𝑥]𝜑 → 𝜑) | ||
Theorem | sbtr 2554 | A partial converse to sbt 2067. 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 2386. (Contributed by BJ, 15-Sep-2018.) (New usage is discouraged.) |
⊢ Ⅎ𝑦𝜑 & ⊢ [𝑦 / 𝑥]𝜑 ⇒ ⊢ 𝜑 | ||
Theorem | sb8 2555 | Substitution of variable in universal quantifier. Usage of this theorem is discouraged because it depends on ax-13 2386. For a version requiring disjoint variables, but fewer axioms, see sb8v 2369. (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 2556 | Substitution of variable in existential quantifier. Usage of this theorem is discouraged because it depends on ax-13 2386. For a version requiring disjoint variables, but fewer axioms, see sb8ev 2370. (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 2557 | Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 5-Aug-1993.) Allow a shortening of sb9i 2558. (Revised by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 ↔ ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sb9i 2558 | Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Jun-2019.) (New usage is discouraged.) |
⊢ (∀𝑥[𝑥 / 𝑦]𝜑 → ∀𝑦[𝑦 / 𝑥]𝜑) | ||
Theorem | sbhb 2559* | Two ways of expressing "𝑥 is (effectively) not free in 𝜑". Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 29-May-2009.) (New usage is discouraged.) |
⊢ ((𝜑 → ∀𝑥𝜑) ↔ ∀𝑦(𝜑 → [𝑦 / 𝑥]𝜑)) | ||
Theorem | nfsbd 2560* | Deduction version of nfsb 2561. Usage of this theorem is discouraged because it depends on ax-13 2386. (Contributed by NM, 15-Feb-2013.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → Ⅎ𝑧𝜓) ⇒ ⊢ (𝜑 → Ⅎ𝑧[𝑦 / 𝑥]𝜓) | ||
Theorem | nfsb 2561* | 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 2386. For a version requiring more disjoint variables, but fewer axioms, see nfsbv 2345. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 25-Feb-2024.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | nfsbOLD 2562* | Obsolete version of nfsb 2561 as of 25-Feb-2024. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ Ⅎ𝑧[𝑦 / 𝑥]𝜑 | ||
Theorem | hbsb 2563* | 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 2386. Use the weaker hbsbw 2347 when possible. (Contributed by NM, 12-Aug-1993.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑧[𝑦 / 𝑥]𝜑) | ||
Theorem | sb7f 2564* | This version of dfsb7 2281 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 1907 i.e. that doesn't have the concept of a variable not occurring in a wff. (dfsb1 2506 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 2386. (Contributed by NM, 26-Jul-2006.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑧𝜑 ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb7h 2565* | This version of dfsb7 2281 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 1907 i.e. that doesn't have the concept of a variable not occurring in a wff. (dfsb1 2506 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 2386. (Contributed by NM, 26-Jul-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) |
⊢ (𝜑 → ∀𝑧𝜑) ⇒ ⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | dfsb7OLDOLD 2566* |
Obsolete version of dfsb7 2281 as of 8-Jul-2023.
An alternate definition of proper substitution df-sb 2066. 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 2272, first 𝑧 for 𝑥 then 𝑦 for 𝑧. Compare Definition 2.1'' of [Quine] p. 17, which is obtained from this theorem by applying df-clab 2800. Theorem sb7h 2565 provides a version where 𝜑 and 𝑧 don't have to be distinct. (Contributed by NM, 28-Jan-2004.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑧(𝑧 = 𝑦 ∧ ∃𝑥(𝑥 = 𝑧 ∧ 𝜑))) | ||
Theorem | sb10f 2567* | 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 2386. (Contributed by NM, 9-May-2005.) (Revised by Mario Carneiro, 6-Oct-2016.) (New usage is discouraged.) |
⊢ Ⅎ𝑥𝜑 ⇒ ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ [𝑥 / 𝑧]𝜑)) | ||
Theorem | sbal1 2568* | Obsolete version of sbal 2161 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 2569* | Move quantifier in and out of substitution. Usage of this theorem is discouraged because it depends on ax-13 2386. Check out sbal 2161 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 2570* | Obsolete version of sbal2 2569 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 2571* | Obsolete version of sbal 2161 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 2572* | An equivalent expression for double existence. Usage of this theorem is discouraged because it depends on ax-13 2386. For a version requiring more disjoint variables, but fewer axioms, see 2sb8ev 2371. (Contributed by Wolf Lammen, 2-Nov-2019.) (New usage is discouraged.) |
⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑧∃𝑤[𝑧 / 𝑥][𝑤 / 𝑦]𝜑) | ||
The definition of substitution (df-sb 2066) used to be dfsb1 2506. These two definitions are proved equivalent by proving dfsb7 2281 from both, which takes several intermediate theorems and uses many axioms. | ||
Theorem | sbimiALT 2573 | Alternate version of sbimi 2075. (Contributed by NM, 25-Jun-1998.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜑 → 𝜓) ⇒ ⊢ (𝜃 → 𝜏) | ||
Theorem | sbbiiALT 2574 | Alternate version of sbbii 2077. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → 𝜓) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜓))) & ⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜃 ↔ 𝜏) | ||
Theorem | sbequ1ALT 2575 | Alternate version of sbequ1 2244. (Contributed by NM, 16-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜃)) | ||
Theorem | sbequ2ALT 2576 | Alternate version of sbequ2 2245. (Contributed by NM, 16-May-1993.) (Proof shortened by Wolf Lammen, 25-Feb-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜃 → 𝜑)) | ||
Theorem | sbequ12ALT 2577 | Alternate version of sbequ12 2248. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃)) | ||
Theorem | sb1ALT 2578 | Alternate version of sb1 2499. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2vOLDALT 2579* | Alternate version of sb2vOLD 2093. (Contributed by BJ, 31-May-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜃) | ||
Theorem | sb4vOLDALT 2580* | Alternate version of sb4vOLD 2092. (Contributed by BJ, 23-Jul-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb6ALT 2581* | Alternate version of sb6 2089. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 21-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5ALT2 2582* | Alternate version of sb5 2272. (Contributed by NM, 18-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | sb2ALT 2583 | Alternate version of sb2 2500. (Contributed by NM, 13-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥(𝑥 = 𝑦 → 𝜑) → 𝜃) | ||
Theorem | sb4ALT 2584 | Alternate version of one implication of sb4b 2495. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | spsbeALT 2585 | Alternate version of spsbe 2084. (Contributed by NM, 29-Jun-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 → ∃𝑥𝜑) | ||
Theorem | stdpc4ALT 2586 | Alternate version of stdpc4 2069. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥𝜑 → 𝜃) | ||
Theorem | dfsb2ALT 2587 | Alternate version of dfsb2 2528. (Contributed by NM, 17-Feb-2005.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ((𝑥 = 𝑦 ∧ 𝜑) ∨ ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | dfsb3ALT 2588 | Alternate version of dfsb3 2529. (Contributed by NM, 6-Mar-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝜃 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) → ∀𝑥(𝑥 = 𝑦 → 𝜑))) | ||
Theorem | sbftALT 2589 | Alternate version of sbft 2265. (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 2590 | Alternate version of sbf 2266. (Contributed by NM, 14-May-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑥𝜑 ⇒ ⊢ (𝜃 ↔ 𝜑) | ||
Theorem | sbnALT 2591 | Alternate version of sbn 2283. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑥 = 𝑦 → ¬ 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ¬ 𝜑))) ⇒ ⊢ (𝜏 ↔ ¬ 𝜃) | ||
Theorem | sbequiALT 2592 | Alternate version of sbequi 2087. (Contributed by NM, 14-May-1993.) (Proof shortened by Wolf Lammen, 15-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑧 = 𝑥 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑥 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑧 = 𝑦 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜃 → 𝜏)) | ||
Theorem | sbequALT 2593 | Alternate version of sbequ 2086. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑧 = 𝑥 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑥 ∧ 𝜑))) & ⊢ (𝜏 ↔ ((𝑧 = 𝑦 → 𝜑) ∧ ∃𝑧(𝑧 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (𝑥 = 𝑦 → (𝜃 ↔ 𝜏)) | ||
Theorem | sb4aALT 2594 | Alternate version of sb4a 2505. (Contributed by NM, 2-Feb-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → ∀𝑦𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ ∀𝑦𝜑))) ⇒ ⊢ (𝜃 → ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | hbsb2ALT 2595 | Alternate version of hbsb2 2517. (Contributed by NM, 14-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜃 → ∀𝑥𝜃)) | ||
Theorem | nfsb2ALT 2596 | Alternate version of nfsb2 2518. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜃) | ||
Theorem | equsb1ALT 2597 | Alternate version of equsb1 2526. (Contributed by NM, 10-May-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝑥 = 𝑦) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝑥 = 𝑦))) ⇒ ⊢ 𝜃 | ||
Theorem | sb6fALT 2598 | Alternate version of sb6f 2533. (Contributed by NM, 2-Jun-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜃 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜑)) | ||
Theorem | sb5fALT 2599 | Alternate version of sb5f 2534. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) & ⊢ Ⅎ𝑦𝜑 ⇒ ⊢ (𝜃 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) | ||
Theorem | nfsb4tALT 2600 | Alternate version of nfsb4t 2535. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝜃 ↔ ((𝑥 = 𝑦 → 𝜑) ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))) ⇒ ⊢ (∀𝑥Ⅎ𝑧𝜑 → (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝜃)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |