Theorem nfxfr 1625

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 1624	. 2 |- ( F/ x ph <-> F/ x ps )
4	1, 3	mpbir 209	1 |- F/ x ph

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

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

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

This theorem is referenced by:  nfnf1  1847  nfnan  1876  nf3an  1877  nfor  1882  nf3or  1883  nfnf  1896  nfs1f  2097  nfeu1  2288  nfmo1  2289  sb8euOLD  2315  sb8euOLDOLD  2316  nfnfc1  2632  nfnfc  2638  nfnfcALT  2639  nfeqOLD  2641  nfelOLD  2643  nfne  2798  nfnel  2810  nfra1  2845  nfre1  2925  nfrexOLD  2928  nfreu1  3032  nfrmo1  3033  nfrmo  3037  nfss  3497  nfdisj  4429  nfdisj1  4430  nfpo  4805  nfso  4806  nffr  4853  nfse  4854  nfwe  4855  nfrel  5088  sb8iota  5558  nffun  5610  nffn  5677  nff  5727  nff1  5779  nffo  5794  nff1o  5814  nfiso  6209  tz7.49  7111  nfixp  7489  wl-nfae1  29833  wl-ax11-lem4  29881  nfdfat  31909  bnj919  33121  bnj1379  33185  bnj571  33260  bnj607  33270  bnj873  33278  bnj981  33304  bnj1039  33323  bnj1128  33342  bnj1388  33385  bnj1398  33386  bnj1417  33393  bnj1444  33395  bnj1445  33396  bnj1446  33397  bnj1449  33400  bnj1467  33406  bnj1489  33408  bnj1312  33410  bnj1518  33416  bnj1525  33421  bj-nfnfc  33727