Theorem nfxfr 1461

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

Syntax hints:   ↔ wb 104  Ⅎwnf 1447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436

This theorem depends on definitions:  df-bi 116  df-nf 1448

This theorem is referenced by:  nfnf1  1531  nf3an  1553  nfnf  1564  nfdc  1646  nfs1f  1767  nfsbv  1934  nfeu1  2024  nfmo1  2025  sb8eu  2026  nfeu  2032  nfnfc1  2309  nfnfc  2313  nfeq  2314  nfel  2315  nfabdw  2325  nfne  2427  nfnel  2436  nfra1  2495  nfre1  2507  nfreu1  2635  nfrmo1  2636  nfss  3130  rabn0m  3431  nfdisjv  3965  nfdisj1  3966  nfpo  4273  nfso  4274  nfse  4313  nffrfor  4320  nffr  4321  nfwe  4327  nfrel  4683  sb8iota  5154  nffun  5205  nffn  5278  nff  5328  nff1  5385  nffo  5403  nff1o  5424  nfiso  5768  nfixpxy  6674