Theorem nfxfr 1779

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

Syntax hints:   ↔ wb 196  Ⅎwnf 1708

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

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfanOLD  1829  nfnan  1830  nf3an  1831  nfor  1834  nf3or  1835  nfa1  2028  nfnf1  2031  nfa2  2040  nfan1  2068  nfex  2154  nfnf  2158  nfnf1OLD  2159  nfs1f  2383  nfeu1  2480  nfmo1  2481  nfnfc1  2767  nfnfc  2774  nfnfcALT  2775  nfne  2894  nfnel  2904  nfra1  2941  nfre1  3005  nfreu1  3110  nfrmo1  3111  nfrmo  3115  nfss  3596  nfdisj  4632  nfdisj1  4633  nfpo  5040  nfso  5041  nffr  5088  nfse  5089  nfwe  5090  nfrel  5204  sb8iota  5858  nffun  5911  nffn  5987  nff  6041  nff1  6099  nffo  6114  nff1o  6135  nfiso  6572  tz7.49  7540  nfixp  7927  bnj919  30837  bnj1379  30901  bnj571  30976  bnj607  30986  bnj873  30994  bnj981  31020  bnj1039  31039  bnj1128  31058  bnj1388  31101  bnj1398  31102  bnj1417  31109  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1449  31116  bnj1467  31122  bnj1489  31124  bnj1312  31126  bnj1518  31132  bnj1525  31137  bj-nfnfc  32853  wl-nfae1  33315  wl-ax11-lem4  33365  ptrecube  33409  nfdfat  41210