Theorem bj-nfext

Description: Closed form of nfex . (Contributed by BJ, 10-Oct-2019)

	Ref	Expression
Assertion	bj-nfext	|- ( A. x F/ y ph -> F/ y E. x ph )

Proof

Step	Hyp	Ref	Expression
1		nf5	|- ( F/ y ph <-> A. y ( ph -> A. y ph ) )
2	1	biimpi	|- ( F/ y ph -> A. y ( ph -> A. y ph ) )
3	2	alimi	|- ( A. x F/ y ph -> A. x A. y ( ph -> A. y ph ) )
4		nfa2	|- F/ y A. x A. y ( ph -> A. y ph )
5		bj-hbext	|- ( A. x A. y ( ph -> A. y ph ) -> ( E. x ph -> A. y E. x ph ) )
6	4 5	alrimi	|- ( A. x A. y ( ph -> A. y ph ) -> A. y ( E. x ph -> A. y E. x ph ) )
7	3 6	syl	|- ( A. x F/ y ph -> A. y ( E. x ph -> A. y E. x ph ) )
8		nf5	|- ( F/ y E. x ph <-> A. y ( E. x ph -> A. y E. x ph ) )
9	7 8	sylibr	|- ( A. x F/ y ph -> F/ y E. x ph )