Theorem wl-sb8ft

Description: Substitution of variable in universal quantifier. Closed form of sb8f . (Contributed by Wolf Lammen, 27-Apr-2025)

	Ref	Expression
Assertion	wl-sb8ft	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		sbft	⊢ ( Ⅎ 𝑦 𝜑 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
2	1	alimi	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ∀ 𝑥 ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
3		albi	⊢ ( ∀ 𝑥 ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) → ( ∀ 𝑥 [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 𝜑 ) )
4	2 3	syl	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 𝜑 ) )
5		wl-sb9v	⊢ ( ∀ 𝑥 [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
6	4 5	bitr3di	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )