Theorem nfxfr 1855

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 1854	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	mpbir 230	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   ↔ wb 205  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1903  nf3an  1904  nfor  1907  nf3or  1908  nfa1  2148  nfnf1  2151  nfs1v  2153  nfa2  2170  nfan1  2193  nfs1f  2266  nfex  2317  nfnf  2319  nfsbvOLD  2324  nfmo1  2551  nfeu1  2582  nfeu1ALT  2583  nfsab1  2717  nfnfc1  2906  nfnfc  2915  nfabdwOLD  2927  nfne  3043  nfnel  3054  nfra1  3281  nfre1  3282  nfra2w  3296  nfra2wOLD  3297  r19.12  3311  r19.12OLD  3312  nfrmo1  3407  nfreu1  3408  nfrmow  3409  nfreuw  3410  nfrmowOLD  3423  nfrmo  3430  nfss  3974  nfdisjw  5125  nfdisj  5126  nfdisj1  5127  nfpo  5593  nfso  5594  nffr  5650  nfse  5651  nfwe  5652  nfrel  5779  sb8iota  6507  nffun  6571  nffn  6648  nff  6713  nff1  6785  nffo  6804  nff1o  6831  nfiso  7318  tz7.49  8444  nfixpw  8909  nfixp  8910  bnj919  33773  bnj1379  33836  bnj571  33912  bnj607  33922  bnj873  33930  bnj981  33956  bnj1039  33977  bnj1128  33996  bnj1388  34039  bnj1398  34040  bnj1417  34047  bnj1444  34049  bnj1445  34050  bnj1446  34051  bnj1449  34054  bnj1467  34060  bnj1489  34062  bnj1312  34064  bnj1518  34070  bnj1525  34075  wl-nfae1  36391  wl-ax11-lem4  36445  ptrecube  36483  nfdfat  45825  nfich1  46105  nfich2  46106  ichnfimlem  46121  ich2ex  46126