Theorem nfxfr 1488

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

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

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 1461  ax-gen 1463

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

This theorem is referenced by:  nfnf1  1558  nf3an  1580  nfnf  1591  nfdc  1673  nfs1f  1794  nfsbv  1966  nfeu1  2056  nfmo1  2057  sb8eu  2058  nfeu  2064  nfnfc1  2342  nfnfc  2346  nfeq  2347  nfel  2348  nfabdw  2358  nfne  2460  nfnel  2469  nfra1  2528  nfre1  2540  nfreu1  2669  nfrmo1  2670  nfss  3176  rabn0m  3478  nfdisjv  4022  nfdisj1  4023  nfpo  4336  nfso  4337  nfse  4376  nffrfor  4383  nffr  4384  nfwe  4390  nfrel  4748  sb8iota  5226  nffun  5281  nffn  5354  nff  5404  nff1  5461  nffo  5479  nff1o  5502  nfiso  5853  nfixpxy  6776