|   | 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 2304 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 2085 | . . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) | |
| 2 | bi2.04 387 | . . . 4 ⊢ ((𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝑥 = 𝑦 → (𝜑 → 𝜓))) | |
| 3 | 2 | albii 1819 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓))) | 
| 4 | 19.21v 1939 | . . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))) | |
| 5 | 1, 3, 4 | 3bitr2i 299 | . 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓))) | 
| 6 | sb6 2085 | . . 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 1538 [wsb 2064 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 | 
| This theorem is referenced by: sbiedvw 2095 cbvralsvw 3317 | 
| Copyright terms: Public domain | W3C validator |