Theorem nfxfr 1488

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

Syntax hints:   ↔ wb 105  Ⅎwnf 1474

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 1461  ax-gen 1463

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

This theorem is referenced by:  nfnf1  1558  nf3an  1580  nfnf  1591  nfdc  1673  nfs1f  1794  nfsbv  1966  nfeu1  2056  nfmo1  2057  sb8eu  2058  nfeu  2064  nfnfc1  2342  nfnfc  2346  nfeq  2347  nfel  2348  nfabdw  2358  nfne  2460  nfnel  2469  nfra1  2528  nfre1  2540  nfreu1  2669  nfrmo1  2670  nfss  3177  rabn0m  3479  nfdisjv  4023  nfdisj1  4024  nfpo  4337  nfso  4338  nfse  4377  nffrfor  4384  nffr  4385  nfwe  4391  nfrel  4749  sb8iota  5227  nffun  5282  nffn  5355  nff  5407  nff1  5464  nffo  5482  nff1o  5505  nfiso  5856  nfixpxy  6785