Theorem wl-sb6rft

Description: A specialization of wl-equsal1t . Closed form of sb6rf . (Contributed by Wolf Lammen, 27-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜑
2		id	⊢ ( Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
3		sbequ12r	⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) )
4	3	a1i	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) )
5	1 2 4	wl-equsald	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → [ 𝑥 / 𝑦 ] 𝜑 ) ↔ 𝜑 ) )
6	5	bicomd	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → [ 𝑥 / 𝑦 ] 𝜑 ) ) )