Theorem nfxfrd 1528

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 1526	. 2 |- ( F/ x ph <-> F/ x ps )
4	1, 3	sylibr 134	1 |- ( ch -> F/ x ph )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nf3and  1622  nfbid  1641  nfsbxy  2002  nfsbxyt  2003  nfeud  2102  nfmod  2103  nfeqd  2407  nfeld  2408  nfabdw  2411  nfabd  2412  nfned  2514  nfneld  2523  nfraldw  2582  nfraldxy  2583  nfrexdxy  2584  nfraldya  2585  nfrexdya  2586  nfsbc1d  3068  nfsbcd  3071  nfsbcdw  3181  nfbrd  4176