Theorem nfxfr 1462

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

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

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 1435  ax-gen 1437

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

This theorem is referenced by:  nfnf1  1532  nf3an  1554  nfnf  1565  nfdc  1647  nfs1f  1768  nfsbv  1935  nfeu1  2025  nfmo1  2026  sb8eu  2027  nfeu  2033  nfnfc1  2311  nfnfc  2315  nfeq  2316  nfel  2317  nfabdw  2327  nfne  2429  nfnel  2438  nfra1  2497  nfre1  2509  nfreu1  2637  nfrmo1  2638  nfss  3135  rabn0m  3436  nfdisjv  3971  nfdisj1  3972  nfpo  4279  nfso  4280  nfse  4319  nffrfor  4326  nffr  4327  nfwe  4333  nfrel  4689  sb8iota  5160  nffun  5211  nffn  5284  nff  5334  nff1  5391  nffo  5409  nff1o  5430  nfiso  5774  nfixpxy  6683