Theorem bj-nfs1t

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-hbsb3t	|- ( A. x ( ph -> A. y ph ) -> ( [ y / x ] ph -> A. x [ y / x ] ph ) )
2	1	axc4i	|- ( A. x ( ph -> A. y ph ) -> A. x ( [ y / x ] ph -> A. x [ y / x ] ph ) )
3		nf5	|- ( F/ x [ y / x ] ph <-> A. x ( [ y / x ] ph -> A. x [ y / x ] ph ) )
4	2 3	sylibr	|- ( A. x ( ph -> A. y ph ) -> F/ x [ y / x ] ph )