Theorem nfxfr 1885

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

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

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

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816

This theorem is used by:  nfnan  1932  nf3an  1933  nfor  1936  nf3or  1937  nfa1  2187  nfnf1  2190  nfs1v  2192  nfa2  2209  nfan1  2236  nfs1f  2308  nfex  2354  nfnf  2356  nfmo1  2582  nfeu1ALT  2613  nfeu1  2614  nfsab1  2746  nfnfc1  2925  nfaba1  2930  nfnfc  2934  nfne  3058  nfnel  3069  nfra1  3286  nfre1  3287  nfra2w  3298  r19.12  3311  nfrmo1  3392  nfreu1  3393  nfrmow  3394  nfreuw  3395  nfrmo  3410  nfss  3901  nfdif  4066  nfin  4121  nfun  4169  nfiu1  4985  nfdisjw  5081  nfdisj  5082  nfdisj1  5083  nfpo  5564  nfso  5565  nffr  5623  nfse  5624  nfwe  5625  nfrel  5755  sb8iota  6505  nffun  6562  nffn  6638  nff  6705  nff1  6776  nffo  6795  nff1o  6822  nfiso  7330  tz7.49  8455  nfixpw  8944  nfixp  8945  bnj919  35398  bnj1379  35460  bnj571  35536  bnj607  35546  bnj873  35554  bnj981  35580  bnj1039  35601  bnj1128  35620  bnj1388  35663  bnj1398  35664  bnj1417  35671  bnj1444  35673  bnj1445  35674  bnj1446  35675  bnj1449  35678  bnj1467  35684  bnj1489  35686  bnj1312  35688  bnj1518  35694  bnj1525  35699  wl-nfae1  38460  ptrecube  38539  nfe2  43268  nfa1w  43687  nfrelp  45939  nfdfat  48197  nfich1  48529  nfich2  48530  ichnfimlem  48545  ich2ex  48550  nfals  50899  nfrals  50900  nfalseu  50930  nfralseu  50931