Theorem nfbidf

Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021)

	Ref	Expression
Hypotheses	albid.1	|- F/ x ph
	albid.2	|- ( ph -> ( ps <-> ch ) )
Assertion	nfbidf	|- ( ph -> ( F/ x ps <-> F/ x ch ) )

Proof

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