![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbrimvw | Structured version Visualization version GIF version |
Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2303 based on fewer axioms, but with more disjoint variable conditions. Based on an idea of GG. (Contributed by Wolf Lammen, 29-Jan-2024.) |
Ref | Expression |
---|---|
sbrimvw | ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sb6 2083 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) | |
2 | bi2.04 387 | . . . 4 ⊢ ((𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝑥 = 𝑦 → (𝜑 → 𝜓))) | |
3 | 2 | albii 1816 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) |
4 | 19.21v 1937 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))) | |
5 | 1, 3, 4 | 3bitr2i 299 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))) |
6 | sb6 2083 | . . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓)) | |
7 | 6 | imbi2i 336 | . 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))) |
8 | 5, 7 | bitr4i 278 | 1 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∀wal 1535 [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: sbiedvw 2093 cbvralsvw 3315 |
Copyright terms: Public domain | W3C validator |