Theorem nfxfr 1853

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

Syntax hints:   ↔ wb 206  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nf3an  1901  nfor  1904  nf3or  1905  nfa1  2151  nfnf1  2154  nfs1v  2156  nfa2  2176  nfan1  2200  nfs1f  2275  nfex  2324  nfnf  2326  nfsbvOLD  2331  nfmo1  2557  nfeu1  2588  nfeu1ALT  2589  nfsab1  2722  nfnfc1  2908  nfaba1  2913  nfnfc  2918  nfne  3043  nfnel  3054  nfra1  3284  nfre1  3285  nfra2w  3299  nfra2wOLD  3300  r19.12  3314  r19.12OLD  3315  nfrmo1  3411  nfreu1  3412  nfrmow  3413  nfreuw  3414  nfrmowOLD  3427  nfrmo  3434  nfss  3976  nfdif  4129  nfun  4170  nfin  4224  nfiu1  5027  nfdisjw  5122  nfdisj  5123  nfdisj1  5124  nfpo  5598  nfso  5599  nffr  5658  nfse  5659  nfwe  5660  nfrel  5789  sb8iota  6525  nffun  6589  nffn  6667  nff  6732  nff1  6802  nffo  6819  nff1o  6846  nfiso  7342  tz7.49  8485  nfixpw  8956  nfixp  8957  bnj919  34781  bnj1379  34844  bnj571  34920  bnj607  34930  bnj873  34938  bnj981  34964  bnj1039  34985  bnj1128  35004  bnj1388  35047  bnj1398  35048  bnj1417  35055  bnj1444  35057  bnj1445  35058  bnj1446  35059  bnj1449  35062  bnj1467  35068  bnj1489  35070  bnj1312  35072  bnj1518  35078  bnj1525  35083  wl-nfae1  37528  wl-ax11-lem4  37589  ptrecube  37627  nfa1w  42685  nfrelp  44970  nfdfat  47139  nfich1  47434  nfich2  47435  ichnfimlem  47450  ich2ex  47455