Theorem nfxfr 1363

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

Syntax hints:   ↔ wb 98  Ⅎwnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nfnf1  1436  nf3an  1458  nfnf  1469  nfdc  1549  nfs1f  1663  nfeu1  1911  nfmo1  1912  sb8eu  1913  nfeu  1919  nfnfc1  2181  nfnfc  2184  nfeq  2185  nfel  2186  nfne  2297  nfnel  2304  nfra1  2355  nfre1  2365  nfreu1  2481  nfrmo1  2482  nfss  2938  rabn0m  3245  nfdisjv  3757  nfdisj1  3758  nfpo  4038  nfso  4039  nfse  4078  nffrfor  4085  nffr  4086  nfwe  4092  nfrel  4425  sb8iota  4874  nffun  4924  nffn  4995  nff  5043  nff1  5090  nffo  5105  nff1o  5124  nfiso  5446