Theorem nfxfr 1698

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

Syntax hints:   <-> wb 188   F/wnf 1669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684

This theorem depends on definitions:  df-bi 189  df-nf 1670

This theorem is referenced by:  nfnf1  1983  nfnan  2014  nf3an  2015  nfor  2020  nf3or  2021  nfnf  2034  nfs1f  2214  nfeu1  2311  nfmo1  2312  nfnfc1  2597  nfnfc  2603  nfnfcALT  2604  nfne  2725  nfnel  2733  nfra1  2771  nfre1  2850  nfrexOLD  2853  nfreu1  2963  nfrmo1  2964  nfrmo  2968  nfss  3427  nfdisj  4388  nfdisj1  4389  nfpo  4763  nfso  4764  nffr  4811  nfse  4812  nfwe  4813  nfrel  4923  sb8iota  5556  nffun  5607  nffn  5677  nff  5729  nff1  5782  nffo  5797  nff1o  5817  nfiso  6220  tz7.49  7167  nfixp  7546  bnj919  29590  bnj1379  29654  bnj571  29729  bnj607  29739  bnj873  29747  bnj981  29773  bnj1039  29792  bnj1128  29811  bnj1388  29854  bnj1398  29855  bnj1417  29862  bnj1444  29864  bnj1445  29865  bnj1446  29866  bnj1449  29869  bnj1467  29875  bnj1489  29877  bnj1312  29879  bnj1518  29885  bnj1525  29890  bj-nfnfc  31474  wl-nfae1  31872  wl-ax11-lem4  31930  ptrecube  31952  nfdfat  38642