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  2493  nfnfc  2496  nfeq  2497  nfel  2498  nfne  2611  nfnel  2612  nfra1  2665  nfrex  2670  nfre1  2671  nfreu1  2782  nfrmo1  2783  nfrmo  2787  nfss  3267  sb8iota  4347  nffun  5131  nffn  5181  nff  5222  nff1  5257  nffo  5269  nff1o  5286  nfiso  5488