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  3442  nfdisjv  3978  nfdisj1  3979  nfpo  4286  nfso  4287  nfse  4326  nffrfor  4333  nffr  4334  nfwe  4340  nfrel  4696  sb8iota  5167  nffun  5221  nffn  5294  nff  5344  nff1  5401  nffo  5419  nff1o  5440  nfiso  5785  nfixpxy  6695