![]() |
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 2095). Version of sbied 2502 and sbiedv 2503 with more disjoint variable conditions, requiring fewer axioms. (Contributed by NM, 30-Jun-1994.) (Revised by Gino Giotto, 29-Jan-2024.) |
Ref | Expression |
---|---|
sbiedvw.1 | ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
sbiedvw | ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbrimvw 2094 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) | |
2 | sbiedvw.1 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → (𝜓 ↔ 𝜒)) | |
3 | 2 | expcom 414 | . . . . 5 ⊢ (𝑥 = 𝑦 → (𝜑 → (𝜓 ↔ 𝜒))) |
4 | 3 | pm5.74d 272 | . . . 4 ⊢ (𝑥 = 𝑦 → ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))) |
5 | 4 | sbievw 2095 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → 𝜒)) |
6 | 1, 5 | bitr3i 276 | . 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → 𝜒)) |
7 | 6 | pm5.74ri 271 | 1 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 [wsb 2067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 |
This theorem is referenced by: 2sbievw 2097 iscatd2 17621 bj-elabd2ALT 35793 |
Copyright terms: Public domain | W3C validator |