Theorem nfxfr 1403

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

Syntax hints:   <-> wb 103   F/wnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nfnf1  1476  nf3an  1498  nfnf  1509  nfdc  1589  nfs1f  1703  nfeu1  1952  nfmo1  1953  sb8eu  1954  nfeu  1960  nfnfc1  2222  nfnfc  2225  nfeq  2226  nfel  2227  nfne  2337  nfnel  2346  nfra1  2397  nfre1  2407  nfreu1  2525  nfrmo1  2526  nfss  2992  rabn0m  3272  nfdisjv  3778  nfdisj1  3779  nfpo  4056  nfso  4057  nfse  4096  nffrfor  4103  nffr  4104  nfwe  4110  nfrel  4443  sb8iota  4894  nffun  4944  nffn  5015  nff  5063  nff1  5110  nffo  5125  nff1o  5144  nfiso  5466