Theorem nfxfrd 1521

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

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495

This theorem depends on definitions:  df-bi 117  df-nf 1507

This theorem is referenced by:  nf3and  1615  nfbid  1634  nfsbxy  1993  nfsbxyt  1994  nfeud  2093  nfmod  2094  nfeqd  2387  nfeld  2388  nfabdw  2391  nfabd  2392  nfned  2494  nfneld  2503  nfraldw  2562  nfraldxy  2563  nfrexdxy  2564  nfraldya  2565  nfrexdya  2566  nfsbc1d  3045  nfsbcd  3048  nfsbcdw  3158  nfbrd  4128