Theorem nfxfr 1886

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

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

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

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

This theorem is used by:  nfnan  1935  nf3an  1936  nfor  1939  nf3or  1940  nfa1  2191  nfnf1  2194  nfs1v  2196  nfa2  2213  nfan1  2240  nfs1f  2312  nfex  2358  nfnf  2360  nfmo1  2585  nfeu1ALT  2616  nfeu1  2617  nfsab1  2749  nfnfc1  2929  nfaba1  2934  nfnfc  2938  nfne  3062  nfnel  3073  nfra1  3290  nfre1  3291  nfra2w  3302  r19.12  3315  nfrmo1  3396  nfreu1  3397  nfrmow  3398  nfreuw  3399  nfrmo  3414  nfss  3906  nfdif  4069  nfin  4124  nfun  4172  nfiu1  4989  nfdisjw  5085  nfdisj  5086  nfdisj1  5087  nfpo  5569  nfso  5570  nffr  5628  nfse  5629  nfwe  5630  nfrel  5761  sb8iota  6520  nffun  6579  nffn  6657  nff  6724  nff1  6795  nffo  6814  nff1o  6841  nfiso  7350  tz7.49  8480  nfixpw  8969  nfixp  8970  bnj919  35465  bnj1379  35527  bnj571  35603  bnj607  35613  bnj873  35621  bnj981  35647  bnj1039  35668  bnj1128  35687  bnj1388  35730  bnj1398  35731  bnj1417  35738  bnj1444  35740  bnj1445  35741  bnj1446  35742  bnj1449  35745  bnj1467  35751  bnj1489  35753  bnj1312  35755  bnj1518  35761  bnj1525  35766  wl-nfae1  38650  ptrecube  38729  nfe2  43458  nfa1w  43877  nfrelp  46132  nfdfat  48400  nfich1  48732  nfich2  48733  ichnfimlem  48748  ich2ex  48753  nfals  51177  nfrals  51178  nfalseu  51208  nfralseu  51209