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  3172  rabn0m  3474  nfdisjv  4018  nfdisj1  4019  nfpo  4332  nfso  4333  nfse  4372  nffrfor  4379  nffr  4380  nfwe  4386  nfrel  4744  sb8iota  5222  nffun  5277  nffn  5350  nff  5400  nff1  5457  nffo  5475  nff1o  5498  nfiso  5849  nfixpxy  6771