Theorem nfxfr 1450

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

Syntax hints:   ↔ wb 104  Ⅎwnf 1436

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

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

This theorem is referenced by:  nfnf1  1523  nf3an  1545  nfnf  1556  nfdc  1637  nfs1f  1753  nfeu1  2010  nfmo1  2011  sb8eu  2012  nfeu  2018  nfnfc1  2284  nfnfc  2288  nfeq  2289  nfel  2290  nfne  2401  nfnel  2410  nfra1  2466  nfre1  2476  nfreu1  2602  nfrmo1  2603  nfss  3090  rabn0m  3390  nfdisjv  3918  nfdisj1  3919  nfpo  4223  nfso  4224  nfse  4263  nffrfor  4270  nffr  4271  nfwe  4277  nfrel  4624  sb8iota  5095  nffun  5146  nffn  5219  nff  5269  nff1  5326  nffo  5344  nff1o  5365  nfiso  5707  nfixpxy  6611