Theorem nfxfr 1527

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

This proof depends on syntax axioms:   <-> wb 105   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nfnf1  1597  nf3an  1619  nfnf  1630  nfdc  1711  nfs1f  1833  nfsbv  2007  nfeu1  2097  nfmo1  2098  sb8eu  2099  nfeu  2105  nfnfc1  2395  nfnfc  2399  nfeq  2400  nfel  2401  nfabdw  2411  nfne  2513  nfnel  2522  nfra1  2581  nfre1  2593  nfreu1  2723  nfrmo1  2724  nfss  3241  rabn0m  3549  nfdisjv  4118  nfdisj1  4119  nfpo  4446  nfso  4447  nfse  4486  nffrfor  4493  nffr  4494  nfwe  4500  nfrel  4860  sb8iota  5345  nffun  5400  nffn  5477  nff  5530  nff1  5596  nffo  5614  nff1o  5637  nfiso  6012  nfixpxy  6999  nfals  17144  nfrals  17145  nfalseu  17175  nfralseu  17176