Theorem nfxfr 1692

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	|- ( ph <-> ps )
nfxfr.2	|- F/ x ps

Assertion

Ref	Expression
nfxfr	|- F/ x ph

Proof of Theorem nfxfr

Step	Hyp	Ref	Expression
1		nfxfr.2	. 2 |- F/ x ps
2		nfbii.1	. . 3 |- ( ph <-> ps )
3	2	nfbii 1691	. 2 |- ( F/ x ph <-> F/ x ps )
4	1, 3	mpbir 212	1 |- F/ x ph

Syntax hints:   <-> wb 187   F/wnf 1663

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

This theorem depends on definitions:  df-bi 188  df-nf 1664

This theorem is referenced by:  nfnf1  1953  nfnan  1984  nf3an  1985  nfor  1990  nf3or  1991  nfnf  2004  nfs1f  2175  nfeu1  2274  nfmo1  2275  nfnfc1  2585  nfnfc  2591  nfnfcALT  2592  nfeqOLD  2594  nfelOLD  2596  nfne  2754  nfnel  2766  nfra1  2804  nfre1  2884  nfrexOLD  2887  nfreu1  2997  nfrmo1  2998  nfrmo  3002  nfss  3454  nfdisj  4400  nfdisj1  4401  nfpo  4771  nfso  4772  nffr  4819  nfse  4820  nfwe  4821  nfrel  4931  sb8iota  5563  nffun  5614  nffn  5681  nff  5733  nff1  5785  nffo  5800  nff1o  5820  nfiso  6221  tz7.49  7161  nfixp  7540  bnj919  29392  bnj1379  29456  bnj571  29531  bnj607  29541  bnj873  29549  bnj981  29575  bnj1039  29594  bnj1128  29613  bnj1388  29656  bnj1398  29657  bnj1417  29664  bnj1444  29666  bnj1445  29667  bnj1446  29668  bnj1449  29671  bnj1467  29677  bnj1489  29679  bnj1312  29681  bnj1518  29687  bnj1525  29692  bj-nfnfc  31239  wl-nfae1  31593  wl-ax11-lem4  31651  ptrecube  31673  nfdfat  38064