Theorem sbrimvw 2092

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2305 based on fewer axioms, but with more disjoint variable conditions. Based on an idea of GG. (Contributed by Wolf Lammen, 29-Jan-2024.)

Assertion

Ref	Expression
sbrimvw	⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑥

Allowed substitution hints:   𝜑(𝑦)   𝜓(𝑥,𝑦)

Proof of Theorem sbrimvw

Step	Hyp	Ref	Expression
1		sb6 2086	. . 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 2086	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
7	6	imbi2i 336	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
8	5, 7	bitr4i 278	1 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538  [wsb 2065

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 2008

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066

This theorem is referenced by:  sbiedvw  2096  cbvralsvw  3300