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  4448  nfso  4449  nfse  4488  nffrfor  4495  nffr  4496  nfwe  4502  nfrel  4862  sb8iota  5348  nffun  5403  nffn  5480  nff  5533  nff1  5599  nffo  5617  nff1o  5640  nfiso  6015  nfixpxy  7003  nfals  17351  nfrals  17352  nfalseu  17382  nfralseu  17383