Theorem nfxfr 1615

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

Syntax hints:   <-> wb 184   F/wnf 1589

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

This theorem depends on definitions:  df-bi 185  df-nf 1590

This theorem is referenced by:  nfnf1  1833  nfnan  1862  nf3an  1863  nfor  1868  nf3or  1869  nfnf  1875  nfs1f  2074  nfeu1  2266  nfmo1  2267  sb8euOLD  2293  sb8euOLDOLD  2294  nfnfc1  2592  nfnfc  2598  nfeqOLD  2600  nfelOLD  2602  nfne  2722  nfnel  2731  nfra1  2785  nfrex  2790  nfre1  2791  nfreu1  2910  nfrmo1  2911  nfrmo  2915  nfss  3368  nfdisj  4293  nfdisj1  4294  nfpo  4665  nfso  4666  nffr  4713  nfse  4714  nfwe  4715  nfrel  4944  sb8iota  5407  nffun  5459  nffn  5526  nff  5574  nff1  5623  nffo  5638  nff1o  5658  nfiso  6034  tz7.49  6919  nfixp  7301  wl-nfae1  28379  wl-ax11-lem4  28427  nfdfat  30059  bnj919  31783  bnj1379  31847  bnj571  31922  bnj607  31932  bnj873  31940  bnj981  31966  bnj1039  31985  bnj1128  32004  bnj1388  32047  bnj1398  32048  bnj1417  32055  bnj1444  32057  bnj1445  32058  bnj1446  32059  bnj1449  32062  bnj1467  32068  bnj1489  32070  bnj1312  32072  bnj1518  32078  bnj1525  32083  bj-nfnfc  32387