Theorem nfxfrd

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016)

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

Proof

Step	Hyp	Ref	Expression
1		nfbii.1	|- ( ph <-> ps )
2		nfxfrd.2	|- ( ch -> F/ x ps )
3	1	nfbii	|- ( F/ x ph <-> F/ x ps )
4	2 3	sylibr	|- ( ch -> F/ x ph )