Theorem nfxfr 1855

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1902  nf3an  1903  nfor  1906  nf3or  1907  nfa1  2157  nfnf1  2160  nfs1v  2162  nfa2  2182  nfan1  2206  nfs1f  2280  nfex  2328  nfnf  2330  nfmo1  2556  nfeu1  2587  nfeu1ALT  2588  nfsab1  2721  nfnfc1  2900  nfaba1  2905  nfnfc  2910  nfne  3032  nfnel  3043  nfra1  3259  nfre1  3260  nfra2w  3271  r19.12  3284  nfrmo1  3376  nfreu1  3377  nfrmow  3378  nfreuw  3379  nfrmo  3396  nfss  3925  nfdif  4080  nfun  4121  nfin  4175  nfiu1  4981  nfdisjw  5076  nfdisj  5077  nfdisj1  5078  nfpo  5537  nfso  5538  nffr  5596  nfse  5597  nfwe  5598  nfrel  5728  sb8iota  6458  nffun  6514  nffn  6590  nff  6657  nff1  6727  nffo  6744  nff1o  6771  nfiso  7268  tz7.49  8376  nfixpw  8856  nfixp  8857  bnj919  34902  bnj1379  34965  bnj571  35041  bnj607  35051  bnj873  35059  bnj981  35085  bnj1039  35106  bnj1128  35125  bnj1388  35168  bnj1398  35169  bnj1417  35176  bnj1444  35178  bnj1445  35179  bnj1446  35180  bnj1449  35183  bnj1467  35189  bnj1489  35191  bnj1312  35193  bnj1518  35199  bnj1525  35204  wl-nfae1  37701  ptrecube  37790  nfe2  42505  nfa1w  42955  nfrelp  45227  nfdfat  47410  nfich1  47730  nfich2  47731  ichnfimlem  47746  ich2ex  47751