Theorem sbrimvw 2102

Description: Substitution in an implication with a variable not free in the antecedent affects only the consequent. Version of sbrim 2313 and sbrimv 2314 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		19.21v 1940	. 2 ⊢ (∀𝑥(𝜑 → (𝑥 = 𝑦 → 𝜓)) ↔ (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜓)))
2	1	sbrimvlem 2101	1 ⊢ ([𝑦 / 𝑥](𝜑 → 𝜓) ↔ (𝜑 → [𝑦 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 208  [wsb 2069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070

This theorem is referenced by:  sbiedvw  2104