Theorem nfxfr 1498

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

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

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 1471  ax-gen 1473

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

This theorem is referenced by:  nfnf1  1568  nf3an  1590  nfnf  1601  nfdc  1683  nfs1f  1804  nfsbv  1976  nfeu1  2066  nfmo1  2067  sb8eu  2068  nfeu  2074  nfnfc1  2353  nfnfc  2357  nfeq  2358  nfel  2359  nfabdw  2369  nfne  2471  nfnel  2480  nfra1  2539  nfre1  2551  nfreu1  2680  nfrmo1  2681  nfss  3194  rabn0m  3496  nfdisjv  4047  nfdisj1  4048  nfpo  4366  nfso  4367  nfse  4406  nffrfor  4413  nffr  4414  nfwe  4420  nfrel  4778  sb8iota  5258  nffun  5313  nffn  5389  nff  5442  nff1  5501  nffo  5519  nff1o  5542  nfiso  5898  nfixpxy  6827