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  2330  nfnf  2332  nfmo1  2558  nfeu1ALT  2589  nfeu1  2590  nfsab1  2723  nfnfc1  2902  nfaba1  2907  nfnfc  2912  nfne  3034  nfnel  3045  nfra1  3262  nfre1  3263  nfra2w  3274  r19.12  3287  nfrmo1  3370  nfreu1  3371  nfrmow  3372  nfreuw  3373  nfrmo  3388  nfss  3915  nfdif  4070  nfun  4111  nfin  4165  nfiu1  4970  nfdisjw  5065  nfdisj  5066  nfdisj1  5067  nfpo  5540  nfso  5541  nffr  5599  nfse  5600  nfwe  5601  nfrel  5731  sb8iota  6461  nffun  6517  nffn  6593  nff  6660  nff1  6730  nffo  6747  nff1o  6774  nfiso  7272  tz7.49  8379  nfixpw  8859  nfixp  8860  bnj919  34930  bnj1379  34992  bnj571  35068  bnj607  35078  bnj873  35086  bnj981  35112  bnj1039  35133  bnj1128  35152  bnj1388  35195  bnj1398  35196  bnj1417  35203  bnj1444  35205  bnj1445  35206  bnj1446  35207  bnj1449  35210  bnj1467  35216  bnj1489  35218  bnj1312  35220  bnj1518  35226  bnj1525  35231  wl-nfae1  37872  ptrecube  37961  nfe2  42674  nfa1w  43128  nfrelp  45400  nfdfat  47593  nfich1  47925  nfich2  47926  ichnfimlem  47941  ich2ex  47946