Theorem wl-sb8t

Description: Substitution of variable in universal quantifier. Closed form of sb8 . (Contributed by Wolf Lammen, 27-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 Ⅎ 𝑦 𝜑
2		nfnf1	⊢ Ⅎ 𝑦 Ⅎ 𝑦 𝜑
3	2	nfal	⊢ Ⅎ 𝑦 ∀ 𝑥 Ⅎ 𝑦 𝜑
4		sp	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑦 𝜑 )
5		wl-nfs1t	⊢ ( Ⅎ 𝑦 𝜑 → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )
6	5	sps	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )
7		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
8	7	a1i	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) )
9	1 3 4 6 8	cbv2	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ) )