Theorem nfxfr 1853

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1783

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

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

This theorem is referenced by:  nfnan  1900  nf3an  1901  nfor  1904  nf3or  1905  nfa1  2152  nfnf1  2155  nfs1v  2157  nfa2  2177  nfan1  2201  nfs1f  2275  nfex  2323  nfnf  2325  nfmo1  2550  nfeu1  2581  nfeu1ALT  2582  nfsab1  2715  nfnfc1  2894  nfaba1  2899  nfnfc  2904  nfne  3026  nfnel  3037  nfra1  3259  nfre1  3260  nfra2w  3272  r19.12  3285  nfrmo1  3380  nfreu1  3381  nfrmow  3382  nfreuw  3383  nfrmo  3400  nfss  3936  nfdif  4088  nfun  4129  nfin  4183  nfiu1  4987  nfdisjw  5081  nfdisj  5082  nfdisj1  5083  nfpo  5545  nfso  5546  nffr  5604  nfse  5605  nfwe  5606  nfrel  5734  sb8iota  6463  nffun  6523  nffn  6599  nff  6666  nff1  6736  nffo  6753  nff1o  6780  nfiso  7279  tz7.49  8390  nfixpw  8866  nfixp  8867  bnj919  34750  bnj1379  34813  bnj571  34889  bnj607  34899  bnj873  34907  bnj981  34933  bnj1039  34954  bnj1128  34973  bnj1388  35016  bnj1398  35017  bnj1417  35024  bnj1444  35026  bnj1445  35027  bnj1446  35028  bnj1449  35031  bnj1467  35037  bnj1489  35039  bnj1312  35041  bnj1518  35047  bnj1525  35052  wl-nfae1  37508  wl-ax11-lem4  37569  ptrecube  37607  nfa1w  42656  nfrelp  44932  nfdfat  47121  nfich1  47441  nfich2  47442  ichnfimlem  47457  ich2ex  47462