Theorem nfxfr 1860

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

Syntax hints:   ↔ wb 209  Ⅎwnf 1791

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

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfnan  1908  nf3an  1909  nfor  1912  nf3or  1913  nfa1  2154  nfnf1  2157  nfs1v  2159  nfa2  2176  nfan1  2200  nfs1f  2273  nfex  2325  nfnf  2327  nfsbv  2331  nfmo1  2556  nfeu1  2587  nfeu1ALT  2588  nfsab1  2723  nfnfc1  2900  nfnfc  2909  nfabdwOLD  2921  nfne  3032  nfnel  3043  nfra1  3130  nfra2w  3139  nfre1  3215  r19.12  3233  nfreu1  3272  nfrmo1  3273  nfrmow  3277  nfrmo  3279  nfss  3879  nfdisjw  5016  nfdisj  5017  nfdisj1  5018  nfpo  5458  nfso  5459  nffr  5510  nfse  5511  nfwe  5512  nfrel  5636  sb8iota  6328  nffun  6381  nffn  6456  nff  6519  nff1  6591  nffo  6610  nff1o  6637  nfiso  7109  tz7.49  8159  nfixpw  8575  nfixp  8576  bnj919  32413  bnj1379  32477  bnj571  32553  bnj607  32563  bnj873  32571  bnj981  32597  bnj1039  32618  bnj1128  32637  bnj1388  32680  bnj1398  32681  bnj1417  32688  bnj1444  32690  bnj1445  32691  bnj1446  32692  bnj1449  32695  bnj1467  32701  bnj1489  32703  bnj1312  32705  bnj1518  32711  bnj1525  32716  wl-nfae1  35372  wl-ax11-lem4  35425  ptrecube  35463  nfdfat  44234  nfich1  44515  nfich2  44516  ichnfimlem  44531  ich2ex  44536