Theorem sbrimvw 2097

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2311 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 2091	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))
2		bi2.04 387	. . . 4 ⊢ ((𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝑥 = 𝑦 → (𝜑 → 𝜓)))
3	2	albii 1821	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))
4		19.21v 1941	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
5	1, 3, 4	3bitr2i 299	. 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
6		sb6 2091	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
7	6	imbi2i 336	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
8	5, 7	bitr4i 278	1 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1540  [wsb 2068

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 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069

This theorem is referenced by:  sbiedvw  2101  cbvralsvw  3289