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  34751  bnj1379  34814  bnj571  34890  bnj607  34900  bnj873  34908  bnj981  34934  bnj1039  34955  bnj1128  34974  bnj1388  35017  bnj1398  35018  bnj1417  35025  bnj1444  35027  bnj1445  35028  bnj1446  35029  bnj1449  35032  bnj1467  35038  bnj1489  35040  bnj1312  35042  bnj1518  35048  bnj1525  35053  wl-nfae1  37509  wl-ax11-lem4  37570  ptrecube  37608  nfa1w  42657  nfrelp  44933  nfdfat  47122  nfich1  47442  nfich2  47443  ichnfimlem  47458  ich2ex  47463