Theorem nfxfr 1570

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

Syntax hints:   ↔ wb 176  Ⅎwnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557

This theorem depends on definitions:  df-bi 177  df-nf 1545

This theorem is referenced by:  nfnf1  1790  nfnan  1825  nfanOLD  1826  nf3an  1827  nfbiOLD  1835  nfor  1836  nf3or  1837  nfexOLD  1844  nfnf  1845  nfnfOLD  1846  nfs1f  2030  nfeu1  2214  nfmo1  2215  sb8eu  2222  nfnfc1  2492  nfnfc  2495  nfeq  2496  nfel  2497  nfne  2610  nfnel  2611  nfra1  2664  nfrex  2669  nfre1  2670  nfreu1  2781  nfrmo1  2782  nfrmo  2786  nfss  3266  sb8iota  4346  nffun  5130  nffn  5180  nff  5221  nff1  5256  nffo  5268  nff1o  5285  nfiso  5487