Theorem nfbiit

Description: Equivalence theorem for the non-freeness predicate. Closed form of nfbii . (Contributed by Giovanni Mascellani, 10-Apr-2018) Reduce axiom usage. (Revised by BJ, 6-May-2019)

	Ref	Expression
Assertion	nfbiit	|- ( A. x ( ph <-> ps ) -> ( F/ x ph <-> F/ x ps ) )

Proof

Step	Hyp	Ref	Expression
1		exbi	|- ( A. x ( ph <-> ps ) -> ( E. x ph <-> E. x ps ) )
2		albi	|- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
3	1 2	imbi12d	|- ( A. x ( ph <-> ps ) -> ( ( E. x ph -> A. x ph ) <-> ( E. x ps -> A. x ps ) ) )
4		df-nf	|- ( F/ x ph <-> ( E. x ph -> A. x ph ) )
5		df-nf	|- ( F/ x ps <-> ( E. x ps -> A. x ps ) )
6	3 4 5	3bitr4g	|- ( A. x ( ph <-> ps ) -> ( F/ x ph <-> F/ x ps ) )