Theorem nfxfr 1522

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

Syntax hints:   ↔ wb 105  Ⅎwnf 1508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497

This theorem depends on definitions:  df-bi 117  df-nf 1509

This theorem is referenced by:  nfnf1  1592  nf3an  1614  nfnf  1625  nfdc  1707  nfs1f  1828  nfsbv  2000  nfeu1  2090  nfmo1  2091  sb8eu  2092  nfeu  2098  nfnfc1  2377  nfnfc  2381  nfeq  2382  nfel  2383  nfabdw  2393  nfne  2495  nfnel  2504  nfra1  2563  nfre1  2575  nfreu1  2705  nfrmo1  2706  nfss  3220  rabn0m  3522  nfdisjv  4076  nfdisj1  4077  nfpo  4398  nfso  4399  nfse  4438  nffrfor  4445  nffr  4446  nfwe  4452  nfrel  4811  sb8iota  5294  nffun  5349  nffn  5426  nff  5479  nff1  5540  nffo  5558  nff1o  5581  nfiso  5946  nfixpxy  6885