Theorem nfxfr 1854

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnan  1901  nf3an  1902  nfor  1905  nf3or  1906  nfa1  2154  nfnf1  2157  nfs1v  2159  nfa2  2179  nfan1  2203  nfs1f  2277  nfex  2325  nfnf  2327  nfmo1  2552  nfeu1  2583  nfeu1ALT  2584  nfsab1  2717  nfnfc1  2897  nfaba1  2902  nfnfc  2907  nfne  3029  nfnel  3040  nfra1  3256  nfre1  3257  nfra2w  3268  r19.12  3281  nfrmo1  3373  nfreu1  3374  nfrmow  3375  nfreuw  3376  nfrmo  3393  nfss  3922  nfdif  4076  nfun  4117  nfin  4171  nfiu1  4975  nfdisjw  5068  nfdisj  5069  nfdisj1  5070  nfpo  5528  nfso  5529  nffr  5587  nfse  5588  nfwe  5589  nfrel  5719  sb8iota  6448  nffun  6504  nffn  6580  nff  6647  nff1  6717  nffo  6734  nff1o  6761  nfiso  7256  tz7.49  8364  nfixpw  8840  nfixp  8841  bnj919  34779  bnj1379  34842  bnj571  34918  bnj607  34928  bnj873  34936  bnj981  34962  bnj1039  34983  bnj1128  35002  bnj1388  35045  bnj1398  35046  bnj1417  35053  bnj1444  35055  bnj1445  35056  bnj1446  35057  bnj1449  35060  bnj1467  35066  bnj1489  35068  bnj1312  35070  bnj1518  35076  bnj1525  35081  wl-nfae1  37571  ptrecube  37659  nfa1w  42767  nfrelp  45041  nfdfat  47226  nfich1  47546  nfich2  47547  ichnfimlem  47562  ich2ex  47567