Theorem nfxfr 1433

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

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

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

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

This theorem is referenced by:  nfnf1  1506  nf3an  1528  nfnf  1539  nfdc  1620  nfs1f  1736  nfeu1  1986  nfmo1  1987  sb8eu  1988  nfeu  1994  nfnfc1  2258  nfnfc  2262  nfeq  2263  nfel  2264  nfne  2375  nfnel  2384  nfra1  2440  nfre1  2450  nfreu1  2576  nfrmo1  2577  nfss  3056  rabn0m  3356  nfdisjv  3884  nfdisj1  3885  nfpo  4183  nfso  4184  nfse  4223  nffrfor  4230  nffr  4231  nfwe  4237  nfrel  4584  sb8iota  5053  nffun  5104  nffn  5177  nff  5227  nff1  5284  nffo  5302  nff1o  5321  nfiso  5661  nfixpxy  6565