Theorem nfxfr 1520

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

Syntax hints:   ↔ wb 105  Ⅎwnf 1506

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 1493  ax-gen 1495

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

This theorem is referenced by:  nfnf1  1590  nf3an  1612  nfnf  1623  nfdc  1705  nfs1f  1826  nfsbv  1998  nfeu1  2088  nfmo1  2089  sb8eu  2090  nfeu  2096  nfnfc1  2375  nfnfc  2379  nfeq  2380  nfel  2381  nfabdw  2391  nfne  2493  nfnel  2502  nfra1  2561  nfre1  2573  nfreu1  2703  nfrmo1  2704  nfss  3217  rabn0m  3519  nfdisjv  4071  nfdisj1  4072  nfpo  4392  nfso  4393  nfse  4432  nffrfor  4439  nffr  4440  nfwe  4446  nfrel  4804  sb8iota  5286  nffun  5341  nffn  5417  nff  5470  nff1  5529  nffo  5547  nff1o  5570  nfiso  5930  nfixpxy  6864