Theorem bj-nfs1t2

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

	Ref	Expression
Assertion	bj-nfs1t2	|- ( A. x F/ y ph -> F/ x [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		nf5r	|- ( F/ y ph -> ( ph -> A. y ph ) )
2	1	alimi	|- ( A. x F/ y ph -> A. x ( ph -> A. y ph ) )
3		bj-nfs1t	|- ( A. x ( ph -> A. y ph ) -> F/ x [ y / x ] ph )
4	2 3	syl	|- ( A. x F/ y ph -> F/ x [ y / x ] ph )