Theorem nfxfr 1497

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

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

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 1470  ax-gen 1472

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

This theorem is referenced by:  nfnf1  1567  nf3an  1589  nfnf  1600  nfdc  1682  nfs1f  1803  nfsbv  1975  nfeu1  2065  nfmo1  2066  sb8eu  2067  nfeu  2073  nfnfc1  2351  nfnfc  2355  nfeq  2356  nfel  2357  nfabdw  2367  nfne  2469  nfnel  2478  nfra1  2537  nfre1  2549  nfreu1  2678  nfrmo1  2679  nfss  3186  rabn0m  3488  nfdisjv  4033  nfdisj1  4034  nfpo  4349  nfso  4350  nfse  4389  nffrfor  4396  nffr  4397  nfwe  4403  nfrel  4761  sb8iota  5240  nffun  5295  nffn  5371  nff  5424  nff1  5481  nffo  5499  nff1o  5522  nfiso  5877  nfixpxy  6806