Theorem nfxfr 1882

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

This proof depends on syntax axioms:   ↔ wb 209  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-ex 1809  df-nf 1813

This theorem is used by:  nfnan  1929  nf3an  1930  nfor  1933  nf3or  1934  nfa1  2185  nfnf1  2188  nfs1v  2190  nfa2  2209  nfan1  2235  nfs1f  2309  nfex  2356  nfnf  2358  nfmo1  2584  nfeu1ALT  2615  nfeu1  2616  nfsab1  2748  nfnfc1  2927  nfaba1  2932  nfnfc  2936  nfne  3060  nfnel  3071  nfra1  3288  nfre1  3289  nfra2w  3300  r19.12  3313  nfrmo1  3395  nfreu1  3396  nfrmow  3397  nfreuw  3398  nfrmo  3413  nfss  3929  nfdif  4083  nfun  4123  nfin  4176  nfiu1  4991  nfdisjw  5087  nfdisj  5088  nfdisj1  5089  nfpo  5574  nfso  5575  nffr  5633  nfse  5634  nfwe  5635  nfrel  5765  sb8iota  6503  nffun  6559  nffn  6634  nff  6701  nff1  6772  nffo  6791  nff1o  6818  nfiso  7320  tz7.49  8430  nfixpw  8912  nfixp  8913  bnj919  35165  bnj1379  35227  bnj571  35303  bnj607  35313  bnj873  35321  bnj981  35347  bnj1039  35368  bnj1128  35387  bnj1388  35430  bnj1398  35431  bnj1417  35438  bnj1444  35440  bnj1445  35441  bnj1446  35442  bnj1449  35445  bnj1467  35451  bnj1489  35453  bnj1312  35455  bnj1518  35461  bnj1525  35466  wl-nfae1  38210  ptrecube  38299  nfe2  43012  nfa1w  43435  nfrelp  45686  nfdfat  47892  nfich1  48224  nfich2  48225  ichnfimlem  48240  ich2ex  48245  nfals  50609  nfrals  50610  nfalseu  50640  nfralseu  50641