Theorem nfxfr 1523

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

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

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 1496  ax-gen 1498

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

This theorem is referenced by:  nfnf1  1593  nf3an  1615  nfnf  1626  nfdc  1707  nfs1f  1828  nfsbv  2000  nfeu1  2090  nfmo1  2091  sb8eu  2092  nfeu  2098  nfnfc1  2378  nfnfc  2382  nfeq  2383  nfel  2384  nfabdw  2394  nfne  2496  nfnel  2505  nfra1  2564  nfre1  2576  nfreu1  2706  nfrmo1  2707  nfss  3221  rabn0m  3524  nfdisjv  4081  nfdisj1  4082  nfpo  4404  nfso  4405  nfse  4444  nffrfor  4451  nffr  4452  nfwe  4458  nfrel  4817  sb8iota  5301  nffun  5356  nffn  5433  nff  5486  nff1  5549  nffo  5567  nff1o  5590  nfiso  5957  nfixpxy  6929