Theorem nfxfr 1467

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

Syntax hints:   <-> wb 104   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116  df-nf 1454

This theorem is referenced by:  nfnf1  1537  nf3an  1559  nfnf  1570  nfdc  1652  nfs1f  1773  nfsbv  1940  nfeu1  2030  nfmo1  2031  sb8eu  2032  nfeu  2038  nfnfc1  2315  nfnfc  2319  nfeq  2320  nfel  2321  nfabdw  2331  nfne  2433  nfnel  2442  nfra1  2501  nfre1  2513  nfreu1  2641  nfrmo1  2642  nfss  3140  rabn0m  3441  nfdisjv  3976  nfdisj1  3977  nfpo  4284  nfso  4285  nfse  4324  nffrfor  4331  nffr  4332  nfwe  4338  nfrel  4694  sb8iota  5165  nffun  5219  nffn  5292  nff  5342  nff1  5399  nffo  5417  nff1o  5438  nfiso  5782  nfixpxy  6691