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  3261  nfre1  3262  nfra2w  3274  r19.12  3288  nfrmo1  3383  nfreu1  3384  nfrmow  3385  nfreuw  3386  nfrmo  3403  nfss  3939  nfdif  4092  nfun  4133  nfin  4187  nfiu1  4991  nfdisjw  5086  nfdisj  5087  nfdisj1  5088  nfpo  5552  nfso  5553  nffr  5611  nfse  5612  nfwe  5613  nfrel  5742  sb8iota  6475  nffun  6539  nffn  6617  nff  6684  nff1  6754  nffo  6771  nff1o  6798  nfiso  7297  tz7.49  8413  nfixpw  8889  nfixp  8890  bnj919  34757  bnj1379  34820  bnj571  34896  bnj607  34906  bnj873  34914  bnj981  34940  bnj1039  34961  bnj1128  34980  bnj1388  35023  bnj1398  35024  bnj1417  35031  bnj1444  35033  bnj1445  35034  bnj1446  35035  bnj1449  35038  bnj1467  35044  bnj1489  35046  bnj1312  35048  bnj1518  35054  bnj1525  35059  wl-nfae1  37515  wl-ax11-lem4  37576  ptrecube  37614  nfa1w  42663  nfrelp  44939  nfdfat  47128  nfich1  47448  nfich2  47449  ichnfimlem  47464  ich2ex  47469