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  3235  rabn0m  3540  nfdisjv  4102  nfdisj1  4103  nfpo  4427  nfso  4428  nfse  4467  nffrfor  4474  nffr  4475  nfwe  4481  nfrel  4840  sb8iota  5325  nffun  5380  nffn  5457  nff  5510  nff1  5576  nffo  5594  nff1o  5617  nfiso  5985  nfixpxy  6965