Theorem nfxfr 1418

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

Syntax hints:   ↔ wb 104  Ⅎwnf 1404

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393

This theorem depends on definitions:  df-bi 116  df-nf 1405

This theorem is referenced by:  nfnf1  1491  nf3an  1513  nfnf  1524  nfdc  1605  nfs1f  1721  nfeu1  1971  nfmo1  1972  sb8eu  1973  nfeu  1979  nfnfc1  2243  nfnfc  2247  nfeq  2248  nfel  2249  nfne  2360  nfnel  2369  nfra1  2425  nfre1  2435  nfreu1  2560  nfrmo1  2561  nfss  3040  rabn0m  3337  nfdisjv  3864  nfdisj1  3865  nfpo  4161  nfso  4162  nfse  4201  nffrfor  4208  nffr  4209  nfwe  4215  nfrel  4562  sb8iota  5031  nffun  5082  nffn  5155  nff  5205  nff1  5262  nffo  5280  nff1o  5299  nfiso  5639  nfixpxy  6541