Theorem nfxfr 1343

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 1342	. 2 ⊢ (Ⅎxφ ↔ Ⅎxψ)
4	1, 3	mpbir 134	1 ⊢ Ⅎxφ

Syntax hints:   ↔ wb 98  Ⅎwnf 1329

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 1316  ax-gen 1318

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

This theorem is referenced by:  nfnf1  1418  nf3an  1440  nfnf  1451  nfdc  1531  nfs1f  1645  nfeu1  1893  nfmo1  1894  sb8eu  1895  nfeu  1901  nfnfc1  2163  nfnfc  2166  nfeq  2167  nfel  2168  nfne  2275  nfnel  2282  nfra1  2333  nfre1  2343  nfreu1  2459  nfrmo1  2460  nfss  2915  rabn0m  3222  nfdisjv  3731  nfdisj1  3732  nfpo  4012  nfso  4013  nfse  4046  nfrel  4352  sb8iota  4801  nffun  4850  nffn  4921  nff  4969  nff1  5015  nffo  5030  nff1o  5049  nfiso  5371