Theorem nfxfr 1856

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

Syntax hints:   ↔ wb 205  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfnan  1904  nf3an  1905  nfor  1908  nf3or  1909  nfa1  2150  nfnf1  2153  nfs1v  2155  nfa2  2172  nfan1  2196  nfs1f  2270  nfex  2322  nfnf  2324  nfsbvOLD  2329  nfmo1  2557  nfeu1  2588  nfeu1ALT  2589  nfsab1  2723  nfnfc1  2909  nfnfc  2918  nfabdwOLD  2930  nfne  3044  nfnel  3055  nfra1  3142  nfra2w  3151  nfra2wOLD  3152  nfre1  3234  r19.12  3252  r19.12OLD  3253  nfreu1  3296  nfrmo1  3297  nfrmow  3301  nfrmo  3303  nfss  3909  nfdisjw  5047  nfdisj  5048  nfdisj1  5049  nfpo  5499  nfso  5500  nffr  5554  nfse  5555  nfwe  5556  nfrel  5680  sb8iota  6388  nffun  6441  nffn  6516  nff  6580  nff1  6652  nffo  6671  nff1o  6698  nfiso  7173  tz7.49  8246  nfixpw  8662  nfixp  8663  bnj919  32647  bnj1379  32710  bnj571  32786  bnj607  32796  bnj873  32804  bnj981  32830  bnj1039  32851  bnj1128  32870  bnj1388  32913  bnj1398  32914  bnj1417  32921  bnj1444  32923  bnj1445  32924  bnj1446  32925  bnj1449  32928  bnj1467  32934  bnj1489  32936  bnj1312  32938  bnj1518  32944  bnj1525  32949  wl-nfae1  35613  wl-ax11-lem4  35666  ptrecube  35704  nfdfat  44506  nfich1  44787  nfich2  44788  ichnfimlem  44803  ich2ex  44808