Theorem nfxfr 1485

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

Syntax hints:   <-> wb 105   F/wnf 1471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  nfnf1  1555  nf3an  1577  nfnf  1588  nfdc  1670  nfs1f  1791  nfsbv  1963  nfeu1  2053  nfmo1  2054  sb8eu  2055  nfeu  2061  nfnfc1  2339  nfnfc  2343  nfeq  2344  nfel  2345  nfabdw  2355  nfne  2457  nfnel  2466  nfra1  2525  nfre1  2537  nfreu1  2666  nfrmo1  2667  nfss  3173  rabn0m  3475  nfdisjv  4019  nfdisj1  4020  nfpo  4333  nfso  4334  nfse  4373  nffrfor  4380  nffr  4381  nfwe  4387  nfrel  4745  sb8iota  5223  nffun  5278  nffn  5351  nff  5401  nff1  5458  nffo  5476  nff1o  5499  nfiso  5850  nfixpxy  6773