Theorem nfxfr 1851

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1781

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

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

This theorem is referenced by:  nfnan  1899  nf3an  1900  nfor  1903  nf3or  1904  nfa1  2152  nfnf1  2155  nfs1v  2157  nfa2  2177  nfan1  2201  nfs1f  2276  nfex  2328  nfnf  2330  nfsbvOLD  2335  nfmo1  2560  nfeu1  2591  nfeu1ALT  2592  nfsab1  2725  nfnfc1  2911  nfaba1  2916  nfnfc  2921  nfabdwOLD  2933  nfne  3049  nfnel  3060  nfra1  3290  nfre1  3291  nfra2w  3305  nfra2wOLD  3306  r19.12  3320  r19.12OLD  3321  nfrmo1  3419  nfreu1  3420  nfrmow  3421  nfreuw  3422  nfrmowOLD  3434  nfrmo  3441  nfss  4001  nfdif  4152  nfun  4193  nfin  4245  nfiu1  5050  nfdisjw  5145  nfdisj  5146  nfdisj1  5147  nfpo  5613  nfso  5614  nffr  5673  nfse  5674  nfwe  5675  nfrel  5803  sb8iota  6537  nffun  6601  nffn  6678  nff  6743  nff1  6815  nffo  6833  nff1o  6860  nfiso  7358  tz7.49  8501  nfixpw  8974  nfixp  8975  bnj919  34743  bnj1379  34806  bnj571  34882  bnj607  34892  bnj873  34900  bnj981  34926  bnj1039  34947  bnj1128  34966  bnj1388  35009  bnj1398  35010  bnj1417  35017  bnj1444  35019  bnj1445  35020  bnj1446  35021  bnj1449  35024  bnj1467  35030  bnj1489  35032  bnj1312  35034  bnj1518  35040  bnj1525  35045  wl-nfae1  37481  wl-ax11-lem4  37542  ptrecube  37580  nfa1w  42630  nfdfat  47042  nfich1  47321  nfich2  47322  ichnfimlem  47337  ich2ex  47342