Theorem nfxfrd 1697

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

Hypotheses

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

Assertion

Ref	Expression
nfxfrd	|- ( ch -> F/ x ph )

Proof of Theorem nfxfrd

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

Syntax hints:   -> wi 4   <-> wb 188   F/wnf 1667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682

This theorem depends on definitions:  df-bi 189  df-nf 1668

This theorem is referenced by:  nfand  2008  nf3and  2009  nfbid  2016  nfexd  2035  dvelimhw  2060  nfexd2  2166  dvelimf  2168  nfeud2  2311  nfmod2  2312  nfeqd  2599  nfeld  2600  nfabd2  2611  nfned  2724  nfneld  2732  nfrald  2773  nfrexd  2849  nfreud  2963  nfrmod  2964  nfsbc1d  3285  nfsbcd  3288  nfbrd  4446  wl-nfnbi  31859  wl-sb8eut  31906