Theorem nfxfr 1819

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

Syntax hints:   ↔ wb 196  Ⅎwnf 1748

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

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750

This theorem is referenced by:  nfanOLD  1869  nfnan  1870  nf3an  1871  nfor  1874  nf3or  1875  nfa1  2068  nfnf1  2071  nfa2  2080  nfan1  2106  nfex  2192  nfnf  2196  nfnf1OLD  2197  nfs1f  2411  nfeu1  2508  nfmo1  2509  nfnfc1  2796  nfnfc  2803  nfnfcALT  2804  nfne  2923  nfnel  2933  nfra1  2970  nfre1  3034  nfreu1  3139  nfrmo1  3140  nfrmo  3144  nfss  3629  nfdisj  4664  nfdisj1  4665  nfpo  5069  nfso  5070  nffr  5117  nfse  5118  nfwe  5119  nfrel  5238  sb8iota  5896  nffun  5949  nffn  6025  nff  6079  nff1  6137  nffo  6152  nff1o  6173  nfiso  6612  tz7.49  7585  nfixp  7969  bnj919  30963  bnj1379  31027  bnj571  31102  bnj607  31112  bnj873  31120  bnj981  31146  bnj1039  31165  bnj1128  31184  bnj1388  31227  bnj1398  31228  bnj1417  31235  bnj1444  31237  bnj1445  31238  bnj1446  31239  bnj1449  31242  bnj1467  31248  bnj1489  31250  bnj1312  31252  bnj1518  31258  bnj1525  31263  bj-nfnfc  32978  wl-nfae1  33445  wl-ax11-lem4  33495  ptrecube  33539  nfdfat  41531