Theorem nfceqdf

Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypotheses	nfceqdf.1	|- F/ x ph
	nfceqdf.2	|- ( ph -> A = B )
Assertion	nfceqdf	|- ( ph -> ( F/_ x A <-> F/_ x B ) )

Proof

Step	Hyp	Ref	Expression
1		nfceqdf.1	|- F/ x ph
2		nfceqdf.2	|- ( ph -> A = B )
3	2	eleq2d	|- ( ph -> ( y e. A <-> y e. B ) )
4	1 3	nfbidf	|- ( ph -> ( F/ x y e. A <-> F/ x y e. B ) )
5	4	albidv	|- ( ph -> ( A. y F/ x y e. A <-> A. y F/ x y e. B ) )
6		df-nfc	|- ( F/_ x A <-> A. y F/ x y e. A )
7		df-nfc	|- ( F/_ x B <-> A. y F/ x y e. B )
8	5 6 7	3bitr4g	|- ( ph -> ( F/_ x A <-> F/_ x B ) )