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  3253  nfre1  3254  nfra2w  3265  r19.12  3278  nfrmo1  3372  nfreu1  3373  nfrmow  3374  nfreuw  3375  nfrmo  3392  nfss  3928  nfdif  4080  nfun  4121  nfin  4175  nfiu1  4977  nfdisjw  5071  nfdisj  5072  nfdisj1  5073  nfpo  5533  nfso  5534  nffr  5592  nfse  5593  nfwe  5594  nfrel  5723  sb8iota  6449  nffun  6505  nffn  6581  nff  6648  nff1  6718  nffo  6735  nff1o  6762  nfiso  7259  tz7.49  8367  nfixpw  8843  nfixp  8844  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  37521  wl-ax11-lem4  37582  ptrecube  37620  nfa1w  42668  nfrelp  44943  nfdfat  47131  nfich1  47451  nfich2  47452  ichnfimlem  47467  ich2ex  47472