Theorem sbrimvw 2096

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

Syntax hints:   → wi 4   ↔ wb 205  [wsb 2068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069

This theorem is referenced by:  sbiedvw  2098