Theorem nfxfr 1527

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

Syntax hints:   ↔ wb 105  Ⅎwnf 1513

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 1500  ax-gen 1502

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

This theorem is referenced by:  nfnf1  1597  nf3an  1619  nfnf  1630  nfdc  1711  nfs1f  1833  nfsbv  2007  nfeu1  2097  nfmo1  2098  sb8eu  2099  nfeu  2105  nfnfc1  2395  nfnfc  2399  nfeq  2400  nfel  2401  nfabdw  2411  nfne  2513  nfnel  2522  nfra1  2581  nfre1  2593  nfreu1  2723  nfrmo1  2724  nfss  3241  rabn0m  3549  nfdisjv  4116  nfdisj1  4117  nfpo  4444  nfso  4445  nfse  4484  nffrfor  4491  nffr  4492  nfwe  4498  nfrel  4858  sb8iota  5343  nffun  5398  nffn  5475  nff  5528  nff1  5594  nffo  5612  nff1o  5635  nfiso  6005  nfixpxy  6992  nfals  17052  nfrals  17053