Theorem nfxfr 1450

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

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

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 1423  ax-gen 1425

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

This theorem is referenced by:  nfnf1  1523  nf3an  1545  nfnf  1556  nfdc  1637  nfs1f  1753  nfeu1  2008  nfmo1  2009  sb8eu  2010  nfeu  2016  nfnfc1  2282  nfnfc  2286  nfeq  2287  nfel  2288  nfne  2399  nfnel  2408  nfra1  2464  nfre1  2474  nfreu1  2600  nfrmo1  2601  nfss  3085  rabn0m  3385  nfdisjv  3913  nfdisj1  3914  nfpo  4218  nfso  4219  nfse  4258  nffrfor  4265  nffr  4266  nfwe  4272  nfrel  4619  sb8iota  5090  nffun  5141  nffn  5214  nff  5264  nff1  5321  nffo  5339  nff1o  5358  nfiso  5700  nfixpxy  6604