Theorem nfxfr 1360

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	⊢ Ⅎxψ

Assertion

Ref	Expression
nfxfr	⊢ Ⅎxφ

Proof of Theorem nfxfr

Step	Hyp	Ref	Expression
1		nfxfr.2	. 2 ⊢ Ⅎxψ
2		nfbii.1	. . 3 ⊢ (φ ↔ ψ)
3	2	nfbii 1359	. 2 ⊢ (Ⅎxφ ↔ Ⅎxψ)
4	1, 3	mpbir 134	1 ⊢ Ⅎxφ

Syntax hints:   ↔ wb 98  Ⅎwnf 1346

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 1333  ax-gen 1335

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

This theorem is referenced by:  nfnf1  1433  nf3an  1455  nfnf  1466  nfdc  1546  nfs1f  1660  nfeu1  1908  nfmo1  1909  sb8eu  1910  nfeu  1916  nfnfc1  2178  nfnfc  2181  nfeq  2182  nfel  2183  nfne  2291  nfnel  2298  nfra1  2349  nfre1  2359  nfreu1  2475  nfrmo1  2476  nfss  2932  rabn0m  3239  nfdisjv  3748  nfdisj1  3749  nfpo  4029  nfso  4030  nfse  4063  nfrel  4368  sb8iota  4817  nffun  4867  nffn  4938  nff  4986  nff1  5033  nffo  5048  nff1o  5067  nfiso  5389