Theorem nfxfr 1645

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

Hypotheses

Ref	Expression
nfbii.1
nfxfr.2

Assertion

Ref	Expression
nfxfr

Proof of Theorem nfxfr

Step	Hyp	Ref	Expression
1		nfxfr.2	. 2
2		nfbii.1	. . 3
3	2	nfbii 1644	. 2
4	1, 3	mpbir 209	1

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

This theorem is referenced by:  nfnf1  1899  nfnan  1929  nf3an  1930  nfor  1935  nf3or  1936  nfnf  1949  nfs1f  2124  nfeu1  2294  nfmo1  2295  sb8euOLD  2319  nfnfc1  2622  nfnfc  2628  nfnfcALT  2629  nfeqOLD  2631  nfelOLD  2633  nfne  2788  nfnel  2800  nfra1  2838  nfre1  2918  nfrexOLD  2921  nfreu1  3028  nfrmo1  3029  nfrmo  3033  nfss  3496  nfdisj  4434  nfdisj1  4435  nfpo  4810  nfso  4811  nffr  4858  nfse  4859  nfwe  4860  nfrel  5093  sb8iota  5563  nffun  5615  nffn  5682  nff  5732  nff1  5784  nffo  5799  nff1o  5819  nfiso  6220  tz7.49  7129  nfixp  7508  wl-nfae1  29980  wl-ax11-lem4  30028  nfdfat  32215  bnj919  33825  bnj1379  33889  bnj571  33964  bnj607  33974  bnj873  33982  bnj981  34008  bnj1039  34027  bnj1128  34046  bnj1388  34089  bnj1398  34090  bnj1417  34097  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1449  34104  bnj1467  34110  bnj1489  34112  bnj1312  34114  bnj1518  34120  bnj1525  34125  bj-nfnfc  34429

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