Theorem nfxfr 1875

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

Syntax hints:   ↔ wb 208  Ⅎwnf 1805

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

This theorem depends on definitions:  df-bi 209  df-ex 1802  df-nf 1806

This theorem is referenced by:  nfnan  1922  nf3an  1923  nfor  1926  nf3or  1927  nfa1  2187  nfnf1  2190  nfs1v  2192  nfa2  2211  nfan1  2237  nfs1f  2311  nfex  2358  nfnf  2360  nfmo1  2586  nfeu1ALT  2617  nfeu1  2618  nfsab1  2750  nfnfc1  2929  nfaba1  2934  nfnfc  2938  nfne  3060  nfnel  3071  nfra1  3288  nfre1  3289  nfra2w  3300  r19.12  3313  nfrmo1  3396  nfreu1  3397  nfrmow  3398  nfreuw  3399  nfrmo  3414  nfss  3931  nfdif  4085  nfun  4125  nfin  4178  nfiu1  4987  nfdisjw  5081  nfdisj  5082  nfdisj1  5083  nfpo  5563  nfso  5564  nffr  5622  nfse  5623  nfwe  5624  nfrel  5754  sb8iota  6490  nffun  6546  nffn  6622  nff  6689  nff1  6760  nffo  6779  nff1o  6806  nfiso  7308  tz7.49  8418  nfixpw  8900  nfixp  8901  bnj919  35065  bnj1379  35127  bnj571  35203  bnj607  35213  bnj873  35221  bnj981  35247  bnj1039  35268  bnj1128  35287  bnj1388  35330  bnj1398  35331  bnj1417  35338  bnj1444  35340  bnj1445  35341  bnj1446  35342  bnj1449  35345  bnj1467  35351  bnj1489  35353  bnj1312  35355  bnj1518  35361  bnj1525  35366  wl-nfae1  38035  ptrecube  38124  nfe2  42837  nfa1w  43262  nfrelp  45530  nfdfat  47726  nfich1  48058  nfich2  48059  ichnfimlem  48074  ich2ex  48079