Theorem nfxfr 1853

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  nfor  1904  nf3or  1905  nfa1  2151  nfnf1  2154  nfs1v  2156  nfa2  2176  nfan1  2200  nfs1f  2275  nfex  2324  nfnf  2326  nfmo1  2556  nfeu1  2587  nfeu1ALT  2588  nfsab1  2721  nfnfc1  2901  nfaba1  2906  nfnfc  2911  nfne  3033  nfnel  3044  nfra1  3266  nfre1  3267  nfra2w  3280  r19.12  3294  nfrmo1  3390  nfreu1  3391  nfrmow  3392  nfreuw  3393  nfrmowOLD  3406  nfrmo  3413  nfss  3951  nfdif  4104  nfun  4145  nfin  4199  nfiu1  5003  nfdisjw  5098  nfdisj  5099  nfdisj1  5100  nfpo  5567  nfso  5568  nffr  5627  nfse  5628  nfwe  5629  nfrel  5758  sb8iota  6495  nffun  6559  nffn  6637  nff  6702  nff1  6772  nffo  6789  nff1o  6816  nfiso  7315  tz7.49  8459  nfixpw  8930  nfixp  8931  bnj919  34798  bnj1379  34861  bnj571  34937  bnj607  34947  bnj873  34955  bnj981  34981  bnj1039  35002  bnj1128  35021  bnj1388  35064  bnj1398  35065  bnj1417  35072  bnj1444  35074  bnj1445  35075  bnj1446  35076  bnj1449  35079  bnj1467  35085  bnj1489  35087  bnj1312  35089  bnj1518  35095  bnj1525  35100  wl-nfae1  37545  wl-ax11-lem4  37606  ptrecube  37644  nfa1w  42698  nfrelp  44974  nfdfat  47156  nfich1  47461  nfich2  47462  ichnfimlem  47477  ich2ex  47482