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  2208  nfs1f  2282  nfex  2330  nfnf  2332  nfmo1  2558  nfeu1ALT  2589  nfeu1  2590  nfsab1  2723  nfnfc1  2902  nfaba1  2907  nfnfc  2912  nfne  3034  nfnel  3045  nfra1  3261  nfre1  3262  nfra2w  3273  r19.12  3286  nfrmo1  3378  nfreu1  3379  nfrmow  3380  nfreuw  3381  nfrmo  3398  nfss  3927  nfdif  4082  nfun  4123  nfin  4177  nfiu1  4983  nfdisjw  5078  nfdisj  5079  nfdisj1  5080  nfpo  5539  nfso  5540  nffr  5598  nfse  5599  nfwe  5600  nfrel  5730  sb8iota  6460  nffun  6516  nffn  6592  nff  6659  nff1  6729  nffo  6746  nff1o  6773  nfiso  7270  tz7.49  8378  nfixpw  8858  nfixp  8859  bnj919  34925  bnj1379  34988  bnj571  35064  bnj607  35074  bnj873  35082  bnj981  35108  bnj1039  35129  bnj1128  35148  bnj1388  35191  bnj1398  35192  bnj1417  35199  bnj1444  35201  bnj1445  35202  bnj1446  35203  bnj1449  35206  bnj1467  35212  bnj1489  35214  bnj1312  35216  bnj1518  35222  bnj1525  35227  wl-nfae1  37734  ptrecube  37823  nfe2  42537  nfa1w  42985  nfrelp  45257  nfdfat  47440  nfich1  47760  nfich2  47761  ichnfimlem  47776  ich2ex  47781