Theorem nfxfr 1861

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

Syntax hints:   ↔ wb 208  Ⅎwnf 1791

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

This theorem depends on definitions:  df-bi 209  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfnan  1908  nf3an  1909  nfor  1912  nf3or  1913  nfa1  2164  nfnf1  2167  nfs1v  2169  nfa2  2188  nfan1  2214  nfs1f  2288  nfex  2335  nfnf  2337  nfmo1  2563  nfeu1ALT  2594  nfeu1  2595  nfsab1  2727  nfnfc1  2906  nfaba1  2911  nfnfc  2915  nfne  3037  nfnel  3048  nfra1  3265  nfre1  3266  nfra2w  3277  r19.12  3290  nfrmo1  3373  nfreu1  3374  nfrmow  3375  nfreuw  3376  nfrmo  3391  nfss  3910  nfdif  4063  nfun  4103  nfin  4156  nfiu1  4960  nfdisjw  5054  nfdisj  5055  nfdisj1  5056  nfpo  5535  nfso  5536  nffr  5594  nfse  5595  nfwe  5596  nfrel  5726  sb8iota  6456  nffun  6512  nffn  6588  nff  6655  nff1  6725  nffo  6742  nff1o  6769  nfiso  7270  tz7.49  8378  nfixpw  8858  nfixp  8859  bnj919  34965  bnj1379  35027  bnj571  35103  bnj607  35113  bnj873  35121  bnj981  35147  bnj1039  35168  bnj1128  35187  bnj1388  35230  bnj1398  35231  bnj1417  35238  bnj1444  35240  bnj1445  35241  bnj1446  35242  bnj1449  35245  bnj1467  35251  bnj1489  35253  bnj1312  35255  bnj1518  35261  bnj1525  35266  wl-nfae1  37913  ptrecube  38002  nfe2  42715  nfa1w  43140  nfrelp  45408  nfdfat  47604  nfich1  47936  nfich2  47937  ichnfimlem  47952  ich2ex  47957