Theorem nfxfr 1853

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  nfor  1904  nf3or  1905  nfa1  2152  nfnf1  2155  nfs1v  2157  nfa2  2177  nfan1  2201  nfs1f  2275  nfex  2323  nfnf  2325  nfmo1  2551  nfeu1  2582  nfeu1ALT  2583  nfsab1  2716  nfnfc1  2895  nfaba1  2900  nfnfc  2905  nfne  3027  nfnel  3038  nfra1  3262  nfre1  3263  nfra2w  3276  r19.12  3290  nfrmo1  3385  nfreu1  3386  nfrmow  3387  nfreuw  3388  nfrmo  3406  nfss  3942  nfdif  4095  nfun  4136  nfin  4190  nfiu1  4994  nfdisjw  5089  nfdisj  5090  nfdisj1  5091  nfpo  5555  nfso  5556  nffr  5614  nfse  5615  nfwe  5616  nfrel  5745  sb8iota  6478  nffun  6542  nffn  6620  nff  6687  nff1  6757  nffo  6774  nff1o  6801  nfiso  7300  tz7.49  8416  nfixpw  8892  nfixp  8893  bnj919  34764  bnj1379  34827  bnj571  34903  bnj607  34913  bnj873  34921  bnj981  34947  bnj1039  34968  bnj1128  34987  bnj1388  35030  bnj1398  35031  bnj1417  35038  bnj1444  35040  bnj1445  35041  bnj1446  35042  bnj1449  35045  bnj1467  35051  bnj1489  35053  bnj1312  35055  bnj1518  35061  bnj1525  35066  wl-nfae1  37522  wl-ax11-lem4  37583  ptrecube  37621  nfa1w  42670  nfrelp  44946  nfdfat  47132  nfich1  47452  nfich2  47453  ichnfimlem  47468  ich2ex  47473