Theorem nfxfrd 1646

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
nfxfrd.2

Assertion

Ref	Expression
nfxfrd

Proof of Theorem nfxfrd

Step	Hyp	Ref	Expression
1		nfxfrd.2	. 2
2		nfbii.1	. . 3
3	2	nfbii 1644	. 2
4	1, 3	sylibr 212	1

Syntax hints:  ->wi 4  <->wb 184  F/wnf 1616

This theorem is referenced by:  nfand  1925  nf3and  1926  nfbid  1933  nfexd  1952  dvelimhw  1955  nfexd2  2074  dvelimf  2076  nfeud2  2296  nfmod2  2297  nfeqd  2626  nfeld  2627  nfabd2  2640  nfned  2789  nfneld  2801  nfrald  2842  nfrexd  2919  nfreud  3030  nfrmod  3031  nfsbc1d  3345  nfsbcd  3348  nfbrd  4495  wl-nfnbi  29979  wl-sb8eut  30022

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

This theorem depends on definitions:  df-bi 185  df-nf 1617