Theorem nfxfr 1835

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

Syntax hints:   ↔ wb 207  Ⅎwnf 1766

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

This theorem depends on definitions:  df-bi 208  df-ex 1763  df-nf 1767

This theorem is referenced by:  nfnan  1883  nf3an  1884  nfor  1887  nf3or  1888  nfa1  2120  nfnf1  2123  nfa2  2139  nfan1  2164  nfs1v  2236  nfs1f  2238  nfex  2305  nfnf  2307  nfsbv  2311  nfsbvOLD  2312  2sb8evOLD  2331  nfmo1  2596  nfeu1  2634  nfeu1ALT  2635  nfsab1  2783  nfnfc1  2951  nfnfc  2958  nfne  3086  nfnel  3096  nfra1  3185  nfre1  3268  r19.12  3284  nfreu1  3330  nfrmo1  3331  nfrmo  3335  nfss  3884  nfdisj  4944  nfdisj1  4945  nfpo  5370  nfso  5371  nffr  5420  nfse  5421  nfwe  5422  nfrel  5543  sb8iota  6199  nffun  6251  nffn  6325  nff  6381  nff1  6444  nffo  6460  nff1o  6484  nfiso  6941  tz7.49  7935  nfixp  8332  bnj919  31647  bnj1379  31711  bnj571  31786  bnj607  31796  bnj873  31804  bnj981  31830  bnj1039  31849  bnj1128  31868  bnj1388  31911  bnj1398  31912  bnj1417  31919  bnj1444  31921  bnj1445  31922  bnj1446  31923  bnj1449  31926  bnj1467  31932  bnj1489  31934  bnj1312  31936  bnj1518  31942  bnj1525  31947  wl-nfae1  34313  wl-ax11-lem4  34364  ptrecube  34436  nfdfat  42856  nfich1  43103  nfich2  43104  ich2ex  43125