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 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfnan  1904  nf3an  1905  nfor  1908  nf3or  1909  nfa1  2149  nfnf1  2152  nfs1v  2154  nfa2  2171  nfan1  2194  nfs1f  2268  nfex  2319  nfnf  2321  nfsbvOLD  2326  nfmo1  2558  nfeu1  2589  nfeu1ALT  2590  nfsab1  2724  nfnfc1  2911  nfnfc  2920  nfabdwOLD  2932  nfne  3046  nfnel  3057  nfra1  3145  nfra2w  3155  nfra2wOLD  3156  nfre1  3240  r19.12  3258  r19.12OLD  3259  nfreu1  3301  nfrmo1  3302  nfrmow  3305  nfreuw  3306  nfrmowOLD  3308  nfrmo  3310  nfss  3914  nfdisjw  5052  nfdisj  5053  nfdisj1  5054  nfpo  5509  nfso  5510  nffr  5564  nfse  5565  nfwe  5566  nfrel  5691  sb8iota  6407  nffun  6464  nffn  6541  nff  6605  nff1  6677  nffo  6696  nff1o  6723  nfiso  7202  tz7.49  8285  nfixpw  8713  nfixp  8714  bnj919  32756  bnj1379  32819  bnj571  32895  bnj607  32905  bnj873  32913  bnj981  32939  bnj1039  32960  bnj1128  32979  bnj1388  33022  bnj1398  33023  bnj1417  33030  bnj1444  33032  bnj1445  33033  bnj1446  33034  bnj1449  33037  bnj1467  33043  bnj1489  33045  bnj1312  33047  bnj1518  33053  bnj1525  33058  wl-nfae1  35695  wl-ax11-lem4  35748  ptrecube  35786  nfdfat  44630  nfich1  44910  nfich2  44911  ichnfimlem  44926  ich2ex  44931