Theorem wl-sbid2ft

Description: A more general version of sbid2vw . (Contributed by Wolf Lammen, 14-May-2019)

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

Proof

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