Theorem nfxfr 1876

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

Syntax hints:   ↔ wb 209  Ⅎwnf 1806

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

This theorem depends on definitions:  df-bi 210  df-ex 1803  df-nf 1807

This theorem is referenced by:  nfnan  1923  nf3an  1924  nfor  1927  nf3or  1928  nfa1  2188  nfnf1  2191  nfs1v  2193  nfa2  2212  nfan1  2238  nfs1f  2312  nfex  2359  nfnf  2361  nfmo1  2587  nfeu1ALT  2618  nfeu1  2619  nfsab1  2751  nfnfc1  2930  nfaba1  2935  nfnfc  2939  nfne  3061  nfnel  3072  nfra1  3289  nfre1  3290  nfra2w  3301  r19.12  3314  nfrmo1  3397  nfreu1  3398  nfrmow  3399  nfreuw  3400  nfrmo  3415  nfss  3932  nfdif  4086  nfun  4126  nfin  4179  nfiu1  4987  nfdisjw  5083  nfdisj  5084  nfdisj1  5085  nfpo  5565  nfso  5566  nffr  5624  nfse  5625  nfwe  5626  nfrel  5756  sb8iota  6492  nffun  6548  nffn  6624  nff  6691  nff1  6762  nffo  6781  nff1o  6808  nfiso  7310  tz7.49  8420  nfixpw  8902  nfixp  8903  bnj919  35068  bnj1379  35130  bnj571  35206  bnj607  35216  bnj873  35224  bnj981  35250  bnj1039  35271  bnj1128  35290  bnj1388  35333  bnj1398  35334  bnj1417  35341  bnj1444  35343  bnj1445  35344  bnj1446  35345  bnj1449  35348  bnj1467  35354  bnj1489  35356  bnj1312  35358  bnj1518  35364  bnj1525  35369  wl-nfae1  38037  ptrecube  38126  nfe2  42839  nfa1w  43264  nfrelp  45517  nfdfat  47720  nfich1  48052  nfich2  48053  ichnfimlem  48068  ich2ex  48073