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  3218  rabn0m  3520  nfdisjv  4074  nfdisj1  4075  nfpo  4396  nfso  4397  nfse  4436  nffrfor  4443  nffr  4444  nfwe  4450  nfrel  4809  sb8iota  5292  nffun  5347  nffn  5423  nff  5476  nff1  5537  nffo  5555  nff1o  5578  nfiso  5942  nfixpxy  6881