![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbiedvw | Structured version Visualization version GIF version |
Description: Conversion of implicit substitution to explicit substitution (deduction version of sbievw 2091). Version of sbied 2506 and sbiedv 2507 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by GG, 29-Jan-2024.) |
Ref | Expression |
---|---|
sbiedvw.1 | ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbiedvw | ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbrimvw 2089 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | |
2 | sbiedvw.1 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) | |
3 | 2 | expcom 413 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 → (𝜓 ↔ 𝜒))) |
4 | 3 | pm5.74d 273 | . . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) |
5 | 4 | sbievw 2091 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
6 | 1, 5 | bitr3i 277 | . 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → 𝜒)) |
7 | 6 | pm5.74ri 272 | 1 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 [wsb 2062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-sb 2063 |
This theorem is referenced by: 2sbievw 2094 iscatd2 17726 bj-elabd2ALT 36908 |
Copyright terms: Public domain | W3C validator |