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  2210  nfan1  2236  nfs1f  2308  nfex  2354  nfnf  2356  nfmo1  2582  nfeu1ALT  2613  nfeu1  2614  nfsab1  2746  nfnfc1  2925  nfaba1  2930  nfnfc  2934  nfne  3058  nfnel  3069  nfra1  3286  nfre1  3287  nfra2w  3298  r19.12  3311  nfrmo1  3392  nfreu1  3393  nfrmow  3394  nfreuw  3395  nfrmo  3410  nfss  3924  nfdif  4077  nfun  4117  nfin  4170  nfiu1  4986  nfdisjw  5082  nfdisj  5083  nfdisj1  5084  nfpo  5562  nfso  5563  nffr  5621  nfse  5622  nfwe  5623  nfrel  5753  sb8iota  6495  nffun  6551  nffn  6627  nff  6694  nff1  6765  nffo  6784  nff1o  6811  nfiso  7319  tz7.49  8434  nfixpw  8923  nfixp  8924  bnj919  35318  bnj1379  35380  bnj571  35456  bnj607  35466  bnj873  35474  bnj981  35500  bnj1039  35521  bnj1128  35540  bnj1388  35583  bnj1398  35584  bnj1417  35591  bnj1444  35593  bnj1445  35594  bnj1446  35595  bnj1449  35598  bnj1467  35604  bnj1489  35606  bnj1312  35608  bnj1518  35614  bnj1525  35619  wl-nfae1  38373  ptrecube  38452  nfe2  43181  nfa1w  43619  nfrelp  45870  nfdfat  48113  nfich1  48445  nfich2  48446  ichnfimlem  48461  ich2ex  48466  nfals  50815  nfrals  50816  nfalseu  50846  nfralseu  50847