Theorem nfxfr 1474

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

Syntax hints:   ↔ wb 105  Ⅎwnf 1460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449

This theorem depends on definitions:  df-bi 117  df-nf 1461

This theorem is referenced by:  nfnf1  1544  nf3an  1566  nfnf  1577  nfdc  1659  nfs1f  1780  nfsbv  1947  nfeu1  2037  nfmo1  2038  sb8eu  2039  nfeu  2045  nfnfc1  2322  nfnfc  2326  nfeq  2327  nfel  2328  nfabdw  2338  nfne  2440  nfnel  2449  nfra1  2508  nfre1  2520  nfreu1  2649  nfrmo1  2650  nfss  3150  rabn0m  3452  nfdisjv  3994  nfdisj1  3995  nfpo  4303  nfso  4304  nfse  4343  nffrfor  4350  nffr  4351  nfwe  4357  nfrel  4713  sb8iota  5187  nffun  5241  nffn  5314  nff  5364  nff1  5421  nffo  5439  nff1o  5461  nfiso  5809  nfixpxy  6719