Theorem nfxfr 1929

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

Syntax hints:   ↔ wb 196  Ⅎwnf 1856

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

This theorem depends on definitions:  df-bi 197  df-ex 1853  df-nf 1858

This theorem is referenced by:  nfanOLD  1981  nfnan  1982  nf3an  1983  nfor  1986  nf3or  1987  nfa1  2184  nfnf1  2187  nfa2  2196  nfan1  2222  nfan1OLDOLD  2223  nfs1v  2274  nfex  2318  nfnf  2322  nfnf1OLD  2323  nfs1f  2530  nfeu1  2628  nfmo1  2629  nfnfc1  2916  nfnfc  2923  nfnfcALT  2924  nfne  3043  nfnel  3053  nfra1  3090  nfre1  3153  nfreu1  3258  nfrmo1  3259  nfrmo  3263  nfss  3745  nfdisj  4766  nfdisj1  4767  nfpo  5175  nfso  5176  nffr  5223  nfse  5224  nfwe  5225  nfrel  5344  sb8iota  6001  nffun  6054  nffn  6127  nff  6181  nff1  6239  nffo  6255  nff1o  6276  nfiso  6715  tz7.49  7693  nfixp  8081  bnj919  31175  bnj1379  31239  bnj571  31314  bnj607  31324  bnj873  31332  bnj981  31358  bnj1039  31377  bnj1128  31396  bnj1388  31439  bnj1398  31440  bnj1417  31447  bnj1444  31449  bnj1445  31450  bnj1446  31451  bnj1449  31454  bnj1467  31460  bnj1489  31462  bnj1312  31464  bnj1518  31470  bnj1525  31475  wl-nfae1  33650  wl-ax11-lem4  33699  ptrecube  33742  nfdfat  41730