Theorem bj-nfs1t

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-hbsb3t	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ) )
2	1	axc4i	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → ∀ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ) )
3		nf5	⊢ ( Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ) )
4	2 3	sylibr	⊢ ( ∀ 𝑥 ( 𝜑 → ∀ 𝑦 𝜑 ) → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )