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  1829  nfsbv  2003  nfeu1  2093  nfmo1  2094  sb8eu  2095  nfeu  2101  nfnfc1  2389  nfnfc  2393  nfeq  2394  nfel  2395  nfabdw  2405  nfne  2507  nfnel  2516  nfra1  2575  nfre1  2587  nfreu1  2717  nfrmo1  2718  nfss  3233  rabn0m  3538  nfdisjv  4099  nfdisj1  4100  nfpo  4424  nfso  4425  nfse  4464  nffrfor  4471  nffr  4472  nfwe  4478  nfrel  4837  sb8iota  5322  nffun  5377  nffn  5454  nff  5507  nff1  5573  nffo  5591  nff1o  5614  nfiso  5981  nfixpxy  6954