Theorem nfxfr 1849

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

Syntax hints:   ↔ wb 208  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfnan  1897  nf3an  1898  nfor  1901  nf3or  1902  nfa1  2151  nfnf1  2154  nfs1v  2156  nfa2  2172  nfan1  2196  nfs1f  2271  nfex  2339  nfnf  2341  nfsbv  2345  nfsbvOLD  2346  nfmo1  2637  nfeu1  2670  nfeu1ALT  2671  nfsab1  2808  nfnfc1  2980  nfnfc  2990  nfabdw  3000  nfne  3119  nfnel  3130  nfra1  3219  nfre1  3306  r19.12  3324  nfreu1  3370  nfrmo1  3371  nfrmow  3375  nfrmo  3377  nfss  3959  nfdisjw  5035  nfdisj  5036  nfdisj1  5037  nfpo  5473  nfso  5474  nffr  5523  nfse  5524  nfwe  5525  nfrel  5648  sb8iota  6319  nffun  6372  nffn  6446  nff  6504  nff1  6567  nffo  6583  nff1o  6607  nfiso  7069  tz7.49  8075  nfixpw  8474  nfixp  8475  bnj919  32033  bnj1379  32097  bnj571  32173  bnj607  32183  bnj873  32191  bnj981  32217  bnj1039  32238  bnj1128  32257  bnj1388  32300  bnj1398  32301  bnj1417  32308  bnj1444  32310  bnj1445  32311  bnj1446  32312  bnj1449  32315  bnj1467  32321  bnj1489  32323  bnj1312  32325  bnj1518  32331  bnj1525  32336  wl-nfae1  34761  wl-ax11-lem4  34814  ptrecube  34886  nfdfat  43320  nfich1  43601  nfich2  43602  ich2ex  43623