Theorem bj-nfs1t2

Description: A theorem close to a closed form of nfs1 . (Contributed by BJ, 2-May-2019)

	Ref	Expression
Assertion	bj-nfs1t2	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		nf5r	⊢ ( Ⅎ 𝑦 𝜑 → ( 𝜑 → ∀ 𝑦 𝜑 ) )
2	1	alimi	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) )
3		bj-nfs1t	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )
4	2 3	syl	⊢ ( ∀ 𝑥 Ⅎ 𝑦 𝜑 → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )