Theorem nfxfr 1849

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	⊢ (𝜑 ↔ 𝜓)
nfxfr.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfxfr	⊢ Ⅎ𝑥𝜑

Proof of Theorem nfxfr

Step	Hyp	Ref	Expression
1		nfxfr.2	. 2 ⊢ Ⅎ𝑥𝜓
2		nfbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	nfbii 1848	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	mpbir 231	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   ↔ wb 206  Ⅎwnf 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-nf 1780

This theorem is referenced by:  nfnan  1897  nf3an  1898  nfor  1901  nf3or  1902  nfa1  2148  nfnf1  2151  nfs1v  2153  nfa2  2173  nfan1  2197  nfs1f  2272  nfex  2322  nfnf  2324  nfsbvOLD  2329  nfmo1  2554  nfeu1  2585  nfeu1ALT  2586  nfsab1  2719  nfnfc1  2905  nfaba1  2910  nfnfc  2915  nfne  3040  nfnel  3051  nfra1  3281  nfre1  3282  nfra2w  3296  nfra2wOLD  3297  r19.12  3311  r19.12OLD  3312  nfrmo1  3408  nfreu1  3409  nfrmow  3410  nfreuw  3411  nfrmowOLD  3423  nfrmo  3430  nfss  3987  nfdif  4138  nfun  4179  nfin  4231  nfiu1  5031  nfdisjw  5126  nfdisj  5127  nfdisj1  5128  nfpo  5602  nfso  5603  nffr  5661  nfse  5662  nfwe  5663  nfrel  5791  sb8iota  6526  nffun  6590  nffn  6667  nff  6732  nff1  6802  nffo  6819  nff1o  6846  nfiso  7341  tz7.49  8483  nfixpw  8954  nfixp  8955  bnj919  34759  bnj1379  34822  bnj571  34898  bnj607  34908  bnj873  34916  bnj981  34942  bnj1039  34963  bnj1128  34982  bnj1388  35025  bnj1398  35026  bnj1417  35033  bnj1444  35035  bnj1445  35036  bnj1446  35037  bnj1449  35040  bnj1467  35046  bnj1489  35048  bnj1312  35050  bnj1518  35056  bnj1525  35061  wl-nfae1  37507  wl-ax11-lem4  37568  ptrecube  37606  nfa1w  42661  nfdfat  47076  nfich1  47371  nfich2  47372  ichnfimlem  47387  ich2ex  47392