Theorem nfxfr 1886

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

This proof depends on syntax axioms:   ↔ wb 209  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfnan  1933  nf3an  1934  nfor  1937  nf3or  1938  nfa1  2188  nfnf1  2191  nfs1v  2193  nfa2  2212  nfan1  2238  nfs1f  2310  nfex  2356  nfnf  2358  nfmo1  2584  nfeu1ALT  2615  nfeu1  2616  nfsab1  2748  nfnfc1  2927  nfaba1  2932  nfnfc  2936  nfne  3060  nfnel  3071  nfra1  3288  nfre1  3289  nfra2w  3300  r19.12  3313  nfrmo1  3394  nfreu1  3395  nfrmow  3396  nfreuw  3397  nfrmo  3412  nfss  3927  nfdif  4080  nfun  4120  nfin  4173  nfiu1  4990  nfdisjw  5086  nfdisj  5087  nfdisj1  5088  nfpo  5573  nfso  5574  nffr  5632  nfse  5633  nfwe  5634  nfrel  5764  sb8iota  6504  nffun  6560  nffn  6635  nff  6702  nff1  6773  nffo  6792  nff1o  6819  nfiso  7326  tz7.49  8437  nfixpw  8926  nfixp  8927  bnj919  35264  bnj1379  35326  bnj571  35402  bnj607  35412  bnj873  35420  bnj981  35446  bnj1039  35467  bnj1128  35486  bnj1388  35529  bnj1398  35530  bnj1417  35537  bnj1444  35539  bnj1445  35540  bnj1446  35541  bnj1449  35544  bnj1467  35550  bnj1489  35552  bnj1312  35554  bnj1518  35560  bnj1525  35565  wl-nfae1  38277  ptrecube  38356  nfe2  43070  nfa1w  43508  nfrelp  45759  nfdfat  48002  nfich1  48334  nfich2  48335  ichnfimlem  48350  ich2ex  48355  nfals  50719  nfrals  50720  nfalseu  50750  nfralseu  50751