Theorem nfxfr 1497

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

Syntax hints:   ↔ wb 105  Ⅎwnf 1483

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 1470  ax-gen 1472

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

This theorem is referenced by:  nfnf1  1567  nf3an  1589  nfnf  1600  nfdc  1682  nfs1f  1803  nfsbv  1975  nfeu1  2065  nfmo1  2066  sb8eu  2067  nfeu  2073  nfnfc1  2351  nfnfc  2355  nfeq  2356  nfel  2357  nfabdw  2367  nfne  2469  nfnel  2478  nfra1  2537  nfre1  2549  nfreu1  2678  nfrmo1  2679  nfss  3186  rabn0m  3488  nfdisjv  4033  nfdisj1  4034  nfpo  4348  nfso  4349  nfse  4388  nffrfor  4395  nffr  4396  nfwe  4402  nfrel  4760  sb8iota  5239  nffun  5294  nffn  5370  nff  5422  nff1  5479  nffo  5497  nff1o  5520  nfiso  5875  nfixpxy  6804