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  3379  nfreu1  3380  nfrmow  3381  nfreuw  3382  nfrmo  3399  nfss  3928  nfdif  4083  nfun  4124  nfin  4178  nfiu1  4984  nfdisjw  5079  nfdisj  5080  nfdisj1  5081  nfpo  5548  nfso  5549  nffr  5607  nfse  5608  nfwe  5609  nfrel  5739  sb8iota  6469  nffun  6525  nffn  6601  nff  6668  nff1  6738  nffo  6755  nff1o  6782  nfiso  7280  tz7.49  8388  nfixpw  8868  nfixp  8869  bnj919  34950  bnj1379  35012  bnj571  35088  bnj607  35098  bnj873  35106  bnj981  35132  bnj1039  35153  bnj1128  35172  bnj1388  35215  bnj1398  35216  bnj1417  35223  bnj1444  35225  bnj1445  35226  bnj1446  35227  bnj1449  35230  bnj1467  35236  bnj1489  35238  bnj1312  35240  bnj1518  35246  bnj1525  35251  wl-nfae1  37811  ptrecube  37900  nfe2  42614  nfa1w  43062  nfrelp  45334  nfdfat  47516  nfich1  47836  nfich2  47837  ichnfimlem  47852  ich2ex  47857