Theorem sbrimvw 2094

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2300 based on fewer axioms, but with more disjoint variable conditions. Based on an idea of Gino Giotto. (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 2088	. . 3 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))
2		bi2.04 388	. . . 4 ⊢ ((𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝑥 = 𝑦 → (𝜑 → 𝜓)))
3	2	albii 1821	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ ∀𝑥(𝑥 = 𝑦 → (𝜑 → 𝜓)))
4		19.21v 1942	. . 3 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
5	1, 3, 4	3bitr2i 298	. 2 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
6		sb6 2088	. . 3 ⊢ ([𝑦 / 𝑥]𝜓 ↔ ∀𝑥(𝑥 = 𝑦 → 𝜓))
7	6	imbi2i 335	. 2 ⊢ ((𝜑 → [𝑦 / 𝑥]𝜓) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
8	5, 7	bitr4i 277	1 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539  [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:  sbiedvw  2096