Theorem sbrimvw

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

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

Proof

Step	Hyp	Ref	Expression
1		sb6	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) )
2		bi2.04	⊢ ( ( 𝜑 → ( 𝑥 = 𝑦 → 𝜓 ) ) ↔ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) )
3	2	albii	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 = 𝑦 → 𝜓 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) ) )
4		19.21v	⊢ ( ∀ 𝑥 ( 𝜑 → ( 𝑥 = 𝑦 → 𝜓 ) ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) )
5	1 3 4	3bitr2i	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) )
6		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) )
7	6	imbi2i	⊢ ( ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) ↔ ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ) )
8	5 7	bitr4i	⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜓 ) )