|   | 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 2092). Version of sbied 2507 and sbiedv 2508 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 2090 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | |
| 2 | sbiedvw.1 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) | |
| 3 | 2 | expcom 413 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 → (𝜓 ↔ 𝜒))) | 
| 4 | 3 | pm5.74d 273 | . . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) | 
| 5 | 4 | sbievw 2092 | . . 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 2063 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 | 
| This theorem is referenced by: 2sbievw 2095 iscatd2 17725 bj-elabd2ALT 36927 | 
| Copyright terms: Public domain | W3C validator |