Theorem nfxfr 1880

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

Syntax hints:   ↔ wb 209  Ⅎwnf 1810

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

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

This theorem is referenced by:  nfnan  1927  nf3an  1928  nfor  1931  nf3or  1932  nfa1  2192  nfnf1  2195  nfs1v  2197  nfa2  2216  nfan1  2242  nfs1f  2316  nfex  2363  nfnf  2365  nfmo1  2591  nfeu1ALT  2622  nfeu1  2623  nfsab1  2755  nfnfc1  2934  nfaba1  2939  nfnfc  2943  nfne  3067  nfnel  3078  nfra1  3295  nfre1  3296  nfra2w  3307  r19.12  3320  nfrmo1  3402  nfreu1  3403  nfrmow  3404  nfreuw  3405  nfrmo  3420  nfss  3936  nfdif  4090  nfun  4130  nfin  4183  nfiu1  4994  nfdisjw  5090  nfdisj  5091  nfdisj1  5092  nfpo  5576  nfso  5577  nffr  5635  nfse  5636  nfwe  5637  nfrel  5767  sb8iota  6504  nffun  6560  nffn  6635  nff  6702  nff1  6773  nffo  6792  nff1o  6819  nfiso  7321  tz7.49  8432  nfixpw  8914  nfixp  8915  bnj919  35101  bnj1379  35163  bnj571  35239  bnj607  35249  bnj873  35257  bnj981  35283  bnj1039  35304  bnj1128  35323  bnj1388  35366  bnj1398  35367  bnj1417  35374  bnj1444  35376  bnj1445  35377  bnj1446  35378  bnj1449  35381  bnj1467  35387  bnj1489  35389  bnj1312  35391  bnj1518  35397  bnj1525  35402  wl-nfae1  38105  ptrecube  38194  nfe2  42909  nfa1w  43334  nfrelp  45585  nfdfat  47788  nfich1  48120  nfich2  48121  ichnfimlem  48136  ich2ex  48141  nfals  50501  nfrals  50502