Theorem nfxfr 1855

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1902  nf3an  1903  nfor  1906  nf3or  1907  nfa1  2157  nfnf1  2160  nfs1v  2162  nfa2  2182  nfan1  2208  nfs1f  2282  nfex  2329  nfnf  2331  nfmo1  2557  nfeu1ALT  2588  nfeu1  2589  nfsab1  2722  nfnfc1  2901  nfaba1  2906  nfnfc  2911  nfne  3033  nfnel  3044  nfra1  3261  nfre1  3262  nfra2w  3273  r19.12  3286  nfrmo1  3369  nfreu1  3370  nfrmow  3371  nfreuw  3372  nfrmo  3387  nfss  3914  nfdif  4069  nfun  4110  nfin  4164  nfiu1  4969  nfdisjw  5064  nfdisj  5065  nfdisj1  5066  nfpo  5545  nfso  5546  nffr  5604  nfse  5605  nfwe  5606  nfrel  5736  sb8iota  6465  nffun  6521  nffn  6597  nff  6664  nff1  6734  nffo  6751  nff1o  6778  nfiso  7277  tz7.49  8384  nfixpw  8864  nfixp  8865  bnj919  34910  bnj1379  34972  bnj571  35048  bnj607  35058  bnj873  35066  bnj981  35092  bnj1039  35113  bnj1128  35132  bnj1388  35175  bnj1398  35176  bnj1417  35183  bnj1444  35185  bnj1445  35186  bnj1446  35187  bnj1449  35190  bnj1467  35196  bnj1489  35198  bnj1312  35200  bnj1518  35206  bnj1525  35211  wl-nfae1  37852  ptrecube  37941  nfe2  42654  nfa1w  43108  nfrelp  45376  nfdfat  47575  nfich1  47907  nfich2  47908  ichnfimlem  47923  ich2ex  47928