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  1959  nfeu1  2049  nfmo1  2050  sb8eu  2051  nfeu  2057  nfnfc1  2335  nfnfc  2339  nfeq  2340  nfel  2341  nfabdw  2351  nfne  2453  nfnel  2462  nfra1  2521  nfre1  2533  nfreu1  2662  nfrmo1  2663  nfss  3167  rabn0m  3469  nfdisjv  4014  nfdisj1  4015  nfpo  4326  nfso  4327  nfse  4366  nffrfor  4373  nffr  4374  nfwe  4380  nfrel  4736  sb8iota  5210  nffun  5265  nffn  5338  nff  5388  nff1  5445  nffo  5463  nff1o  5485  nfiso  5835  nfixpxy  6751