Theorem nfxfr 1474

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

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

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 1447  ax-gen 1449

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

This theorem is referenced by:  nfnf1  1544  nf3an  1566  nfnf  1577  nfdc  1659  nfs1f  1780  nfsbv  1947  nfeu1  2037  nfmo1  2038  sb8eu  2039  nfeu  2045  nfnfc1  2322  nfnfc  2326  nfeq  2327  nfel  2328  nfabdw  2338  nfne  2440  nfnel  2449  nfra1  2508  nfre1  2520  nfreu1  2648  nfrmo1  2649  nfss  3148  rabn0m  3450  nfdisjv  3992  nfdisj1  3993  nfpo  4301  nfso  4302  nfse  4341  nffrfor  4348  nffr  4349  nfwe  4355  nfrel  4711  sb8iota  5185  nffun  5239  nffn  5312  nff  5362  nff1  5419  nffo  5437  nff1o  5459  nfiso  5806  nfixpxy  6716